116 have "\<exists>m\<in>Field ?R. \<forall>a\<in>Field ?R. (m, a) \<in> ?R \<longrightarrow> a = m" (is "\<exists>m\<in>?A. ?B m") |
116 have "\<exists>m\<in>Field ?R. \<forall>a\<in>Field ?R. (m, a) \<in> ?R \<longrightarrow> a = m" (is "\<exists>m\<in>?A. ?B m") |
117 proof (rule Zorns_po_lemma) |
117 proof (rule Zorns_po_lemma) |
118 show "Partial_order ?R" |
118 show "Partial_order ?R" |
119 by (auto simp: partial_order_on_def preorder_on_def |
119 by (auto simp: partial_order_on_def preorder_on_def |
120 antisym_def refl_on_def trans_def Field_def bot_unique) |
120 antisym_def refl_on_def trans_def Field_def bot_unique) |
121 show "\<forall>C\<in>Chains ?R. \<exists>u\<in>Field ?R. \<forall>a\<in>C. (a, u) \<in> ?R" |
121 show "\<exists>u\<in>Field ?R. \<forall>a\<in>C. (a, u) \<in> ?R" if C: "C \<in> Chains ?R" for C |
122 proof (safe intro!: bexI del: notI) |
122 proof (simp, intro exI conjI ballI) |
123 fix c x |
123 have Inf_C: "Inf C \<noteq> bot" "Inf C \<le> F" if "C \<noteq> {}" |
124 assume c: "c \<in> Chains ?R" |
|
125 |
|
126 have Inf_c: "Inf c \<noteq> bot" "Inf c \<le> F" if "c \<noteq> {}" |
|
127 proof - |
124 proof - |
128 from c that have "Inf c = bot \<longleftrightarrow> (\<exists>x\<in>c. x = bot)" |
125 from C that have "Inf C = bot \<longleftrightarrow> (\<exists>x\<in>C. x = bot)" |
129 unfolding trivial_limit_def by (intro eventually_Inf_base) (auto simp: Chains_def) |
126 unfolding trivial_limit_def by (intro eventually_Inf_base) (auto simp: Chains_def) |
130 with c show "Inf c \<noteq> bot" |
127 with C show "Inf C \<noteq> bot" |
131 by (simp add: bot_notin_R) |
128 by (simp add: bot_notin_R) |
132 from that obtain x where "x \<in> c" by auto |
129 from that obtain x where "x \<in> C" by auto |
133 with c show "Inf c \<le> F" |
130 with C show "Inf C \<le> F" |
134 by (auto intro!: Inf_lower2[of x] simp: Chains_def) |
131 by (auto intro!: Inf_lower2[of x] simp: Chains_def) |
135 qed |
132 qed |
136 then have [simp]: "inf F (Inf c) = (if c = {} then F else Inf c)" |
133 then have [simp]: "inf F (Inf C) = (if C = {} then F else Inf C)" |
137 using c by (auto simp add: inf_absorb2) |
134 using C by (auto simp add: inf_absorb2) |
138 |
135 from C show "inf F (Inf C) \<noteq> bot" |
139 from c show "inf F (Inf c) \<noteq> bot" |
136 by (simp add: F Inf_C) |
140 by (simp add: F Inf_c) |
137 from C show "inf F (Inf C) \<le> F" |
141 from c show "inf F (Inf c) \<in> Field ?R" |
138 by (simp add: Chains_def Inf_C F) |
142 by (simp add: Chains_def Inf_c F) |
139 with C show "inf F (Inf C) \<le> x" "x \<le> F" if "x \<in> C" for x |
143 |
140 using that by (auto intro: Inf_lower simp: Chains_def) |
144 assume "x \<in> c" |
|
145 with c show "inf F (Inf c) \<le> x" "x \<le> F" |
|
146 by (auto intro: Inf_lower simp: Chains_def) |
|
147 qed |
141 qed |
148 qed |
142 qed |
149 then obtain U where U: "U \<in> ?A" "?B U" .. |
143 then obtain U where U: "U \<in> ?A" "?B U" .. |
150 show ?thesis |
144 show ?thesis |
151 proof |
145 proof |