Beginning of Section **Ex**

Variable A : SType

End of Section **Ex**

∀P : set → prop, (∀X : set, (∀x ∈ X, P x) → P X) → ∀X : set, P X

∀A : set, ∀F : set → set, ∀y : set, y ∈ {F x|x ∈ A} ↔ ∃x ∈ A, y = F x

Beginning of Section **PropN**

Variable P1 P2 P3 : prop

P1 ∧ P2 ∧ P3 → (∀p : prop, (P1 → P2 → P3 → p) → p)

P1 ∨ P2 ∨ P3 → (∀p : prop, (P1 → p) → (P2 → p) → (P3 → p) → p)

Variable P4 : prop

P1 ∧ P2 ∧ P3 ∧ P4 → (∀p : prop, (P1 → P2 → P3 → P4 → p) → p)

P1 ∨ P2 ∨ P3 ∨ P4 → (∀p : prop, (P1 → p) → (P2 → p) → (P3 → p) → (P4 → p) → p)

Variable P5 : prop

P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5 → (∀p : prop, (P1 → P2 → P3 → P4 → P5 → p) → p)

P1 ∨ P2 ∨ P3 ∨ P4 ∨ P5 → (∀p : prop, (P1 → p) → (P2 → p) → (P3 → p) → (P4 → p) → (P5 → p) → p)

Variable P6 : prop

P1 → P2 → P3 → P4 → P5 → P6 → P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5 ∧ P6

P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5 ∧ P6 → (∀p : prop, (P1 → P2 → P3 → P4 → P5 → P6 → p) → p)

Variable P7 : prop

P1 → P2 → P3 → P4 → P5 → P6 → P7 → P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5 ∧ P6 ∧ P7

P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5 ∧ P6 ∧ P7 → (∀p : prop, (P1 → P2 → P3 → P4 → P5 → P6 → P7 → p) → p)

End of Section **PropN**

∀X x : set, x ∈ ⋃ X → ∀p : prop, (∀Y : set, x ∈ Y → Y ∈ X → p) → p

∀A B : prop, (A → ¬ B) → (¬ A → B) → exactly1of2 A B

∀A B : prop, (B → ¬ A) → (¬ B → A) → exactly1of2 A B

∀A B : prop, exactly1of2 A B → ∀p : prop, (A → ¬ B → p) → (¬ A → B → p) → p

∀A B : prop, exactly1of2 A B → A → ¬ B

∀A B : prop, exactly1of2 A B → B → ¬ A

∀A B : prop, exactly1of2 A B → ¬ A → B

∀A B : prop, exactly1of2 A B → ¬ B → A

∀A B C : prop, A → ¬ B → ¬ C → exactly1of3 A B C

∀A B C : prop, ¬ A → B → ¬ C → exactly1of3 A B C

∀A B C : prop, ¬ A → ¬ B → C → exactly1of3 A B C

∀A B C : prop, (A → ¬ B) → (A → ¬ C) → (B → ¬ C) → (¬ A → B ∨ C) → exactly1of3 A B C

∀A B C : prop, (B → ¬ A) → (B → ¬ C) → (A → ¬ C) → (¬ B → A ∨ C) → exactly1of3 A B C

∀A B C : prop, (C → ¬ A) → (C → ¬ B) → (A → ¬ B) → (¬ A → B) → exactly1of3 A B C

∀A B C : prop, exactly1of3 A B C → ∀p : prop, (A → ¬ B → ¬ C → p) → (¬ A → B → ¬ C → p) → (¬ A → ¬ B → C → p) → p

∀A B C : prop, exactly1of3 A B C → A ∨ B ∨ C

∀A B C : prop, exactly1of3 A B C → A → ¬ B

∀A B C : prop, exactly1of3 A B C → A → ¬ C

∀A B C : prop, exactly1of3 A B C → B → ¬ A

∀A B C : prop, exactly1of3 A B C → B → ¬ C

∀A B C : prop, exactly1of3 A B C → C → ¬ A

∀A B C : prop, exactly1of3 A B C → C → ¬ B

∀A B C : prop, exactly1of3 A B C → ¬ A → B ∨ C

∀A B C : prop, exactly1of3 A B C → ¬ B → A ∨ C

∀A B C : prop, exactly1of3 A B C → ¬ C → A ∨ B

∀A : set, ∀F : set → set, ∀x : set, x ∈ A → F x ∈ {F x|x ∈ A}

∀A : set, ∀F : set → set, ∀y : set, y ∈ {F x|x ∈ A} → ∃x ∈ A, y = F x

∀A : set, ∀F : set → set, ∀y : set, y ∈ {F x|x ∈ A} → ∀p : prop, (∀x : set, x ∈ A → y = F x → p) → p

∀X, ∀F G : set → set, (∀x ∈ X, F x = G x) → {F x|x ∈ X} ⊆ {G x|x ∈ X}

∀X, ∀F G : set → set, (∀x ∈ X, F x = G x) → {F x|x ∈ X} = {G x|x ∈ X}

∀p : prop, ∀x y : set, p ∧ (if p then x else y) = x ∨ ¬ p ∧ (if p then x else y) = y

∀p : prop, ∀x y : set, ¬ p → (if p then x else y) = y

∀p : prop, ∀x y : set, p → (if p then x else y) = x

∀p : prop, ∀x y : set, (if p then x else y) = x ∨ (if p then x else y) = y

