108 by (rule chain_subset_extension_on_Union [OF subch \<open>\<And>r. r \<in> R \<Longrightarrow> extension_on (Field r) r p\<close>]) |
108 by (rule chain_subset_extension_on_Union [OF subch \<open>\<And>r. r \<in> R \<Longrightarrow> extension_on (Field r) r p\<close>]) |
109 ultimately have "\<Union>R \<in> ?K \<and> (\<forall>r\<in>R. (r,\<Union>R) \<in> I)" |
109 ultimately have "\<Union>R \<in> ?K \<and> (\<forall>r\<in>R. (r,\<Union>R) \<in> I)" |
110 using mono_Chains [OF I_init] and \<open>R \<in> Chains I\<close> |
110 using mono_Chains [OF I_init] and \<open>R \<in> Chains I\<close> |
111 by (simp (no_asm) add: I_def del: Field_Union) (metis Chains_wo) |
111 by (simp (no_asm) add: I_def del: Field_Union) (metis Chains_wo) |
112 } |
112 } |
113 then have 1: "\<forall>R\<in>Chains I. \<exists>u\<in>Field I. \<forall>r\<in>R. (r, u) \<in> I" by (subst FI) blast |
113 then have 1: "\<exists>u\<in>Field I. \<forall>r\<in>R. (r, u) \<in> I" if "R\<in>Chains I" for R |
|
114 using that by (subst FI) blast |
114 txt \<open>Zorn's Lemma yields a maximal wellorder m.\<close> |
115 txt \<open>Zorn's Lemma yields a maximal wellorder m.\<close> |
115 from Zorns_po_lemma [OF 0 1] obtain m :: "('a \<times> 'a) set" |
116 from Zorns_po_lemma [OF 0 1] obtain m :: "('a \<times> 'a) set" |
116 where "Well_order m" and "downset_on (Field m) p" and "extension_on (Field m) m p" and |
117 where "Well_order m" and "downset_on (Field m) p" and "extension_on (Field m) m p" and |
117 max: "\<forall>r. Well_order r \<and> downset_on (Field r) p \<and> extension_on (Field r) r p \<and> |
118 max: "\<forall>r. Well_order r \<and> downset_on (Field r) p \<and> extension_on (Field r) r p \<and> |
118 (m, r) \<in> I \<longrightarrow> r = m" |
119 (m, r) \<in> I \<longrightarrow> r = m" |