(* Title: ZF/Constructible/Reflection.thy ID: $Id: Reflection.thy,v 1.11 2005/06/17 14:15:10 haftmann Exp $ Author: Lawrence C Paulson, Cambridge University Computer Laboratory *) header {* The Reflection Theorem*} theory Reflection imports Normal begin lemma all_iff_not_ex_not: "(∀x. P(x)) <-> (~ (∃x. ~ P(x)))"; by blast lemma ball_iff_not_bex_not: "(∀x∈A. P(x)) <-> (~ (∃x∈A. ~ P(x)))"; by blast text{*From the notes of A. S. Kechris, page 6, and from Andrzej Mostowski, \emph{Constructible Sets with Applications}, North-Holland, 1969, page 23.*} subsection{*Basic Definitions*} text{*First part: the cumulative hierarchy defining the class @{text M}. To avoid handling multiple arguments, we assume that @{text "Mset(l)"} is closed under ordered pairing provided @{text l} is limit. Possibly this could be avoided: the induction hypothesis @{term Cl_reflects} (in locale @{text ex_reflection}) could be weakened to @{term "∀y∈Mset(a). ∀z∈Mset(a). P(<y,z>) <-> Q(a,<y,z>)"}, removing most uses of @{term Pair_in_Mset}. But there isn't much point in doing so, since ultimately the @{text ex_reflection} proof is packaged up using the predicate @{text Reflects}. *} locale reflection = fixes Mset and M and Reflects assumes Mset_mono_le : "mono_le_subset(Mset)" and Mset_cont : "cont_Ord(Mset)" and Pair_in_Mset : "[| x ∈ Mset(a); y ∈ Mset(a); Limit(a) |] ==> <x,y> ∈ Mset(a)" defines "M(x) == ∃a. Ord(a) & x ∈ Mset(a)" and "Reflects(Cl,P,Q) == Closed_Unbounded(Cl) & (∀a. Cl(a) --> (∀x∈Mset(a). P(x) <-> Q(a,x)))" fixes F0 --{*ordinal for a specific value @{term y}*} fixes FF --{*sup over the whole level, @{term "y∈Mset(a)"}*} fixes ClEx --{*Reflecting ordinals for the formula @{term "∃z. P"}*} defines "F0(P,y) == μ b. (∃z. M(z) & P(<y,z>)) --> (∃z∈Mset(b). P(<y,z>))" and "FF(P) == λa. \<Union>y∈Mset(a). F0(P,y)" and "ClEx(P,a) == Limit(a) & normalize(FF(P),a) = a" lemma (in reflection) Mset_mono: "i≤j ==> Mset(i) <= Mset(j)" apply (insert Mset_mono_le) apply (simp add: mono_le_subset_def leI) done text{*Awkward: we need a version of @{text ClEx_def} as an equality at the level of classes, which do not really exist*} lemma (in reflection) ClEx_eq: "ClEx(P) == λa. Limit(a) & normalize(FF(P),a) = a" by (simp add: ClEx_def [symmetric]) subsection{*Easy Cases of the Reflection Theorem*} theorem (in reflection) Triv_reflection [intro]: "Reflects(Ord, P, λa x. P(x))" by (simp add: Reflects_def) theorem (in reflection) Not_reflection [intro]: "Reflects(Cl,P,Q) ==> Reflects(Cl, λx. ~P(x), λa x. ~Q(a,x))" by (simp add: Reflects_def) theorem (in reflection) And_reflection [intro]: "[| Reflects(Cl,P,Q); Reflects(C',P',Q') |] ==> Reflects(λa. Cl(a) & C'(a), λx. P(x) & P'(x), λa x. Q(a,x) & Q'(a,x))" by (simp add: Reflects_def Closed_Unbounded_Int, blast) theorem (in reflection) Or_reflection [intro]: "[| Reflects(Cl,P,Q); Reflects(C',P',Q') |] ==> Reflects(λa. Cl(a) & C'(a), λx. P(x) | P'(x), λa x. Q(a,x) | Q'(a,x))" by (simp add: Reflects_def Closed_Unbounded_Int, blast) theorem (in reflection) Imp_reflection [intro]: "[| Reflects(Cl,P,Q); Reflects(C',P',Q') |] ==> Reflects(λa. Cl(a) & C'(a), λx. P(x) --> P'(x), λa x. Q(a,x) --> Q'(a,x))" by (simp add: Reflects_def Closed_Unbounded_Int, blast) theorem (in reflection) Iff_reflection [intro]: "[| Reflects(Cl,P,Q); Reflects(C',P',Q') |] ==> Reflects(λa. Cl(a) & C'(a), λx. P(x) <-> P'(x), λa x. Q(a,x) <-> Q'(a,x))" by (simp add: Reflects_def Closed_Unbounded_Int, blast) subsection{*Reflection for Existential Quantifiers*} lemma (in reflection) F0_works: "[| y∈Mset(a); Ord(a); M(z); P(<y,z>) |] ==> ∃z∈Mset(F0(P,y)). P(<y,z>)" apply (unfold F0_def M_def, clarify) apply (rule LeastI2) apply (blast intro: Mset_mono [THEN subsetD]) apply (blast intro: lt_Ord2, blast) done lemma (in reflection) Ord_F0 [intro,simp]: "Ord(F0(P,y))" by (simp add: F0_def) lemma (in reflection) Ord_FF [intro,simp]: "Ord(FF(P,y))" by (simp add: FF_def) lemma (in reflection) cont_Ord_FF: "cont_Ord(FF(P))" apply (insert Mset_cont) apply (simp add: cont_Ord_def FF_def, blast) done text{*Recall that @{term F0} depends upon @{term "y∈Mset(a)"}, while @{term FF} depends only upon @{term a}. *} lemma (in reflection) FF_works: "[| M(z); y∈Mset(a); P(<y,z>); Ord(a) |] ==> ∃z∈Mset(FF(P,a)). P(<y,z>)" apply (simp add: FF_def) apply (simp_all add: cont_Ord_Union [of concl: Mset] Mset_cont Mset_mono_le not_emptyI Ord_F0) apply (blast intro: F0_works) done lemma (in reflection) FFN_works: "[| M(z); y∈Mset(a); P(<y,z>); Ord(a) |] ==> ∃z∈Mset(normalize(FF(P),a)). P(<y,z>)" apply (drule FF_works [of concl: P], assumption+) apply (blast intro: cont_Ord_FF le_normalize [THEN Mset_mono, THEN subsetD]) done text{*Locale for the induction hypothesis*} locale ex_reflection = reflection + fixes P --"the original formula" fixes Q --"the reflected formula" fixes Cl --"the class of reflecting ordinals" assumes Cl_reflects: "[| Cl(a); Ord(a) |] ==> ∀x∈Mset(a). P(x) <-> Q(a,x)" lemma (in ex_reflection) ClEx_downward: "[| M(z); y∈Mset(a); P(<y,z>); Cl(a); ClEx(P,a) |] ==> ∃z∈Mset(a). Q(a,<y,z>)" apply (simp add: ClEx_def, clarify) apply (frule Limit_is_Ord) apply (frule FFN_works [of concl: P], assumption+) apply (drule Cl_reflects, assumption+) apply (auto simp add: Limit_is_Ord Pair_in_Mset) done lemma (in ex_reflection) ClEx_upward: "[| z∈Mset(a); y∈Mset(a); Q(a,<y,z>); Cl(a); ClEx(P,a) |] ==> ∃z. M(z) & P(<y,z>)" apply (simp add: ClEx_def M_def) apply (blast dest: Cl_reflects intro: Limit_is_Ord Pair_in_Mset) done text{*Class @{text ClEx} indeed consists of reflecting ordinals...*} lemma (in ex_reflection) ZF_ClEx_iff: "[| y∈Mset(a); Cl(a); ClEx(P,a) |] ==> (∃z. M(z) & P(<y,z>)) <-> (∃z∈Mset(a). Q(a,<y,z>))" by (blast intro: dest: ClEx_downward ClEx_upward) text{*...and it is closed and unbounded*} lemma (in ex_reflection) ZF_Closed_Unbounded_ClEx: "Closed_Unbounded(ClEx(P))" apply (simp add: ClEx_eq) apply (fast intro: Closed_Unbounded_Int Normal_imp_fp_Closed_Unbounded Closed_Unbounded_Limit Normal_normalize) done text{*The same two theorems, exported to locale @{text reflection}.*} text{*Class @{text ClEx} indeed consists of reflecting ordinals...*} lemma (in reflection) ClEx_iff: "[| y∈Mset(a); Cl(a); ClEx(P,a); !!a. [| Cl(a); Ord(a) |] ==> ∀x∈Mset(a). P(x) <-> Q(a,x) |] ==> (∃z. M(z) & P(<y,z>)) <-> (∃z∈Mset(a). Q(a,<y,z>))" apply (unfold ClEx_def FF_def F0_def M_def) apply (rule ex_reflection.ZF_ClEx_iff [OF ex_reflection.intro, OF reflection.intro ex_reflection_axioms.intro, of Mset Cl]) apply (simp_all add: Mset_mono_le Mset_cont Pair_in_Mset) done (*Alternative proof, less unfolding: apply (rule Reflection.ZF_ClEx_iff [of Mset _ _ Cl, folded M_def]) apply (fold ClEx_def FF_def F0_def) apply (rule ex_reflection.intro, assumption) apply (simp add: ex_reflection_axioms.intro, assumption+) *) lemma (in reflection) Closed_Unbounded_ClEx: "(!!a. [| Cl(a); Ord(a) |] ==> ∀x∈Mset(a). P(x) <-> Q(a,x)) ==> Closed_Unbounded(ClEx(P))" apply (unfold ClEx_eq FF_def F0_def M_def) apply (rule Reflection.ZF_Closed_Unbounded_ClEx [of Mset _ _ Cl]) apply (rule ex_reflection.intro, assumption) apply (blast intro: ex_reflection_axioms.intro) done subsection{*Packaging the Quantifier Reflection Rules*} lemma (in reflection) Ex_reflection_0: "Reflects(Cl,P0,Q0) ==> Reflects(λa. Cl(a) & ClEx(P0,a), λx. ∃z. M(z) & P0(<x,z>), λa x. ∃z∈Mset(a). Q0(a,<x,z>))" apply (simp add: Reflects_def) apply (intro conjI Closed_Unbounded_Int) apply blast apply (rule Closed_Unbounded_ClEx [of Cl P0 Q0], blast, clarify) apply (rule_tac Cl=Cl in ClEx_iff, assumption+, blast) done lemma (in reflection) All_reflection_0: "Reflects(Cl,P0,Q0) ==> Reflects(λa. Cl(a) & ClEx(λx.~P0(x), a), λx. ∀z. M(z) --> P0(<x,z>), λa x. ∀z∈Mset(a). Q0(a,<x,z>))" apply (simp only: all_iff_not_ex_not ball_iff_not_bex_not) apply (rule Not_reflection, drule Not_reflection, simp) apply (erule Ex_reflection_0) done theorem (in reflection) Ex_reflection [intro]: "Reflects(Cl, λx. P(fst(x),snd(x)), λa x. Q(a,fst(x),snd(x))) ==> Reflects(λa. Cl(a) & ClEx(λx. P(fst(x),snd(x)), a), λx. ∃z. M(z) & P(x,z), λa x. ∃z∈Mset(a). Q(a,x,z))" by (rule Ex_reflection_0 [of _ " λx. P(fst(x),snd(x))" "λa x. Q(a,fst(x),snd(x))", simplified]) theorem (in reflection) All_reflection [intro]: "Reflects(Cl, λx. P(fst(x),snd(x)), λa x. Q(a,fst(x),snd(x))) ==> Reflects(λa. Cl(a) & ClEx(λx. ~P(fst(x),snd(x)), a), λx. ∀z. M(z) --> P(x,z), λa x. ∀z∈Mset(a). Q(a,x,z))" by (rule All_reflection_0 [of _ "λx. P(fst(x),snd(x))" "λa x. Q(a,fst(x),snd(x))", simplified]) text{*And again, this time using class-bounded quantifiers*} theorem (in reflection) Rex_reflection [intro]: "Reflects(Cl, λx. P(fst(x),snd(x)), λa x. Q(a,fst(x),snd(x))) ==> Reflects(λa. Cl(a) & ClEx(λx. P(fst(x),snd(x)), a), λx. ∃z[M]. P(x,z), λa x. ∃z∈Mset(a). Q(a,x,z))" by (unfold rex_def, blast) theorem (in reflection) Rall_reflection [intro]: "Reflects(Cl, λx. P(fst(x),snd(x)), λa x. Q(a,fst(x),snd(x))) ==> Reflects(λa. Cl(a) & ClEx(λx. ~P(fst(x),snd(x)), a), λx. ∀z[M]. P(x,z), λa x. ∀z∈Mset(a). Q(a,x,z))" by (unfold rall_def, blast) text{*No point considering bounded quantifiers, where reflection is trivial.*} subsection{*Simple Examples of Reflection*} text{*Example 1: reflecting a simple formula. The reflecting class is first given as the variable @{text ?Cl} and later retrieved from the final proof state.*} lemma (in reflection) "Reflects(?Cl, λx. ∃y. M(y) & x ∈ y, λa x. ∃y∈Mset(a). x ∈ y)" by fast text{*Problem here: there needs to be a conjunction (class intersection) in the class of reflecting ordinals. The @{term "Ord(a)"} is redundant, though harmless.*} lemma (in reflection) "Reflects(λa. Ord(a) & ClEx(λx. fst(x) ∈ snd(x), a), λx. ∃y. M(y) & x ∈ y, λa x. ∃y∈Mset(a). x ∈ y)" by fast text{*Example 2*} lemma (in reflection) "Reflects(?Cl, λx. ∃y. M(y) & (∀z. M(z) --> z ⊆ x --> z ∈ y), λa x. ∃y∈Mset(a). ∀z∈Mset(a). z ⊆ x --> z ∈ y)" by fast text{*Example 2'. We give the reflecting class explicitly. *} lemma (in reflection) "Reflects (λa. (Ord(a) & ClEx(λx. ~ (snd(x) ⊆ fst(fst(x)) --> snd(x) ∈ snd(fst(x))), a)) & ClEx(λx. ∀z. M(z) --> z ⊆ fst(x) --> z ∈ snd(x), a), λx. ∃y. M(y) & (∀z. M(z) --> z ⊆ x --> z ∈ y), λa x. ∃y∈Mset(a). ∀z∈Mset(a). z ⊆ x --> z ∈ y)" by fast text{*Example 2''. We expand the subset relation.*} lemma (in reflection) "Reflects(?Cl, λx. ∃y. M(y) & (∀z. M(z) --> (∀w. M(w) --> w∈z --> w∈x) --> z∈y), λa x. ∃y∈Mset(a). ∀z∈Mset(a). (∀w∈Mset(a). w∈z --> w∈x) --> z∈y)" by fast text{*Example 2'''. Single-step version, to reveal the reflecting class.*} lemma (in reflection) "Reflects(?Cl, λx. ∃y. M(y) & (∀z. M(z) --> z ⊆ x --> z ∈ y), λa x. ∃y∈Mset(a). ∀z∈Mset(a). z ⊆ x --> z ∈ y)" apply (rule Ex_reflection) txt{* @{goals[display,indent=0,margin=60]} *} apply (rule All_reflection) txt{* @{goals[display,indent=0,margin=60]} *} apply (rule Triv_reflection) txt{* @{goals[display,indent=0,margin=60]} *} done text{*Example 3. Warning: the following examples make sense only if @{term P} is quantifier-free, since it is not being relativized.*} lemma (in reflection) "Reflects(?Cl, λx. ∃y. M(y) & (∀z. M(z) --> z ∈ y <-> z ∈ x & P(z)), λa x. ∃y∈Mset(a). ∀z∈Mset(a). z ∈ y <-> z ∈ x & P(z))" by fast text{*Example 3'*} lemma (in reflection) "Reflects(?Cl, λx. ∃y. M(y) & y = Collect(x,P), λa x. ∃y∈Mset(a). y = Collect(x,P))"; by fast text{*Example 3''*} lemma (in reflection) "Reflects(?Cl, λx. ∃y. M(y) & y = Replace(x,P), λa x. ∃y∈Mset(a). y = Replace(x,P))"; by fast text{*Example 4: Axiom of Choice. Possibly wrong, since @{text Π} needs to be relativized.*} lemma (in reflection) "Reflects(?Cl, λA. 0∉A --> (∃f. M(f) & f ∈ (Π X ∈ A. X)), λa A. 0∉A --> (∃f∈Mset(a). f ∈ (Π X ∈ A. X)))" by fast end
lemma all_iff_not_ex_not:
(∀x. P(x)) <-> ¬ (∃x. ¬ P(x))
lemma ball_iff_not_bex_not:
(∀x∈A. P(x)) <-> ¬ (∃x∈A. ¬ P(x))
lemma Mset_mono:
[| reflection(Mset); i ≤ j |] ==> Mset(i) ⊆ Mset(j)
lemma ClEx_eq:
reflection(Mset) ==> %a. Limit(a) ∧ normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ P(〈y, z〉)) --> (∃z∈Mset(b). P(〈y, z〉)), a) = a == %a. Limit(a) ∧ normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ P(〈y, z〉)) --> (∃z∈Mset(b). P(〈y, z〉)), a) = a
theorem Triv_reflection:
reflection(Mset) ==> Closed_Unbounded(Ord) ∧ (∀a. Ord(a) --> (∀x∈Mset(a). P(x) <-> P(x)))
theorem Not_reflection:
[| reflection(Mset); Closed_Unbounded(Cl) ∧ (∀a. Cl(a) --> (∀x∈Mset(a). P(x) <-> Q(a, x))) |] ==> Closed_Unbounded(Cl) ∧ (∀a. Cl(a) --> (∀x∈Mset(a). ¬ P(x) <-> ¬ Q(a, x)))
theorem And_reflection:
[| reflection(Mset); Closed_Unbounded(Cl) ∧ (∀a. Cl(a) --> (∀x∈Mset(a). P(x) <-> Q(a, x))); Closed_Unbounded(C') ∧ (∀a. C'(a) --> (∀x∈Mset(a). P'(x) <-> Q'(a, x))) |] ==> Closed_Unbounded(%a. Cl(a) ∧ C'(a)) ∧ (∀a. Cl(a) ∧ C'(a) --> (∀x∈Mset(a). P(x) ∧ P'(x) <-> Q(a, x) ∧ Q'(a, x)))
theorem Or_reflection:
[| reflection(Mset); Closed_Unbounded(Cl) ∧ (∀a. Cl(a) --> (∀x∈Mset(a). P(x) <-> Q(a, x))); Closed_Unbounded(C') ∧ (∀a. C'(a) --> (∀x∈Mset(a). P'(x) <-> Q'(a, x))) |] ==> Closed_Unbounded(%a. Cl(a) ∧ C'(a)) ∧ (∀a. Cl(a) ∧ C'(a) --> (∀x∈Mset(a). P(x) ∨ P'(x) <-> Q(a, x) ∨ Q'(a, x)))
theorem Imp_reflection:
[| reflection(Mset); Closed_Unbounded(Cl) ∧ (∀a. Cl(a) --> (∀x∈Mset(a). P(x) <-> Q(a, x))); Closed_Unbounded(C') ∧ (∀a. C'(a) --> (∀x∈Mset(a). P'(x) <-> Q'(a, x))) |] ==> Closed_Unbounded(%a. Cl(a) ∧ C'(a)) ∧ (∀a. Cl(a) ∧ C'(a) --> (∀x∈Mset(a). (P(x) --> P'(x)) <-> Q(a, x) --> Q'(a, x)))
theorem Iff_reflection:
[| reflection(Mset); Closed_Unbounded(Cl) ∧ (∀a. Cl(a) --> (∀x∈Mset(a). P(x) <-> Q(a, x))); Closed_Unbounded(C') ∧ (∀a. C'(a) --> (∀x∈Mset(a). P'(x) <-> Q'(a, x))) |] ==> Closed_Unbounded(%a. Cl(a) ∧ C'(a)) ∧ (∀a. Cl(a) ∧ C'(a) --> (∀x∈Mset(a). (P(x) <-> P'(x)) <-> Q(a, x) <-> Q'(a, x)))
lemma F0_works:
[| reflection(Mset); y ∈ Mset(a); Ord(a); ∃a. Ord(a) ∧ z ∈ Mset(a); P(〈y, z〉) |] ==> ∃z∈Mset(μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ P(〈y, z〉)) --> (∃z∈Mset(b). P(〈y, z〉))). P(〈y, z〉)
lemma Ord_F0:
reflection(Mset) ==> Ord(μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ P(〈y, z〉)) --> (∃z∈Mset(b). P(〈y, z〉)))
lemma Ord_FF:
reflection(Mset) ==> Ord(\<Union>y∈Mset(y). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ P(〈y, z〉)) --> (∃z∈Mset(b). P(〈y, z〉)))
lemma cont_Ord_FF:
reflection(Mset) ==> cont_Ord (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ P(〈y, z〉)) --> (∃z∈Mset(b). P(〈y, z〉)))
lemma FF_works:
[| reflection(Mset); ∃a. Ord(a) ∧ z ∈ Mset(a); y ∈ Mset(a); P(〈y, z〉); Ord(a) |] ==> ∃z∈Mset(\<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ P(〈y, z〉)) --> (∃z∈Mset(b). P(〈y, z〉))). P(〈y, z〉)
lemma FFN_works:
[| reflection(Mset); ∃a. Ord(a) ∧ z ∈ Mset(a); y ∈ Mset(a); P(〈y, z〉); Ord(a) |] ==> ∃z∈Mset(normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ P(〈y, z〉)) --> (∃z∈Mset(b). P(〈y, z〉)), a)). P(〈y, z〉)
lemma ClEx_downward:
[| ex_reflection(Mset, P, Q, Cl); ∃a. Ord(a) ∧ z ∈ Mset(a); y ∈ Mset(a); P(〈y, z〉); Cl(a); Limit(a) ∧ normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ P(〈y, z〉)) --> (∃z∈Mset(b). P(〈y, z〉)), a) = a |] ==> ∃z∈Mset(a). Q(a, 〈y, z〉)
lemma ClEx_upward:
[| ex_reflection(Mset, P, Q, Cl); z ∈ Mset(a); y ∈ Mset(a); Q(a, 〈y, z〉); Cl(a); Limit(a) ∧ normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ P(〈y, z〉)) --> (∃z∈Mset(b). P(〈y, z〉)), a) = a |] ==> ∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ P(〈y, z〉)
lemma ZF_ClEx_iff:
[| ex_reflection(Mset, P, Q, Cl); y ∈ Mset(a); Cl(a); Limit(a) ∧ normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ P(〈y, z〉)) --> (∃z∈Mset(b). P(〈y, z〉)), a) = a |] ==> (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ P(〈y, z〉)) <-> (∃z∈Mset(a). Q(a, 〈y, z〉))
lemma ZF_Closed_Unbounded_ClEx:
ex_reflection(Mset, P, Q, Cl) ==> Closed_Unbounded (%a. Limit(a) ∧ normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ P(〈y, z〉)) --> (∃z∈Mset(b). P(〈y, z〉)), a) = a)
lemma ClEx_iff:
[| reflection(Mset); y ∈ Mset(a); Cl(a); Limit(a) ∧ normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ P(〈y, z〉)) --> (∃z∈Mset(b). P(〈y, z〉)), a) = a; !!a. [| Cl(a); Ord(a) |] ==> ∀x∈Mset(a). P(x) <-> Q(a, x) |] ==> (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ P(〈y, z〉)) <-> (∃z∈Mset(a). Q(a, 〈y, z〉))
lemma Closed_Unbounded_ClEx:
[| reflection(Mset); !!a. [| Cl(a); Ord(a) |] ==> ∀x∈Mset(a). P(x) <-> Q(a, x) |] ==> Closed_Unbounded (%a. Limit(a) ∧ normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ P(〈y, z〉)) --> (∃z∈Mset(b). P(〈y, z〉)), a) = a)
lemma Ex_reflection_0:
[| reflection(Mset); Closed_Unbounded(Cl) ∧ (∀a. Cl(a) --> (∀x∈Mset(a). P0.0(x) <-> Q0.0(a, x))) |] ==> Closed_Unbounded (%a. Cl(a) ∧ Limit(a) ∧ normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ P0.0(〈y, z〉)) --> (∃z∈Mset(b). P0.0(〈y, z〉)), a) = a) ∧ (∀a. Cl(a) ∧ Limit(a) ∧ normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ P0.0(〈y, z〉)) --> (∃z∈Mset(b). P0.0(〈y, z〉)), a) = a --> (∀x∈Mset(a). (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ P0.0(〈x, z〉)) <-> (∃z∈Mset(a). Q0.0(a, 〈x, z〉))))
lemma All_reflection_0:
[| reflection(Mset); Closed_Unbounded(Cl) ∧ (∀a. Cl(a) --> (∀x∈Mset(a). P0.0(x) <-> Q0.0(a, x))) |] ==> Closed_Unbounded (%a. Cl(a) ∧ Limit(a) ∧ normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ ¬ P0.0(〈y, z〉)) --> (∃z∈Mset(b). ¬ P0.0(〈y, z〉)), a) = a) ∧ (∀a. Cl(a) ∧ Limit(a) ∧ normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ ¬ P0.0(〈y, z〉)) --> (∃z∈Mset(b). ¬ P0.0(〈y, z〉)), a) = a --> (∀x∈Mset(a). (∀z. (∃a. Ord(a) ∧ z ∈ Mset(a)) --> P0.0(〈x, z〉)) <-> (∀z∈Mset(a). Q0.0(a, 〈x, z〉))))
theorem Ex_reflection:
[| reflection(Mset); Closed_Unbounded(Cl) ∧ (∀a. Cl(a) --> (∀x∈Mset(a). P(fst(x), snd(x)) <-> Q(a, fst(x), snd(x)))) |] ==> Closed_Unbounded (%a. Cl(a) ∧ Limit(a) ∧ normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ P(fst(〈y, z〉), snd(〈y, z〉))) --> (∃z∈Mset(b). P(fst(〈y, z〉), snd(〈y, z〉))), a) = a) ∧ (∀a. Cl(a) ∧ Limit(a) ∧ normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ P(fst(〈y, z〉), snd(〈y, z〉))) --> (∃z∈Mset(b). P(fst(〈y, z〉), snd(〈y, z〉))), a) = a --> (∀x∈Mset(a). (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ P(x, z)) <-> (∃z∈Mset(a). Q(a, x, z))))
theorem All_reflection:
[| reflection(Mset); Closed_Unbounded(Cl) ∧ (∀a. Cl(a) --> (∀x∈Mset(a). P(fst(x), snd(x)) <-> Q(a, fst(x), snd(x)))) |] ==> Closed_Unbounded (%a. Cl(a) ∧ Limit(a) ∧ normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ ¬ P(fst(〈y, z〉), snd(〈y, z〉))) --> (∃z∈Mset(b). ¬ P(fst(〈y, z〉), snd(〈y, z〉))), a) = a) ∧ (∀a. Cl(a) ∧ Limit(a) ∧ normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ ¬ P(fst(〈y, z〉), snd(〈y, z〉))) --> (∃z∈Mset(b). ¬ P(fst(〈y, z〉), snd(〈y, z〉))), a) = a --> (∀x∈Mset(a). (∀z. (∃a. Ord(a) ∧ z ∈ Mset(a)) --> P(x, z)) <-> (∀z∈Mset(a). Q(a, x, z))))
theorem Rex_reflection:
[| reflection(Mset); Closed_Unbounded(Cl) ∧ (∀a. Cl(a) --> (∀x∈Mset(a). P(fst(x), snd(x)) <-> Q(a, fst(x), snd(x)))) |] ==> Closed_Unbounded (%a. Cl(a) ∧ Limit(a) ∧ normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ P(fst(〈y, z〉), snd(〈y, z〉))) --> (∃z∈Mset(b). P(fst(〈y, z〉), snd(〈y, z〉))), a) = a) ∧ (∀a. Cl(a) ∧ Limit(a) ∧ normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ P(fst(〈y, z〉), snd(〈y, z〉))) --> (∃z∈Mset(b). P(fst(〈y, z〉), snd(〈y, z〉))), a) = a --> (∀x∈Mset(a). (∃z[%x. ∃a. Ord(a) ∧ x ∈ Mset(a)]. P(x, z)) <-> (∃z∈Mset(a). Q(a, x, z))))
theorem Rall_reflection:
[| reflection(Mset); Closed_Unbounded(Cl) ∧ (∀a. Cl(a) --> (∀x∈Mset(a). P(fst(x), snd(x)) <-> Q(a, fst(x), snd(x)))) |] ==> Closed_Unbounded (%a. Cl(a) ∧ Limit(a) ∧ normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ ¬ P(fst(〈y, z〉), snd(〈y, z〉))) --> (∃z∈Mset(b). ¬ P(fst(〈y, z〉), snd(〈y, z〉))), a) = a) ∧ (∀a. Cl(a) ∧ Limit(a) ∧ normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ ¬ P(fst(〈y, z〉), snd(〈y, z〉))) --> (∃z∈Mset(b). ¬ P(fst(〈y, z〉), snd(〈y, z〉))), a) = a --> (∀x∈Mset(a). (∀z[%x. ∃a. Ord(a) ∧ x ∈ Mset(a)]. P(x, z)) <-> (∀z∈Mset(a). Q(a, x, z))))
lemma
reflection(Mset) ==> Closed_Unbounded (%a. Ord(a) ∧ Limit(a) ∧ normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ fst(〈y, z〉) ∈ snd(〈y, z〉)) --> (∃z∈Mset(b). fst(〈y, z〉) ∈ snd(〈y, z〉)), a) = a) ∧ (∀a. Ord(a) ∧ Limit(a) ∧ normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ fst(〈y, z〉) ∈ snd(〈y, z〉)) --> (∃z∈Mset(b). fst(〈y, z〉) ∈ snd(〈y, z〉)), a) = a --> (∀x∈Mset(a). (∃y. (∃a. Ord(a) ∧ y ∈ Mset(a)) ∧ x ∈ y) <-> (∃y∈Mset(a). x ∈ y)))
lemma
reflection(Mset) ==> Closed_Unbounded (%a. Ord(a) ∧ Limit(a) ∧ normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ fst(〈y, z〉) ∈ snd(〈y, z〉)) --> (∃z∈Mset(b). fst(〈y, z〉) ∈ snd(〈y, z〉)), a) = a) ∧ (∀a. Ord(a) ∧ Limit(a) ∧ normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ fst(〈y, z〉) ∈ snd(〈y, z〉)) --> (∃z∈Mset(b). fst(〈y, z〉) ∈ snd(〈y, z〉)), a) = a --> (∀x∈Mset(a). (∃y. (∃a. Ord(a) ∧ y ∈ Mset(a)) ∧ x ∈ y) <-> (∃y∈Mset(a). x ∈ y)))
lemma
reflection(Mset) ==> Closed_Unbounded (%a. (Ord(a) ∧ Limit(a) ∧ normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ ¬ (snd(〈y, z〉) ⊆ fst(fst(〈y, z〉)) --> snd(〈y, z〉) ∈ snd(fst(〈y, z〉)))) --> (∃z∈Mset(b). ¬ (snd(〈y, z〉) ⊆ fst(fst(〈y, z〉)) --> snd(〈y, z〉) ∈ snd(fst(〈y, z〉)))), a) = a) ∧ Limit(a) ∧ normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ (∀za. (∃a. Ord(a) ∧ za ∈ Mset(a)) --> za ⊆ fst(〈y, z〉) --> za ∈ snd(〈y, z〉))) --> (∃z∈Mset(b). ∀za. (∃a. Ord(a) ∧ za ∈ Mset(a)) --> za ⊆ fst(〈y, z〉) --> za ∈ snd(〈y, z〉)), a) = a) ∧ (∀a. (Ord(a) ∧ Limit(a) ∧ normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ ¬ (snd(〈y, z〉) ⊆ fst(fst(〈y, z〉)) --> snd(〈y, z〉) ∈ snd(fst(〈y, z〉)))) --> (∃z∈Mset(b). ¬ (snd(〈y, z〉) ⊆ fst(fst(〈y, z〉)) --> snd(〈y, z〉) ∈ snd(fst(〈y, z〉)))), a) = a) ∧ Limit(a) ∧ normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ (∀za. (∃a. Ord(a) ∧ za ∈ Mset(a)) --> za ⊆ fst(〈y, z〉) --> za ∈ snd(〈y, z〉))) --> (∃z∈Mset(b). ∀za. (∃a. Ord(a) ∧ za ∈ Mset(a)) --> za ⊆ fst(〈y, z〉) --> za ∈ snd(〈y, z〉)), a) = a --> (∀x∈Mset(a). (∃y. (∃a. Ord(a) ∧ y ∈ Mset(a)) ∧ (∀z. (∃a. Ord(a) ∧ z ∈ Mset(a)) --> z ⊆ x --> z ∈ y)) <-> (∃y∈Mset(a). ∀z∈Mset(a). z ⊆ x --> z ∈ y)))
lemma
reflection(Mset) ==> Closed_Unbounded (%a. (Ord(a) ∧ Limit(a) ∧ normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ ¬ (snd(〈y, z〉) ⊆ fst(fst(〈y, z〉)) --> snd(〈y, z〉) ∈ snd(fst(〈y, z〉)))) --> (∃z∈Mset(b). ¬ (snd(〈y, z〉) ⊆ fst(fst(〈y, z〉)) --> snd(〈y, z〉) ∈ snd(fst(〈y, z〉)))), a) = a) ∧ Limit(a) ∧ normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ (∀za. (∃a. Ord(a) ∧ za ∈ Mset(a)) --> za ⊆ fst(〈y, z〉) --> za ∈ snd(〈y, z〉))) --> (∃z∈Mset(b). ∀za. (∃a. Ord(a) ∧ za ∈ Mset(a)) --> za ⊆ fst(〈y, z〉) --> za ∈ snd(〈y, z〉)), a) = a) ∧ (∀a. (Ord(a) ∧ Limit(a) ∧ normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ ¬ (snd(〈y, z〉) ⊆ fst(fst(〈y, z〉)) --> snd(〈y, z〉) ∈ snd(fst(〈y, z〉)))) --> (∃z∈Mset(b). ¬ (snd(〈y, z〉) ⊆ fst(fst(〈y, z〉)) --> snd(〈y, z〉) ∈ snd(fst(〈y, z〉)))), a) = a) ∧ Limit(a) ∧ normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ (∀za. (∃a. Ord(a) ∧ za ∈ Mset(a)) --> za ⊆ fst(〈y, z〉) --> za ∈ snd(〈y, z〉))) --> (∃z∈Mset(b). ∀za. (∃a. Ord(a) ∧ za ∈ Mset(a)) --> za ⊆ fst(〈y, z〉) --> za ∈ snd(〈y, z〉)), a) = a --> (∀x∈Mset(a). (∃y. (∃a. Ord(a) ∧ y ∈ Mset(a)) ∧ (∀z. (∃a. Ord(a) ∧ z ∈ Mset(a)) --> z ⊆ x --> z ∈ y)) <-> (∃y∈Mset(a). ∀z∈Mset(a). z ⊆ x --> z ∈ y)))
lemma
reflection(Mset) ==> Closed_Unbounded (%a. (((Ord(a) ∧ Limit(a) ∧ normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ ¬ (snd(〈y, z〉) ∈ snd(fst(〈y, z〉)) --> snd(〈y, z〉) ∈ fst(fst(fst(〈y, z〉))))) --> (∃z∈Mset(b). ¬ (snd(〈y, z〉) ∈ snd(fst(〈y, z〉)) --> snd(〈y, z〉) ∈ fst(fst(fst(〈y, z〉))))), a) = a) ∧ Ord(a)) ∧ Limit(a) ∧ normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ ¬ ((∀w. (∃a. Ord(a) ∧ w ∈ Mset(a)) --> w ∈ snd(〈y, z〉) --> w ∈ fst(fst(〈y, z〉))) --> snd(〈y, z〉) ∈ snd(fst(〈y, z〉)))) --> (∃z∈Mset(b). ¬ ((∀w. (∃a. Ord(a) ∧ w ∈ Mset(a)) --> w ∈ snd(〈y, z〉) --> w ∈ fst(fst(〈y, z〉))) --> snd(〈y, z〉) ∈ snd(fst(〈y, z〉)))), a) = a) ∧ Limit(a) ∧ normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ (∀za. (∃a. Ord(a) ∧ za ∈ Mset(a)) --> (∀w. (∃a. Ord(a) ∧ w ∈ Mset(a)) --> w ∈ za --> w ∈ fst(〈y, z〉)) --> za ∈ snd(〈y, z〉))) --> (∃z∈Mset(b). ∀za. (∃a. Ord(a) ∧ za ∈ Mset(a)) --> (∀w. (∃a. Ord(a) ∧ w ∈ Mset(a)) --> w ∈ za --> w ∈ fst(〈y, z〉)) --> za ∈ snd(〈y, z〉)), a) = a) ∧ (∀a. (((Ord(a) ∧ Limit(a) ∧ normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ ¬ (snd(〈y, z〉) ∈ snd(fst(〈y, z〉)) --> snd(〈y, z〉) ∈ fst(fst(fst(〈y, z〉))))) --> (∃z∈Mset(b). ¬ (snd(〈y, z〉) ∈ snd(fst(〈y, z〉)) --> snd(〈y, z〉) ∈ fst(fst(fst(〈y, z〉))))), a) = a) ∧ Ord(a)) ∧ Limit(a) ∧ normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ ¬ ((∀w. (∃a. Ord(a) ∧ w ∈ Mset(a)) --> w ∈ snd(〈y, z〉) --> w ∈ fst(fst(〈y, z〉))) --> snd(〈y, z〉) ∈ snd(fst(〈y, z〉)))) --> (∃z∈Mset(b). ¬ ((∀w. (∃a. Ord(a) ∧ w ∈ Mset(a)) --> w ∈ snd(〈y, z〉) --> w ∈ fst(fst(〈y, z〉))) --> snd(〈y, z〉) ∈ snd(fst(〈y, z〉)))), a) = a) ∧ Limit(a) ∧ normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ (∀za. (∃a. Ord(a) ∧ za ∈ Mset(a)) --> (∀w. (∃a. Ord(a) ∧ w ∈ Mset(a)) --> w ∈ za --> w ∈ fst(〈y, z〉)) --> za ∈ snd(〈y, z〉))) --> (∃z∈Mset(b). ∀za. (∃a. Ord(a) ∧ za ∈ Mset(a)) --> (∀w. (∃a. Ord(a) ∧ w ∈ Mset(a)) --> w ∈ za --> w ∈ fst(〈y, z〉)) --> za ∈ snd(〈y, z〉)), a) = a --> (∀x∈Mset(a). (∃y. (∃a. Ord(a) ∧ y ∈ Mset(a)) ∧ (∀z. (∃a. Ord(a) ∧ z ∈ Mset(a)) --> (∀w. (∃a. Ord(a) ∧ w ∈ Mset(a)) --> w ∈ z --> w ∈ x) --> z ∈ y)) <-> (∃y∈Mset(a). ∀z∈Mset(a). (∀w∈Mset(a). w ∈ z --> w ∈ x) --> z ∈ y)))
lemma
reflection(Mset) ==> Closed_Unbounded (%a. (Ord(a) ∧ Limit(a) ∧ normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ ¬ (snd(〈y, z〉) ⊆ fst(fst(〈y, z〉)) --> snd(〈y, z〉) ∈ snd(fst(〈y, z〉)))) --> (∃z∈Mset(b). ¬ (snd(〈y, z〉) ⊆ fst(fst(〈y, z〉)) --> snd(〈y, z〉) ∈ snd(fst(〈y, z〉)))), a) = a) ∧ Limit(a) ∧ normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ (∀za. (∃a. Ord(a) ∧ za ∈ Mset(a)) --> za ⊆ fst(〈y, z〉) --> za ∈ snd(〈y, z〉))) --> (∃z∈Mset(b). ∀za. (∃a. Ord(a) ∧ za ∈ Mset(a)) --> za ⊆ fst(〈y, z〉) --> za ∈ snd(〈y, z〉)), a) = a) ∧ (∀a. (Ord(a) ∧ Limit(a) ∧ normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ ¬ (snd(〈y, z〉) ⊆ fst(fst(〈y, z〉)) --> snd(〈y, z〉) ∈ snd(fst(〈y, z〉)))) --> (∃z∈Mset(b). ¬ (snd(〈y, z〉) ⊆ fst(fst(〈y, z〉)) --> snd(〈y, z〉) ∈ snd(fst(〈y, z〉)))), a) = a) ∧ Limit(a) ∧ normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ (∀za. (∃a. Ord(a) ∧ za ∈ Mset(a)) --> za ⊆ fst(〈y, z〉) --> za ∈ snd(〈y, z〉))) --> (∃z∈Mset(b). ∀za. (∃a. Ord(a) ∧ za ∈ Mset(a)) --> za ⊆ fst(〈y, z〉) --> za ∈ snd(〈y, z〉)), a) = a --> (∀x∈Mset(a). (∃y. (∃a. Ord(a) ∧ y ∈ Mset(a)) ∧ (∀z. (∃a. Ord(a) ∧ z ∈ Mset(a)) --> z ⊆ x --> z ∈ y)) <-> (∃y∈Mset(a). ∀z∈Mset(a). z ⊆ x --> z ∈ y)))
lemma
reflection(Mset) ==> Closed_Unbounded (%a. (Ord(a) ∧ Limit(a) ∧ normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ ¬ (snd(〈y, z〉) ∈ snd(fst(〈y, z〉)) <-> snd(〈y, z〉) ∈ fst(fst(〈y, z〉)) ∧ P(snd(〈y, z〉)))) --> (∃z∈Mset(b). ¬ (snd(〈y, z〉) ∈ snd(fst(〈y, z〉)) <-> snd(〈y, z〉) ∈ fst(fst(〈y, z〉)) ∧ P(snd(〈y, z〉)))), a) = a) ∧ Limit(a) ∧ normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ (∀za. (∃a. Ord(a) ∧ za ∈ Mset(a)) --> za ∈ snd(〈y, z〉) <-> za ∈ fst(〈y, z〉) ∧ P(za))) --> (∃z∈Mset(b). ∀za. (∃a. Ord(a) ∧ za ∈ Mset(a)) --> za ∈ snd(〈y, z〉) <-> za ∈ fst(〈y, z〉) ∧ P(za)), a) = a) ∧ (∀a. (Ord(a) ∧ Limit(a) ∧ normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ ¬ (snd(〈y, z〉) ∈ snd(fst(〈y, z〉)) <-> snd(〈y, z〉) ∈ fst(fst(〈y, z〉)) ∧ P(snd(〈y, z〉)))) --> (∃z∈Mset(b). ¬ (snd(〈y, z〉) ∈ snd(fst(〈y, z〉)) <-> snd(〈y, z〉) ∈ fst(fst(〈y, z〉)) ∧ P(snd(〈y, z〉)))), a) = a) ∧ Limit(a) ∧ normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ (∀za. (∃a. Ord(a) ∧ za ∈ Mset(a)) --> za ∈ snd(〈y, z〉) <-> za ∈ fst(〈y, z〉) ∧ P(za))) --> (∃z∈Mset(b). ∀za. (∃a. Ord(a) ∧ za ∈ Mset(a)) --> za ∈ snd(〈y, z〉) <-> za ∈ fst(〈y, z〉) ∧ P(za)), a) = a --> (∀x∈Mset(a). (∃y. (∃a. Ord(a) ∧ y ∈ Mset(a)) ∧ (∀z. (∃a. Ord(a) ∧ z ∈ Mset(a)) --> z ∈ y <-> z ∈ x ∧ P(z))) <-> (∃y∈Mset(a). ∀z∈Mset(a). z ∈ y <-> z ∈ x ∧ P(z))))
lemma
reflection(Mset) ==> Closed_Unbounded (%a. Ord(a) ∧ Limit(a) ∧ normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ snd(〈y, z〉) = Collect(fst(〈y, z〉), P)) --> (∃z∈Mset(b). snd(〈y, z〉) = Collect(fst(〈y, z〉), P)), a) = a) ∧ (∀a. Ord(a) ∧ Limit(a) ∧ normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ snd(〈y, z〉) = Collect(fst(〈y, z〉), P)) --> (∃z∈Mset(b). snd(〈y, z〉) = Collect(fst(〈y, z〉), P)), a) = a --> (∀x∈Mset(a). (∃y. (∃a. Ord(a) ∧ y ∈ Mset(a)) ∧ y = Collect(x, P)) <-> (∃y∈Mset(a). y = Collect(x, P))))
lemma
reflection(Mset) ==> Closed_Unbounded (%a. Ord(a) ∧ Limit(a) ∧ normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ snd(〈y, z〉) = Replace(fst(〈y, z〉), P)) --> (∃z∈Mset(b). snd(〈y, z〉) = Replace(fst(〈y, z〉), P)), a) = a) ∧ (∀a. Ord(a) ∧ Limit(a) ∧ normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ snd(〈y, z〉) = Replace(fst(〈y, z〉), P)) --> (∃z∈Mset(b). snd(〈y, z〉) = Replace(fst(〈y, z〉), P)), a) = a --> (∀x∈Mset(a). (∃y. (∃a. Ord(a) ∧ y ∈ Mset(a)) ∧ y = Replace(x, P)) <-> (∃y∈Mset(a). y = Replace(x, P))))
lemma
reflection(Mset) ==> Closed_Unbounded (%a. Ord(a) ∧ Ord(a) ∧ Limit(a) ∧ normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ snd(〈y, z〉) ∈ (ΠX∈fst(〈y, z〉). X)) --> (∃z∈Mset(b). snd(〈y, z〉) ∈ (ΠX∈fst(〈y, z〉). X)), a) = a) ∧ (∀a. Ord(a) ∧ Ord(a) ∧ Limit(a) ∧ normalize (%a. \<Union>y∈Mset(a). μb. (∃z. (∃a. Ord(a) ∧ z ∈ Mset(a)) ∧ snd(〈y, z〉) ∈ (ΠX∈fst(〈y, z〉). X)) --> (∃z∈Mset(b). snd(〈y, z〉) ∈ (ΠX∈fst(〈y, z〉). X)), a) = a --> (∀x∈Mset(a). (0 ∉ x --> (∃f. (∃a. Ord(a) ∧ f ∈ Mset(a)) ∧ f ∈ (ΠX∈x. X))) <-> 0 ∉ x --> (∃f∈Mset(a). f ∈ (ΠX∈x. X))))