∀F : set → set, ∀x y : set, {F z|z ∈ {x,y}} = {F x,F y}

∀F : set → set, ∀x : set, {F z|z ∈ {x}} = {F x}

∀X : set, ∀F G : set → set, (∀x : set, x ∈ X → F x = G x) → {F x|x ∈ X} = {G x|x ∈ X}

∀X : set, ∀F : (set → set), ∀x y : set, x ∈ X → y ∈ F x → y ∈ ⋃_{x ∈ X}F x

∀X : set, ∀F : (set → set), ∀y : set, y ∈ (⋃_{x ∈ X}F x) → ∃x ∈ X, y ∈ F x

∀X : set, ∀F : (set → set), ∀y : set, y ∈ (⋃_{x ∈ X}F x) → ∀p : prop, (∀x, x ∈ X → y ∈ F x → p) → p

∀X : set, ∀F : (set → set), {F x|x ∈ X} = ⋃_{x ∈ X}{F x}

∀X : set, ∀P : (set → prop), ∀x : set, x ∈ X → P x → x ∈ {x ∈ X|P x}

∀X : set, ∀P : (set → prop), ∀x : set, x ∈ {x ∈ X|P x} → x ∈ X ∧ P x

∀X : set, ∀P : (set → prop), ∀x : set, x ∈ {x ∈ X|P x} → x ∈ X

∀X : set, ∀P : (set → prop), ∀x : set, x ∈ {x ∈ X|P x} → P x

∀X : set, ∀P : set → prop, {x ∈ X|P x} ∈ 𝒫 X

∀X : set, ∀P : set → prop, ∀F : set → set, ∀x : set, x ∈ X → P x → F x ∈ {F x|x ∈ X, P x}

∀X : set, ∀P : set → prop, ∀F : set → set, ∀y : set, y ∈ {F x|x ∈ X, P x} → ∃x : set, x ∈ X ∧ P x ∧ y = F x

∀X : set, ∀P : set → prop, ∀F : set → set, ∀y : set, y ∈ {F x|x ∈ X, P x} → ∀p : prop, (∀x ∈ X, P x → y = F x → p) → p

∀A, ∀B : set → set, ∀P : set → set → prop, ∀F : set → set → set, ∀x ∈ A, ∀y ∈ B x, P x y → F x y ∈ ReplSep2 A B P F

∀A, ∀B : set → set, ∀P : set → set → prop, ∀F : set → set → set, ∀r ∈ ReplSep2 A B P F, ∀p : prop, (∀x ∈ A, ∀y ∈ B x, P x y → r = F x y → p) → p

∀A, ∀B : set → set, ∀P : set → set → prop, ∀F : set → set → set, ∀r ∈ ReplSep2 A B P F, ∃x ∈ A, ∃y ∈ B x, P x y ∧ r = F x y

∀X Y Z : set, X ⊆ Z → Y ⊆ Z → X ∪ Y ⊆ Z

∀X Y Z : set, Z ⊆ X → Z ⊆ Y → Z ⊆ X ∩ Y

∀X Y Z : set, X ∩ (Y ∩ Z) = (X ∩ Y) ∩ Z

∀X Y Z : set, X ∩ (Y ∪ Z) = X ∩ Y ∪ X ∩ Z

∀X Y Z : set, X ∪ Y ∩ Z = (X ∪ Y) ∩ (X ∪ Z)

∀X Y : set, (X ⊆ Y) = (X ∩ Y = X)

∀X Y z : set, z ∉ X ∩ Y → z ∉ X ∨ z ∉ Y

∀X Y Z : set, Z ⊆ Y → X ∖ Y ⊆ X ∖ Z

∀X Y Z : set, X ∖ Y ∩ Z = (X ∖ Y) ∪ (X ∖ Z)

∀X Y Z : set, (X ∩ Y) ∖ Z = X ∩ (Y ∖ Z)

∀X Y Z : set, X ∪ Y ∖ Z = (X ∖ Z) ∪ (Y ∖ Z)

∀X Y Z : set, X ∖ (Y ∖ Z) = (X ∖ Y) ∪ (X ∩ Z)

∀i ∈ 4, ∀p : set → prop, p 0 → p 1 → p 2 → p 3 → p i

∀i ∈ 5, ∀p : set → prop, p 0 → p 1 → p 2 → p 3 → p 4 → p i

∀i ∈ 6, ∀p : set → prop, p 0 → p 1 → p 2 → p 3 → p 4 → p 5 → p i

∀U, Union_closed U → Power_closed U → Repl_closed U → ZF_closed U

∀U, ZF_closed U → ∀p : prop, (Union_closed U → Power_closed U → Repl_closed U → p) → p

∀U, ZF_closed U → ∀X ∈ U, ∀F : set → set, (∀x ∈ X, F x ∈ U) → {F x|x ∈ X} ∈ U

∀U, ZF_closed U → ∀X Y ∈ U, (X ∪ Y) ∈ U

∀X Y, ∀f : set → set, (∀u ∈ X, f u ∈ Y) → (∀u v ∈ X, f u = f v → u = v) → (∀w ∈ Y, ∃u ∈ X, f u = w) → bij X Y f

∀X Y, ∀f : set → set, bij X Y f → ∀p : prop, ((∀u ∈ X, f u ∈ Y) → (∀u v ∈ X, f u = f v → u = v) → (∀w ∈ Y, ∃u ∈ X, f u = w) → p) → p

