# Theory Reflection

Up to index of Isabelle/ZF/Constructible

theory Reflection
imports Normal
begin

    (*  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))

### Basic Definitions

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

### Easy Cases of the Reflection Theorem

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)))

### Reflection for Existential Quantifiers

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)

### Packaging the Quantifier Reflection Rules

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))))

### Simple Examples of Reflection

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))))