Beginning of Section Eq
Variable A : SType
End of Section Eq
Beginning of Section FE
Variable A B : SType
Axiom. (func_ext) We take the following as an axiom:
∀f g : A → B, (∀x : A, f x = g x) → f = g
End of Section FE
Beginning of Section Ex
Variable A : SType
End of Section Ex
Axiom. (In_ind) We take the following as an axiom:
∀P : set → prop, (∀X : set, (∀x ∈ X, P x) → P X) → ∀X : set, P X
Axiom. (ReplEq) We take the following as an axiom:
∀A : set, ∀F : set → set, ∀y : set, y ∈ {F x|x ∈ A} ↔ ∃x ∈ A, y = F x
Axiom. (andI) We take the following as an axiom:
∀A B : prop, A → B → A ∧ B
Axiom. (orE) We take the following as an axiom:
∀A B C : prop, (A → C) → (B → C) → A ∨ B → C
Beginning of Section PropN
Variable P1 P2 P3 : prop
Axiom. (and3I) We take the following as an axiom:
P1 → P2 → P3 → P1 ∧ P2 ∧ P3
Axiom. (and3E) We take the following as an axiom:
P1 ∧ P2 ∧ P3 → (∀p : prop, (P1 → P2 → P3 → p) → p)
Axiom. (or3E) We take the following as an axiom:
P1 ∨ P2 ∨ P3 → (∀p : prop, (P1 → p) → (P2 → p) → (P3 → p) → p)
Variable P4 : prop
Axiom. (and4I) We take the following as an axiom:
P1 → P2 → P3 → P4 → P1 ∧ P2 ∧ P3 ∧ P4
Axiom. (and4E) We take the following as an axiom:
P1 ∧ P2 ∧ P3 ∧ P4 → (∀p : prop, (P1 → P2 → P3 → P4 → p) → p)
Axiom. (or4E) We take the following as an axiom:
P1 ∨ P2 ∨ P3 ∨ P4 → (∀p : prop, (P1 → p) → (P2 → p) → (P3 → p) → (P4 → p) → p)
Variable P5 : prop
Axiom. (and5I) We take the following as an axiom:
P1 → P2 → P3 → P4 → P5 → P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5
Axiom. (and5E) We take the following as an axiom:
P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5 → (∀p : prop, (P1 → P2 → P3 → P4 → P5 → p) → p)
Axiom. (or5E) We take the following as an axiom:
P1 ∨ P2 ∨ P3 ∨ P4 ∨ P5 → (∀p : prop, (P1 → p) → (P2 → p) → (P3 → p) → (P4 → p) → (P5 → p) → p)
Variable P6 : prop
Axiom. (and6I) We take the following as an axiom:
P1 → P2 → P3 → P4 → P5 → P6 → P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5 ∧ P6
Axiom. (and6E) We take the following as an axiom:
P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5 ∧ P6 → (∀p : prop, (P1 → P2 → P3 → P4 → P5 → P6 → p) → p)
Variable P7 : prop
Axiom. (and7I) We take the following as an axiom:
P1 → P2 → P3 → P4 → P5 → P6 → P7 → P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5 ∧ P6 ∧ P7
Axiom. (and7E) We take the following as an axiom:
P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5 ∧ P6 ∧ P7 → (∀p : prop, (P1 → P2 → P3 → P4 → P5 → P6 → P7 → p) → p)
End of Section PropN
Axiom. (and8I) We take the following as an axiom:
∀P0 P1 P2 P3 P4 P5 P6 P7 : prop, P0 → P1 → P2 → P3 → P4 → P5 → P6 → P7 → P0 ∧ P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5 ∧ P6 ∧ P7
Axiom. (and9I) We take the following as an axiom:
∀P0 P1 P2 P3 P4 P5 P6 P7 P8 : prop, P0 → P1 → P2 → P3 → P4 → P5 → P6 → P7 → P8 → P0 ∧ P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5 ∧ P6 ∧ P7 ∧ P8
Axiom. (and10I) We take the following as an axiom:
∀P0 P1 P2 P3 P4 P5 P6 P7 P8 P9 : prop, P0 → P1 → P2 → P3 → P4 → P5 → P6 → P7 → P8 → P9 → P0 ∧ P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5 ∧ P6 ∧ P7 ∧ P8 ∧ P9
Axiom. (iffI) We take the following as an axiom:
∀A B : prop, (A → B) → (B → A) → (A ↔ B)
Axiom. (iffEL) We take the following as an axiom:
∀A B : prop, (A ↔ B) → A → B
Axiom. (iffER) We take the following as an axiom:
∀A B : prop, (A ↔ B) → B → A
Axiom. (pred_ext) We take the following as an axiom:
∀P Q : set → prop, (∀x, P x ↔ Q x) → P = Q
Axiom. (ReplI) We take the following as an axiom:
∀A : set, ∀F : set → set, ∀x : set, x ∈ A → F x ∈ {F x|x ∈ A}
Axiom. (ReplE) We take the following as an axiom:
∀A : set, ∀F : set → set, ∀y : set, y ∈ {F x|x ∈ A} → ∃x ∈ A, y = F x
Axiom. (ReplE_impred) We take the following as an axiom:
∀A : set, ∀F : set → set, ∀y : set, y ∈ {F x|x ∈ A} → ∀p : prop, (∀x : set, x ∈ A → y = F x → p) → p
Axiom. (famunionI) We take the following as an axiom:
∀X : set, ∀F : (set → set), ∀x y : set, x ∈ X → y ∈ F x → y ∈ ⋃x ∈ XF x
Axiom. (famunionE) We take the following as an axiom:
∀X : set, ∀F : (set → set), ∀y : set, y ∈ (⋃x ∈ XF x) → ∃x ∈ X, y ∈ F x
Axiom. (famunionE_impred) We take the following as an axiom:
∀X : set, ∀F : (set → set), ∀y : set, y ∈ (⋃x ∈ XF x) → ∀p : prop, (∀x, x ∈ X → y ∈ F x → p) → p
Axiom. (SepI) We take the following as an axiom:
∀X : set, ∀P : (set → prop), ∀x : set, x ∈ X → P x → x ∈ {x ∈ X|P x}
Axiom. (SepE) We take the following as an axiom:
∀X : set, ∀P : (set → prop), ∀x : set, x ∈ {x ∈ X|P x} → x ∈ X ∧ P x
Axiom. (SepE1) We take the following as an axiom:
∀X : set, ∀P : (set → prop), ∀x : set, x ∈ {x ∈ X|P x} → x ∈ X
Axiom. (SepE2) We take the following as an axiom:
∀X : set, ∀P : (set → prop), ∀x : set, x ∈ {x ∈ X|P x} → P x
Axiom. (ReplSepI) We take the following as an axiom:
∀X : set, ∀P : set → prop, ∀F : set → set, ∀x : set, x ∈ X → P x → F x ∈ {F x|x ∈ X, P x}
Axiom. (ReplSepE) We take the following as an axiom:
∀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
Axiom. (ReplSepE_impred) We take the following as an axiom:
∀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
Axiom. (ReplSep2I) We take the following as an axiom:
∀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
Axiom. (ReplSep2E_impred) We take the following as an axiom:
∀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
Axiom. (ReplSep2E) We take the following as an axiom:
∀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
Axiom. (cases_5) We take the following as an axiom:
∀i ∈ 5, ∀p : set → prop, p 0 → p 1 → p 2 → p 3 → p 4 → p i
Axiom. (cases_6) We take the following as an axiom:
∀i ∈ 6, ∀p : set → prop, p 0 → p 1 → p 2 → p 3 → p 4 → p 5 → p i
Axiom. (bijI) We take the following as an axiom:
∀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
Axiom. (bijE) We take the following as an axiom:
∀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
Axiom. (inj_linv) We take the following as an axiom:
∀X, ∀f : set → set, (∀u v ∈ X, f u = f v → u = v) → ∀x ∈ X, inv X f (f x) = x
Axiom. (bij_comp) We take the following as an axiom:
∀X Y Z : set, ∀f g : set → set, bij X Y f → bij Y Z g → bij X Z (λx ⇒ g (f x))
Axiom. (f_eq_i) We take the following as an axiom:
∀f : set → set, ∀x y, x = y → f x = f y
Axiom. (f_eq_i_i) We take the following as an axiom:
∀f : set → set → set, ∀x y z w, x = y → z = w → f x z = f y w
Axiom. (exandE_i) We take the following as an axiom:
∀P Q : set → prop, (∃x, P x ∧ Q x) → ∀r : prop, (∀x, P x → Q x → r) → r
Axiom. (exandE_ii) We take the following as an axiom:
∀P Q : (set → set) → prop, (∃x : set → set, P x ∧ Q x) → ∀p : prop, (∀x : set → set, P x → Q x → p) → p
Axiom. (exandE_iii) We take the following as an axiom:
∀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
Axiom. (exandE_iiii) We take the following as an axiom:
∀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
Axiom. (exandE_iio) We take the following as an axiom:
∀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
Axiom. (exandE_iiio) We take the following as an axiom:
∀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
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
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 If_ii
Variable p : prop
Variable f g : set → set
End of Section If_ii
Beginning of Section If_iii
Variable p : prop
Variable f g : set → set → set
End of Section If_iii
Beginning of Section If_Vo1
Variable p : prop
End of Section If_Vo1
Beginning of Section If_iio
Variable p : prop
Variable f g : set → set → prop
End of Section If_iio
Beginning of Section If_Vo2
Variable p : prop
End of Section If_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 If_Vo3
Variable p : prop
End of Section If_Vo3
Beginning of Section Descr_Vo3
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 If_Vo4
Variable p : prop
End of Section If_Vo4
Beginning of Section Descr_Vo4
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
Axiom. (per_stra1) We take the following as an axiom:
∀R : set → set → prop, per R → ∀x y z : set, R y x → R y z → R x z
Axiom. (per_stra2) We take the following as an axiom:
∀R : set → set → prop, per R → ∀x y z : set, R x y → R z y → R x z
Axiom. (per_stra3) We take the following as an axiom:
∀R : set → set → prop, per R → ∀x y z : set, R y x → R z y → R x z
Axiom. (per_ref1) We take the following as an axiom:
∀R : set → set → prop, per R → ∀x y : set, R x y → R x x
Axiom. (per_ref2) We take the following as an axiom:
∀R : set → set → prop, per R → ∀x y : set, R x y → R y y
Beginning of Section Zermelo1908
Axiom. (Zermelo_WO) We take the following as an axiom:
∃r : set → set → prop, totalorder r ∧ (∀p : set → prop, (∃x : set, p x) → ∃x : set, p x ∧ ∀y : set, p y → r x y)
End of Section Zermelo1908
Axiom. (eq_imp_or) We take the following as an axiom:
(λx y : prop ⇒ (x → y)) = (λx y : prop ⇒ (¬ x ∨ y))
Beginning of Section NatRec
Variable z : set
Variable f : set → set → set
Let F : set → (set → set) → set ≝ λn g ⇒ if ⋃ n ∈ n then f (⋃ n) (g (⋃ n)) else z
Axiom. (nat_primrec_r) We take the following as an axiom:
∀X : set, ∀g h : set → set, (∀x ∈ X, g x = h x) → F X g = F X h
End of Section NatRec
Beginning of Section NatArith
End of Section NatArith
Axiom. (cases_7) We take the following as an axiom:
∀i ∈ 7, ∀p : set → prop, p 0 → p 1 → p 2 → p 3 → p 4 → p 5 → p 6 → p i
Axiom. (cases_8) We take the following as an axiom:
∀i ∈ 8, ∀p : set → prop, p 0 → p 1 → p 2 → p 3 → p 4 → p 5 → p 6 → p 7 → p i
Axiom. (cases_9) We take the following as an axiom:
∀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
Beginning of Section pair_setsum
Axiom. (pairI0) We take the following as an axiom:
∀X Y x, x ∈ X → pair 0 x ∈ pair X Y
Axiom. (pairI1) We take the following as an axiom:
∀X Y y, y ∈ Y → pair 1 y ∈ pair X Y
Axiom. (pairE) We take the following as an axiom:
∀X Y z, z ∈ pair X Y → (∃x ∈ X, z = pair 0 x) ∨ (∃y ∈ Y, z = pair 1 y)
Axiom. (pairE0) We take the following as an axiom:
∀X Y x, pair 0 x ∈ pair X Y → x ∈ X
Axiom. (pairE1) We take the following as an axiom:
∀X Y y, pair 1 y ∈ pair X Y → y ∈ Y
Axiom. (pairEq) We take the following as an axiom:
∀X Y z, z ∈ pair X Y ↔ (∃x ∈ X, z = pair 0 x) ∨ (∃y ∈ Y, z = pair 1 y)
Axiom. (pairSubq) We take the following as an axiom:
∀X Y W Z, X ⊆ W → Y ⊆ Z → pair X Y ⊆ pair W Z
Axiom. (pair_inj) We take the following as an axiom:
∀x y w z : set, pair x y = pair w z → x = w ∧ y = z
Axiom. (pair_Sigma) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀x ∈ X, ∀y ∈ Y x, pair x y ∈ ∑x ∈ X, Y x
Axiom. (pair_Sigma_E0) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀x y : set, pair x y ∈ (∑x ∈ X, Y x) → x ∈ X
Axiom. (pair_Sigma_E1) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀x y : set, pair x y ∈ (∑x ∈ X, Y x) → y ∈ Y x
Axiom. (Sigma_E) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀z : set, z ∈ (∑x ∈ X, Y x) → ∃x ∈ X, ∃y ∈ Y x, z = pair x y
Axiom. (Sigma_Eq) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀z : set, z ∈ (∑x ∈ X, Y x) ↔ ∃x ∈ X, ∃y ∈ Y x, z = pair x y
Axiom. (Sigma_mon) We take the following as an axiom:
∀X Y : set, X ⊆ Y → ∀Z W : set → set, (∀x ∈ X, Z x ⊆ W x) → (∑x ∈ X, Z x) ⊆ ∑y ∈ Y, W y
Axiom. (Sigma_mon1) We take the following as an axiom:
∀X : set, ∀Z W : set → set, (∀x, x ∈ X → Z x ⊆ W x) → (∑x ∈ X, Z x) ⊆ ∑x ∈ X, W x
Let lam : set → (set → set) → set ≝ Sigma
Axiom. (lamI) We take the following as an axiom:
∀X : set, ∀F : set → set, ∀x ∈ X, ∀y ∈ F x, pair x y ∈ λx ∈ X ⇒ F x
Axiom. (lamE) We take the following as an axiom:
∀X : set, ∀F : set → set, ∀z : set, z ∈ (λx ∈ X ⇒ F x) → ∃x ∈ X, ∃y ∈ F x, z = pair x y
Axiom. (lamEq) We take the following as an axiom:
∀X : set, ∀F : set → set, ∀z, z ∈ (λx ∈ X ⇒ F x) ↔ ∃x ∈ X, ∃y ∈ F x, z = pair x y
Axiom. (apI) We take the following as an axiom:
∀f x y, pair x y ∈ f → y ∈ f x
Axiom. (apE) We take the following as an axiom:
∀f x y, y ∈ f x → pair x y ∈ f
Axiom. (apEq) We take the following as an axiom:
∀f x y, y ∈ f x ↔ pair x y ∈ f
Axiom. (beta) We take the following as an axiom:
∀X : set, ∀F : set → set, ∀x : set, x ∈ X → (λx ∈ X ⇒ F x) x = F x
Axiom. (beta0) We take the following as an axiom:
∀X : set, ∀F : set → set, ∀x : set, x ∉ X → (λx ∈ X ⇒ F x) x = 0
Axiom. (ap0_Sigma) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀z : set, z ∈ (∑x ∈ X, Y x) → (z 0) ∈ X
Axiom. (ap1_Sigma) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀z : set, z ∈ (∑x ∈ X, Y x) → (z 1) ∈ (Y (z 0))
Axiom. (PiI) We take the following as an axiom:
∀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
Axiom. (PiE) We take the following as an axiom:
∀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)
Axiom. (PiEq) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀f : set, f ∈ Pi X Y ↔ (∀u ∈ f, pair_p u ∧ u 0 ∈ X) ∧ (∀x ∈ X, f x ∈ Y x)
Axiom. (lam_Pi) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀F : set → set, (∀x ∈ X, F x ∈ Y x) → (λx ∈ X ⇒ F x) ∈ (∏x ∈ X, Y x)
Axiom. (ap_Pi) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀f : set, ∀x : set, f ∈ (∏x ∈ X, Y x) → x ∈ X → f x ∈ Y x
Axiom. (Pi_ext_Subq) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀f g ∈ (∏x ∈ X, Y x), (∀x ∈ X, f x ⊆ g x) → f ⊆ g
Axiom. (Pi_ext) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀f g ∈ (∏x ∈ X, Y x), (∀x ∈ X, f x = g x) → f = g
Axiom. (Pi_eta) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀f : set, f ∈ (∏x ∈ X, Y x) → (λx ∈ X ⇒ f x) = f
Axiom. (lamI2) We take the following as an axiom:
∀X, ∀F : set → set, ∀x ∈ X, ∀y ∈ F x, (x,y) ∈ λx ∈ X ⇒ F x
Axiom. (lamE2) We take the following as an axiom:
∀X, ∀F : set → set, ∀z : set, z ∈ (λx ∈ X ⇒ F x) → ∃x ∈ X, ∃y ∈ F x, z = (x,y)
Beginning of Section Tuples
Variable x0 x1 : set
End of Section Tuples
Axiom. (Sep2I) We take the following as an axiom:
∀X, ∀Y : set → set, ∀R : set → set → prop, ∀x ∈ X, ∀y ∈ Y x, R x y → (x,y) ∈ Sep2 X Y R
Axiom. (Sep2E) We take the following as an axiom:
∀X, ∀Y : set → set, ∀R : set → set → prop, ∀u ∈ Sep2 X Y R, ∃x ∈ X, ∃y ∈ Y x, u = (x,y) ∧ R x y
Axiom. (Sep2E') We take the following as an axiom:
∀X, ∀Y : set → set, ∀R : set → set → prop, ∀x y, (x,y) ∈ Sep2 X Y R → x ∈ X ∧ y ∈ Y x ∧ R x y
Axiom. (Sep2E'1) We take the following as an axiom:
∀X, ∀Y : set → set, ∀R : set → set → prop, ∀x y, (x,y) ∈ Sep2 X Y R → x ∈ X
Axiom. (Sep2E'2) We take the following as an axiom:
∀X, ∀Y : set → set, ∀R : set → set → prop, ∀x y, (x,y) ∈ Sep2 X Y R → y ∈ Y x
Axiom. (Sep2E'3) We take the following as an axiom:
∀X, ∀Y : set → set, ∀R : set → set → prop, ∀x y, (x,y) ∈ Sep2 X Y R → R x y
Axiom. (Sep2_ext) We take the following as an axiom:
∀X, ∀Y : set → set, ∀R R' : set → set → prop, (∀x ∈ X, ∀y ∈ Y x, R x y ↔ R' x y) → Sep2 X Y R = Sep2 X Y R'
Axiom. (lam_ext_sub) We take the following as an axiom:
∀X, ∀F G : set → set, (∀x ∈ X, F x = G x) → (λx ∈ X ⇒ F x) ⊆ (λx ∈ X ⇒ G x)
Axiom. (lam_ext) We take the following as an axiom:
∀X, ∀F G : set → set, (∀x ∈ X, F x = G x) → (λx ∈ X ⇒ F x) = (λx ∈ X ⇒ G x)
Axiom. (lam_eta) We take the following as an axiom:
∀X, ∀F : set → set, (λx ∈ X ⇒ (λx ∈ X ⇒ F x) x) = (λx ∈ X ⇒ F x)
Axiom. (beta2) We take the following as an axiom:
∀X, ∀Y : set → set, ∀F : set → set → set, ∀x ∈ X, ∀y ∈ Y x, lam2 X Y F x y = F x y
Axiom. (lam2_ext) We take the following as an axiom:
∀X, ∀Y : set → set, ∀F G : set → set → set, (∀x ∈ X, ∀y ∈ Y x, F x y = G x y) → lam2 X Y F = lam2 X Y G
Axiom. (Sigma_eta) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀z ∈ (∑x ∈ X, Y x), pair (z 0) (z 1) = z
Axiom. (Pi_cod_mon) We take the following as an axiom:
∀X : set, ∀A B : set → set, (∀x ∈ X, A x ⊆ B x) → (∏x ∈ X, A x) ⊆ ∏x ∈ X, B x
Axiom. (Pi_0_mon) We take the following as an axiom:
∀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
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
Beginning of Section TaggedSets
End of Section TaggedSets
Beginning of Section TaggedSets2
End of Section TaggedSets2
Beginning of Section SurrealRecI
Variable F : set → (set → set) → set
Hypothesis Fr : ∀z, SNo z → ∀g h : set → set, (∀w ∈ SNoS_ (SNoLev z), g w = h w) → F z g = F z h
End of Section SurrealRecI
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
End of Section SurrealRec2
Axiom. (SNoLev_ind3) We take the following as an axiom:
∀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
Axiom. (unpack_u_i_eq) We take the following as an axiom:
∀Phi : set → (set → set) → set, ∀X, ∀F : set → set, (∀F' : set → set, (∀x ∈ X, F x = F' x) → Phi X F' = Phi X F) → unpack_u_i (pack_u X F) Phi = Phi X F
Axiom. (unpack_u_o_eq) We take the following as an axiom:
∀Phi : set → (set → set) → prop, ∀X, ∀F : set → set, (∀F' : set → set, (∀x ∈ X, F x = F' x) → Phi X F' = Phi X F) → unpack_u_o (pack_u X F) Phi = Phi X F
Axiom. (unpack_b_i_eq) We take the following as an axiom:
∀Phi : set → (set → set → set) → set, ∀X, ∀F : set → set → set, (∀F' : set → set → set, (∀x y ∈ X, F x y = F' x y) → Phi X F' = Phi X F) → unpack_b_i (pack_b X F) Phi = Phi X F
Axiom. (unpack_b_o_eq) We take the following as an axiom:
∀Phi : set → (set → set → set) → prop, ∀X, ∀F : set → set → set, (∀F' : set → set → set, (∀x y ∈ X, F x y = F' x y) → Phi X F' = Phi X F) → unpack_b_o (pack_b X F) Phi = Phi X F
Axiom. (unpack_p_i_eq) We take the following as an axiom:
∀Phi : set → (set → prop) → set, ∀X, ∀P : set → prop, (∀P' : set → prop, (∀x ∈ X, P x ↔ P' x) → Phi X P' = Phi X P) → unpack_p_i (pack_p X P) Phi = Phi X P
Axiom. (unpack_p_o_eq) We take the following as an axiom:
∀Phi : set → (set → prop) → prop, ∀X, ∀P : set → prop, (∀P' : set → prop, (∀x ∈ X, P x ↔ P' x) → Phi X P' = Phi X P) → unpack_p_o (pack_p X P) Phi = Phi X P
Axiom. (unpack_r_i_eq) We take the following as an axiom:
∀Phi : set → (set → set → prop) → set, ∀X, ∀R : set → set → prop, (∀R' : set → set → prop, (∀x y ∈ X, R x y ↔ R' x y) → Phi X R' = Phi X R) → unpack_r_i (pack_r X R) Phi = Phi X R
Axiom. (unpack_r_o_eq) We take the following as an axiom:
∀Phi : set → (set → set → prop) → prop, ∀X, ∀R : set → set → prop, (∀R' : set → set → prop, (∀x y ∈ X, R x y ↔ R' x y) → Phi X R' = Phi X R) → unpack_r_o (pack_r X R) Phi = Phi X R
Axiom. (pack_c_inj) We take the following as an axiom:
∀X X', ∀C C' : (set → prop) → prop, pack_c X C = pack_c X' C' → X = X' ∧ ∀U : set → prop, (∀x, U x → x ∈ X) → C U = C' U
Axiom. (pack_c_ext) We take the following as an axiom:
∀X, ∀C C' : (set → prop) → prop, (∀U : set → prop, (∀x, U x → x ∈ X) → (C U ↔ C' U)) → pack_c X C = pack_c X C'
Axiom. (unpack_c_i_eq) We take the following as an axiom:
∀Phi : set → ((set → prop) → prop) → set, ∀X, ∀C : (set → prop) → prop, (∀C' : (set → prop) → prop, (∀U : set → prop, (∀x, U x → x ∈ X) → (C U ↔ C' U)) → Phi X C' = Phi X C) → unpack_c_i (pack_c X C) Phi = Phi X C
Axiom. (unpack_c_o_eq) We take the following as an axiom:
∀Phi : set → ((set → prop) → prop) → prop, ∀X, ∀C : (set → prop) → prop, (∀C' : (set → prop) → prop, (∀U : set → prop, (∀x, U x → x ∈ X) → (C U ↔ C' U)) → Phi X C' = Phi X C) → unpack_c_o (pack_c X C) Phi = Phi X C
Beginning of Section explicit_Nats
Variable N : set
Variable base : set
Variable S : set → set
Axiom. (explicit_Nats_I) We take the following as an axiom:
(base ∈ N) → (∀m ∈ N, S m ∈ N) → (∀m ∈ N, S m ≠ base) → (∀m n ∈ N, S m = S n → m = n) → (∀p : set → prop, p base → (∀m, p m → p (S m)) → (∀m ∈ N, p m)) → explicit_Nats
End of Section explicit_Nats
Beginning of Section explicit_Nats_zero
Variable N : set
Variable zero : set
Variable S : set → set
End of Section explicit_Nats_zero
Beginning of Section explicit_Nats_one
Variable N : set
Variable one : set
Variable S : set → set
End of Section explicit_Nats_one
Beginning of Section explicit_Nats_transfer
Variable N : set
Variable base : set
Variable S : set → set
Variable N' : set
Variable base' : set
Variable S' : set → set
Variable f : set → set
End of Section explicit_Nats_transfer
Beginning of Section AssocComm
Variable R : set
Variable plus : set → set → set
Axiom. (AssocComm_identities) We take the following as an axiom:
(∀x y ∈ R, x + y ∈ R) → (∀x y z ∈ R, x + (y + z) = (x + y) + z) → (∀x y ∈ R, x + y = y + x) → ∀p : prop, ((∀x y z ∈ R, x + y + z = y + x + z) → (∀x y z ∈ R, x + y + z = z + x + y) → (∀x y z w ∈ R, (x + y) + (z + w) = (x + z) + (y + w)) → (∀x y z w ∈ R, x + y + z + w = w + x + y + z) → (∀x y z w ∈ R, x + y + z + w = z + w + x + y) → p) → p
End of Section AssocComm
Beginning of Section Group1
Variable G : set
Beginning of Section Group1Explicit
Variable op : set → set → set
End of Section Group1Explicit
Beginning of Section Group1Explicit2
Variable op : set → set → set
End of Section Group1Explicit2
End of Section Group1
Beginning of Section Group2
Variable G : set
Variable op : set → set → set
Variable H : set
End of Section Group2
Beginning of Section Group3
Variable H G : set
Variable op op' : set → set → set
Hypothesis Hopop' : ∀a b ∈ G, a * b = a ⨯ b
End of Section Group3
Beginning of Section Group4
Variable A : set
Let G ≝ {f ∈ AA|bij A A (λx ⇒ f x)}
Let op ≝ λf g : set ⇒ λx ∈ A ⇒ g (f x)
Let id ≝ λx ∈ A ⇒ x
Variable B : set
Let H ≝ {f ∈ AA|bij A A (λx ⇒ f x) ∧ ∀x ∈ B, f x = x}
End of Section Group4
Beginning of Section Group2
Variable Gs : set
Variable Gs' : set
End of Section Group2
Beginning of Section explicit_Rng
Variable R : set
Variable zero : set
Variable plus mult : set → set → set
Axiom. (explicit_Rng_I) We take the following as an axiom:
(∀x y ∈ R, x + y ∈ R) → (∀x y z ∈ R, x + (y + z) = (x + y) + z) → (∀x y ∈ R, x + y = y + x) → zero ∈ R → (∀x ∈ R, zero + x = x) → (∀x ∈ R, ∃y ∈ R, x + y = zero) → (∀x y ∈ R, x * y ∈ R) → (∀x y z ∈ R, x * (y * z) = (x * y) * z) → (∀x y z ∈ R, x * (y + z) = x * y + x * z) → (∀x y z ∈ R, (x + y) * z = x * z + y * z) → explicit_Rng
Axiom. (explicit_Rng_E) We take the following as an axiom:
∀q : prop, (explicit_Rng → (∀x y ∈ R, x + y ∈ R) → (∀x y z ∈ R, x + (y + z) = (x + y) + z) → (∀x y ∈ R, x + y = y + x) → (zero ∈ R) → (∀x ∈ R, zero + x = x) → (∀x ∈ R, ∃y ∈ R, x + y = zero) → (∀x y ∈ R, x * y ∈ R) → (∀x y z ∈ R, x * (y * z) = (x * y) * z) → (∀x y z ∈ R, x * (y + z) = x * y + x * z) → (∀x y z ∈ R, (x + y) * z = x * z + y * z) → q) → explicit_Rng → q
End of Section explicit_Rng
Beginning of Section explicit_Ring
Variable R : set
Variable zero one : set
Variable plus mult : set → set → set
Axiom. (explicit_Ring_I) We take the following as an axiom:
(∀x y ∈ R, x + y ∈ R) → (∀x y z ∈ R, x + (y + z) = (x + y) + z) → (∀x y ∈ R, x + y = y + x) → zero ∈ R → (∀x ∈ R, zero + x = x) → (∀x ∈ R, ∃y ∈ R, x + y = zero) → (∀x y ∈ R, x * y ∈ R) → (∀x y z ∈ R, x * (y * z) = (x * y) * z) → (one ∈ R) → (one ≠ zero) → (∀x ∈ R, one * x = x) → (∀x ∈ R, x * one = x) → (∀x y z ∈ R, x * (y + z) = x * y + x * z) → (∀x y z ∈ R, (x + y) * z = x * z + y * z) → explicit_Ring
Axiom. (explicit_Ring_E) We take the following as an axiom:
∀q : prop, (explicit_Ring → (∀x y ∈ R, x + y ∈ R) → (∀x y z ∈ R, x + (y + z) = (x + y) + z) → (∀x y ∈ R, x + y = y + x) → (zero ∈ R) → (∀x ∈ R, zero + x = x) → (∀x ∈ R, ∃y ∈ R, x + y = zero) → (∀x y ∈ R, x * y ∈ R) → (∀x y z ∈ R, x * (y * z) = (x * y) * z) → (one ∈ R) → (one ≠ zero) → (∀x ∈ R, one * x = x) → (∀x ∈ R, x * one = x) → (∀x y z ∈ R, x * (y + z) = x * y + x * z) → (∀x y z ∈ R, (x + y) * z = x * z + y * z) → q) → explicit_Ring → q
End of Section explicit_Ring
Beginning of Section explicit_Ring_RepIndep2
Variable R : set
Variable zero one : set
Variable plus mult : set → set → set
Variable plus' mult' : set → set → set
Hypothesis Hmm' : ∀a b ∈ R, a * b = a ⨯ b
End of Section explicit_Ring_RepIndep2
Beginning of Section explicit_CRing
Variable R : set
Variable zero one : set
Variable plus mult : set → set → set
Axiom. (explicit_CRing_I) We take the following as an axiom:
(∀x y ∈ R, x + y ∈ R) → (∀x y z ∈ R, x + (y + z) = (x + y) + z) → (∀x y ∈ R, x + y = y + x) → zero ∈ R → (∀x ∈ R, zero + x = x) → (∀x ∈ R, ∃y ∈ R, x + y = zero) → (∀x y ∈ R, x * y ∈ R) → (∀x y z ∈ R, x * (y * z) = (x * y) * z) → (∀x y ∈ R, x * y = y * x) → (one ∈ R) → (one ≠ zero) → (∀x ∈ R, one * x = x) → (∀x y z ∈ R, x * (y + z) = x * y + x * z) → explicit_CRing
Axiom. (explicit_CRing_E) We take the following as an axiom:
∀q : prop, (explicit_CRing → (∀x y ∈ R, x + y ∈ R) → (∀x y z ∈ R, x + (y + z) = (x + y) + z) → (∀x y ∈ R, x + y = y + x) → (zero ∈ R) → (∀x ∈ R, zero + x = x) → (∀x ∈ R, ∃y ∈ R, x + y = zero) → (∀x y ∈ R, x * y ∈ R) → (∀x y z ∈ R, x * (y * z) = (x * y) * z) → (∀x y ∈ R, x * y = y * x) → (one ∈ R) → (one ≠ zero) → (∀x ∈ R, one * x = x) → (∀x y z ∈ R, x * (y + z) = x * y + x * z) → q) → explicit_CRing → q
End of Section explicit_CRing
Beginning of Section explicit_CRing_RepIndep2
Variable R : set
Variable zero one : set
Variable plus mult : set → set → set
Variable plus' mult' : set → set → set
Hypothesis Hmm' : ∀a b ∈ R, a * b = a ⨯ b
End of Section explicit_CRing_RepIndep2
Axiom. (unpack_b_b_e_o_eq) We take the following as an axiom:
∀Phi : set → (set → set → set) → (set → set → set) → set → prop, ∀X, ∀f : set → set → set, ∀g : set → set → set, ∀c : set, (∀f' : set → set → set, (∀x y ∈ X, f x y = f' x y) → ∀g' : set → set → set, (∀x y ∈ X, g x y = g' x y) → Phi X f' g' c = Phi X f g c) → unpack_b_b_e_o (pack_b_b_e X f g c) Phi = Phi X f g c
Axiom. (unpack_b_b_e_e_o_eq) We take the following as an axiom:
∀Phi : set → (set → set → set) → (set → set → set) → set → set → prop, ∀X, ∀f : set → set → set, ∀g : set → set → set, ∀c : set, ∀d : set, (∀f' : set → set → set, (∀x y ∈ X, f x y = f' x y) → ∀g' : set → set → set, (∀x y ∈ X, g x y = g' x y) → Phi X f' g' c d = Phi X f g c d) → unpack_b_b_e_e_o (pack_b_b_e_e X f g c d) Phi = Phi X f g c d
Beginning of Section explicit_Reals
Variable R : set
Variable zero one : set
Variable plus mult : set → set → set
Axiom. (explicit_Field_I) We take the following as an axiom:
(∀x y ∈ R, x + y ∈ R) → (∀x y z ∈ R, x + (y + z) = (x + y) + z) → (∀x y ∈ R, x + y = y + x) → zero ∈ R → (∀x ∈ R, zero + x = x) → (∀x ∈ R, ∃y ∈ R, x + y = zero) → (∀x y ∈ R, x * y ∈ R) → (∀x y z ∈ R, x * (y * z) = (x * y) * z) → (∀x y ∈ R, x * y = y * x) → (one ∈ R) → (one ≠ zero) → (∀x ∈ R, one * x = x) → (∀x ∈ R, x ≠ zero → ∃y ∈ R, x * y = one) → (∀x y z ∈ R, x * (y + z) = x * y + x * z) → explicit_Field
Axiom. (explicit_Field_E) We take the following as an axiom:
∀q : prop, (explicit_Field → (∀x y ∈ R, x + y ∈ R) → (∀x y z ∈ R, x + (y + z) = (x + y) + z) → (∀x y ∈ R, x + y = y + x) → (zero ∈ R) → (∀x ∈ R, zero + x = x) → (∀x ∈ R, ∃y ∈ R, x + y = zero) → (∀x y ∈ R, x * y ∈ R) → (∀x y z ∈ R, x * (y * z) = (x * y) * z) → (∀x y ∈ R, x * y = y * x) → (one ∈ R) → (one ≠ zero) → (∀x ∈ R, one * x = x) → (∀x ∈ R, x ≠ zero → ∃y ∈ R, x * y = one) → (∀x y z ∈ R, x * (y + z) = x * y + x * z) → q) → explicit_Field → q
Variable leq : set → set → prop
Let Npos ≝ {n ∈ N|n ≠ zero}
End of Section explicit_Reals
Beginning of Section CRing
Variable Rs : set
Hypothesis HRs : CRing Rs
End of Section CRing
Beginning of Section explicit_Reals
Variable R : set
Variable zero one : set
Variable plus mult : set → set → set
Variable leq : set → set → prop
Let Npos ≝ {n ∈ N|n ≠ zero}
Beginning of Section explicit_Reals_Q_min_props
Variable R' : set
Let Npos' ≝ {n ∈ N'|n ≠ zero}
End of Section explicit_Reals_Q_min_props
End of Section explicit_Reals
Beginning of Section explicit_Field_RepIndep2
Variable R : set
Variable zero one : set
Variable plus mult : set → set → set
Variable plus' mult' : set → set → set
Hypothesis Hmm' : ∀a b ∈ R, a * b = a ⨯ b
End of Section explicit_Field_RepIndep2
Beginning of Section Field
Variable Fs : set
Hypothesis HFs : Field Fs
End of Section Field
Beginning of Section Field2
Variable Fs : set
Variable Fs' : set
End of Section Field2
Axiom. (radical_field_extension_E) We take the following as an axiom:
∀Fs Fs', radical_field_extension Fs Fs' → ∀p : prop, (Field Fs → Field Fs' → subfield Fs Fs' → ∀r ∈ omega, ∀Fseq, Fseq 0 = Fs → Fseq r = Fs' → (∀i ∈ ordsucc r, Field (Fseq i)) → (∀i ∈ ordsucc r, ∀j ∈ ordsucc i, subfield (Fseq j) (Fseq i)) → (∀i ∈ r, ∃a ∈ Field_carrier (Fseq (ordsucc i)), ∃n ∈ omega, CRing_omega_exp (Fseq (ordsucc i)) a n ∈ Field_carrier (Fseq i) ∧ Field_extension_by_1 (Fseq i) (Fseq (ordsucc i)) a) → p) → p
Beginning of Section explicit_Complex
Variable C : set
Variable Re Im : set → set
Variable zero one i : set
Variable plus mult : set → set → set
End of Section explicit_Complex
Beginning of Section RealsToComplex
Variable R : set
Variable zero one : set
Variable plus mult : set → set → set
Variable leq : set → set → prop
Variable pa : set → set → set
Let Re : set → set ≝ λz ⇒ Eps_i (λx ⇒ x ∈ R ∧ ∃y ∈ R, z = pa x y)
Let Im : set → set ≝ λz ⇒ Eps_i (λy ⇒ y ∈ R ∧ z = pa (Re z) y)
Let Re' : set → set ≝ λz ⇒ pa (Re z) zero
Let Im' : set → set ≝ λz ⇒ pa (Im z) zero
Let R' ≝ {z ∈ C|Re' z = z}
Let zero' : set ≝ pa zero zero
Let one' : set ≝ pa one zero
Let i' : set ≝ pa zero one
Let plus' : set → set → set ≝ λz w ⇒ pa (Re z + Re w) (Im z + Im w)
Let mult' : set → set → set ≝ λz w ⇒ pa (Re z * Re w + - (Im z * Im w)) (Re z * Im w + Im z * Re w)
End of Section RealsToComplex
Beginning of Section SurrealArithmetic
Axiom. (mul_SNo_eq_2) We take the following as an axiom:
∀x y, SNo x → SNo y → ∀p : prop, (∀L R, (∀u, u ∈ L → (∀q : prop, (∀w0 ∈ SNoL x, ∀w1 ∈ SNoL y, u = w0 * y + x * w1 + - w0 * w1 → q) → (∀z0 ∈ SNoR x, ∀z1 ∈ SNoR y, u = z0 * y + x * z1 + - z0 * z1 → q) → q)) → (∀w0 ∈ SNoL x, ∀w1 ∈ SNoL y, w0 * y + x * w1 + - w0 * w1 ∈ L) → (∀z0 ∈ SNoR x, ∀z1 ∈ SNoR y, z0 * y + x * z1 + - z0 * z1 ∈ L) → (∀u, u ∈ R → (∀q : prop, (∀w0 ∈ SNoL x, ∀z1 ∈ SNoR y, u = w0 * y + x * z1 + - w0 * z1 → q) → (∀z0 ∈ SNoR x, ∀w1 ∈ SNoL y, u = z0 * y + x * w1 + - z0 * w1 → q) → q)) → (∀w0 ∈ SNoL x, ∀z1 ∈ SNoR y, w0 * y + x * z1 + - w0 * z1 ∈ R) → (∀z0 ∈ SNoR x, ∀w1 ∈ SNoL y, z0 * y + x * w1 + - z0 * w1 ∈ R) → x * y = SNoCut L R → p) → p
Axiom. (mul_SNo_prop_1) We take the following as an axiom:
∀x, SNo x → ∀y, SNo y → ∀p : prop, (SNo (x * y) → (∀u ∈ SNoL x, ∀v ∈ SNoL y, u * y + x * v < x * y + u * v) → (∀u ∈ SNoR x, ∀v ∈ SNoR y, u * y + x * v < x * y + u * v) → (∀u ∈ SNoL x, ∀v ∈ SNoR y, x * y + u * v < u * y + x * v) → (∀u ∈ SNoR x, ∀v ∈ SNoL y, x * y + u * v < u * y + x * v) → p) → p
Axiom. (mul_SNo_eq_3) We take the following as an axiom:
∀x y, SNo x → SNo y → ∀p : prop, (∀L R, SNoCutP L R → (∀u, u ∈ L → (∀q : prop, (∀w0 ∈ SNoL x, ∀w1 ∈ SNoL y, u = w0 * y + x * w1 + - w0 * w1 → q) → (∀z0 ∈ SNoR x, ∀z1 ∈ SNoR y, u = z0 * y + x * z1 + - z0 * z1 → q) → q)) → (∀w0 ∈ SNoL x, ∀w1 ∈ SNoL y, w0 * y + x * w1 + - w0 * w1 ∈ L) → (∀z0 ∈ SNoR x, ∀z1 ∈ SNoR y, z0 * y + x * z1 + - z0 * z1 ∈ L) → (∀u, u ∈ R → (∀q : prop, (∀w0 ∈ SNoL x, ∀z1 ∈ SNoR y, u = w0 * y + x * z1 + - w0 * z1 → q) → (∀z0 ∈ SNoR x, ∀w1 ∈ SNoL y, u = z0 * y + x * w1 + - z0 * w1 → q) → q)) → (∀w0 ∈ SNoL x, ∀z1 ∈ SNoR y, w0 * y + x * z1 + - w0 * z1 ∈ R) → (∀z0 ∈ SNoR x, ∀w1 ∈ SNoL y, z0 * y + x * w1 + - z0 * w1 ∈ R) → x * y = SNoCut L R → p) → p
End of Section SurrealArithmetic
Beginning of Section Complex
End of Section Complex
Beginning of Section Complex
End of Section Complex
Beginning of Section Int
End of Section Int
Axiom. (pack_b_b_r_e_e_inj) We take the following as an axiom:
∀X X', ∀f f' : set → set → set, ∀g g' : set → set → set, ∀R R' : set → set → prop, ∀c c' : set, ∀d d' : set, pack_b_b_r_e_e X f g R c d = pack_b_b_r_e_e X' f' g' R' c' d' → X = X' ∧ (∀x y ∈ X, f x y = f' x y) ∧ (∀x y ∈ X, g x y = g' x y) ∧ (∀x y ∈ X, R x y = R' x y) ∧ c = c' ∧ d = d'
Definition. We define struct_b_b_r_e_e to be
λS ⇒ ∀q : set → prop, (∀X : set, ∀f : set → set → set, (∀x y ∈ X, f x y ∈ X) → ∀g : set → set → set, (∀x y ∈ X, g x y ∈ X) → ∀R : set → set → prop, ∀c : set, c ∈ X → ∀d : set, d ∈ X → q (pack_b_b_r_e_e X f g R c d)) → q S of type
set → prop.
Axiom. (unpack_b_b_r_e_e_i_eq) We take the following as an axiom:
∀Phi : set → (set → set → set) → (set → set → set) → (set → set → prop) → set → set → set, ∀X, ∀f : set → set → set, ∀g : set → set → set, ∀R : set → set → prop, ∀c : set, ∀d : set, (∀f' : set → set → set, (∀x y ∈ X, f x y = f' x y) → ∀g' : set → set → set, (∀x y ∈ X, g x y = g' x y) → ∀R' : set → set → prop, (∀x y ∈ X, R x y ↔ R' x y) → Phi X f' g' R' c d = Phi X f g R c d) → unpack_b_b_r_e_e_i (pack_b_b_r_e_e X f g R c d) Phi = Phi X f g R c d
Axiom. (unpack_b_b_r_e_e_o_eq) We take the following as an axiom:
∀Phi : set → (set → set → set) → (set → set → set) → (set → set → prop) → set → set → prop, ∀X, ∀f : set → set → set, ∀g : set → set → set, ∀R : set → set → prop, ∀c : set, ∀d : set, (∀f' : set → set → set, (∀x y ∈ X, f x y = f' x y) → ∀g' : set → set → set, (∀x y ∈ X, g x y = g' x y) → ∀R' : set → set → prop, (∀x y ∈ X, R x y ↔ R' x y) → Phi X f' g' R' c d = Phi X f g R c d) → unpack_b_b_r_e_e_o (pack_b_b_r_e_e X f g R c d) Phi = Phi X f g R c d
Beginning of Section RealsStruct
Variable Rs : set
Axiom. (RealsStruct_Z_props) We take the following as an axiom:
∀p : prop, ((∀n ∈ Npos, - n ∈ Z) → zero ∈ Z → Npos ⊆ Z → Z ⊆ R → (∀n ∈ Z, ∀q : prop, (- n ∈ Npos → q) → (n = zero → q) → (n ∈ Npos → q) → q) → one ∈ Z → - one ∈ Z → (∀m ∈ Z, - m ∈ Z) → (∀n m ∈ Z, n + m ∈ Z) → (∀n m ∈ Z, n * m ∈ Z) → p) → p
Axiom. (RealsStruct_Q_props) We take the following as an axiom:
∀p : prop, (Q ⊆ R → (∀x ∈ Q, ∀q : prop, (x ∈ R → ∀n ∈ Z, ∀m ∈ Npos, m * x = n → q) → q) → (∀x ∈ R, ∀n ∈ Z, ∀m ∈ Npos, m * x = n → x ∈ Q) → p) → p
End of Section RealsStruct