∀X Y, ∀f : set → set, (∀u v ∈ X, f u = f v → u = v) → ∀x ∈ X, inv X f (f x) = x

∀f : set → set, ∀U V, U ⊆ V → {f x|x ∈ U} ⊆ {f x|x ∈ V}

∀f : set → set → set, ∀x y z w, x = y → z = w → f x z = f y w

∀X, ∀f g : set → set, (∀x ∈ X, f (g x) = x) → {f y|y ∈ {g x|x ∈ X}} = X

∀X, ∀f : set → set, (∀x ∈ X, f (f x) = x) → {f y|y ∈ {f x|x ∈ X}} = X

∀P Q : set → prop, (∃x, P x ∧ Q x) → ∀r : prop, (∀x, P x → Q x → r) → r

∀P Q : (set → set) → prop, (∃x : set → set, P x ∧ Q x) → ∀p : prop, (∀x : set → set, P x → Q x → p) → p

∀P Q : (set → set → set) → prop, (∃x : set → set → set, P x ∧ Q x) → ∀p : prop, (∀x : set → set → set, P x → Q x → p) → p

∀P Q : (set → set → set → set) → prop, (∃x : set → set → set → set, P x ∧ Q x) → ∀p : prop, (∀x : set → set → set → set, P x → Q x → p) → p

∀P Q : (set → set → prop) → prop, (∃x : set → set → prop, P x ∧ Q x) → ∀p : prop, (∀x : set → set → prop, P x → Q x → p) → p

∀P Q : (set → set → set → prop) → prop, (∃x : set → set → set → prop, P x ∧ Q x) → ∀p : prop, (∀x : set → set → set → prop, P x → Q x → p) → p

Beginning of Section **Descr_ii**

Variable P : (set → set) → prop

Hypothesis Pex : ∃f : set → set, P f

Hypothesis Puniq : ∀f g : set → set, P f → P g → f = g

End of Section **Descr_ii**

Beginning of Section **Descr_iii**

Variable P : (set → set → set) → prop

Hypothesis Pex : ∃f : set → set → set, P f

Hypothesis Puniq : ∀f g : set → set → set, P f → P g → f = g

End of Section **Descr_iii**

Beginning of Section **Descr_iio**

Variable P : (set → set → prop) → prop

Hypothesis Pex : ∃f : set → set → prop, P f

Hypothesis Puniq : ∀f g : set → set → prop, P f → P g → f = g

End of Section **Descr_iio**

Beginning of Section **Descr_Vo1**

Variable P : Vo 1 → prop

Hypothesis Pex : ∃f : Vo 1, P f

Hypothesis Puniq : ∀f g : Vo 1, P f → P g → f = g

End of Section **Descr_Vo1**

Beginning of Section **Descr_Vo2**

Variable P : Vo 2 → prop

Hypothesis Pex : ∃f : Vo 2, P f

Hypothesis Puniq : ∀f g : Vo 2, P f → P g → f = g

End of Section **Descr_Vo2**

Beginning of Section **EpsilonRec_i**

Variable F : set → (set → set) → set

Hypothesis Fr : ∀X : set, ∀g h : set → set, (∀x ∈ X, g x = h x) → F X g = F X h

End of Section **EpsilonRec_i**

Beginning of Section **EpsilonRec_ii**

Variable F : set → (set → (set → set)) → (set → set)

Hypothesis Fr : ∀X : set, ∀g h : set → (set → set), (∀x ∈ X, g x = h x) → F X g = F X h

End of Section **EpsilonRec_ii**

Beginning of Section **EpsilonRec_iii**

Variable F : set → (set → (set → set → set)) → (set → set → set)

Hypothesis Fr : ∀X : set, ∀g h : set → (set → set → set), (∀x ∈ X, g x = h x) → F X g = F X h

End of Section **EpsilonRec_iii**

Beginning of Section **EpsilonRec_iio**

Variable F : set → (set → (set → set → prop)) → (set → set → prop)

Hypothesis Fr : ∀X : set, ∀g h : set → (set → set → prop), (∀x ∈ X, g x = h x) → F X g = F X h

End of Section **EpsilonRec_iio**

Beginning of Section **EpsilonRec_Vo1**

Variable F : set → (set → Vo 1) → Vo 1

Hypothesis Fr : ∀X : set, ∀g h : set → Vo 1, (∀x ∈ X, g x = h x) → F X g = F X h

End of Section **EpsilonRec_Vo1**

Beginning of Section **EpsilonRec_Vo2**

Variable F : set → (set → Vo 2) → Vo 2

Hypothesis Fr : ∀X : set, ∀g h : set → Vo 2, (∀x ∈ X, g x = h x) → F X g = F X h

End of Section **EpsilonRec_Vo2**

Beginning of Section **Descr_Vo3**

Variable P : Vo 3 → prop

Hypothesis Pex : ∃f : Vo 3, P f

Hypothesis Puniq : ∀f g : Vo 3, P f → P g → f = g

End of Section **Descr_Vo3**

Beginning of Section **EpsilonRec_Vo3**

Variable F : set → (set → Vo 3) → Vo 3

Hypothesis Fr : ∀X : set, ∀g h : set → Vo 3, (∀x ∈ X, g x = h x) → F X g = F X h

End of Section **EpsilonRec_Vo3**

Beginning of Section **Descr_Vo4**

Variable P : Vo 4 → prop

Hypothesis Pex : ∃f : Vo 4, P f

Hypothesis Puniq : ∀f g : Vo 4, P f → P g → f = g

End of Section **Descr_Vo4**

Beginning of Section **EpsilonRec_Vo4**

Variable F : set → (set → Vo 4) → Vo 4

Hypothesis Fr : ∀X : set, ∀g h : set → Vo 4, (∀x ∈ X, g x = h x) → F X g = F X h

End of Section **EpsilonRec_Vo4**

∀R : set → set → prop, per R → ∀x y z : set, R y x → R y z → R x z

∀R : set → set → prop, per R → ∀x y z : set, R x y → R z y → R x z

∀R : set → set → prop, per R → ∀x y z : set, R y x → R z y → R x z

∀R : set → set → prop, per R → ∀x y : set, R x y → R x x

∀R : set → set → prop, per R → ∀x y : set, R x y → R y y

∀R : set → set → prop, partialorder R → strictpartialorder (λx y ⇒ R x y ∧ x ≠ y)

∀R : set → set → prop, strictpartialorder R → partialorder (reflclos R)

∀R : set → set → prop, stricttotalorder R → totalorder (reflclos R)

Beginning of Section **Zermelo1908**

∀p : set → prop, (∃x : set, p x) → ∃x : set, p x ∧ ∀y : set, p y → ZermeloWO x y

∀p : set → prop, (∃x : set, p x) → ∃x : set, p x ∧ ∀y : set, p y ∧ y ≠ x → ZermeloWOstrict x y

∃r : set → set → prop, totalorder r ∧ (∀p : set → prop, (∃x : set, p x) → ∃x : set, p x ∧ ∀y : set, p y → r x y)

∃r : set → set → prop, stricttotalorder r ∧ (∀p : set → prop, (∃x : set, p x) → ∃x : set, p x ∧ ∀y : set, p y ∧ y ≠ x → r x y)

End of Section **Zermelo1908**

(λx y : prop ⇒ (x → y)) = (λx y : prop ⇒ (¬ x ∨ y))

Beginning of Section **NatRec**

Variable z : set

Variable f : set → set → set

∀X : set, ∀g h : set → set, (∀x ∈ X, g x = h x) → F X g = F X h

∀n : set, nat_p n → nat_primrec (ordsucc n) = f n (nat_primrec n)

End of Section **NatRec**

Beginning of Section **NatArith**

End of Section **NatArith**

∀i ∈ 7, ∀p : set → prop, p 0 → p 1 → p 2 → p 3 → p 4 → p 5 → p 6 → p i

∀i ∈ 8, ∀p : set → prop, p 0 → p 1 → p 2 → p 3 → p 4 → p 5 → p 6 → p 7 → p i

∀i ∈ 9, ∀p : set → prop, p 0 → p 1 → p 2 → p 3 → p 4 → p 5 → p 6 → p 7 → p 8 → p i

∀alpha beta : set, ordinal alpha → ordinal beta → exactly1of3 (alpha ∈ beta) (alpha = beta) (beta ∈ alpha)

∀X Y, ∀f g : set → set, ∀x, combine_funcs X Y f g (Inj0 x) = f x

∀X Y, ∀f g : set → set, ∀y, combine_funcs X Y f g (Inj1 y) = g y

Beginning of Section **pair_setsum**

Let pair ≝ setsum

∀X Y z, z ∈ pair X Y → (∃x ∈ X, z = pair 0 x) ∨ (∃y ∈ Y, z = pair 1 y)

∀X Y z, z ∈ pair X Y ↔ (∃x ∈ X, z = pair 0 x) ∨ (∃y ∈ Y, z = pair 1 y)

∀x y w z : set, pair x y = pair w z → x = w ∧ y = z

∀X : set, ∀Y : set → set, ∀x ∈ X, ∀y ∈ Y x, pair x y ∈ ∑x ∈ X, Y x

∀X : set, ∀Y : set → set, ∀z : set, z ∈ (∑x ∈ X, Y x) → proj0 z ∈ X

∀X : set, ∀Y : set → set, ∀x y : set, pair x y ∈ (∑x ∈ X, Y x) → x ∈ X

∀X : set, ∀Y : set → set, ∀x y : set, pair x y ∈ (∑x ∈ X, Y x) → y ∈ Y x

∀X : set, ∀Y : set → set, ∀z : set, z ∈ (∑x ∈ X, Y x) → ∃x ∈ X, ∃y ∈ Y x, z = pair x y

∀X : set, ∀Y : set → set, ∀z : set, z ∈ (∑x ∈ X, Y x) ↔ ∃x ∈ X, ∃y ∈ Y x, z = pair x y

∀X Y : set, X ⊆ Y → ∀Z W : set → set, (∀x ∈ X, Z x ⊆ W x) → (∑x ∈ X, Z x) ⊆ ∑y ∈ Y, W y

∀X Y : set, X ⊆ Y → ∀Z : set → set, (∑x ∈ X, Z x) ⊆ ∑y ∈ Y, Z y

∀X : set, ∀Z W : set → set, (∀x, x ∈ X → Z x ⊆ W x) → (∑x ∈ X, Z x) ⊆ ∑x ∈ X, W x

∀X Y : set, ∀(x ∈ X)(y ∈ Y), pair x y ∈ X ⨯ Y

∀X Y x y : set, pair x y ∈ X ⨯ Y → x ∈ X

∀X Y x y : set, pair x y ∈ X ⨯ Y → y ∈ Y

Let lam : set → (set → set) → set ≝ Sigma

∀X : set, ∀F : set → set, ∀x ∈ X, ∀y ∈ F x, pair x y ∈ λx ∈ X ⇒ F x

∀X : set, ∀F : set → set, ∀z : set, z ∈ (λx ∈ X ⇒ F x) → ∃x ∈ X, ∃y ∈ F x, z = pair x y

∀X : set, ∀F : set → set, ∀z, z ∈ (λx ∈ X ⇒ F x) ↔ ∃x ∈ X, ∃y ∈ F x, z = pair x y

∀X : set, ∀F : set → set, ∀x : set, x ∈ X → (λx ∈ X ⇒ F x) x = F x

∀X : set, ∀F : set → set, ∀x : set, x ∉ X → (λx ∈ X ⇒ F x) x = 0

∀X : set, ∀Y : set → set, ∀z : set, z ∈ (∑x ∈ X, Y x) → (z 0) ∈ X

∀X : set, ∀Y : set → set, ∀z : set, z ∈ (∑x ∈ X, Y x) → (z 1) ∈ (Y (z 0))

∀X : set, ∀Y : set → set, ∀f : set, (∀u ∈ f, pair_p u ∧ u 0 ∈ X) → (∀x ∈ X, f x ∈ Y x) → f ∈ ∏x ∈ X, Y x

∀X : set, ∀Y : set → set, ∀f : set, f ∈ (∏x ∈ X, Y x) → (∀u ∈ f, pair_p u ∧ u 0 ∈ X) ∧ (∀x ∈ X, f x ∈ Y x)

∀X : set, ∀Y : set → set, ∀F : set → set, (∀x ∈ X, F x ∈ Y x) → (λx ∈ X ⇒ F x) ∈ (∏x ∈ X, Y x)

∀X : set, ∀Y : set → set, ∀f : set, ∀x : set, f ∈ (∏x ∈ X, Y x) → x ∈ X → f x ∈ Y x

∀X : set, ∀Y : set → set, ∀f g ∈ (∏x ∈ X, Y x), (∀x ∈ X, f x ⊆ g x) → f ⊆ g

∀X : set, ∀Y : set → set, ∀f g ∈ (∏x ∈ X, Y x), (∀x ∈ X, f x = g x) → f = g

∀X : set, ∀Y : set → set, ∀f : set, f ∈ (∏x ∈ X, Y x) → (λx ∈ X ⇒ f x) = f

∀X, ∀F : set → set, ∀x ∈ X, ∀y ∈ F x, (x,y) ∈ λx ∈ X ⇒ F x

∀X, ∀F : set → set, ∀z : set, z ∈ (λx ∈ X ⇒ F x) → ∃x ∈ X, ∃y ∈ F x, z = (x,y)

∀x y w z : set, (x,y) = (w,z) → x = w ∧ y = z

∀X, ∀Y : set → set, ∀R : set → set → prop, ∀x ∈ X, ∀y ∈ Y x, R x y → (x,y) ∈ Sep2 X Y R

∀X, ∀Y : set → set, ∀R : set → set → prop, ∀u ∈ Sep2 X Y R, ∃x ∈ X, ∃y ∈ Y x, u = (x,y) ∧ R x y

∀X, ∀Y : set → set, ∀R : set → set → prop, ∀x y, (x,y) ∈ Sep2 X Y R → x ∈ X ∧ y ∈ Y x ∧ R x y

∀X, ∀Y : set → set, ∀R : set → set → prop, ∀x y, (x,y) ∈ Sep2 X Y R → x ∈ X

∀X, ∀Y : set → set, ∀R : set → set → prop, ∀x y, (x,y) ∈ Sep2 X Y R → y ∈ Y x

∀X, ∀Y : set → set, ∀R : set → set → prop, ∀x y, (x,y) ∈ Sep2 X Y R → R x y

∀X Y, set_of_pairs X → set_of_pairs Y → (∀v w, (v,w) ∈ X ↔ (v,w) ∈ Y) → X = Y

∀X, ∀Y : set → set, ∀R : set → set → prop, set_of_pairs (Sep2 X Y R)

∀X, ∀F G : set → set, (∀x ∈ X, F x = G x) → (λx ∈ X ⇒ F x) ⊆ (λx ∈ X ⇒ G x)

∀X, ∀F G : set → set, (∀x ∈ X, F x = G x) → (λx ∈ X ⇒ F x) = (λx ∈ X ⇒ G x)

∀X, ∀F : set → set, (λx ∈ X ⇒ (λx ∈ X ⇒ F x) x) = (λx ∈ X ⇒ F x)

∀X, ∀Y : set → set, ∀F : set → set → set, ∀x ∈ X, ∀y ∈ Y x, lam2 X Y F x y = F x y

∀X Y : set, X ⊆ Y → ∀Z W : set, Z ⊆ W → X ⨯ Z ⊆ Y ⨯ W

∀X Y : set, X ⊆ Y → ∀Z : set, X ⨯ Z ⊆ Y ⨯ Z

∀X : set, ∀Z W : set, Z ⊆ W → X ⨯ Z ⊆ X ⨯ W

∀X : set, ∀Y : set → set, ∀z ∈ (∑x ∈ X, Y x), pair (z 0) (z 1) = z

∀X Y, ∀F G : set → set → set, (∀x ∈ X, ∀y ∈ Y, F x y = G x y) → {F (w 0) (w 1)|w ∈ X ⨯ Y} = {G (w 0) (w 1)|w ∈ X ⨯ Y}

∀X Y : set, ∀A : set → set, X ⊆ Y → (∀y ∈ Y, y ∉ X → 0 ∈ A y) → (∏x ∈ X, A x) ⊆ ∏y ∈ Y, A y

∀X : set, ∀A B : set → set, (∀x ∈ X, A x ⊆ B x) → (∏x ∈ X, A x) ⊆ ∏x ∈ X, B x

∀X Y : set, ∀A B : set → set, (∀x ∈ X, A x ⊆ B x) → X ⊆ Y → (∀y ∈ Y, y ∉ X → 0 ∈ B y) → (∏x ∈ X, A x) ⊆ ∏y ∈ Y, B y

∀A : set, 0 ∈ A → ∀X Y : set, X ⊆ Y → A^{X} ⊆ A^{Y}

∀X Y A B : set, 0 ∈ B → A ⊆ B → X ⊆ Y → A^{X} ⊆ B^{Y}

∀A : set, 0 ∈ A → ∀n, nat_p n → ∀m ∈ n, A^{m} ⊆ A^{n}

∀X Y z, z ∈ (X,Y) → (∃x ∈ X, z = (0,x)) ∨ (∃y ∈ Y, z = (1,y))

∀X : set, ∀Y : set → set, ∀x ∈ X, ∀y ∈ Y x, (x,y) ∈ ∑x ∈ X, Y x

∀X : set, ∀Y : set, ∀x ∈ X, ∀y ∈ Y, (x,y) ∈ X ⨯ Y

∀X : set, ∀Y : set → set, ∀z ∈ (∑x ∈ X, Y x), (z 0,z 1) = z

∀x y, x ∈ 2 → y ∈ 2 → x ≠ y → bij 2 2 (λi ⇒ (x,y) i)

∀x y z w, (λi ∈ 4 ⇒ (x,y,z,w) i) = (x,y,z,w)

Beginning of Section **Tuples**

Variable x0 x1 x2 : set

Variable x3 : set

Variable x4 : set

Variable x5 : set

Variable x6 : set

Variable x7 : set

Variable x8 : set

End of Section **Tuples**

End of Section **pair_setsum**

∀x y z A, x ∈ A → y ∈ A → z ∈ A → (x,y,z) ∈ A^{3}

∀x y z, x ∈ 3 → y ∈ 3 → z ∈ 3 → x ≠ y → x ≠ z → y ≠ z → bij 3 3 (λi ⇒ (x,y,z) i)

∀x y z w A, x ∈ A → y ∈ A → z ∈ A → w ∈ A → (x,y,z,w) ∈ A^{4}

∀x y z w, x ∈ 4 → y ∈ 4 → z ∈ 4 → w ∈ 4 → x ≠ y → x ≠ z → x ≠ w → y ≠ z → y ≠ w → z ≠ w → bij 4 4 (λi ⇒ (x,y,z,w) i)

∀P : set → prop, (¬ ∃x, P x) → ∀x, ¬ P x

∀P : set → prop, ¬ (∀x, P x) → ∃x, ¬ P x

∀R : set → set → prop, (∃x y, R x y) → R (EpsR_i_i_1 R) (EpsR_i_i_2 R)

∀R : set → (set → prop) → prop, (∃x, (∃y : set → prop, R x y) ∧ (∀y z : set → prop, R x y → R x z → y = z)) → R (DescrR_i_io_1 R) (DescrR_i_io_2 R)

∀alpha, ∀p : set → prop, ¬ PNoLt_ alpha p p

∀alpha, ∀p : set → prop, ¬ PNoLt alpha p alpha p

∀alpha, ∀p : set → prop, PNoLe alpha p alpha p

∀L R : set → (set → prop) → prop, PNoLt_pwise L R → PNoLt_pwise (PNo_downc L) (PNo_upc R)

∀L : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀p q : set → prop, PNoEq_ alpha p q → PNo_rel_strict_upperbd L alpha p → PNo_rel_strict_upperbd L alpha q

∀L : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀p : set → prop, ∀beta ∈ alpha, PNo_rel_strict_upperbd L alpha p → PNo_rel_strict_upperbd L beta p

∀R : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀p q : set → prop, PNoEq_ alpha p q → PNo_rel_strict_lowerbd R alpha p → PNo_rel_strict_lowerbd R alpha q

∀R : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀p : set → prop, ∀beta ∈ alpha, PNo_rel_strict_lowerbd R alpha p → PNo_rel_strict_lowerbd R beta p

∀L R : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀p q : set → prop, PNoEq_ alpha p q → PNo_rel_strict_imv L R alpha p → PNo_rel_strict_imv L R alpha q

∀L R : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀p : set → prop, ∀beta ∈ alpha, PNo_rel_strict_imv L R alpha p → PNo_rel_strict_imv L R beta p

∀alpha, ∀p : set → prop, PNoEq_ alpha p (λdelta ⇒ p delta ∧ delta ≠ alpha)

∀alpha, ∀p : set → prop, PNoEq_ alpha p (λdelta ⇒ p delta ∨ delta = alpha)

∀L R : set → (set → prop) → prop, PNoLt_pwise L R → ∀alpha, ordinal alpha → (∃p : set → prop, PNo_rel_strict_uniq_imv L R alpha p) ∨ (∃tau ∈ alpha, ∃p : set → prop, PNo_rel_strict_split_imv L R tau p)

∀L R : set → (set → prop) → prop, ∀alpha, ordinal alpha → PNo_lenbdd alpha L → PNo_lenbdd alpha R → ∀p : set → prop, PNo_rel_strict_imv L R alpha p → PNo_rel_strict_imv L R (ordsucc alpha) (λdelta ⇒ p delta ∧ delta ≠ alpha)

∀L R : set → (set → prop) → prop, ∀alpha, ordinal alpha → PNo_lenbdd alpha L → PNo_lenbdd alpha R → ∀p : set → prop, PNo_rel_strict_imv L R alpha p → PNo_rel_strict_imv L R (ordsucc alpha) (λdelta ⇒ p delta ∨ delta = alpha)

∀L R : set → (set → prop) → prop, ∀alpha, ordinal alpha → PNo_lenbdd alpha L → PNo_lenbdd alpha R → ∀p : set → prop, PNo_rel_strict_imv L R alpha p → PNo_rel_strict_split_imv L R alpha p

∀L R : set → (set → prop) → prop, PNoLt_pwise L R → ∀alpha, ordinal alpha → PNo_lenbdd alpha L → PNo_lenbdd alpha R → ∃beta ∈ ordsucc alpha, ∃p : set → prop, PNo_rel_strict_split_imv L R beta p

∀L : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀p q : set → prop, PNoEq_ alpha p q → PNo_strict_upperbd L alpha p → PNo_strict_upperbd L alpha q

∀R : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀p q : set → prop, PNoEq_ alpha p q → PNo_strict_lowerbd R alpha p → PNo_strict_lowerbd R alpha q

∀L R : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀p q : set → prop, PNoEq_ alpha p q → PNo_strict_imv L R alpha p → PNo_strict_imv L R alpha q

∀L : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀beta ∈ ordsucc alpha, ∀p : set → prop, PNo_strict_upperbd L alpha p → PNo_rel_strict_upperbd L beta p

∀R : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀beta ∈ ordsucc alpha, ∀p : set → prop, PNo_strict_lowerbd R alpha p → PNo_rel_strict_lowerbd R beta p

∀L R : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀beta ∈ ordsucc alpha, ∀p : set → prop, PNo_strict_imv L R alpha p → PNo_rel_strict_imv L R beta p

∀L R : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀p : set → prop, PNo_rel_strict_split_imv L R alpha p → PNo_strict_imv L R alpha p

∀L R : set → (set → prop) → prop, PNoLt_pwise L R → ∀alpha, ordinal alpha → PNo_lenbdd alpha L → PNo_lenbdd alpha R → ∃beta ∈ ordsucc alpha, ∃p : set → prop, PNo_strict_imv L R beta p

∀L R : set → (set → prop) → prop, PNoLt_pwise L R → ∀alpha, ordinal alpha → PNo_lenbdd alpha L → PNo_lenbdd alpha R → ∃beta, ∃p : set → prop, PNo_least_rep L R beta p

∀L R : set → (set → prop) → prop, PNoLt_pwise L R → ∀alpha, ordinal alpha → ∀p q : set → prop, PNo_least_rep L R alpha p → PNo_strict_imv L R alpha q → ∀beta ∈ alpha, p beta ↔ q beta

∀L R : set → (set → prop) → prop, PNoLt_pwise L R → ∀alpha, ordinal alpha → PNo_lenbdd alpha L → PNo_lenbdd alpha R → ∃beta, (∃p : set → prop, PNo_least_rep2 L R beta p) ∧ (∀p q : set → prop, PNo_least_rep2 L R beta p → PNo_least_rep2 L R beta q → p = q)

∀L R : set → (set → prop) → prop, PNoLt_pwise L R → ∀alpha, ordinal alpha → PNo_lenbdd alpha L → PNo_lenbdd alpha R → PNo_least_rep2 L R (PNo_bd L R) (PNo_pred L R)

∀L R : set → (set → prop) → prop, PNoLt_pwise L R → ∀alpha, ordinal alpha → PNo_lenbdd alpha L → PNo_lenbdd alpha R → PNo_least_rep L R (PNo_bd L R) (PNo_pred L R)

∀L R : set → (set → prop) → prop, PNoLt_pwise L R → ∀alpha, ordinal alpha → PNo_lenbdd alpha L → PNo_lenbdd alpha R → ordinal (PNo_bd L R)

∀L R : set → (set → prop) → prop, PNoLt_pwise L R → ∀alpha, ordinal alpha → PNo_lenbdd alpha L → PNo_lenbdd alpha R → PNo_strict_imv L R (PNo_bd L R) (PNo_pred L R)

∀L R : set → (set → prop) → prop, PNoLt_pwise L R → ∀alpha, ordinal alpha → PNo_lenbdd alpha L → PNo_lenbdd alpha R → ∀gamma ∈ PNo_bd L R, ∀q : set → prop, ¬ PNo_strict_imv L R gamma q

∀L R : set → (set → prop) → prop, PNoLt_pwise L R → ∀alpha, ordinal alpha → PNo_lenbdd alpha L → PNo_lenbdd alpha R → PNo_bd L R ∈ ordsucc alpha

∀alpha, ∀p : set → prop, PNo_lenbdd alpha (PNoCutL alpha p)

∀alpha, ∀p : set → prop, PNo_lenbdd alpha (PNoCutR alpha p)

∀alpha, ordinal alpha → ∀p : set → prop, PNoLt_pwise (PNoCutL alpha p) (PNoCutR alpha p)

∀alpha, ordinal alpha → ∀p : set → prop, PNo_strict_imv (PNoCutL alpha p) (PNoCutR alpha p) alpha p

Beginning of Section **TaggedSets**

Let tag : set → set ≝ λalpha ⇒ SetAdjoin alpha {1}

∀alpha y, ordinal alpha → (y ') ∉ alpha

∀alpha Y, ordinal alpha → alpha ∉ {y '|y ∈ Y}

Let ctag : set → set ≝ λalpha ⇒ SetAdjoin alpha {2}

∀alpha y, ordinal alpha → (y '') ∉ alpha

End of Section **TaggedSets**

∀x y, SNo x → SNo y → x < y → ∀p : prop, (∀z, SNo z → SNoLev z ∈ SNoLev x ∩ SNoLev y → SNoEq_ (SNoLev z) z x → SNoEq_ (SNoLev z) z y → x < z → z < y → SNoLev z ∉ x → SNoLev z ∈ y → p) → (SNoLev x ∈ SNoLev y → SNoEq_ (SNoLev x) x y → SNoLev x ∈ y → p) → (SNoLev y ∈ SNoLev x → SNoEq_ (SNoLev y) x y → SNoLev y ∉ x → p) → p

∀L R, SNoCutP L R → SNo (SNoCut L R) ∧ SNoLev (SNoCut L R) ∈ ordsucc ((⋃_{x ∈ L}ordsucc (SNoLev x)) ∪ (⋃_{y ∈ R}ordsucc (SNoLev y))) ∧ (∀x ∈ L, x < SNoCut L R) ∧ (∀y ∈ R, SNoCut L R < y) ∧ (∀z, SNo z → (∀x ∈ L, x < z) → (∀y ∈ R, z < y) → SNoLev (SNoCut L R) ⊆ SNoLev z ∧ SNoEq_ (SNoLev (SNoCut L R)) (SNoCut L R) z)

∀L R, SNoCutP L R → ∀p : prop, (SNo (SNoCut L R) → SNoLev (SNoCut L R) ∈ ordsucc ((⋃_{x ∈ L}ordsucc (SNoLev x)) ∪ (⋃_{y ∈ R}ordsucc (SNoLev y))) → (∀x ∈ L, x < SNoCut L R) → (∀y ∈ R, SNoCut L R < y) → (∀z, SNo z → (∀x ∈ L, x < z) → (∀y ∈ R, z < y) → SNoLev (SNoCut L R) ⊆ SNoLev z ∧ SNoEq_ (SNoLev (SNoCut L R)) (SNoCut L R) z) → p) → p

Beginning of Section **TaggedSets2**

Let tag : set → set ≝ λalpha ⇒ SetAdjoin alpha {1}

∀x, SNo x → SNo_ (ordsucc (SNoLev x)) (SNo_extend0 x)

∀x, SNo x → SNo_ (ordsucc (SNoLev x)) (SNo_extend1 x)

∀x, SNo x → SNoLev (SNo_extend0 x) = ordsucc (SNoLev x)

∀x, SNo x → SNoLev (SNo_extend1 x) = ordsucc (SNoLev x)

∀x, SNo x → SNoEq_ (SNoLev x) (SNo_extend0 x) x

∀x, SNo x → SNoEq_ (SNoLev x) (SNo_extend1 x) x

End of Section **TaggedSets2**

Beginning of Section **SurrealRecII**

Variable F : set → (set → (set → set)) → (set → set)

Hypothesis Fr : ∀z, SNo z → ∀g h : set → (set → set), (∀w ∈ SNoS_ (SNoLev z), g w = h w) → F z g = F z h

End of Section **SurrealRecII**

Beginning of Section **SurrealRec2**

Variable F : set → set → (set → set → set) → set

Hypothesis Fr : ∀w, SNo w → ∀z, SNo z → ∀g h : set → set → set, (∀x ∈ SNoS_ (SNoLev w), ∀y, SNo y → g x y = h x y) → (∀y ∈ SNoS_ (SNoLev z), g w y = h w y) → F w z g = F w z h

End of Section **SurrealRec2**

∀P : set → set → set → prop, (∀x y z, SNo x → SNo y → SNo z → (∀u ∈ SNoS_ (SNoLev x), P u y z) → (∀v ∈ SNoS_ (SNoLev y), P x v z) → (∀w ∈ SNoS_ (SNoLev z), P x y w) → (∀u ∈ SNoS_ (SNoLev x), ∀v ∈ SNoS_ (SNoLev y), P u v z) → (∀u ∈ SNoS_ (SNoLev x), ∀w ∈ SNoS_ (SNoLev z), P u y w) → (∀v ∈ SNoS_ (SNoLev y), ∀w ∈ SNoS_ (SNoLev z), P x v w) → (∀u ∈ SNoS_ (SNoLev x), ∀v ∈ SNoS_ (SNoLev y), ∀w ∈ SNoS_ (SNoLev z), P u v w) → P x y z) → ∀x y z, SNo x → SNo y → SNo z → P x y z

∀Phi : set → set → set, ∀X, ∀c : set, unpack_e_i (pack_e X c) Phi = Phi X c

∀Phi : set → set → prop, ∀X, ∀c : set, unpack_e_o (pack_e X c) Phi = Phi X c