Primitive. The name Eps_i is a term of type (set → prop) → set.
L2
Axiom. (Eps_i_ax) We take the following as an axiom:
∀P : set → prop, ∀x : set, P x → P (Eps_i P)
L3
Definition. We define True to be ∀p : prop, p → p of type prop.
L4
Definition. We define False to be ∀p : prop, p of type prop.
L5
Definition. We define not to be λA : prop ⇒ A → False of type prop → prop.
Notation. We use ¬ as a prefix operator with priority 700 corresponding to applying term not.
L8
Definition. We define and to be λA B : prop ⇒ ∀p : prop, (A → B → p) → p of type prop → prop → prop.
Notation. We use ∧ as an infix operator with priority 780 and which associates to the left corresponding to applying term and.
L11
Definition. We define or to be λA B : prop ⇒ ∀p : prop, (A → p) → (B → p) → p of type prop → prop → prop.
Notation. We use ∨ as an infix operator with priority 785 and which associates to the left corresponding to applying term or.
L14
Definition. We define iff to be λA B : prop ⇒ and (A → B) (B → A) of type prop → prop → prop.
Notation. We use ↔ as an infix operator with priority 805 and no associativity corresponding to applying term iff.
Beginning of Section Eq
L18
Variable A : SType
L19
Definition. We define eq to be λx y : A ⇒ ∀Q : A → A → prop, Q x y → Q y x of type A → A → prop.
L20
Definition. We define neq to be λx y : A ⇒ ¬ eq x y of type A → A → prop.
End of Section Eq
Notation. We use = as an infix operator with priority 502 and no associativity corresponding to applying term eq.
Notation. We use ≠ as an infix operator with priority 502 and no associativity corresponding to applying term neq.
Beginning of Section FE
L26
Variable A B : SType
L27
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
L30
Variable A : SType
L31
Definition. We define ex to be λQ : A → prop ⇒ ∀P : prop, (∀x : A, Q x → P) → P of type (A → prop) → prop.
End of Section Ex
Notation. We use ∃ x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using ex.
L35
Axiom. (prop_ext) We take the following as an axiom:
∀p q : prop, iff p q → p = q
Primitive. The name In is a term of type set → set → prop.
Notation. We use ∈ as an infix operator with priority 500 and no associativity corresponding to applying term In. Furthermore, we may write ∀ x ∈ A, B to mean ∀ x : set, x ∈ A → B.
L37
Definition. We define Subq to be λA B ⇒ ∀x ∈ A, x ∈ B of type set → set → prop.
Notation. We use ⊆ as an infix operator with priority 500 and no associativity corresponding to applying term Subq. Furthermore, we may write ∀ x ⊆ A, B to mean ∀ x : set, x ⊆ A → B.
L38
Axiom. (set_ext) We take the following as an axiom:
∀X Y : set, X ⊆ Y → Y ⊆ X → X = Y
L39
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
Notation. We use ∃ x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using ex and handling ∈ or ⊆ ascriptions using and.
Primitive. The name Empty is a term of type set.
L42
Axiom. (EmptyAx) We take the following as an axiom:
¬ ∃x : set, x ∈ Empty
Primitive. The name ⋃ is a term of type set → set.
L45
Axiom. (UnionEq) We take the following as an axiom:
∀X x, x ∈ ⋃ X ↔ ∃Y, x ∈ Y ∧ Y ∈ X
Primitive. The name 𝒫 is a term of type set → set.
L48
Axiom. (PowerEq) We take the following as an axiom:
∀X Y : set, Y ∈ 𝒫 X ↔ Y ⊆ X
Primitive. The name Repl is a term of type set → (set → set) → set.
Notation. {B| x ∈ A} is notation for Repl A (λ x . B).
L51
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
L52
Definition. We define TransSet to be λU : set ⇒ ∀x ∈ U, x ⊆ U of type set → prop.
L53
Definition. We define Union_closed to be λU : set ⇒ ∀X : set, X ∈ U → ⋃ X ∈ U of type set → prop.
L54
Definition. We define Power_closed to be λU : set ⇒ ∀X : set, X ∈ U → 𝒫 X ∈ U of type set → prop.
L55
Definition. We define Repl_closed to be λU : set ⇒ ∀X : set, X ∈ U → ∀F : set → set, (∀x : set, x ∈ X → F x ∈ U) → {F x|x ∈ X} ∈ U of type set → prop.
L57
Definition. We define ZF_closed to be λU : set ⇒ Union_closed U ∧ Power_closed U ∧ Repl_closed U of type set → prop.
Primitive. The name UnivOf is a term of type set → set.
L62
Axiom. (UnivOf_In) We take the following as an axiom:
∀N : set, N ∈ UnivOf N
L63
Axiom. (UnivOf_TransSet) We take the following as an axiom:
∀N : set, TransSet (UnivOf N)
L64
Axiom. (UnivOf_ZF_closed) We take the following as an axiom:
∀N : set, ZF_closed (UnivOf N)
L65
Axiom. (UnivOf_Min) We take the following as an axiom:
∀N U : set, N ∈ U → TransSet U → ZF_closed U → UnivOf N ⊆ U
L69
Theorem. (andI)
∀A B : prop, A → B → A ∧ B
Proof:
Proof not loaded.
L73
Theorem. (orIL)
∀A B : prop, A → A ∨ B
Proof:
Proof not loaded.
L77
Theorem. (orIR)
∀A B : prop, B → A ∨ B
Proof:
Proof not loaded.
L81
Theorem. (iffI)
∀A B : prop, (A → B) → (B → A) → (A ↔ B)
Proof:
Proof not loaded.
L85
Theorem. (pred_ext)
∀P Q : set → prop, (∀x, P x ↔ Q x) → P = Q
Proof:
Proof not loaded.
L91
Definition. We define nIn to be λx X ⇒ ¬ In x X of type set → set → prop.
Notation. We use ∉ as an infix operator with priority 502 and no associativity corresponding to applying term nIn.
L96
Theorem. (EmptyE)
∀x : set, x ∉ Empty
Proof:
Proof not loaded.
L102
Theorem. (PowerI)
∀X Y : set, Y ⊆ X → Y ∈ 𝒫 X
Proof:
Proof not loaded.
L106
Theorem. (Subq_Empty)
∀X : set, Empty ⊆ X
Proof:
Proof not loaded.
L110
Theorem. (Empty_In_Power)
∀X : set, Empty ∈ 𝒫 X
Proof:
Proof not loaded.
L114
Theorem. (xm)
∀P : prop, P ∨ ¬ P
Proof:
Proof not loaded.
L165
Theorem. (FalseE)
False → ∀p : prop, p
Proof:
Proof not loaded.
L169
Theorem. (andEL)
∀A B : prop, A ∧ B → A
Proof:
Proof not loaded.
L173
Theorem. (andER)
∀A B : prop, A ∧ B → B
Proof:
Proof not loaded.
Beginning of Section PropN
L179
Variable P1 P2 P3 : prop
L180
Theorem. (and3I)
P1 → P2 → P3 → P1 ∧ P2 ∧ P3
Proof:
Proof not loaded.
L184
Theorem. (and3E)
P1 ∧ P2 ∧ P3 → (∀p : prop, (P1 → P2 → P3 → p) → p)
Proof:
Proof not loaded.
L188
Theorem. (or3I1)
P1 → P1 ∨ P2 ∨ P3
Proof:
Proof not loaded.
L192
Theorem. (or3I2)
P2 → P1 ∨ P2 ∨ P3
Proof:
Proof not loaded.
L196
Theorem. (or3I3)
P3 → P1 ∨ P2 ∨ P3
Proof:
Proof not loaded.
L200
Theorem. (or3E)
P1 ∨ P2 ∨ P3 → (∀p : prop, (P1 → p) → (P2 → p) → (P3 → p) → p)
Proof:
Proof not loaded.
L204
Variable P4 : prop
L206
Theorem. (and4I)
P1 → P2 → P3 → P4 → P1 ∧ P2 ∧ P3 ∧ P4
Proof:
Proof not loaded.
L210
Variable P5 : prop
L212
Theorem. (and5I)
P1 → P2 → P3 → P4 → P5 → P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5
Proof:
Proof not loaded.
L216
Variable P6 : prop
L218
Theorem. (and6I)
P1 → P2 → P3 → P4 → P5 → P6 → P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5 ∧ P6
Proof:
Proof not loaded.
L222
Variable P7 : prop
L224
Theorem. (and7I)
P1 → P2 → P3 → P4 → P5 → P6 → P7 → P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5 ∧ P6 ∧ P7
Proof:
Proof not loaded.
End of Section PropN
L230
Theorem. (not_or_and_demorgan)
∀A B : prop, ¬ (A ∨ B) → ¬ A ∧ ¬ B
Proof:
Proof not loaded.
L238
Theorem. (not_ex_all_demorgan_i)
∀P : set → prop, (¬ ∃x, P x) → ∀x, ¬ P x
Proof:
Proof not loaded.
L244
Theorem. (iffEL)
∀A B : prop, (A ↔ B) → A → B
Proof:
Proof not loaded.
L248
Theorem. (iffER)
∀A B : prop, (A ↔ B) → B → A
Proof:
Proof not loaded.
L252
Theorem. (iff_refl)
∀A : prop, A ↔ A
Proof:
Proof not loaded.
L256
Theorem. (iff_sym)
∀A B : prop, (A ↔ B) → (B ↔ A)
Proof:
Proof not loaded.
L265
Theorem. (iff_trans)
∀A B C : prop, (A ↔ B) → (B ↔ C) → (A ↔ C)
Proof:
Proof not loaded.
L278
Theorem. (eq_i_tra)
∀x y z, x = y → y = z → x = z
Proof:
Proof not loaded.
L282
Theorem. (neq_i_sym)
∀x y, x ≠ y → y ≠ x
Proof:
Proof not loaded.
L286
Theorem. (Eps_i_ex)
∀P : set → prop, (∃x, P x) → P (Eps_i P)
Proof:
Proof not loaded.
L292
Theorem. (prop_ext_2)
∀p q : prop, (p → q) → (q → p) → p = q
Proof:
Proof not loaded.
L298
Theorem. (Subq_ref)
∀X : set, X ⊆ X
Proof:
Proof not loaded.
L302
Theorem. (Subq_tra)
∀X Y Z : set, X ⊆ Y → Y ⊆ Z → X ⊆ Z
Proof:
Proof not loaded.
L306
Theorem. (Empty_Subq_eq)
∀X : set, X ⊆ Empty → X = Empty
Proof:
Proof not loaded.
L314
Theorem. (Empty_eq)
∀X : set, (∀x, x ∉ X) → X = Empty
Proof:
Proof not loaded.
L324
Theorem. (UnionI)
∀X x Y : set, x ∈ Y → Y ∈ X → x ∈ ⋃ X
Proof:
Proof not loaded.
L337
Theorem. (UnionE)
∀X x : set, x ∈ ⋃ X → ∃Y : set, x ∈ Y ∧ Y ∈ X
Proof:
Proof not loaded.
L341
Theorem. (UnionE_impred)
∀X x : set, x ∈ ⋃ X → ∀p : prop, (∀Y : set, x ∈ Y → Y ∈ X → p) → p
Proof:
Proof not loaded.
L349
Theorem. (PowerE)
∀X Y : set, Y ∈ 𝒫 X → Y ⊆ X
Proof:
Proof not loaded.
L353
Theorem. (Self_In_Power)
∀X : set, X ∈ 𝒫 X
Proof:
Proof not loaded.
L357
Theorem. (dneg)
∀P : prop, ¬ ¬ P → P
Proof:
Proof not loaded.
L366
Theorem. (not_all_ex_demorgan_i)
∀P : set → prop, ¬ (∀x, P x) → ∃x, ¬ P x
Proof:
Proof not loaded.
L376
Theorem. (eq_or_nand)
or = (λx y : prop ⇒ ¬ (¬ x ∧ ¬ y))
Proof:
Proof not loaded.
L393
Definition. We define exactly1of2 to be λA B : prop ⇒ A ∧ ¬ B ∨ ¬ A ∧ B of type prop → prop → prop.
L395
Theorem. (exactly1of2_I1)
∀A B : prop, A → ¬ B → exactly1of2 A B
Proof:
Proof not loaded.
L405
Theorem. (exactly1of2_I2)
∀A B : prop, ¬ A → B → exactly1of2 A B
Proof:
Proof not loaded.
L415
Theorem. (exactly1of2_E)
∀A B : prop, exactly1of2 A B → ∀p : prop, (A → ¬ B → p) → (¬ A → B → p) → p
Proof:
Proof not loaded.
L430
Theorem. (exactly1of2_or)
∀A B : prop, exactly1of2 A B → A ∨ B
Proof:
Proof not loaded.
L438
Theorem. (ReplI)
∀A : set, ∀F : set → set, ∀x : set, x ∈ A → F x ∈ {F x|x ∈ A}
Proof:
Proof not loaded.
L448
Theorem. (ReplE)
∀A : set, ∀F : set → set, ∀y : set, y ∈ {F x|x ∈ A} → ∃x ∈ A, y = F x
Proof:
Proof not loaded.
L452
Theorem. (ReplE_impred)
∀A : set, ∀F : set → set, ∀y : set, y ∈ {F x|x ∈ A} → ∀p : prop, (∀x : set, x ∈ A → y = F x → p) → p
Proof:
Proof not loaded.
L461
Theorem. (ReplE')
∀X, ∀f : set → set, ∀p : set → prop, (∀x ∈ X, p (f x)) → ∀y ∈ {f x|x ∈ X}, p y
Proof:
Proof not loaded.
L468
Theorem. (Repl_Empty)
∀F : set → set, {F x|x ∈ Empty} = Empty
Proof:
Proof not loaded.
L479
Theorem. (ReplEq_ext_sub)
∀X, ∀F G : set → set, (∀x ∈ X, F x = G x) → {F x|x ∈ X} ⊆ {G x|x ∈ X}
Proof:
Proof not loaded.
L494
Theorem. (ReplEq_ext)
∀X, ∀F G : set → set, (∀x ∈ X, F x = G x) → {F x|x ∈ X} = {G x|x ∈ X}
Proof:
Proof not loaded.
L503
Theorem. (Repl_inv_eq)
∀P : set → prop, ∀f g : set → set, (∀x, P x → g (f x) = x) → ∀X, (∀x ∈ X, P x) → {g y|y ∈ {f x|x ∈ X}} = X
Proof:
Proof not loaded.
L527
Theorem. (Repl_invol_eq)
∀P : set → prop, ∀f : set → set, (∀x, P x → f (f x) = x) → ∀X, (∀x ∈ X, P x) → {f y|y ∈ {f x|x ∈ X}} = X
Proof:
Proof not loaded.
L536
Definition. We define If_i to be (λp x y ⇒ Eps_i (λz : set ⇒ p ∧ z = x ∨ ¬ p ∧ z = y)) of type prop → set → set → set.
Notation. if cond then T else E is notation corresponding to If_i type cond T E where type is the inferred type of T.
L538
Theorem. (If_i_correct)
∀p : prop, ∀x y : set, p ∧ (if p then x else y) = x ∨ ¬ p ∧ (if p then x else y) = y
Proof:
Proof not loaded.
L560
Theorem. (If_i_0)
∀p : prop, ∀x y : set, ¬ p → (if p then x else y) = y
Proof:
Proof not loaded.
L571
Theorem. (If_i_1)
∀p : prop, ∀x y : set, p → (if p then x else y) = x
Proof:
Proof not loaded.
L582
Theorem. (If_i_or)
∀p : prop, ∀x y : set, (if p then x else y) = x ∨ (if p then x else y) = y
Proof:
Proof not loaded.
L591
Definition. We define UPair to be λy z ⇒ {if Empty ∈ X then y else z|X ∈ 𝒫 (𝒫 Empty)} of type set → set → set.
Notation. {x,y} is notation for UPair x y.
L594
Theorem. (UPairE)
∀x y z : set, x ∈ {y,z} → x = y ∨ x = z
Proof:
Proof not loaded.
L614
Theorem. (UPairI1)
∀y z : set, y ∈ {y,z}
Proof:
Proof not loaded.
L625
Theorem. (UPairI2)
∀y z : set, z ∈ {y,z}
Proof:
Proof not loaded.
L638
Definition. We define Sing to be λx ⇒ {x,x} of type set → set.
Notation. {x} is notation for Sing x.
L640
Theorem. (SingI)
∀x : set, x ∈ {x}
Proof:
Proof not loaded.
L644
Theorem. (SingE)
∀x y : set, y ∈ {x} → y = x
Proof:
Proof not loaded.
L650
Definition. We define binunion to be λX Y ⇒ ⋃ {X,Y} of type set → set → set.
Notation. We use ∪ as an infix operator with priority 345 and which associates to the left corresponding to applying term binunion.
L653
Theorem. (binunionI1)
∀X Y z : set, z ∈ X → z ∈ X ∪ Y
Proof:
Proof not loaded.
L663
Theorem. (binunionI2)
∀X Y z : set, z ∈ Y → z ∈ X ∪ Y
Proof:
Proof not loaded.
L673
Theorem. (binunionE)
∀X Y z : set, z ∈ X ∪ Y → z ∈ X ∨ z ∈ Y
Proof:
Proof not loaded.
L696
Theorem. (binunionE')
∀X Y z, ∀p : prop, (z ∈ X → p) → (z ∈ Y → p) → (z ∈ X ∪ Y → p)
Proof:
Proof not loaded.
L703
Theorem. (binunion_asso)
∀X Y Z : set, X ∪ (Y ∪ Z) = (X ∪ Y) ∪ Z
Proof:
Proof not loaded.
L729
Theorem. (binunion_com_Subq)
∀X Y : set, X ∪ Y ⊆ Y ∪ X
Proof:
Proof not loaded.
L737
Theorem. (binunion_com)
∀X Y : set, X ∪ Y = Y ∪ X
Proof:
Proof not loaded.
L743
Theorem. (binunion_idl)
∀X : set, Empty ∪ X = X
Proof:
Proof not loaded.
L752
Theorem. (binunion_idr)
∀X : set, X ∪ Empty = X
Proof:
Proof not loaded.
L758
Theorem. (binunion_Subq_1)
∀X Y : set, X ⊆ X ∪ Y
Proof:
Proof not loaded.
L762
Theorem. (binunion_Subq_2)
∀X Y : set, Y ⊆ X ∪ Y
Proof:
Proof not loaded.
L766
Theorem. (binunion_Subq_min)
∀X Y Z : set, X ⊆ Z → Y ⊆ Z → X ∪ Y ⊆ Z
Proof:
Proof not loaded.
L777
Theorem. (Subq_binunion_eq)
∀X Y, (X ⊆ Y) = (X ∪ Y = Y)
Proof:
Proof not loaded.
L793
Definition. We define SetAdjoin to be λX y ⇒ X ∪ {y} of type set → set → set.
Notation. We now use the set enumeration notation {...,...,...} in general. If 0 elements are given, then Empty is used to form the corresponding term. If 1 element is given, then Sing is used to form the corresponding term. If 2 elements are given, then UPair is used to form the corresponding term. If more than elements are given, then SetAdjoin is used to reduce to the case with one fewer elements.
L797
Definition. We define famunion to be λX F ⇒ ⋃ {F x|x ∈ X} of type set → (set → set) → set.
Notation. We use ⋃ x [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using famunion.
L802
Theorem. (famunionI)
∀X : set, ∀F : (set → set), ∀x y : set, x ∈ X → y ∈ F x → y ∈ ⋃x ∈ XF x
Proof:
Proof not loaded.
L806
Theorem. (famunionE)
∀X : set, ∀F : (set → set), ∀y : set, y ∈ (⋃x ∈ XF x) → ∃x ∈ X, y ∈ F x
Proof:
Proof not loaded.
L827
Theorem. (famunionE_impred)
∀X : set, ∀F : (set → set), ∀y : set, y ∈ (⋃x ∈ XF x) → ∀p : prop, (∀x, x ∈ X → y ∈ F x → p) → p
Proof:
Proof not loaded.
L835
Theorem. (famunion_Empty)
∀F : set → set, (⋃x ∈ EmptyF x) = Empty
Proof:
Proof not loaded.
L842
Theorem. (famunion_Subq)
∀X, ∀f g : set → set, (∀x ∈ X, f x ⊆ g x) → famunion X f ⊆ famunion X g
Proof:
Proof not loaded.
L852
Theorem. (famunion_ext)
∀X, ∀f g : set → set, (∀x ∈ X, f x = g x) → famunion X f = famunion X g
Proof:
Proof not loaded.
Beginning of Section SepSec
L863
Variable X : set
L864
Variable P : set → prop
L865
Let z : set ≝ Eps_i (λz ⇒ z ∈ X ∧ P z)
L866
Let F : set → set ≝ λx ⇒ if P x then x else z
L868
Definition. We define Sep to be if (∃z ∈ X, P z) then {F x|x ∈ X} else Empty of type set.
End of Section SepSec
Notation. {x ∈ A | B} is notation for Sep A (λ x . B).
L872
Theorem. (SepI)
∀X : set, ∀P : (set → prop), ∀x : set, x ∈ X → P x → x ∈ {x ∈ X|P x}
Proof:
Proof not loaded.
L910
Theorem. (SepE)
∀X : set, ∀P : (set → prop), ∀x : set, x ∈ {x ∈ X|P x} → x ∈ X ∧ P x
Proof:
Proof not loaded.
L961
Theorem. (SepE1)
∀X : set, ∀P : (set → prop), ∀x : set, x ∈ {x ∈ X|P x} → x ∈ X
Proof:
Proof not loaded.
L965
Theorem. (SepE2)
∀X : set, ∀P : (set → prop), ∀x : set, x ∈ {x ∈ X|P x} → P x
Proof:
Proof not loaded.
L969
Theorem. (Sep_Empty)
∀P : set → prop, {x ∈ Empty|P x} = Empty
Proof:
Proof not loaded.
L975
Theorem. (Sep_Subq)
∀X : set, ∀P : set → prop, {x ∈ X|P x} ⊆ X
Proof:
Proof not loaded.
L979
Theorem. (Sep_In_Power)
∀X : set, ∀P : set → prop, {x ∈ X|P x} ∈ 𝒫 X
Proof:
Proof not loaded.
L985
Definition. We define ReplSep to be λX P F ⇒ {F x|x ∈ {z ∈ X|P z}} of type set → (set → prop) → (set → set) → set.
Notation. {B| x ∈ A, C} is notation for ReplSep A (λ x . C) (λ x . B).
L987
Theorem. (ReplSepI)
∀X : set, ∀P : set → prop, ∀F : set → set, ∀x : set, x ∈ X → P x → F x ∈ {F x|x ∈ X, P x}
Proof:
Proof not loaded.
L991
Theorem. (ReplSepE)
∀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
Proof:
Proof not loaded.
L1010
Theorem. (ReplSepE_impred)
∀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
Proof:
Proof not loaded.
L1023
Definition. We define binintersect to be λX Y ⇒ {x ∈ X|x ∈ Y} of type set → set → set.
Notation. We use ∩ as an infix operator with priority 340 and which associates to the left corresponding to applying term binintersect.
L1027
Theorem. (binintersectI)
∀X Y z, z ∈ X → z ∈ Y → z ∈ X ∩ Y
Proof:
Proof not loaded.
L1031
Theorem. (binintersectE)
∀X Y z, z ∈ X ∩ Y → z ∈ X ∧ z ∈ Y
Proof:
Proof not loaded.
L1035
Theorem. (binintersectE1)
∀X Y z, z ∈ X ∩ Y → z ∈ X
Proof:
Proof not loaded.
L1039
Theorem. (binintersectE2)
∀X Y z, z ∈ X ∩ Y → z ∈ Y
Proof:
Proof not loaded.
L1043
Theorem. (binintersect_Subq_1)
∀X Y : set, X ∩ Y ⊆ X
Proof:
Proof not loaded.
L1047
Theorem. (binintersect_Subq_2)
∀X Y : set, X ∩ Y ⊆ Y
Proof:
Proof not loaded.
L1051
Theorem. (binintersect_Subq_eq_1)
∀X Y, X ⊆ Y → X ∩ Y = X
Proof:
Proof not loaded.
L1062
Theorem. (binintersect_Subq_max)
∀X Y Z : set, Z ⊆ X → Z ⊆ Y → Z ⊆ X ∩ Y
Proof:
Proof not loaded.
L1073
Theorem. (binintersect_com_Subq)
∀X Y : set, X ∩ Y ⊆ Y ∩ X
Proof:
Proof not loaded.
L1079
Theorem. (binintersect_com)
∀X Y : set, X ∩ Y = Y ∩ X
Proof:
Proof not loaded.
L1087
Definition. We define setminus to be λX Y ⇒ Sep X (λx ⇒ x ∉ Y) of type set → set → set.
Notation. We use ∖ as an infix operator with priority 350 and no associativity corresponding to applying term setminus.
L1091
Theorem. (setminusI)
∀X Y z, (z ∈ X) → (z ∉ Y) → z ∈ X ∖ Y
Proof:
Proof not loaded.
L1095
Theorem. (setminusE)
∀X Y z, (z ∈ X ∖ Y) → z ∈ X ∧ z ∉ Y
Proof:
Proof not loaded.
L1099
Theorem. (setminusE1)
∀X Y z, (z ∈ X ∖ Y) → z ∈ X
Proof:
Proof not loaded.
L1103
Theorem. (setminusE2)
∀X Y z, (z ∈ X ∖ Y) → z ∉ Y
Proof:
Proof not loaded.
L1107
Theorem. (setminus_Subq)
∀X Y : set, X ∖ Y ⊆ X
Proof:
Proof not loaded.
L1111
Theorem. (setminus_In_Power)
∀A U, A ∖ U ∈ 𝒫 A
Proof:
Proof not loaded.
L1115
Theorem. (binunion_remove1_eq)
∀X, ∀x ∈ X, X = (X ∖ {x}) ∪ {x}
Proof:
Proof not loaded.
L1140
Theorem. (In_irref)
∀x, x ∉ x
Proof:
Proof not loaded.
L1149
Theorem. (In_no2cycle)
∀x y, x ∈ y → y ∈ x → False
Proof:
Proof not loaded.
L1161
Definition. We define ordsucc to be λx : set ⇒ x ∪ {x} of type set → set.
L1162
Theorem. (ordsuccI1)
∀x : set, x ⊆ ordsucc x
Proof:
Proof not loaded.
L1167
Theorem. (ordsuccI2)
∀x : set, x ∈ ordsucc x
Proof:
Proof not loaded.
L1171
Theorem. (ordsuccE)
∀x y : set, y ∈ ordsucc x → y ∈ x ∨ y = x
Proof:
Proof not loaded.
Notation. Natural numbers 0,1,2,... are notation for the terms formed using Empty as 0 and forming successors with ordsucc.
L1181
Theorem. (neq_0_ordsucc)
∀a : set, 0 ≠ ordsucc a
Proof:
Proof not loaded.
L1189
Theorem. (neq_ordsucc_0)
∀a : set, ordsucc a ≠ 0
Proof:
Proof not loaded.
L1193
Theorem. (ordsucc_inj)
∀a b : set, ordsucc a = ordsucc b → a = b
Proof:
Proof not loaded.
L1214
Theorem. (In_0_1)
Proof:
Proof not loaded.
L1218
Theorem. (In_0_2)
Proof:
Proof not loaded.
L1222
Theorem. (In_1_2)
Proof:
Proof not loaded.
L1226
Definition. We define nat_p to be λn : set ⇒ ∀p : set → prop, p 0 → (∀x : set, p x → p (ordsucc x)) → p n of type set → prop.
L1228
Theorem. (nat_0)
Proof:
Proof not loaded.
L1232
Theorem. (nat_ordsucc)
∀n : set, nat_p n → nat_p (ordsucc n)
Proof:
Proof not loaded.
L1236
Theorem. (nat_1)
Proof:
Proof not loaded.
L1240
Theorem. (nat_2)
Proof:
Proof not loaded.
L1244
Theorem. (nat_0_in_ordsucc)
∀n, nat_p n → 0 ∈ ordsucc n
Proof:
Proof not loaded.
L1256
Theorem. (nat_ordsucc_in_ordsucc)
∀n, nat_p n → ∀m ∈ n, ordsucc m ∈ ordsucc n
Proof:
Proof not loaded.
L1282
Theorem. (nat_ind)
∀p : set → prop, p 0 → (∀n, nat_p n → p n → p (ordsucc n)) → ∀n, nat_p n → p n
Proof:
Proof not loaded.
L1307
Theorem. (nat_complete_ind)
∀p : set → prop, (∀n, nat_p n → (∀m ∈ n, p m) → p n) → ∀n, nat_p n → p n
Proof:
Proof not loaded.
L1337
Theorem. (nat_inv_impred)
∀p : set → prop, p 0 → (∀n, nat_p n → p (ordsucc n)) → ∀n, nat_p n → p n
Proof:
Proof not loaded.
L1341
Theorem. (nat_inv)
∀n, nat_p n → n = 0 ∨ ∃x, nat_p x ∧ n = ordsucc x
Proof:
Proof not loaded.
L1349
Theorem. (nat_p_trans)
∀n, nat_p n → ∀m ∈ n, nat_p m
Proof:
Proof not loaded.
L1370
Theorem. (nat_trans)
∀n, nat_p n → ∀m ∈ n, m ⊆ n
Proof:
Proof not loaded.
L1396
Theorem. (nat_ordsucc_trans)
∀n, nat_p n → ∀m ∈ ordsucc n, m ⊆ n
Proof:
Proof not loaded.
L1412
Definition. We define surj to be λX Y f ⇒ (∀u ∈ X, f u ∈ Y) ∧ (∀w ∈ Y, ∃u ∈ X, f u = w) of type set → set → (set → set) → prop.
L1418
Theorem. (form100_63_surjCantor)
∀A : set, ∀f : set → set, ¬ surj A (𝒫 A) f
Proof:
Proof not loaded.
L1444
Definition. We define inj to be λX Y f ⇒ (∀u ∈ X, f u ∈ Y) ∧ (∀u v ∈ X, f u = f v → u = v) of type set → set → (set → set) → prop.
L1450
Theorem. (form100_63_injCantor)
∀A : set, ∀f : set → set, ¬ inj (𝒫 A) A f
Proof:
Proof not loaded.
L1481
Theorem. (injI)
∀X Y, ∀f : set → set, (∀x ∈ X, f x ∈ Y) → (∀x z ∈ X, f x = f z → x = z) → inj X Y f
Proof:
Proof not loaded.
L1489
Theorem. (inj_comp)
∀X Y Z : set, ∀f g : set → set, inj X Y f → inj Y Z g → inj X Z (λx ⇒ g (f x))
Proof:
Proof not loaded.
L1509
Definition. We define bij to be λX Y f ⇒ (∀u ∈ X, f u ∈ Y) ∧ (∀u v ∈ X, f u = f v → u = v) ∧ (∀w ∈ Y, ∃u ∈ X, f u = w) of type set → set → (set → set) → prop.
L1517
Theorem. (bijI)
∀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
Proof:
Proof not loaded.
L1532
Theorem. (bijE)
∀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
Proof:
Proof not loaded.
L1546
Theorem. (bij_inj)
∀X Y, ∀f : set → set, bij X Y f → inj X Y f
Proof:
Proof not loaded.
L1550
Theorem. (bij_id)
∀X, bij X X (λx ⇒ x)
Proof:
Proof not loaded.
L1561
Theorem. (bij_comp)
∀X Y Z : set, ∀f g : set → set, bij X Y f → bij Y Z g → bij X Z (λx ⇒ g (f x))
Proof:
Proof not loaded.
L1593
Theorem. (bij_surj)
∀X Y, ∀f : set → set, bij X Y f → surj X Y f
Proof:
Proof not loaded.
L1603
Definition. We define inv to be λX f ⇒ λy : set ⇒ Eps_i (λx ⇒ x ∈ X ∧ f x = y) of type set → (set → set) → set → set.
L1605
Theorem. (surj_rinv)
∀X Y, ∀f : set → set, (∀w ∈ Y, ∃u ∈ X, f u = w) → ∀y ∈ Y, inv X f y ∈ X ∧ f (inv X f y) = y
Proof:
Proof not loaded.
L1614
Theorem. (inj_linv)
∀X, ∀f : set → set, (∀u v ∈ X, f u = f v → u = v) → ∀x ∈ X, inv X f (f x) = x
Proof:
Proof not loaded.
L1629
Theorem. (bij_inv)
∀X Y, ∀f : set → set, bij X Y f → bij Y X (inv X f)
Proof:
Proof not loaded.
L1670
Definition. We define atleastp to be λX Y : set ⇒ ∃f : set → set, inj X Y f of type set → set → prop.
L1673
Theorem. (atleastp_tra)
∀X Y Z, atleastp X Y → atleastp Y Z → atleastp X Z
Proof:
Proof not loaded.
L1687
Theorem. (Subq_atleastp)
∀X Y, X ⊆ Y → atleastp X Y
Proof:
Proof not loaded.
L1700
Definition. We define equip to be λX Y : set ⇒ ∃f : set → set, bij X Y f of type set → set → prop.
L1703
Theorem. (equip_atleastp)
∀X Y, equip X Y → atleastp X Y
Proof:
Proof not loaded.
L1713
Theorem. (equip_ref)
∀X, equip X X
Proof:
Proof not loaded.
L1720
Theorem. (equip_sym)
∀X Y, equip X Y → equip Y X
Proof:
Proof not loaded.
L1729
Theorem. (equip_tra)
∀X Y Z, equip X Y → equip Y Z → equip X Z
Proof:
Proof not loaded.
L1740
Theorem. (equip_0_Empty)
∀X, equip X 0 → X = 0
Proof:
Proof not loaded.
L1753
Theorem. (equip_adjoin_ordsucc)
∀N X y, y ∉ X → equip N X → equip (ordsucc N) (X ∪ {y})
Proof:
Proof not loaded.
L1843
Theorem. (equip_ordsucc_remove1)
∀X N, ∀x ∈ X, equip X (ordsucc N) → equip (X ∖ {x}) N
Proof:
Proof not loaded.
Beginning of Section SchroederBernstein
L2039
Theorem. (KnasterTarski_set)
∀A, ∀F : set → set, (∀U ∈ 𝒫 A, F U ∈ 𝒫 A) → (∀U V ∈ 𝒫 A, U ⊆ V → F U ⊆ F V) → ∃Y ∈ 𝒫 A, F Y = Y
Proof:
Proof not loaded.
L2080
Theorem. (image_In_Power)
∀A B, ∀f : set → set, (∀x ∈ A, f x ∈ B) → ∀U ∈ 𝒫 A, {f x|x ∈ U} ∈ 𝒫 B
Proof:
Proof not loaded.
L2093
Theorem. (image_monotone)
∀f : set → set, ∀U V, U ⊆ V → {f x|x ∈ U} ⊆ {f x|x ∈ V}
Proof:
Proof not loaded.
L2104
Theorem. (setminus_antimonotone)
∀A U V, U ⊆ V → A ∖ V ⊆ A ∖ U
Proof:
Proof not loaded.
L2112
Theorem. (SchroederBernstein)
∀A B, ∀f g : set → set, inj A B f → inj B A g → equip A B
Proof:
Proof not loaded.
L2266
Theorem. (atleastp_antisym_equip)
∀A B, atleastp A B → atleastp B A → equip A B
Proof:
Proof not loaded.
End of Section SchroederBernstein
Beginning of Section PigeonHole
L2281
Theorem. (PigeonHole_nat)
∀n, nat_p n → ∀f : set → set, (∀i ∈ ordsucc n, f i ∈ n) → ¬ (∀i j ∈ ordsucc n, f i = f j → i = j)
Proof:
Proof not loaded.
L2428
Proof:
Proof not loaded.
End of Section PigeonHole
L2440
Theorem. (Union_ordsucc_eq)
∀n, nat_p n → ⋃ (ordsucc n) = n
Proof:
Proof not loaded.
L2463
Theorem. (cases_1)
∀i ∈ 1, ∀p : set → prop, p 0 → p i
Proof:
Proof not loaded.
L2472
Theorem. (cases_2)
∀i ∈ 2, ∀p : set → prop, p 0 → p 1 → p i
Proof:
Proof not loaded.
L2481
Theorem. (neq_0_1)
Proof:
Proof not loaded.
L2485
Theorem. (neq_1_0)
Proof:
Proof not loaded.
L2489
Theorem. (neq_0_2)
Proof:
Proof not loaded.
L2493
Theorem. (neq_2_0)
Proof:
Proof not loaded.
L2497
Definition. We define ordinal to be λalpha : set ⇒ TransSet alpha ∧ ∀beta ∈ alpha, TransSet beta of type set → prop.
L2499
Theorem. (ordinal_TransSet)
∀alpha : set, ordinal alpha → TransSet alpha
Proof:
Proof not loaded.
L2503
Proof:
Proof not loaded.
L2516
Theorem. (ordinal_Hered)
∀alpha : set, ordinal alpha → ∀beta ∈ alpha, ordinal beta
Proof:
Proof not loaded.
L2536
Theorem. (TransSet_ordsucc)
∀X : set, TransSet X → TransSet (ordsucc X)
Proof:
Proof not loaded.
L2557
Theorem. (ordinal_ordsucc)
∀alpha : set, ordinal alpha → ordinal (ordsucc alpha)
Proof:
Proof not loaded.
L2577
Theorem. (nat_p_ordinal)
∀n : set, nat_p n → ordinal n
Proof:
Proof not loaded.
L2588
Theorem. (ordinal_1)
Proof:
Proof not loaded.
L2592
Theorem. (ordinal_2)
Proof:
Proof not loaded.
L2596
Theorem. (TransSet_ordsucc_In_Subq)
∀X : set, TransSet X → ∀x ∈ X, ordsucc x ⊆ X
Proof:
Proof not loaded.
L2613
Theorem. (ordinal_ordsucc_In_Subq)
∀alpha, ordinal alpha → ∀beta ∈ alpha, ordsucc beta ⊆ alpha
Proof:
Proof not loaded.
L2619
Theorem. (ordinal_trichotomy_or)
∀alpha beta : set, ordinal alpha → ordinal beta → alpha ∈ beta ∨ alpha = beta ∨ beta ∈ alpha
Proof:
Proof not loaded.
L2687
Theorem. (ordinal_trichotomy_or_impred)
∀alpha beta : set, ordinal alpha → ordinal beta → ∀p : prop, (alpha ∈ beta → p) → (alpha = beta → p) → (beta ∈ alpha → p) → p
Proof:
Proof not loaded.
L2692
Theorem. (ordinal_In_Or_Subq)
∀alpha beta, ordinal alpha → ordinal beta → alpha ∈ beta ∨ beta ⊆ alpha
Proof:
Proof not loaded.
L2709
Theorem. (ordinal_linear)
∀alpha beta, ordinal alpha → ordinal beta → alpha ⊆ beta ∨ beta ⊆ alpha
Proof:
Proof not loaded.
L2722
Theorem. (ordinal_ordsucc_In_eq)
∀alpha beta, ordinal alpha → beta ∈ alpha → ordsucc beta ∈ alpha ∨ alpha = ordsucc beta
Proof:
Proof not loaded.
L2739
Theorem. (ordinal_lim_or_succ)
∀alpha, ordinal alpha → (∀beta ∈ alpha, ordsucc beta ∈ alpha) ∨ (∃beta ∈ alpha, alpha = ordsucc beta)
Proof:
Proof not loaded.
L2754
Theorem. (ordinal_ordsucc_In)
∀alpha, ordinal alpha → ∀beta ∈ alpha, ordsucc beta ∈ ordsucc alpha
Proof:
Proof not loaded.
L2769
Theorem. (ordinal_famunion)
∀X, ∀F : set → set, (∀x ∈ X, ordinal (F x)) → ordinal (⋃x ∈ XF x)
Proof:
Proof not loaded.
L2800
Theorem. (ordinal_binintersect)
∀alpha beta, ordinal alpha → ordinal beta → ordinal (alpha ∩ beta)
Proof:
Proof not loaded.
L2814
Theorem. (ordinal_binunion)
∀alpha beta, ordinal alpha → ordinal beta → ordinal (alpha ∪ beta)
Proof:
Proof not loaded.
L2829
Theorem. (ordinal_ind)
∀p : set → prop, (∀alpha, ordinal alpha → (∀beta ∈ alpha, p beta) → p alpha) → ∀alpha, ordinal alpha → p alpha
Proof:
Proof not loaded.
L2849
Theorem. (least_ordinal_ex)
∀p : set → prop, (∃alpha, ordinal alpha ∧ p alpha) → ∃alpha, ordinal alpha ∧ p alpha ∧ ∀beta ∈ alpha, ¬ p beta
Proof:
Proof not loaded.
L2871
Theorem. (equip_Sing_1)
∀x, equip {x} 1
Proof:
Proof not loaded.
L2890
Theorem. (TransSet_In_ordsucc_Subq)
∀x y, TransSet y → x ∈ ordsucc y → x ⊆ y
Proof:
Proof not loaded.
L2896
Theorem. (exandE_i)
∀P Q : set → prop, (∃x, P x ∧ Q x) → ∀r : prop, (∀x, P x → Q x → r) → r
Proof:
Proof not loaded.
L2901
Theorem. (exandE_ii)
∀P Q : (set → set) → prop, (∃x : set → set, P x ∧ Q x) → ∀p : prop, (∀x : set → set, P x → Q x → p) → p
Proof:
Proof not loaded.
L2908
Theorem. (exandE_iii)
∀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
Proof:
Proof not loaded.
L2915
Theorem. (exandE_iiii)
∀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
Proof:
Proof not loaded.
Beginning of Section Descr_ii
L2924
Variable P : (set → set) → prop
L2926
Definition. We define Descr_ii to be λx : set ⇒ Eps_i (λy ⇒ ∀h : set → set, P h → h x = y) of type set → set.
L2927
Hypothesis Pex : ∃f : set → set, P f
L2928
Hypothesis Puniq : ∀f g : set → set, P f → P g → f = g
L2929
Theorem. (Descr_ii_prop)
Proof:
Proof not loaded.
End of Section Descr_ii
Beginning of Section Descr_iii
L2949
Variable P : (set → set → set) → prop
L2951
Definition. We define Descr_iii to be λx y : set ⇒ Eps_i (λz ⇒ ∀h : set → set → set, P h → h x y = z) of type set → set → set.
L2952
Hypothesis Pex : ∃f : set → set → set, P f
L2953
Hypothesis Puniq : ∀f g : set → set → set, P f → P g → f = g
L2954
Proof:
Proof not loaded.
End of Section Descr_iii
Beginning of Section Descr_Vo1
L2976
Variable P : Vo 1 → prop
L2978
Definition. We define Descr_Vo1 to be λx : set ⇒ ∀h : set → prop, P h → h x of type Vo 1.
L2979
Hypothesis Pex : ∃f : Vo 1, P f
L2980
Hypothesis Puniq : ∀f g : Vo 1, P f → P g → f = g
L2981
Proof:
Proof not loaded.
End of Section Descr_Vo1
Beginning of Section If_ii
L3000
Variable p : prop
L3001
Variable f g : set → set
L3003
Definition. We define If_ii to be λx ⇒ if p then f x else g x of type set → set.
L3004
Theorem. (If_ii_1)
p → If_ii = f
Proof:
Proof not loaded.
L3011
Theorem. (If_ii_0)
¬ p → If_ii = g
Proof:
Proof not loaded.
End of Section If_ii
Beginning of Section If_iii
L3021
Variable p : prop
L3022
Variable f g : set → set → set
L3024
Definition. We define If_iii to be λx y ⇒ if p then f x y else g x y of type set → set → set.
L3025
Theorem. (If_iii_1)
p → If_iii = f
Proof:
Proof not loaded.
L3035
Theorem. (If_iii_0)
¬ p → If_iii = g
Proof:
Proof not loaded.
End of Section If_iii
Beginning of Section EpsilonRec_i
L3048
Variable F : set → (set → set) → set
L3049
Definition. We define In_rec_i_G to be λX Y ⇒ ∀R : set → set → prop, (∀X : set, ∀f : set → set, (∀x ∈ X, R x (f x)) → R X (F X f)) → R X Y of type set → set → prop.
L3055
Definition. We define In_rec_i to be λX ⇒ Eps_i (In_rec_i_G X) of type set → set.
L3056
Theorem. (In_rec_i_G_c)
∀X : set, ∀f : set → set, (∀x ∈ X, In_rec_i_G x (f x)) → In_rec_i_G X (F X f)
Proof:
Proof not loaded.
L3072
Theorem. (In_rec_i_G_inv)
∀X : set, ∀Y : set, In_rec_i_G X Y → ∃f : set → set, (∀x ∈ X, In_rec_i_G x (f x)) ∧ Y = F X f
Proof:
Proof not loaded.
L3095
Hypothesis Fr : ∀X : set, ∀g h : set → set, (∀x ∈ X, g x = h x) → F X g = F X h
L3097
Theorem. (In_rec_i_G_f)
∀X : set, ∀Y Z : set, In_rec_i_G X Y → In_rec_i_G X Z → Y = Z
Proof:
Proof not loaded.
L3128
Theorem. (In_rec_i_G_In_rec_i)
∀X : set, In_rec_i_G X (In_rec_i X)
Proof:
Proof not loaded.
L3139
Theorem. (In_rec_i_G_In_rec_i_d)
∀X : set, In_rec_i_G X (F X In_rec_i)
Proof:
Proof not loaded.
L3147
Theorem. (In_rec_i_eq)
∀X : set, In_rec_i X = F X In_rec_i
Proof:
Proof not loaded.
End of Section EpsilonRec_i
Beginning of Section EpsilonRec_ii
L3154
Variable F : set → (set → (set → set)) → (set → set)
L3155
Definition. We define In_rec_G_ii to be λX Y ⇒ ∀R : set → (set → set) → prop, (∀X : set, ∀f : set → (set → set), (∀x ∈ X, R x (f x)) → R X (F X f)) → R X Y of type set → (set → set) → prop.
L3161
Definition. We define In_rec_ii to be λX ⇒ Descr_ii (In_rec_G_ii X) of type set → (set → set).
L3162
Theorem. (In_rec_G_ii_c)
∀X : set, ∀f : set → (set → set), (∀x ∈ X, In_rec_G_ii x (f x)) → In_rec_G_ii X (F X f)
Proof:
Proof not loaded.
L3178
Theorem. (In_rec_G_ii_inv)
∀X : set, ∀Y : (set → set), In_rec_G_ii X Y → ∃f : set → (set → set), (∀x ∈ X, In_rec_G_ii x (f x)) ∧ Y = F X f
Proof:
Proof not loaded.
L3201
Hypothesis Fr : ∀X : set, ∀g h : set → (set → set), (∀x ∈ X, g x = h x) → F X g = F X h
L3203
Theorem. (In_rec_G_ii_f)
∀X : set, ∀Y Z : (set → set), In_rec_G_ii X Y → In_rec_G_ii X Z → Y = Z
Proof:
Proof not loaded.
L3234
Theorem. (In_rec_G_ii_In_rec_ii)
∀X : set, In_rec_G_ii X (In_rec_ii X)
Proof:
Proof not loaded.
L3247
Theorem. (In_rec_G_ii_In_rec_ii_d)
∀X : set, In_rec_G_ii X (F X In_rec_ii)
Proof:
Proof not loaded.
L3255
Theorem. (In_rec_ii_eq)
∀X : set, In_rec_ii X = F X In_rec_ii
Proof:
Proof not loaded.
End of Section EpsilonRec_ii
Beginning of Section EpsilonRec_iii
L3262
Variable F : set → (set → (set → set → set)) → (set → set → set)
L3263
Definition. We define In_rec_G_iii to be λX Y ⇒ ∀R : set → (set → set → set) → prop, (∀X : set, ∀f : set → (set → set → set), (∀x ∈ X, R x (f x)) → R X (F X f)) → R X Y of type set → (set → set → set) → prop.
L3269
Definition. We define In_rec_iii to be λX ⇒ Descr_iii (In_rec_G_iii X) of type set → (set → set → set).
L3270
Theorem. (In_rec_G_iii_c)
∀X : set, ∀f : set → (set → set → set), (∀x ∈ X, In_rec_G_iii x (f x)) → In_rec_G_iii X (F X f)
Proof:
Proof not loaded.
L3286
Theorem. (In_rec_G_iii_inv)
∀X : set, ∀Y : (set → set → set), In_rec_G_iii X Y → ∃f : set → (set → set → set), (∀x ∈ X, In_rec_G_iii x (f x)) ∧ Y = F X f
Proof:
Proof not loaded.
L3309
Hypothesis Fr : ∀X : set, ∀g h : set → (set → set → set), (∀x ∈ X, g x = h x) → F X g = F X h
L3311
Theorem. (In_rec_G_iii_f)
∀X : set, ∀Y Z : (set → set → set), In_rec_G_iii X Y → In_rec_G_iii X Z → Y = Z
Proof:
Proof not loaded.
L3342
Theorem. (In_rec_G_iii_In_rec_iii)
∀X : set, In_rec_G_iii X (In_rec_iii X)
Proof:
Proof not loaded.
L3355
Theorem. (In_rec_G_iii_In_rec_iii_d)
∀X : set, In_rec_G_iii X (F X In_rec_iii)
Proof:
Proof not loaded.
L3363
Theorem. (In_rec_iii_eq)
∀X : set, In_rec_iii X = F X In_rec_iii
Proof:
Proof not loaded.
End of Section EpsilonRec_iii
Beginning of Section NatRec
L3370
Variable z : set
L3371
Variable f : set → set → set
L3372
Let F : set → (set → set) → set ≝ λn g ⇒ if ⋃ n ∈ n then f (⋃ n) (g (⋃ n)) else z
L3373
Definition. We define nat_primrec to be In_rec_i F of type set → set.
L3374
Theorem. (nat_primrec_r)
∀X : set, ∀g h : set → set, (∀x ∈ X, g x = h x) → F X g = F X h
Proof:
Proof not loaded.
L3394
Proof:
Proof not loaded.
L3402
Theorem. (nat_primrec_S)
∀n : set, nat_p n → nat_primrec (ordsucc n) = f n (nat_primrec n)
Proof:
Proof not loaded.
End of Section NatRec
Beginning of Section NatAdd
L3418
Definition. We define add_nat to be λn m : set ⇒ nat_primrec n (λ_ r ⇒ ordsucc r) m of type set → set → set.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_nat.
L3421
Theorem. (add_nat_0R)
∀n : set, n + 0 = n
Proof:
Proof not loaded.
L3426
Theorem. (add_nat_SR)
∀n m : set, nat_p m → n + ordsucc m = ordsucc (n + m)
Proof:
Proof not loaded.
L3431
Theorem. (add_nat_p)
∀n : set, nat_p n → ∀m : set, nat_p m → nat_p (n + m)
Proof:
Proof not loaded.
L3450
Theorem. (add_nat_1_1_2)
1 + 1 = 2
Proof:
Proof not loaded.
L3459
Theorem. (add_nat_asso)
∀n : set, nat_p n → ∀m : set, nat_p m → ∀k : set, nat_p k → (n + m) + k = n + (m + k)
Proof:
Proof not loaded.
L3481
Theorem. (add_nat_0L)
∀m : set, nat_p m → 0 + m = m
Proof:
Proof not loaded.
L3495
Theorem. (add_nat_SL)
∀n : set, nat_p n → ∀m : set, nat_p m → ordsucc n + m = ordsucc (n + m)
Proof:
Proof not loaded.
L3514
Theorem. (add_nat_com)
∀n : set, nat_p n → ∀m : set, nat_p m → n + m = m + n
Proof:
Proof not loaded.
L3532
Theorem. (add_nat_In_R)
∀m, nat_p m → ∀k ∈ m, ∀n, nat_p n → k + n ∈ m + n
Proof:
Proof not loaded.
L3550
Theorem. (add_nat_In_L)
∀n, nat_p n → ∀m, nat_p m → ∀k ∈ m, n + k ∈ n + m
Proof:
Proof not loaded.
L3558
Theorem. (add_nat_Subq_R)
∀k, nat_p k → ∀m, nat_p m → k ⊆ m → ∀n, nat_p n → k + n ⊆ m + n
Proof:
Proof not loaded.
L3580
Theorem. (add_nat_Subq_L)
∀n, nat_p n → ∀k, nat_p k → ∀m, nat_p m → k ⊆ m → n + k ⊆ n + m
Proof:
Proof not loaded.
L3590
Theorem. (add_nat_Subq_R')
∀m, nat_p m → ∀n, nat_p n → m ⊆ m + n
Proof:
Proof not loaded.
L3604
Theorem. (nat_Subq_add_ex)
∀n, nat_p n → ∀m, nat_p m → n ⊆ m → ∃k, nat_p k ∧ m = k + n
Proof:
Proof not loaded.
L3642
Theorem. (add_nat_cancel_R)
∀k, nat_p k → ∀m, nat_p m → ∀n, nat_p n → k + n = m + n → k = m
Proof:
Proof not loaded.
End of Section NatAdd
Beginning of Section NatMul
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_nat.
L3669
Definition. We define mul_nat to be λn m : set ⇒ nat_primrec 0 (λ_ r ⇒ n + r) m of type set → set → set.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_nat.
L3672
Theorem. (mul_nat_0R)
∀n : set, n * 0 = 0
Proof:
Proof not loaded.
L3677
Theorem. (mul_nat_SR)
∀n m, nat_p m → n * ordsucc m = n + n * m
Proof:
Proof not loaded.
L3682
Theorem. (mul_nat_1R)
∀n, n * 1 = n
Proof:
Proof not loaded.
L3691
Theorem. (mul_nat_p)
∀n : set, nat_p n → ∀m : set, nat_p m → nat_p (n * m)
Proof:
Proof not loaded.
L3708
Theorem. (mul_nat_0L)
∀m : set, nat_p m → 0 * m = 0
Proof:
Proof not loaded.
L3723
Theorem. (mul_nat_SL)
∀n : set, nat_p n → ∀m : set, nat_p m → ordsucc n * m = n * m + m
Proof:
Proof not loaded.
L3755
Theorem. (mul_nat_com)
∀n : set, nat_p n → ∀m : set, nat_p m → n * m = m * n
Proof:
Proof not loaded.
L3775
Theorem. (mul_add_nat_distrL)
∀n : set, nat_p n → ∀m : set, nat_p m → ∀k : set, nat_p k → n * (m + k) = n * m + n * k
Proof:
Proof not loaded.
L3806
Theorem. (mul_nat_asso)
∀n : set, nat_p n → ∀m : set, nat_p m → ∀k : set, nat_p k → (n * m) * k = n * (m * k)
Proof:
Proof not loaded.
L3835
Theorem. (mul_nat_Subq_R)
∀m n, nat_p m → nat_p n → m ⊆ n → ∀k, nat_p k → m * k ⊆ n * k
Proof:
Proof not loaded.
L3857
Theorem. (mul_nat_Subq_L)
∀m n, nat_p m → nat_p n → m ⊆ n → ∀k, nat_p k → k * m ⊆ k * n
Proof:
Proof not loaded.
L3865
Theorem. (mul_nat_0_or_Subq)
∀m, nat_p m → ∀n, nat_p n → n = 0 ∨ m ⊆ m * n
Proof:
Proof not loaded.
L3880
Theorem. (mul_nat_0_inv)
∀m, nat_p m → ∀n, nat_p n → m * n = 0 → m = 0 ∨ n = 0
Proof:
Proof not loaded.
L3901
Theorem. (mul_nat_0m_1n_In)
∀m, nat_p m → ∀n, nat_p n → 0 ∈ m → 1 ∈ n → m ∈ m * n
Proof:
Proof not loaded.
L3937
Theorem. (nat_le1_cases)
∀m, nat_p m → m ⊆ 1 → m = 0 ∨ m = 1
Proof:
Proof not loaded.
L3954
Definition. We define Pi_nat to be λf n ⇒ nat_primrec 1 (λi r ⇒ r * f i) n of type (set → set) → set → set.
L3957
Theorem. (Pi_nat_0)
∀f : set → set, Pi_nat f 0 = 1
Proof:
Proof not loaded.
L3962
Theorem. (Pi_nat_S)
∀f : set → set, ∀n, nat_p n → Pi_nat f (ordsucc n) = Pi_nat f n * f n
Proof:
Proof not loaded.
L3968
Theorem. (Pi_nat_p)
∀f : set → set, ∀n, nat_p n → (∀i ∈ n, nat_p (f i)) → nat_p (Pi_nat f n)
Proof:
Proof not loaded.
L3993
Theorem. (Pi_nat_0_inv)
∀f : set → set, ∀n, nat_p n → (∀i ∈ n, nat_p (f i)) → Pi_nat f n = 0 → (∃i ∈ n, f i = 0)
Proof:
Proof not loaded.
L4036
Definition. We define exp_nat to be λn m : set ⇒ nat_primrec 1 (λ_ r ⇒ n * r) m of type set → set → set.
Notation. We use ^ as an infix operator with priority 342 and which associates to the right corresponding to applying term exp_nat.
L4040
Theorem. (exp_nat_0)
∀n, n ^ 0 = 1
Proof:
Proof not loaded.
L4046
Theorem. (exp_nat_S)
∀n m, nat_p m → n ^ (ordsucc m) = n * n ^ m
Proof:
Proof not loaded.
L4052
Theorem. (exp_nat_p)
∀n, nat_p n → ∀m, nat_p m → nat_p (n ^ m)
Proof:
Proof not loaded.
L4063
Theorem. (exp_nat_1)
∀n, n ^ 1 = n
Proof:
Proof not loaded.
End of Section NatMul
Beginning of Section form100_52
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_nat.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_nat.
Notation. We use ^ as an infix operator with priority 342 and which associates to the right corresponding to applying term exp_nat.
L4080
Theorem. (Subq_Sing0_1)
Proof:
Proof not loaded.
L4084
Theorem. (Subq_1_Sing0)
Proof:
Proof not loaded.
L4098
Theorem. (eq_1_Sing0)
Proof:
Proof not loaded.
L4102
Proof:
Proof not loaded.
L4123
Theorem. (equip_finite_Power)
∀n, nat_p n → ∀X, equip X n → equip (𝒫 X) (2 ^ n)
Proof:
Proof not loaded.
End of Section form100_52
L4496
Theorem. (ZF_closed_E)
∀U, ZF_closed U → ∀p : prop, (Union_closed U → Power_closed U → Repl_closed U → p) → p
Proof:
Proof not loaded.
L4505
Theorem. (ZF_Union_closed)
∀U, ZF_closed U → ∀X ∈ U, ⋃ X ∈ U
Proof:
Proof not loaded.
L4510
Theorem. (ZF_Power_closed)
∀U, ZF_closed U → ∀X ∈ U, 𝒫 X ∈ U
Proof:
Proof not loaded.
L4515
Theorem. (ZF_Repl_closed)
∀U, ZF_closed U → ∀X ∈ U, ∀F : set → set, (∀x ∈ X, F x ∈ U) → {F x|x ∈ X} ∈ U
Proof:
Proof not loaded.
L4520
Theorem. (ZF_UPair_closed)
∀U, ZF_closed U → ∀x y ∈ U, {x,y} ∈ U
Proof:
Proof not loaded.
L4604
Theorem. (ZF_Sing_closed)
∀U, ZF_closed U → ∀x ∈ U, {x} ∈ U
Proof:
Proof not loaded.
L4609
Theorem. (ZF_binunion_closed)
∀U, ZF_closed U → ∀X Y ∈ U, (X ∪ Y) ∈ U
Proof:
Proof not loaded.
L4614
Theorem. (ZF_ordsucc_closed)
∀U, ZF_closed U → ∀x ∈ U, ordsucc x ∈ U
Proof:
Proof not loaded.
L4619
Theorem. (nat_p_UnivOf_Empty)
∀n : set, nat_p n → n ∈ UnivOf Empty
Proof:
Proof not loaded.
L4633
Definition. We define ω to be {n ∈ UnivOf Empty|nat_p n} of type set.
L4634
Theorem. (omega_nat_p)
∀n ∈ ω, nat_p n
Proof:
Proof not loaded.
L4638
Theorem. (nat_p_omega)
∀n : set, nat_p n → n ∈ ω
Proof:
Proof not loaded.
L4647
Theorem. (omega_ordsucc)
Proof:
Proof not loaded.
L4655
Theorem. (form100_22_v2)
∀f : set → set, ¬ inj (𝒫 ω) ω f
Proof:
Proof not loaded.
L4659
Theorem. (form100_22_v3)
∀g : set → set, ¬ surj ω (𝒫 ω) g
Proof:
Proof not loaded.
L4684
Proof:
Proof not loaded.
L4693
Proof:
Proof not loaded.
L4706
Proof:
Proof not loaded.
L4720
Proof:
Proof not loaded.
L4724
Definition. We define finite to be λX ⇒ ∃n ∈ ω, equip X n of type set → prop.
L4726
Theorem. (nat_finite)
∀n, nat_p n → finite n
Proof:
Proof not loaded.
L4734
Theorem. (finite_ind)
∀p : set → prop, p Empty → (∀X y, finite X → y ∉ X → p X → p (X ∪ {y})) → ∀X, finite X → p X
Proof:
Proof not loaded.
L4826
Theorem. (finite_Empty)
Proof:
Proof not loaded.
L4833
Theorem. (Sing_finite)
∀x, finite {x}
Proof:
Proof not loaded.
L4841
Theorem. (adjoin_finite)
∀X y, finite X → finite (X ∪ {y})
Proof:
Proof not loaded.
L4924
Theorem. (binunion_finite)
∀X, finite X → ∀Y, finite Y → finite (X ∪ Y)
Proof:
Proof not loaded.
L4939
Theorem. (famunion_nat_finite)
∀X : set → set, ∀n, nat_p n → (∀i ∈ n, finite (X i)) → finite (⋃i ∈ nX i)
Proof:
Proof not loaded.
L4978
Theorem. (Subq_finite)
∀X, finite X → ∀Y, Y ⊆ X → finite Y
Proof:
Proof not loaded.
L5031
Definition. We define infinite to be λA ⇒ ¬ finite A of type set → prop.
Beginning of Section InfinitePrimes
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_nat.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_nat.
L5038
Definition. We define divides_nat to be λm n ⇒ m ∈ ω ∧ n ∈ ω ∧ ∃k ∈ ω, m * k = n of type set → set → prop.
L5041
Theorem. (divides_nat_ref)
∀n, nat_p n → divides_nat n n
Proof:
Proof not loaded.
L5055
Theorem. (divides_nat_tra)
∀k m n, divides_nat k m → divides_nat m n → divides_nat k n
Proof:
Proof not loaded.
L5093
Definition. We define prime_nat to be λn ⇒ n ∈ ω ∧ 1 ∈ n ∧ ∀k ∈ ω, divides_nat k n → k = 1 ∨ k = n of type set → prop.
L5096
Theorem. (divides_nat_mulR)
∀m n ∈ ω, divides_nat m (m * n)
Proof:
Proof not loaded.
L5109
Theorem. (divides_nat_mulL)
∀m n ∈ ω, divides_nat n (m * n)
Proof:
Proof not loaded.
L5116
Theorem. (Pi_nat_divides)
∀f : set → set, ∀n, nat_p n → (∀i ∈ n, nat_p (f i)) → (∀i ∈ n, divides_nat (f i) (Pi_nat f n))
Proof:
Proof not loaded.
L5150
Definition. We define composite_nat to be λn ⇒ n ∈ ω ∧ ∃k m ∈ ω, 1 ∈ k ∧ 1 ∈ m ∧ k * m = n of type set → prop.
L5153
Proof:
Proof not loaded.
L5235
Theorem. (prime_nat_divisor_ex)
∀n, nat_p n → 1 ∈ n → ∃p, prime_nat p ∧ divides_nat p n
Proof:
Proof not loaded.
L5277
Theorem. (nat_1In_not_divides_ordsucc)
∀m n, 1 ∈ m → divides_nat m n → ¬ divides_nat m (ordsucc n)
Proof:
Proof not loaded.
L5344
Definition. We define primes to be {n ∈ ω|prime_nat n} of type set.
L5346
Proof:
Proof not loaded.
End of Section InfinitePrimes
Beginning of Section InfiniteRamsey
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_nat.
L5477
Theorem. (atleastp_omega_infinite)
∀X, atleastp ω X → infinite X
Proof:
Proof not loaded.
L5503
Theorem. (infinite_remove1)
∀X, infinite X → ∀y, infinite (X ∖ {y})
Proof:
Proof not loaded.
L5536
Theorem. (infinite_Finite_Subq_ex)
∀X, infinite X → ∀n, nat_p n → ∃Y ⊆ X, equip Y n
Proof:
Proof not loaded.
L5675
Theorem. (infiniteRamsey_lem)
∀X, ∀f g f' : set → set, infinite X → (∀Z ⊆ X, infinite Z → f Z ⊆ Z ∧ infinite (f Z)) → (∀Z ⊆ X, infinite Z → g Z ∈ Z ∧ g Z ∉ f Z) → f' 0 = f X → (∀m, nat_p m → f' (ordsucc m) = f (f' m)) → (∀m, nat_p m → f' m ⊆ X ∧ infinite (f' m)) ∧ (∀m m' ∈ ω, m ⊆ m' → f' m' ⊆ f' m) ∧ (∀m m' ∈ ω, g (f' m) = g (f' m') → m = m')
Proof:
Proof not loaded.
L5801
Theorem. (infiniteRamsey)
∀c, nat_p c → ∀n, nat_p n → ∀X, infinite X → ∀C : set → set, (∀Y ⊆ X, equip Y n → C Y ∈ c) → ∃H ⊆ X, ∃i ∈ c, infinite H ∧ ∀Y ⊆ H, equip Y n → C Y = i
Proof:
Proof not loaded.
End of Section InfiniteRamsey
L6649
Definition. We define Inj1 to be In_rec_i (λX f ⇒ {0} ∪ {f x|x ∈ X}) of type set → set.
L6652
Theorem. (Inj1_eq)
∀X : set, Inj1 X = {0} ∪ {Inj1 x|x ∈ X}
Proof:
Proof not loaded.
(*** Injection of set into itself that will correspond to x |-> (1,x) after pairing is defined. ***)
L6669
Theorem. (Inj1I1)
∀X : set, 0 ∈ Inj1 X
Proof:
Proof not loaded.
L6677
Theorem. (Inj1I2)
∀X x : set, x ∈ X → Inj1 x ∈ Inj1 X
Proof:
Proof not loaded.
L6686
Theorem. (Inj1E)
∀X y : set, y ∈ Inj1 X → y = 0 ∨ ∃x ∈ X, y = Inj1 x
Proof:
Proof not loaded.
L6701
Theorem. (Inj1NE1)
∀x : set, Inj1 x ≠ 0
Proof:
Proof not loaded.
L6711
Theorem. (Inj1NE2)
∀x : set, Inj1 x ∉ {0}
Proof:
Proof not loaded.
L6717
Definition. We define Inj0 to be λX ⇒ {Inj1 x|x ∈ X} of type set → set.
L6720
Theorem. (Inj0I)
∀X x : set, x ∈ X → Inj1 x ∈ Inj0 X
Proof:
Proof not loaded.
(*** Injection of set into itself that will correspond to x |-> (0,x) after pairing is defined. ***)
L6724
Theorem. (Inj0E)
∀X y : set, y ∈ Inj0 X → ∃x : set, x ∈ X ∧ y = Inj1 x
Proof:
Proof not loaded.
L6728
Definition. We define Unj to be In_rec_i (λX f ⇒ {f x|x ∈ X ∖ {0}}) of type set → set.
L6731
Theorem. (Unj_eq)
∀X : set, Unj X = {Unj x|x ∈ X ∖ {0}}
Proof:
Proof not loaded.
(*** Unj : Left inverse of Inj1 and Inj0 ***)
L6748
Theorem. (Unj_Inj1_eq)
∀X : set, Unj (Inj1 X) = X
Proof:
Proof not loaded.
L6800
Theorem. (Inj1_inj)
∀X Y : set, Inj1 X = Inj1 Y → X = Y
Proof:
Proof not loaded.
L6810
Theorem. (Unj_Inj0_eq)
∀X : set, Unj (Inj0 X) = X
Proof:
Proof not loaded.
L6858
Theorem. (Inj0_inj)
∀X Y : set, Inj0 X = Inj0 Y → X = Y
Proof:
Proof not loaded.
L6868
Theorem. (Inj0_0)
Proof:
Proof not loaded.
L6872
Theorem. (Inj0_Inj1_neq)
∀X Y : set, Inj0 X ≠ Inj1 Y
Proof:
Proof not loaded.
L6887
Definition. We define setsum to be λX Y ⇒ {Inj0 x|x ∈ X} ∪ {Inj1 y|y ∈ Y} of type set → set → set.
Notation. We use + as an infix operator with priority 450 and which associates to the left corresponding to applying term setsum.
(*** setsum ***)
L6892
Theorem. (Inj0_setsum)
∀X Y x : set, x ∈ X → Inj0 x ∈ X + Y
Proof:
Proof not loaded.
L6902
Theorem. (Inj1_setsum)
∀X Y y : set, y ∈ Y → Inj1 y ∈ X + Y
Proof:
Proof not loaded.
L6912
Theorem. (setsum_Inj_inv)
∀X Y z : set, z ∈ X + Y → (∃x ∈ X, z = Inj0 x) ∨ (∃y ∈ Y, z = Inj1 y)
Proof:
Proof not loaded.
L6924
Theorem. (Inj0_setsum_0L)
∀X : set, 0 + X = Inj0 X
Proof:
Proof not loaded.
L6957
Theorem. (Inj1_setsum_1L)
∀X : set, 1 + X = Inj1 X
Proof:
Proof not loaded.
Beginning of Section pair_setsum
L7010
Let pair ≝ setsum
L7011
Definition. We define proj0 to be λZ ⇒ {Unj z|z ∈ Z, ∃x : set, Inj0 x = z} of type set → set.
L7012
Definition. We define proj1 to be λZ ⇒ {Unj z|z ∈ Z, ∃y : set, Inj1 y = z} of type set → set.
L7013
Theorem. (Inj0_pair_0_eq)
Inj0 = pair 0
Proof:
Proof not loaded.
L7021
Theorem. (Inj1_pair_1_eq)
Inj1 = pair 1
Proof:
Proof not loaded.
L7029
Theorem. (pairI0)
∀X Y x, x ∈ X → pair 0 x ∈ pair X Y
Proof:
Proof not loaded.
L7034
Theorem. (pairI1)
∀X Y y, y ∈ Y → pair 1 y ∈ pair X Y
Proof:
Proof not loaded.
L7039
Theorem. (pairE)
∀X Y z, z ∈ pair X Y → (∃x ∈ X, z = pair 0 x) ∨ (∃y ∈ Y, z = pair 1 y)
Proof:
Proof not loaded.
L7045
Theorem. (pairE0)
∀X Y x, pair 0 x ∈ pair X Y → x ∈ X
Proof:
Proof not loaded.
L7071
Theorem. (pairE1)
∀X Y y, pair 1 y ∈ pair X Y → y ∈ Y
Proof:
Proof not loaded.
L7099
Theorem. (proj0I)
∀w u : set, pair 0 u ∈ w → u ∈ proj0 w
Proof:
Proof not loaded.
L7114
Theorem. (proj0E)
∀w u : set, u ∈ proj0 w → pair 0 u ∈ w
Proof:
Proof not loaded.
L7138
Theorem. (proj1I)
∀w u : set, pair 1 u ∈ w → u ∈ proj1 w
Proof:
Proof not loaded.
L7153
Theorem. (proj1E)
∀w u : set, u ∈ proj1 w → pair 1 u ∈ w
Proof:
Proof not loaded.
L7177
Theorem. (proj0_pair_eq)
∀X Y : set, proj0 (pair X Y) = X
Proof:
Proof not loaded.
L7197
Theorem. (proj1_pair_eq)
∀X Y : set, proj1 (pair X Y) = Y
Proof:
Proof not loaded.
L7219
Definition. We define Sigma to be λX Y ⇒ ⋃x ∈ X{pair x y|y ∈ Y x} of type set → (set → set) → set.
Notation. We use ∑ x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using Sigma.
(*** Sigma X Y = {(x,y) | x in X, y in Y x} ***)
L7225
Theorem. (Sigma_eta_proj0_proj1)
∀X : set, ∀Y : set → set, ∀z ∈ (∑x ∈ X, Y x), pair (proj0 z) (proj1 z) = z ∧ proj0 z ∈ X ∧ proj1 z ∈ Y (proj0 z)
Proof:
Proof not loaded.
L7253
Theorem. (proj0_Sigma)
∀X : set, ∀Y : set → set, ∀z : set, z ∈ (∑x ∈ X, Y x) → proj0 z ∈ X
Proof:
Proof not loaded.
L7261
Theorem. (proj1_Sigma)
∀X : set, ∀Y : set → set, ∀z : set, z ∈ (∑x ∈ X, Y x) → proj1 z ∈ Y (proj0 z)
Proof:
Proof not loaded.
L7269
Theorem. (pair_Sigma)
∀X : set, ∀Y : set → set, ∀x ∈ X, ∀y ∈ Y x, pair x y ∈ ∑x ∈ X, Y x
Proof:
Proof not loaded.
L7284
Theorem. (pair_Sigma_E1)
∀X : set, ∀Y : set → set, ∀x y : set, pair x y ∈ (∑x ∈ X, Y x) → y ∈ Y x
Proof:
Proof not loaded.
L7295
Theorem. (Sigma_E)
∀X : set, ∀Y : set → set, ∀z : set, z ∈ (∑x ∈ X, Y x) → ∃x ∈ X, ∃y ∈ Y x, z = pair x y
Proof:
Proof not loaded.
L7313
Definition. We define setprod to be λX Y : set ⇒ ∑x ∈ X, Y of type set → set → set.
Notation. We use ⨯ as an infix operator with priority 440 and which associates to the left corresponding to applying term setprod.
L7317
Let lam : set → (set → set) → set ≝ Sigma
L7319
Definition. We define ap to be λf x ⇒ {proj1 z|z ∈ f, ∃y : set, z = pair x y} of type set → set → set.
(*** lam X F = {(x,y) | x :e X, y :e F x} = \/_{x :e X} {(x,y) | y :e (F x)} = Sigma X F ***)
Notation. When x is a set, a term x y is notation for ap x y.
Notation. λ x ∈ A ⇒ B is notation for the set Sigma A (λ x : set ⇒ B).
Notation. We now use n-tuple notation (a0,...,an-1) for n ≥ 2 for λ i ∈ n . if i = 0 then a0 else ... if i = n-2 then an-2 else an-1.
(*** ap f x = {proj1 z | z :e f, exists y, z = pair x y}} ***)
L7323
Theorem. (lamI)
∀X : set, ∀F : set → set, ∀x ∈ X, ∀y ∈ F x, pair x y ∈ λx ∈ X ⇒ F x
Proof:
Proof not loaded.
L7327
Theorem. (lamE)
∀X : set, ∀F : set → set, ∀z : set, z ∈ (λx ∈ X ⇒ F x) → ∃x ∈ X, ∃y ∈ F x, z = pair x y
Proof:
Proof not loaded.
L7331
Theorem. (apI)
∀f x y, pair x y ∈ f → y ∈ f x
Proof:
Proof not loaded.
L7343
Theorem. (apE)
∀f x y, y ∈ f x → pair x y ∈ f
Proof:
Proof not loaded.
L7371
Theorem. (beta)
∀X : set, ∀F : set → set, ∀x : set, x ∈ X → (λx ∈ X ⇒ F x) x = F x
Proof:
Proof not loaded.
L7391
Theorem. (proj0_ap_0)
∀u, proj0 u = u 0
Proof:
Proof not loaded.
L7411
Theorem. (proj1_ap_1)
∀u, proj1 u = u 1
Proof:
Proof not loaded.
L7431
Theorem. (pair_ap_0)
∀x y : set, (pair x y) 0 = x
Proof:
Proof not loaded.
L7438
Theorem. (pair_ap_1)
∀x y : set, (pair x y) 1 = y
Proof:
Proof not loaded.
L7445
Theorem. (ap0_Sigma)
∀X : set, ∀Y : set → set, ∀z : set, z ∈ (∑x ∈ X, Y x) → (z 0) ∈ X
Proof:
Proof not loaded.
L7451
Theorem. (ap1_Sigma)
∀X : set, ∀Y : set → set, ∀z : set, z ∈ (∑x ∈ X, Y x) → (z 1) ∈ (Y (z 0))
Proof:
Proof not loaded.
L7458
Definition. We define pair_p to be λu : set ⇒ pair (u 0) (u 1) = u of type set → prop.
L7461
Theorem. (pair_p_I)
∀x y, pair_p (pair x y)
Proof:
Proof not loaded.
L7469
Proof:
Proof not loaded.
L7487
Theorem. (tuple_pair)
∀x y : set, pair x y = (x,y)
Proof:
Proof not loaded.
L7562
Definition. We define Pi to be λX Y ⇒ {f ∈ 𝒫 (∑x ∈ X, ⋃ (Y x))|∀x ∈ X, f x ∈ Y x} of type set → (set → set) → set.
Notation. We use ∏ x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using Pi.
L7566
Theorem. (PiI)
∀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
Proof:
Proof not loaded.
L7600
Theorem. (lam_Pi)
∀X : set, ∀Y : set → set, ∀F : set → set, (∀x ∈ X, F x ∈ Y x) → (λx ∈ X ⇒ F x) ∈ (∏x ∈ X, Y x)
Proof:
Proof not loaded.
L7639
Theorem. (ap_Pi)
∀X : set, ∀Y : set → set, ∀f : set, ∀x : set, f ∈ (∏x ∈ X, Y x) → x ∈ X → f x ∈ Y x
Proof:
Proof not loaded.
L7645
Definition. We define setexp to be λX Y : set ⇒ ∏y ∈ Y, X of type set → set → set.
Notation. We use :^: as an infix operator with priority 430 and which associates to the left corresponding to applying term setexp.
L7649
Theorem. (pair_tuple_fun)
pair = (λx y ⇒ (x,y))
Proof:
Proof not loaded.
Beginning of Section Tuples
L7658
Variable x0 x1 : set
L7659
Theorem. (tuple_2_0_eq)
(x0,x1) 0 = x0
Proof:
Proof not loaded.
L7664
Theorem. (tuple_2_1_eq)
(x0,x1) 1 = x1
Proof:
Proof not loaded.
End of Section Tuples
L7671
Theorem. (ReplEq_setprod_ext)
∀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}
Proof:
Proof not loaded.
L7682
Theorem. (lamI2)
∀X, ∀F : set → set, ∀x ∈ X, ∀y ∈ F x, (x,y) ∈ λx ∈ X ⇒ F x
Proof:
Proof not loaded.
L7688
Theorem. (tuple_2_Sigma)
∀X : set, ∀Y : set → set, ∀x ∈ X, ∀y ∈ Y x, (x,y) ∈ ∑x ∈ X, Y x
Proof:
Proof not loaded.
L7692
Theorem. (tuple_2_setprod)
∀X : set, ∀Y : set, ∀x ∈ X, ∀y ∈ Y, (x,y) ∈ X ⨯ Y
Proof:
Proof not loaded.
End of Section pair_setsum
Notation. We use ∑ x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using Sigma.
Notation. We use ⨯ as an infix operator with priority 440 and which associates to the left corresponding to applying term setprod.
Notation. We use ∏ x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using Pi.
Notation. We use :^: as an infix operator with priority 430 and which associates to the left corresponding to applying term setexp.
L7707
Definition. We define DescrR_i_io_1 to be λR ⇒ Eps_i (λx ⇒ (∃y : set → prop, R x y) ∧ (∀y z : set → prop, R x y → R x z → y = z)) of type (set → (set → prop) → prop) → set.
L7709
Definition. We define DescrR_i_io_2 to be λR ⇒ Descr_Vo1 (λy ⇒ R (DescrR_i_io_1 R) y) of type (set → (set → prop) → prop) → set → prop.
L7710
Theorem. (DescrR_i_io_12)
∀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)
Proof:
Proof not loaded.
L7720
Definition. We define PNoEq_ to be λalpha p q ⇒ ∀beta ∈ alpha, p beta ↔ q beta of type set → (set → prop) → (set → prop) → prop.
(*** Conway describes this way of formalizing in ZF in an appendix to Part Zero of his book,
but rejects formalization in favor of "Mathematician's Liberation." ***)
L7726
Theorem. (PNoEq_ref_)
∀alpha, ∀p : set → prop, PNoEq_ alpha p p
Proof:
Proof not loaded.
L7732
Theorem. (PNoEq_sym_)
∀alpha, ∀p q : set → prop, PNoEq_ alpha p q → PNoEq_ alpha q p
Proof:
Proof not loaded.
L7740
Theorem. (PNoEq_tra_)
∀alpha, ∀p q r : set → prop, PNoEq_ alpha p q → PNoEq_ alpha q r → PNoEq_ alpha p r
Proof:
Proof not loaded.
L7749
Theorem. (PNoEq_antimon_)
∀p q : set → prop, ∀alpha, ordinal alpha → ∀beta ∈ alpha, PNoEq_ alpha p q → PNoEq_ beta p q
Proof:
Proof not loaded.
L7759
Definition. We define PNoLt_ to be λalpha p q ⇒ ∃beta ∈ alpha, PNoEq_ beta p q ∧ ¬ p beta ∧ q beta of type set → (set → prop) → (set → prop) → prop.
L7762
Theorem. (PNoLt_E_)
∀alpha, ∀p q : set → prop, PNoLt_ alpha p q → ∀R : prop, (∀beta, beta ∈ alpha → PNoEq_ beta p q → ¬ p beta → q beta → R) → R
Proof:
Proof not loaded.
L7773
Theorem. (PNoLt_irref_)
∀alpha, ∀p : set → prop, ¬ PNoLt_ alpha p p
Proof:
Proof not loaded.
L7780
Theorem. (PNoLt_mon_)
∀p q : set → prop, ∀alpha, ordinal alpha → ∀beta ∈ alpha, PNoLt_ beta p q → PNoLt_ alpha p q
Proof:
Proof not loaded.
L7791
Theorem. (PNoLt_trichotomy_or_)
∀p q : set → prop, ∀alpha, ordinal alpha → PNoLt_ alpha p q ∨ PNoEq_ alpha p q ∨ PNoLt_ alpha q p
Proof:
Proof not loaded.
L7866
Definition. We define PNoLt to be λalpha p beta q ⇒ PNoLt_ (alpha ∩ beta) p q ∨ alpha ∈ beta ∧ PNoEq_ alpha p q ∧ q alpha ∨ beta ∈ alpha ∧ PNoEq_ beta p q ∧ ¬ p beta of type set → (set → prop) → set → (set → prop) → prop.
L7871
Theorem. (PNoLtI1)
∀alpha beta, ∀p q : set → prop, PNoLt_ (alpha ∩ beta) p q → PNoLt alpha p beta q
Proof:
Proof not loaded.
L7880
Theorem. (PNoLtI2)
∀alpha beta, ∀p q : set → prop, alpha ∈ beta → PNoEq_ alpha p q → q alpha → PNoLt alpha p beta q
Proof:
Proof not loaded.
L7892
Theorem. (PNoLtI3)
∀alpha beta, ∀p q : set → prop, beta ∈ alpha → PNoEq_ beta p q → ¬ p beta → PNoLt alpha p beta q
Proof:
Proof not loaded.
L7904
Theorem. (PNoLtE)
∀alpha beta, ∀p q : set → prop, PNoLt alpha p beta q → ∀R : prop, (PNoLt_ (alpha ∩ beta) p q → R) → (alpha ∈ beta → PNoEq_ alpha p q → q alpha → R) → (beta ∈ alpha → PNoEq_ beta p q → ¬ p beta → R) → R
Proof:
Proof not loaded.
L7919
Theorem. (PNoLt_irref)
∀alpha, ∀p : set → prop, ¬ PNoLt alpha p alpha p
Proof:
Proof not loaded.
L7930
Theorem. (PNoLt_trichotomy_or)
∀alpha beta, ∀p q : set → prop, ordinal alpha → ordinal beta → PNoLt alpha p beta q ∨ alpha = beta ∧ PNoEq_ alpha p q ∨ PNoLt beta q alpha p
Proof:
Proof not loaded.
L7997
Theorem. (PNoLtEq_tra)
∀alpha beta, ordinal alpha → ordinal beta → ∀p q r : set → prop, PNoLt alpha p beta q → PNoEq_ beta q r → PNoLt alpha p beta r
Proof:
Proof not loaded.
L8051
Theorem. (PNoEqLt_tra)
∀alpha beta, ordinal alpha → ordinal beta → ∀p q r : set → prop, PNoEq_ alpha p q → PNoLt alpha q beta r → PNoLt alpha p beta r
Proof:
Proof not loaded.
L8109
Theorem. (PNoLt_tra)
∀alpha beta gamma, ordinal alpha → ordinal beta → ordinal gamma → ∀p q r : set → prop, PNoLt alpha p beta q → PNoLt beta q gamma r → PNoLt alpha p gamma r
Proof:
Proof not loaded.
L8424
Definition. We define PNoLe to be λalpha p beta q ⇒ PNoLt alpha p beta q ∨ alpha = beta ∧ PNoEq_ alpha p q of type set → (set → prop) → set → (set → prop) → prop.
L8427
Theorem. (PNoLeI1)
∀alpha beta, ∀p q : set → prop, PNoLt alpha p beta q → PNoLe alpha p beta q
Proof:
Proof not loaded.
L8435
Theorem. (PNoLeI2)
∀alpha, ∀p q : set → prop, PNoEq_ alpha p q → PNoLe alpha p alpha q
Proof:
Proof not loaded.
L8445
Theorem. (PNoLe_ref)
∀alpha, ∀p : set → prop, PNoLe alpha p alpha p
Proof:
Proof not loaded.
L8451
Theorem. (PNoLe_antisym)
∀alpha beta, ordinal alpha → ordinal beta → ∀p q : set → prop, PNoLe alpha p beta q → PNoLe beta q alpha p → alpha = beta ∧ PNoEq_ alpha p q
Proof:
Proof not loaded.
L8497
Theorem. (PNoLtLe_tra)
∀alpha beta gamma, ordinal alpha → ordinal beta → ordinal gamma → ∀p q r : set → prop, PNoLt alpha p beta q → PNoLe beta q gamma r → PNoLt alpha p gamma r
Proof:
Proof not loaded.
L8514
Theorem. (PNoLeLt_tra)
∀alpha beta gamma, ordinal alpha → ordinal beta → ordinal gamma → ∀p q r : set → prop, PNoLe alpha p beta q → PNoLt beta q gamma r → PNoLt alpha p gamma r
Proof:
Proof not loaded.
L8533
Theorem. (PNoEqLe_tra)
∀alpha beta, ordinal alpha → ordinal beta → ∀p q r : set → prop, PNoEq_ alpha p q → PNoLe alpha q beta r → PNoLe alpha p beta r
Proof:
Proof not loaded.
L8552
Theorem. (PNoLe_tra)
∀alpha beta gamma, ordinal alpha → ordinal beta → ordinal gamma → ∀p q r : set → prop, PNoLe alpha p beta q → PNoLe beta q gamma r → PNoLe alpha p gamma r
Proof:
Proof not loaded.
L8573
Definition. We define PNo_downc to be λL alpha p ⇒ ∃beta, ordinal beta ∧ ∃q : set → prop, L beta q ∧ PNoLe alpha p beta q of type (set → (set → prop) → prop) → set → (set → prop) → prop.
L8576
Definition. We define PNo_upc to be λR alpha p ⇒ ∃beta, ordinal beta ∧ ∃q : set → prop, R beta q ∧ PNoLe beta q alpha p of type (set → (set → prop) → prop) → set → (set → prop) → prop.
L8578
Theorem. (PNoLe_downc)
∀L : set → (set → prop) → prop, ∀alpha beta, ∀p q : set → prop, ordinal alpha → ordinal beta → PNo_downc L alpha p → PNoLe beta q alpha p → PNo_downc L beta q
Proof:
Proof not loaded.
L8598
Theorem. (PNo_downc_ref)
∀L : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀p : set → prop, L alpha p → PNo_downc L alpha p
Proof:
Proof not loaded.
L8609
Theorem. (PNo_upc_ref)
∀R : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀p : set → prop, R alpha p → PNo_upc R alpha p
Proof:
Proof not loaded.
L8620
Theorem. (PNoLe_upc)
∀R : set → (set → prop) → prop, ∀alpha beta, ∀p q : set → prop, ordinal alpha → ordinal beta → PNo_upc R alpha p → PNoLe alpha p beta q → PNo_upc R beta q
Proof:
Proof not loaded.
L8640
Definition. We define PNoLt_pwise to be λL R ⇒ ∀gamma, ordinal gamma → ∀p : set → prop, L gamma p → ∀delta, ordinal delta → ∀q : set → prop, R delta q → PNoLt gamma p delta q of type (set → (set → prop) → prop) → (set → (set → prop) → prop) → prop.
L8643
Theorem. (PNoLt_pwise_downc_upc)
∀L R : set → (set → prop) → prop, PNoLt_pwise L R → PNoLt_pwise (PNo_downc L) (PNo_upc R)
Proof:
Proof not loaded.
L8684
Definition. We define PNo_rel_strict_upperbd to be λL alpha p ⇒ ∀beta ∈ alpha, ∀q : set → prop, PNo_downc L beta q → PNoLt beta q alpha p of type (set → (set → prop) → prop) → set → (set → prop) → prop.
L8688
Definition. We define PNo_rel_strict_lowerbd to be λR alpha p ⇒ ∀beta ∈ alpha, ∀q : set → prop, PNo_upc R beta q → PNoLt alpha p beta q of type (set → (set → prop) → prop) → set → (set → prop) → prop.
L8691
Definition. We define PNo_rel_strict_imv to be λL R alpha p ⇒ PNo_rel_strict_upperbd L alpha p ∧ PNo_rel_strict_lowerbd R alpha p of type (set → (set → prop) → prop) → (set → (set → prop) → prop) → set → (set → prop) → prop.
L8693
Theorem. (PNoEq_rel_strict_upperbd)
∀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
Proof:
Proof not loaded.
L8710
Theorem. (PNo_rel_strict_upperbd_antimon)
∀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
Proof:
Proof not loaded.
L8751
Theorem. (PNoEq_rel_strict_lowerbd)
∀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
Proof:
Proof not loaded.
L8768
Theorem. (PNo_rel_strict_lowerbd_antimon)
∀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
Proof:
Proof not loaded.
L8809
Theorem. (PNoEq_rel_strict_imv)
∀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
Proof:
Proof not loaded.
L8819
Theorem. (PNo_rel_strict_imv_antimon)
∀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
Proof:
Proof not loaded.
L8829
Definition. We define PNo_rel_strict_uniq_imv to be λL R alpha p ⇒ PNo_rel_strict_imv L R alpha p ∧ ∀q : set → prop, PNo_rel_strict_imv L R alpha q → PNoEq_ alpha p q of type (set → (set → prop) → prop) → (set → (set → prop) → prop) → set → (set → prop) → prop.
L8832
Definition. We define PNo_rel_strict_split_imv to be λL R alpha p ⇒ PNo_rel_strict_imv L R (ordsucc alpha) (λdelta ⇒ p delta ∧ delta ≠ alpha) ∧ PNo_rel_strict_imv L R (ordsucc alpha) (λdelta ⇒ p delta ∨ delta = alpha) of type (set → (set → prop) → prop) → (set → (set → prop) → prop) → set → (set → prop) → prop.
L8836
Theorem. (PNo_extend0_eq)
∀alpha, ∀p : set → prop, PNoEq_ alpha p (λdelta ⇒ p delta ∧ delta ≠ alpha)
Proof:
Proof not loaded.
L8853
Theorem. (PNo_extend1_eq)
∀alpha, ∀p : set → prop, PNoEq_ alpha p (λdelta ⇒ p delta ∨ delta = alpha)
Proof:
Proof not loaded.
L8870
Theorem. (PNo_rel_imv_ex)
∀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)
Proof:
Proof not loaded.
L9947
Definition. We define PNo_lenbdd to be λalpha L ⇒ ∀beta, ∀p : set → prop, L beta p → beta ∈ alpha of type set → (set → (set → prop) → prop) → prop.
L9950
Theorem. (PNo_lenbdd_strict_imv_extend0)
∀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)
Proof:
Proof not loaded.
L10087
Theorem. (PNo_lenbdd_strict_imv_extend1)
∀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)
Proof:
Proof not loaded.
L10229
Theorem. (PNo_lenbdd_strict_imv_split)
∀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
Proof:
Proof not loaded.
L10245
Theorem. (PNo_rel_imv_bdd_ex)
∀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
Proof:
Proof not loaded.
L10279
Definition. We define PNo_strict_upperbd to be λL alpha p ⇒ ∀beta, ordinal beta → ∀q : set → prop, L beta q → PNoLt beta q alpha p of type (set → (set → prop) → prop) → set → (set → prop) → prop.
L10283
Definition. We define PNo_strict_lowerbd to be λR alpha p ⇒ ∀beta, ordinal beta → ∀q : set → prop, R beta q → PNoLt alpha p beta q of type (set → (set → prop) → prop) → set → (set → prop) → prop.
L10286
Definition. We define PNo_strict_imv to be λL R alpha p ⇒ PNo_strict_upperbd L alpha p ∧ PNo_strict_lowerbd R alpha p of type (set → (set → prop) → prop) → (set → (set → prop) → prop) → set → (set → prop) → prop.
L10288
Theorem. (PNoEq_strict_upperbd)
∀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
Proof:
Proof not loaded.
L10303
Theorem. (PNoEq_strict_lowerbd)
∀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
Proof:
Proof not loaded.
L10318
Theorem. (PNoEq_strict_imv)
∀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
Proof:
Proof not loaded.
L10328
Theorem. (PNo_strict_upperbd_imp_rel_strict_upperbd)
∀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
Proof:
Proof not loaded.
L10409
Theorem. (PNo_strict_lowerbd_imp_rel_strict_lowerbd)
∀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
Proof:
Proof not loaded.
L10488
Theorem. (PNo_strict_imv_imp_rel_strict_imv)
∀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
Proof:
Proof not loaded.
L10507
Theorem. (PNo_rel_split_imv_imp_strict_imv)
∀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
Proof:
Proof not loaded.
L10753
Theorem. (PNo_lenbdd_strict_imv_ex)
∀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
Proof:
Proof not loaded.
L10779
Definition. We define PNo_least_rep to be λL R beta p ⇒ ordinal beta ∧ PNo_strict_imv L R beta p ∧ ∀gamma ∈ beta, ∀q : set → prop, ¬ PNo_strict_imv L R gamma q of type (set → (set → prop) → prop) → (set → (set → prop) → prop) → set → (set → prop) → prop.
L10785
Definition. We define PNo_least_rep2 to be λL R beta p ⇒ PNo_least_rep L R beta p ∧ ∀x, x ∉ beta → ¬ p x of type (set → (set → prop) → prop) → (set → (set → prop) → prop) → set → (set → prop) → prop.
L10787
Theorem. (PNo_strict_imv_pred_eq)
∀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
Proof:
Proof not loaded.
L10883
Theorem. (PNo_lenbdd_least_rep2_exuniq2)
∀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)
Proof:
Proof not loaded.
L10971
Definition. We define PNo_bd to be λL R ⇒ DescrR_i_io_1 (PNo_least_rep2 L R) of type (set → (set → prop) → prop) → (set → (set → prop) → prop) → set.
L10974
Definition. We define PNo_pred to be λL R ⇒ DescrR_i_io_2 (PNo_least_rep2 L R) of type (set → (set → prop) → prop) → (set → (set → prop) → prop) → set → prop.
L10976
Theorem. (PNo_bd_pred_lem)
∀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)
Proof:
Proof not loaded.
L10988
Theorem. (PNo_bd_pred)
∀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)
Proof:
Proof not loaded.
L10999
Theorem. (PNo_bd_In)
∀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
Proof:
Proof not loaded.
Beginning of Section TaggedSets
L11033
Let tag : set → set ≝ λalpha ⇒ SetAdjoin alpha {1}
Notation. We use ' as a postfix operator with priority 100 corresponding to applying term tag.
L11035
Proof:
Proof not loaded.
L11043
Proof:
Proof not loaded.
L11047
Theorem. (tagged_not_ordinal)
∀y, ¬ ordinal (y ')
Proof:
Proof not loaded.
L11059
Theorem. (tagged_notin_ordinal)
∀alpha y, ordinal alpha → (y ') ∉ alpha
Proof:
Proof not loaded.
L11066
Theorem. (tagged_eqE_Subq)
∀alpha beta, ordinal alpha → alpha ' = beta ' → alpha ⊆ beta
Proof:
Proof not loaded.
L11087
Theorem. (tagged_eqE_eq)
∀alpha beta, ordinal alpha → ordinal beta → alpha ' = beta ' → alpha = beta
Proof:
Proof not loaded.
L11095
Theorem. (tagged_ReplE)
∀alpha beta, ordinal alpha → ordinal beta → beta ' ∈ {gamma '|gamma ∈ alpha} → beta ∈ alpha
Proof:
Proof not loaded.
L11108
Theorem. (ordinal_notin_tagged_Repl)
∀alpha Y, ordinal alpha → alpha ∉ {y '|y ∈ Y}
Proof:
Proof not loaded.
L11122
Definition. We define SNoElts_ to be λalpha ⇒ alpha ∪ {beta '|beta ∈ alpha} of type set → set.
L11124
Theorem. (SNoElts_mon)
∀alpha beta, alpha ⊆ beta → SNoElts_ alpha ⊆ SNoElts_ beta
Proof:
Proof not loaded.
L11148
Definition. We define SNo_ to be λalpha x ⇒ x ⊆ SNoElts_ alpha ∧ ∀beta ∈ alpha, exactly1of2 (beta ' ∈ x) (beta ∈ x) of type set → set → prop.
L11152
Definition. We define PSNo to be λalpha p ⇒ {beta ∈ alpha|p beta} ∪ {beta '|beta ∈ alpha, ¬ p beta} of type set → (set → prop) → set.
L11154
Theorem. (PNoEq_PSNo)
∀alpha, ordinal alpha → ∀p : set → prop, PNoEq_ alpha (λbeta ⇒ beta ∈ PSNo alpha p) p
Proof:
Proof not loaded.
L11181
Theorem. (SNo_PSNo)
∀alpha, ordinal alpha → ∀p : set → prop, SNo_ alpha (PSNo alpha p)
Proof:
Proof not loaded.
L11261
Theorem. (SNo_PSNo_eta_)
∀alpha x, ordinal alpha → SNo_ alpha x → x = PSNo alpha (λbeta ⇒ beta ∈ x)
Proof:
Proof not loaded.
L11328
Definition. We define SNo to be λx ⇒ ∃alpha, ordinal alpha ∧ SNo_ alpha x of type set → prop.
L11329
Theorem. (SNo_SNo)
∀alpha, ordinal alpha → ∀z, SNo_ alpha z → SNo z
Proof:
Proof not loaded.
L11340
Definition. We define SNoLev to be λx ⇒ Eps_i (λalpha ⇒ ordinal alpha ∧ SNo_ alpha x) of type set → set.
L11341
Theorem. (SNoLev_uniq_Subq)
∀x alpha beta, ordinal alpha → ordinal beta → SNo_ alpha x → SNo_ beta x → alpha ⊆ beta
Proof:
Proof not loaded.
L11374
Theorem. (SNoLev_uniq)
∀x alpha beta, ordinal alpha → ordinal beta → SNo_ alpha x → SNo_ beta x → alpha = beta
Proof:
Proof not loaded.
L11381
Theorem. (SNoLev_prop)
∀x, SNo x → ordinal (SNoLev x) ∧ SNo_ (SNoLev x) x
Proof:
Proof not loaded.
L11387
Theorem. (SNoLev_ordinal)
∀x, SNo x → ordinal (SNoLev x)
Proof:
Proof not loaded.
L11391
Theorem. (SNoLev_)
∀x, SNo x → SNo_ (SNoLev x) x
Proof:
Proof not loaded.
L11395
Theorem. (SNo_PSNo_eta)
∀x, SNo x → x = PSNo (SNoLev x) (λbeta ⇒ beta ∈ x)
Proof:
Proof not loaded.
L11405
Theorem. (SNoLev_PSNo)
∀alpha, ordinal alpha → ∀p : set → prop, SNoLev (PSNo alpha p) = alpha
Proof:
Proof not loaded.
L11422
Theorem. (SNo_Subq)
∀x y, SNo x → SNo y → SNoLev x ⊆ SNoLev y → (∀alpha ∈ SNoLev x, alpha ∈ x ↔ alpha ∈ y) → x ⊆ y
Proof:
Proof not loaded.
L11467
Definition. We define SNoEq_ to be λalpha x y ⇒ PNoEq_ alpha (λbeta ⇒ beta ∈ x) (λbeta ⇒ beta ∈ y) of type set → set → set → prop.
L11470
Theorem. (SNoEq_I)
∀alpha x y, (∀beta ∈ alpha, beta ∈ x ↔ beta ∈ y) → SNoEq_ alpha x y
Proof:
Proof not loaded.
L11474
Theorem. (SNo_eq)
∀x y, SNo x → SNo y → SNoLev x = SNoLev y → SNoEq_ (SNoLev x) x y → x = y
Proof:
Proof not loaded.
End of Section TaggedSets
L11494
Definition. We define SNoLt to be λx y ⇒ PNoLt (SNoLev x) (λbeta ⇒ beta ∈ x) (SNoLev y) (λbeta ⇒ beta ∈ y) of type set → set → prop.
Notation. We use < as an infix operator with priority 490 and no associativity corresponding to applying term SNoLt.
L11497
Definition. We define SNoLe to be λx y ⇒ PNoLe (SNoLev x) (λbeta ⇒ beta ∈ x) (SNoLev y) (λbeta ⇒ beta ∈ y) of type set → set → prop.
Notation. We use ≤ as an infix operator with priority 490 and no associativity corresponding to applying term SNoLe.
L11501
Theorem. (SNoLtLe)
∀x y, x < y → x ≤ y
Proof:
Proof not loaded.
L11508
Theorem. (SNoLeE)
∀x y, SNo x → SNo y → x ≤ y → x < y ∨ x = y
Proof:
Proof not loaded.
L11522
Theorem. (SNoEq_sym_)
∀alpha x y, SNoEq_ alpha x y → SNoEq_ alpha y x
Proof:
Proof not loaded.
L11527
Theorem. (SNoEq_tra_)
∀alpha x y z, SNoEq_ alpha x y → SNoEq_ alpha y z → SNoEq_ alpha x z
Proof:
Proof not loaded.
L11532
Theorem. (SNoLtE)
∀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
Proof:
Proof not loaded.
L11635
Theorem. (SNoLtI2)
∀x y, SNoLev x ∈ SNoLev y → SNoEq_ (SNoLev x) x y → SNoLev x ∈ y → x < y
Proof:
Proof not loaded.
L11650
Theorem. (SNoLtI3)
∀x y, SNoLev y ∈ SNoLev x → SNoEq_ (SNoLev y) x y → SNoLev y ∉ x → x < y
Proof:
Proof not loaded.
L11664
Theorem. (SNoLt_irref)
∀x, ¬ SNoLt x x
Proof:
Proof not loaded.
L11669
Theorem. (SNoLt_trichotomy_or)
∀x y, SNo x → SNo y → x < y ∨ x = y ∨ y < x
Proof:
Proof not loaded.
L11680
Theorem. (SNoLt_trichotomy_or_impred)
∀x y, SNo x → SNo y → ∀p : prop, (x < y → p) → (x = y → p) → (y < x → p) → p
Proof:
Proof not loaded.
L11693
Theorem. (SNoLt_tra)
∀x y z, SNo x → SNo y → SNo z → x < y → y < z → x < z
Proof:
Proof not loaded.
L11699
Theorem. (SNoLe_ref)
∀x, SNoLe x x
Proof:
Proof not loaded.
L11703
Theorem. (SNoLe_antisym)
∀x y, SNo x → SNo y → x ≤ y → y ≤ x → x = y
Proof:
Proof not loaded.
L11711
Theorem. (SNoLtLe_tra)
∀x y z, SNo x → SNo y → SNo z → x < y → y ≤ z → x < z
Proof:
Proof not loaded.
L11716
Theorem. (SNoLeLt_tra)
∀x y z, SNo x → SNo y → SNo z → x ≤ y → y < z → x < z
Proof:
Proof not loaded.
L11721
Theorem. (SNoLe_tra)
∀x y z, SNo x → SNo y → SNo z → x ≤ y → y ≤ z → x ≤ z
Proof:
Proof not loaded.
L11726
Theorem. (SNoLtLe_or)
∀x y, SNo x → SNo y → x < y ∨ y ≤ x
Proof:
Proof not loaded.
L11735
Theorem. (SNoLt_PSNo_PNoLt)
∀alpha beta, ∀p q : set → prop, ordinal alpha → ordinal beta → PSNo alpha p < PSNo beta q → PNoLt alpha p beta q
Proof:
Proof not loaded.
L11758
Theorem. (PNoLt_SNoLt_PSNo)
∀alpha beta, ∀p q : set → prop, ordinal alpha → ordinal beta → PNoLt alpha p beta q → PSNo alpha p < PSNo beta q
Proof:
Proof not loaded.
L11781
Definition. We define SNoCut to be λL R ⇒ PSNo (PNo_bd (λalpha p ⇒ ordinal alpha ∧ PSNo alpha p ∈ L) (λalpha p ⇒ ordinal alpha ∧ PSNo alpha p ∈ R)) (PNo_pred (λalpha p ⇒ ordinal alpha ∧ PSNo alpha p ∈ L) (λalpha p ⇒ ordinal alpha ∧ PSNo alpha p ∈ R)) of type set → set → set.
L11784
Definition. We define SNoCutP to be λL R ⇒ (∀x ∈ L, SNo x) ∧ (∀y ∈ R, SNo y) ∧ (∀x ∈ L, ∀y ∈ R, x < y) of type set → set → prop.
L11789
Theorem. (SNoCutP_SNoCut)
∀L R, SNoCutP L R → SNo (SNoCut L R) ∧ SNoLev (SNoCut L R) ∈ ordsucc ((⋃x ∈ Lordsucc (SNoLev x)) ∪ (⋃y ∈ Rordsucc (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)
Proof:
Proof not loaded.
L12178
Theorem. (SNoCutP_SNoCut_impred)
∀L R, SNoCutP L R → ∀p : prop, (SNo (SNoCut L R) → SNoLev (SNoCut L R) ∈ ordsucc ((⋃x ∈ Lordsucc (SNoLev x)) ∪ (⋃y ∈ Rordsucc (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
Proof:
Proof not loaded.
L12193
Theorem. (SNoCutP_L_0)
∀L, (∀x ∈ L, SNo x) → SNoCutP L 0
Proof:
Proof not loaded.
L12204
Theorem. (SNoCutP_0_0)
Proof:
Proof not loaded.
L12208
Definition. We define SNoS_ to be λalpha ⇒ {x ∈ 𝒫 (SNoElts_ alpha)|∃beta ∈ alpha, SNo_ beta x} of type set → set.
L12210
Theorem. (SNoS_E)
∀alpha, ordinal alpha → ∀x ∈ SNoS_ alpha, ∃beta ∈ alpha, SNo_ beta x
Proof:
Proof not loaded.
Beginning of Section TaggedSets2
L12220
Let tag : set → set ≝ λalpha ⇒ SetAdjoin alpha {1}
Notation. We use ' as a postfix operator with priority 100 corresponding to applying term tag.
L12222
Theorem. (SNoS_I)
∀alpha, ordinal alpha → ∀x, ∀beta ∈ alpha, SNo_ beta x → x ∈ SNoS_ alpha
Proof:
Proof not loaded.
L12247
Theorem. (SNoS_I2)
∀x y, SNo x → SNo y → SNoLev x ∈ SNoLev y → x ∈ SNoS_ (SNoLev y)
Proof:
Proof not loaded.
L12253
Theorem. (SNoS_Subq)
∀alpha beta, ordinal alpha → ordinal beta → alpha ⊆ beta → SNoS_ alpha ⊆ SNoS_ beta
Proof:
Proof not loaded.
L12263
Theorem. (SNoLev_uniq2)
∀alpha, ordinal alpha → ∀x, SNo_ alpha x → SNoLev x = alpha
Proof:
Proof not loaded.
L12276
Theorem. (SNoS_E2)
∀alpha, ordinal alpha → ∀x ∈ SNoS_ alpha, ∀p : prop, (SNoLev x ∈ alpha → ordinal (SNoLev x) → SNo x → SNo_ (SNoLev x) x → p) → p
Proof:
Proof not loaded.
L12300
Theorem. (SNoS_In_neq)
∀w, SNo w → ∀x ∈ SNoS_ (SNoLev w), x ≠ w
Proof:
Proof not loaded.
L12316
Theorem. (SNoS_SNoLev)
∀z, SNo z → z ∈ SNoS_ (ordsucc (SNoLev z))
Proof:
Proof not loaded.
L12324
Definition. We define SNoL to be λz ⇒ {x ∈ SNoS_ (SNoLev z)|x < z} of type set → set.
L12326
Definition. We define SNoR to be λz ⇒ {y ∈ SNoS_ (SNoLev z)|z < y} of type set → set.
L12327
Theorem. (SNoCutP_SNoL_SNoR)
∀z, SNo z → SNoCutP (SNoL z) (SNoR z)
Proof:
Proof not loaded.
L12375
Theorem. (SNoL_E)
∀x, SNo x → ∀w ∈ SNoL x, ∀p : prop, (SNo w → SNoLev w ∈ SNoLev x → w < x → p) → p
Proof:
Proof not loaded.
L12393
Theorem. (SNoR_E)
∀x, SNo x → ∀z ∈ SNoR x, ∀p : prop, (SNo z → SNoLev z ∈ SNoLev x → x < z → p) → p
Proof:
Proof not loaded.
L12411
Theorem. (SNoL_SNoS_)
∀z, SNoL z ⊆ SNoS_ (SNoLev z)
Proof:
Proof not loaded.
L12415
Theorem. (SNoR_SNoS_)
∀z, SNoR z ⊆ SNoS_ (SNoLev z)
Proof:
Proof not loaded.
L12419
Theorem. (SNoL_SNoS)
∀x, SNo x → ∀w ∈ SNoL x, w ∈ SNoS_ (SNoLev x)
Proof:
Proof not loaded.
L12429
Theorem. (SNoR_SNoS)
∀x, SNo x → ∀z ∈ SNoR x, z ∈ SNoS_ (SNoLev x)
Proof:
Proof not loaded.
L12439
Theorem. (SNoL_I)
∀z, SNo z → ∀x, SNo x → SNoLev x ∈ SNoLev z → x < z → x ∈ SNoL z
Proof:
Proof not loaded.
L12449
Theorem. (SNoR_I)
∀z, SNo z → ∀y, SNo y → SNoLev y ∈ SNoLev z → z < y → y ∈ SNoR z
Proof:
Proof not loaded.
L12459
Theorem. (SNo_eta)
∀z, SNo z → z = SNoCut (SNoL z) (SNoR z)
Proof:
Proof not loaded.
L12533
Theorem. (SNoCutP_SNo_SNoCut)
∀L R, SNoCutP L R → SNo (SNoCut L R)
Proof:
Proof not loaded.
L12542
Theorem. (SNoCutP_SNoCut_L)
∀L R, SNoCutP L R → ∀x ∈ L, x < SNoCut L R
Proof:
Proof not loaded.
L12550
Theorem. (SNoCutP_SNoCut_R)
∀L R, SNoCutP L R → ∀y ∈ R, SNoCut L R < y
Proof:
Proof not loaded.
L12557
Theorem. (SNoCutP_SNoCut_fst)
∀L R, SNoCutP L R → ∀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
Proof:
Proof not loaded.
L12569
Theorem. (SNoCut_Le)
∀L1 R1 L2 R2, SNoCutP L1 R1 → SNoCutP L2 R2 → (∀w ∈ L1, w < SNoCut L2 R2) → (∀z ∈ R2, SNoCut L1 R1 < z) → SNoCut L1 R1 ≤ SNoCut L2 R2
Proof:
Proof not loaded.
L12672
Theorem. (SNoCut_ext)
∀L1 R1 L2 R2, SNoCutP L1 R1 → SNoCutP L2 R2 → (∀w ∈ L1, w < SNoCut L2 R2) → (∀z ∈ R1, SNoCut L2 R2 < z) → (∀w ∈ L2, w < SNoCut L1 R1) → (∀z ∈ R2, SNoCut L1 R1 < z) → SNoCut L1 R1 = SNoCut L2 R2
Proof:
Proof not loaded.
L12695
Theorem. (SNoLt_SNoL_or_SNoR_impred)
∀x y, SNo x → SNo y → x < y → ∀p : prop, (∀z ∈ SNoL y, z ∈ SNoR x → p) → (x ∈ SNoL y → p) → (y ∈ SNoR x → p) → p
Proof:
Proof not loaded.
L12717
Theorem. (SNoL_or_SNoR_impred)
∀x y, SNo x → SNo y → ∀p : prop, (x = y → p) → (∀z ∈ SNoL y, z ∈ SNoR x → p) → (x ∈ SNoL y → p) → (y ∈ SNoR x → p) → (∀z ∈ SNoR y, z ∈ SNoL x → p) → (x ∈ SNoR y → p) → (y ∈ SNoL x → p) → p
Proof:
Proof not loaded.
L12743
Theorem. (SNoL_SNoCutP_ex)
∀L R, SNoCutP L R → ∀w ∈ SNoL (SNoCut L R), ∃w' ∈ L, w ≤ w'
Proof:
Proof not loaded.
L12783
Theorem. (SNoR_SNoCutP_ex)
∀L R, SNoCutP L R → ∀z ∈ SNoR (SNoCut L R), ∃z' ∈ R, z' ≤ z
Proof:
Proof not loaded.
L12823
Theorem. (ordinal_SNo_)
∀alpha, ordinal alpha → SNo_ alpha alpha
Proof:
Proof not loaded.
L12846
Theorem. (ordinal_SNo)
∀alpha, ordinal alpha → SNo alpha
Proof:
Proof not loaded.
L12855
Theorem. (ordinal_SNoLev)
∀alpha, ordinal alpha → SNoLev alpha = alpha
Proof:
Proof not loaded.
L12864
Theorem. (ordinal_SNoLev_max)
∀alpha, ordinal alpha → ∀z, SNo z → SNoLev z ∈ alpha → z < alpha
Proof:
Proof not loaded.
L12911
Theorem. (ordinal_SNoL)
∀alpha, ordinal alpha → SNoL alpha = SNoS_ alpha
Proof:
Proof not loaded.
L12943
Theorem. (ordinal_SNoR)
∀alpha, ordinal alpha → SNoR alpha = Empty
Proof:
Proof not loaded.
L12965
Theorem. (nat_p_SNo)
∀n, nat_p n → SNo n
Proof:
Proof not loaded.
L12973
Theorem. (omega_SNo)
∀n ∈ ω, SNo n
Proof:
Proof not loaded.
L12980
Proof:
Proof not loaded.
L12988
Theorem. (ordinal_In_SNoLt)
∀alpha, ordinal alpha → ∀beta ∈ alpha, beta < alpha
Proof:
Proof not loaded.
L13004
Theorem. (ordinal_SNoLev_max_2)
∀alpha, ordinal alpha → ∀z, SNo z → SNoLev z ∈ ordsucc alpha → z ≤ alpha
Proof:
Proof not loaded.
L13083
Theorem. (ordinal_Subq_SNoLe)
∀alpha beta, ordinal alpha → ordinal beta → alpha ⊆ beta → alpha ≤ beta
Proof:
Proof not loaded.
L13105
Theorem. (ordinal_SNoLt_In)
∀alpha beta, ordinal alpha → ordinal beta → alpha < beta → alpha ∈ beta
Proof:
Proof not loaded.
L13118
Theorem. (omega_nonneg)
∀m ∈ ω, 0 ≤ m
Proof:
Proof not loaded.
L13124
Theorem. (SNo_0)
Proof:
Proof not loaded.
L13128
Theorem. (SNo_1)
Proof:
Proof not loaded.
L13132
Theorem. (SNo_2)
Proof:
Proof not loaded.
L13136
Theorem. (SNoLev_0)
Proof:
Proof not loaded.
L13140
Theorem. (SNoCut_0_0)
Proof:
Proof not loaded.
L13165
Theorem. (SNoL_0)
Proof:
Proof not loaded.
L13180
Theorem. (SNoR_0)
Proof:
Proof not loaded.
L13195
Theorem. (SNoL_1)
Proof:
Proof not loaded.
L13231
Theorem. (SNoR_1)
Proof:
Proof not loaded.
L13235
Theorem. (SNo_max_SNoLev)
∀x, SNo x → (∀y ∈ SNoS_ (SNoLev x), y < x) → SNoLev x = x
Proof:
Proof not loaded.
L13282
Theorem. (SNo_max_ordinal)
∀x, SNo x → (∀y ∈ SNoS_ (SNoLev x), y < x) → ordinal x
Proof:
Proof not loaded.
L13291
Theorem. (pos_low_eq_one)
∀x, SNo x → 0 < x → SNoLev x ⊆ 1 → x = 1
Proof:
Proof not loaded.
L13338
Definition. We define SNo_extend0 to be λx ⇒ PSNo (ordsucc (SNoLev x)) (λdelta ⇒ delta ∈ x ∧ delta ≠ SNoLev x) of type set → set.
L13340
Definition. We define SNo_extend1 to be λx ⇒ PSNo (ordsucc (SNoLev x)) (λdelta ⇒ delta ∈ x ∨ delta = SNoLev x) of type set → set.
L13341
Theorem. (SNo_extend0_SNo_)
∀x, SNo x → SNo_ (ordsucc (SNoLev x)) (SNo_extend0 x)
Proof:
Proof not loaded.
L13349
Theorem. (SNo_extend1_SNo_)
∀x, SNo x → SNo_ (ordsucc (SNoLev x)) (SNo_extend1 x)
Proof:
Proof not loaded.
L13357
Theorem. (SNo_extend0_SNo)
∀x, SNo x → SNo (SNo_extend0 x)
Proof:
Proof not loaded.
L13364
Theorem. (SNo_extend1_SNo)
∀x, SNo x → SNo (SNo_extend1 x)
Proof:
Proof not loaded.
L13371
Theorem. (SNo_extend0_SNoLev)
∀x, SNo x → SNoLev (SNo_extend0 x) = ordsucc (SNoLev x)
Proof:
Proof not loaded.
L13378
Theorem. (SNo_extend1_SNoLev)
∀x, SNo x → SNoLev (SNo_extend1 x) = ordsucc (SNoLev x)
Proof:
Proof not loaded.
L13385
Theorem. (SNo_extend0_nIn)
∀x, SNo x → SNoLev x ∉ SNo_extend0 x
Proof:
Proof not loaded.
L13408
Theorem. (SNo_extend1_In)
∀x, SNo x → SNoLev x ∈ SNo_extend1 x
Proof:
Proof not loaded.
L13420
Theorem. (SNo_extend0_SNoEq)
∀x, SNo x → SNoEq_ (SNoLev x) (SNo_extend0 x) x
Proof:
Proof not loaded.
L13444
Theorem. (SNo_extend1_SNoEq)
∀x, SNo x → SNoEq_ (SNoLev x) (SNo_extend1 x) x
Proof:
Proof not loaded.
L13468
Theorem. (SNoLev_0_eq_0)
∀x, SNo x → SNoLev x = 0 → x = 0
Proof:
Proof not loaded.
L13478
Definition. We define eps_ to be λn ⇒ {0} ∪ {(ordsucc m) '|m ∈ n} of type set → set.
L13481
Theorem. (eps_ordinal_In_eq_0)
∀n alpha, ordinal alpha → alpha ∈ eps_ n → alpha = 0
Proof:
Proof not loaded.
(*** eps_ n is the Surreal Number 1/2^n, without needing to define division or exponents first ***)
L13496
Theorem. (eps_0_1)
Proof:
Proof not loaded.
L13511
Theorem. (SNo__eps_)
∀n ∈ ω, SNo_ (ordsucc n) (eps_ n)
Proof:
Proof not loaded.
L13609
Theorem. (SNo_eps_)
∀n ∈ ω, SNo (eps_ n)
Proof:
Proof not loaded.
L13616
Theorem. (SNo_eps_1)
Proof:
Proof not loaded.
L13620
Theorem. (SNoLev_eps_)
Proof:
Proof not loaded.
L13627
Proof:
Proof not loaded.
L13634
Theorem. (SNo_eps_decr)
∀n ∈ ω, ∀m ∈ n, eps_ n < eps_ m
Proof:
Proof not loaded.
L13672
Theorem. (SNo_eps_pos)
∀n ∈ ω, 0 < eps_ n
Proof:
Proof not loaded.
L13689
Theorem. (SNo_pos_eps_Lt)
∀n, nat_p n → ∀x ∈ SNoS_ (ordsucc n), 0 < x → eps_ n < x
Proof:
Proof not loaded.
L13736
Theorem. (SNo_pos_eps_Le)
∀n, nat_p n → ∀x ∈ SNoS_ (ordsucc (ordsucc n)), 0 < x → eps_ n ≤ x
Proof:
Proof not loaded.
L13782
Theorem. (eps_SNo_eq)
∀n, nat_p n → ∀x ∈ SNoS_ (ordsucc n), 0 < x → SNoEq_ (SNoLev x) (eps_ n) x → ∃m ∈ n, x = eps_ m
Proof:
Proof not loaded.
L13840
Proof:
Proof not loaded.
L13867
Proof:
Proof not loaded.
End of Section TaggedSets2
L14047
Theorem. (SNo_etaE)
∀z, SNo z → ∀p : prop, (∀L R, SNoCutP L R → (∀x ∈ L, SNoLev x ∈ SNoLev z) → (∀y ∈ R, SNoLev y ∈ SNoLev z) → z = SNoCut L R → p) → p
Proof:
Proof not loaded.
L14158
Theorem. (SNo_ind)
∀P : set → prop, (∀L R, SNoCutP L R → (∀x ∈ L, P x) → (∀y ∈ R, P y) → P (SNoCut L R)) → ∀z, SNo z → P z
Proof:
Proof not loaded.
Beginning of Section SurrealRecI
L14211
Variable F : set → (set → set) → set
(*** surreal recursion ***)
L14212
Let default : set ≝ Eps_i (λ_ ⇒ True)
L14213
Let G : set → (set → set → set) → set → set ≝ λalpha g ⇒ If_ii (ordinal alpha) (λz : set ⇒ if z ∈ SNoS_ (ordsucc alpha) then F z (λw ⇒ g (SNoLev w) w) else default) (λz : set ⇒ default)
L14223
Definition. We define SNo_rec_i to be λz ⇒ In_rec_ii G (SNoLev z) z of type set → set.
L14225
Hypothesis Fr : ∀z, SNo z → ∀g h : set → set, (∀w ∈ SNoS_ (SNoLev z), g w = h w) → F z g = F z h
L14228
Theorem. (SNo_rec_i_eq)
∀z, SNo z → SNo_rec_i z = F z SNo_rec_i
Proof:
Proof not loaded.
End of Section SurrealRecI
Beginning of Section SurrealRecII
L14305
Variable F : set → (set → (set → set)) → (set → set)
L14306
Let default : (set → set) ≝ Descr_ii (λ_ ⇒ True)
L14307
Let G : set → (set → set → (set → set)) → set → (set → set) ≝ λalpha g ⇒ If_iii (ordinal alpha) (λz : set ⇒ If_ii (z ∈ SNoS_ (ordsucc alpha)) (F z (λw ⇒ g (SNoLev w) w)) default) (λz : set ⇒ default)
L14316
Definition. We define SNo_rec_ii to be λz ⇒ In_rec_iii G (SNoLev z) z of type set → (set → set).
L14318
Hypothesis Fr : ∀z, SNo z → ∀g h : set → (set → set), (∀w ∈ SNoS_ (SNoLev z), g w = h w) → F z g = F z h
L14321
Theorem. (SNo_rec_ii_eq)
∀z, SNo z → SNo_rec_ii z = F z SNo_rec_ii
Proof:
Proof not loaded.
End of Section SurrealRecII
Beginning of Section SurrealRec2
L14398
Variable F : set → set → (set → set → set) → set
L14399
Let G : set → (set → set → set) → set → (set → set) → set ≝ λw f z g ⇒ F w z (λx y ⇒ if x = w then g y else f x y)
L14401
Let H : set → (set → set → set) → set → set ≝ λw f z ⇒ if SNo z then SNo_rec_i (G w f) z else Empty
L14404
Definition. We define SNo_rec2 to be SNo_rec_ii H of type set → set → set.
L14406
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
L14411
Theorem. (SNo_rec2_G_prop)
∀w, SNo w → ∀f k : set → set → set, (∀x ∈ SNoS_ (SNoLev w), f x = k x) → ∀z, SNo z → ∀g h : set → set, (∀u ∈ SNoS_ (SNoLev z), g u = h u) → G w f z g = G w k z h
Proof:
Proof not loaded.
L14448
Theorem. (SNo_rec2_eq_1)
∀w, SNo w → ∀f : set → set → set, ∀z, SNo z → SNo_rec_i (G w f) z = G w f z (SNo_rec_i (G w f))
Proof:
Proof not loaded.
L14462
Theorem. (SNo_rec2_eq)
∀w, SNo w → ∀z, SNo z → SNo_rec2 w z = F w z SNo_rec2
Proof:
Proof not loaded.
End of Section SurrealRec2
L14559
Theorem. (SNo_ordinal_ind)
∀P : set → prop, (∀alpha, ordinal alpha → ∀x ∈ SNoS_ alpha, P x) → (∀x, SNo x → P x)
Proof:
Proof not loaded.
L14575
Theorem. (SNo_ordinal_ind2)
∀P : set → set → prop, (∀alpha, ordinal alpha → ∀beta, ordinal beta → ∀x ∈ SNoS_ alpha, ∀y ∈ SNoS_ beta, P x y) → (∀x y, SNo x → SNo y → P x y)
Proof:
Proof not loaded.
L14603
Theorem. (SNo_ordinal_ind3)
∀P : set → set → set → prop, (∀alpha, ordinal alpha → ∀beta, ordinal beta → ∀gamma, ordinal gamma → ∀x ∈ SNoS_ alpha, ∀y ∈ SNoS_ beta, ∀z ∈ SNoS_ gamma, P x y z) → (∀x y z, SNo x → SNo y → SNo z → P x y z)
Proof:
Proof not loaded.
L14640
Theorem. (SNoLev_ind)
∀P : set → prop, (∀x, SNo x → (∀w ∈ SNoS_ (SNoLev x), P w) → P x) → (∀x, SNo x → P x)
Proof:
Proof not loaded.
L14663
Theorem. (SNoLev_ind2)
∀P : set → set → prop, (∀x y, SNo x → SNo y → (∀w ∈ SNoS_ (SNoLev x), P w y) → (∀z ∈ SNoS_ (SNoLev y), P x z) → (∀w ∈ SNoS_ (SNoLev x), ∀z ∈ SNoS_ (SNoLev y), P w z) → P x y) → ∀x y, SNo x → SNo y → P x y
Proof:
Proof not loaded.
L14709
Theorem. (SNoLev_ind3)
∀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
Proof:
Proof not loaded.
L14788
Theorem. (SNo_omega)
Proof:
Proof not loaded.
L14792
Theorem. (SNoLt_0_1)
0 < 1
Proof:
Proof not loaded.
L14798
Theorem. (SNoLt_0_2)
0 < 2
Proof:
Proof not loaded.
L14804
Theorem. (SNoLt_1_2)
1 < 2
Proof:
Proof not loaded.
L14810
Theorem. (restr_SNo_)
∀x, SNo x → ∀alpha ∈ SNoLev x, SNo_ alpha (x ∩ SNoElts_ alpha)
Proof:
Proof not loaded.
L14850
Theorem. (restr_SNo)
∀x, SNo x → ∀alpha ∈ SNoLev x, SNo (x ∩ SNoElts_ alpha)
Proof:
Proof not loaded.
L14859
Theorem. (restr_SNoLev)
∀x, SNo x → ∀alpha ∈ SNoLev x, SNoLev (x ∩ SNoElts_ alpha) = alpha
Proof:
Proof not loaded.
L14868
Theorem. (restr_SNoEq)
∀x, SNo x → ∀alpha ∈ SNoLev x, SNoEq_ alpha (x ∩ SNoElts_ alpha) x
Proof:
Proof not loaded.
L14884
Theorem. (SNo_extend0_restr_eq)
∀x, SNo x → x = SNo_extend0 x ∩ SNoElts_ (SNoLev x)
Proof:
Proof not loaded.
L14909
Theorem. (SNo_extend1_restr_eq)
∀x, SNo x → x = SNo_extend1 x ∩ SNoElts_ (SNoLev x)
Proof:
Proof not loaded.
Beginning of Section SurrealMinus
L14939
Definition. We define minus_SNo to be SNo_rec_i (λx m ⇒ SNoCut {m z|z ∈ SNoR x} {m w|w ∈ SNoL x}) of type set → set.
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use ≤ as an infix operator with priority 490 and no associativity corresponding to applying term SNoLe.
L14944
Theorem. (minus_SNo_eq)
∀x, SNo x → - x = SNoCut {- z|z ∈ SNoR x} {- w|w ∈ SNoL x}
Proof:
Proof not loaded.
L14975
Theorem. (minus_SNo_prop1)
∀x, SNo x → SNo (- x) ∧ (∀u ∈ SNoL x, - x < - u) ∧ (∀u ∈ SNoR x, - u < - x) ∧ SNoCutP {- z|z ∈ SNoR x} {- w|w ∈ SNoL x}
Proof:
Proof not loaded.
L15166
Theorem. (SNo_minus_SNo)
∀x, SNo x → SNo (- x)
Proof:
Proof not loaded.
L15173
Theorem. (minus_SNo_Lt_contra)
∀x y, SNo x → SNo y → x < y → - y < - x
Proof:
Proof not loaded.
L15242
Theorem. (minus_SNo_Le_contra)
∀x y, SNo x → SNo y → x ≤ y → - y ≤ - x
Proof:
Proof not loaded.
L15260
Theorem. (minus_SNo_SNoCutP)
∀x, SNo x → SNoCutP {- z|z ∈ SNoR x} {- w|w ∈ SNoL x}
Proof:
Proof not loaded.
L15268
Theorem. (minus_SNo_SNoCutP_gen)
∀L R, SNoCutP L R → SNoCutP {- z|z ∈ R} {- w|w ∈ L}
Proof:
Proof not loaded.
L15319
Theorem. (minus_SNo_Lev_lem1)
∀alpha, ordinal alpha → ∀x ∈ SNoS_ alpha, SNoLev (- x) ⊆ SNoLev x
Proof:
Proof not loaded.
L15490
Theorem. (minus_SNo_Lev_lem2)
∀x, SNo x → SNoLev (- x) ⊆ SNoLev x
Proof:
Proof not loaded.
L15501
Theorem. (minus_SNo_invol)
∀x, SNo x → - - x = x
Proof:
Proof not loaded.
L15569
Theorem. (minus_SNo_Lev)
∀x, SNo x → SNoLev (- x) = SNoLev x
Proof:
Proof not loaded.
L15580
Theorem. (minus_SNo_SNo_)
∀alpha, ordinal alpha → ∀x, SNo_ alpha x → SNo_ alpha (- x)
Proof:
Proof not loaded.
L15597
Theorem. (minus_SNo_SNoS_)
∀alpha, ordinal alpha → ∀x, x ∈ SNoS_ alpha → - x ∈ SNoS_ alpha
Proof:
Proof not loaded.
L15610
Theorem. (minus_SNoCut_eq_lem)
∀v, SNo v → ∀L R, SNoCutP L R → v = SNoCut L R → - v = SNoCut {- z|z ∈ R} {- w|w ∈ L}
Proof:
Proof not loaded.
L15720
Theorem. (minus_SNoCut_eq)
∀L R, SNoCutP L R → - SNoCut L R = SNoCut {- z|z ∈ R} {- w|w ∈ L}
Proof:
Proof not loaded.
L15725
Theorem. (minus_SNo_Lt_contra1)
∀x y, SNo x → SNo y → - x < y → - y < x
Proof:
Proof not loaded.
L15738
Theorem. (minus_SNo_Lt_contra2)
∀x y, SNo x → SNo y → x < - y → y < - x
Proof:
Proof not loaded.
L15751
Theorem. (mordinal_SNoLev_min_2)
∀alpha, ordinal alpha → ∀z, SNo z → SNoLev z ∈ ordsucc alpha → - alpha ≤ z
Proof:
Proof not loaded.
L15767
Proof:
Proof not loaded.
L15783
Theorem. (SNoL_minus_SNoR)
∀x, SNo x → SNoL (- x) = {- w|w ∈ SNoR x}
Proof:
Proof not loaded.
End of Section SurrealMinus
Beginning of Section SurrealAdd
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
L15831
Definition. We define add_SNo to be SNo_rec2 (λx y a ⇒ SNoCut ({a w y|w ∈ SNoL x} ∪ {a x w|w ∈ SNoL y}) ({a z y|z ∈ SNoR x} ∪ {a x z|z ∈ SNoR y})) of type set → set → set.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
L15834
Theorem. (add_SNo_eq)
∀x, SNo x → ∀y, SNo y → x + y = SNoCut ({w + y|w ∈ SNoL x} ∪ {x + w|w ∈ SNoL y}) ({z + y|z ∈ SNoR x} ∪ {x + z|z ∈ SNoR y})
Proof:
Proof not loaded.
L15890
Theorem. (add_SNo_prop1)
∀x y, SNo x → SNo y → SNo (x + y) ∧ (∀u ∈ SNoL x, u + y < x + y) ∧ (∀u ∈ SNoR x, x + y < u + y) ∧ (∀u ∈ SNoL y, x + u < x + y) ∧ (∀u ∈ SNoR y, x + y < x + u) ∧ SNoCutP ({w + y|w ∈ SNoL x} ∪ {x + w|w ∈ SNoL y}) ({z + y|z ∈ SNoR x} ∪ {x + z|z ∈ SNoR y})
Proof:
Proof not loaded.
L16351
Theorem. (SNo_add_SNo)
∀x y, SNo x → SNo y → SNo (x + y)
Proof:
Proof not loaded.
L16361
Theorem. (SNo_add_SNo_3)
∀x y z, SNo x → SNo y → SNo z → SNo (x + y + z)
Proof:
Proof not loaded.
L16370
Theorem. (SNo_add_SNo_3c)
∀x y z, SNo x → SNo y → SNo z → SNo (x + y + - z)
Proof:
Proof not loaded.
L16378
Theorem. (SNo_add_SNo_4)
∀x y z w, SNo x → SNo y → SNo z → SNo w → SNo (x + y + z + w)
Proof:
Proof not loaded.
L16383
Theorem. (add_SNo_Lt1)
∀x y z, SNo x → SNo y → SNo z → x < z → x + y < z + y
Proof:
Proof not loaded.
L16448
Theorem. (add_SNo_Le1)
∀x y z, SNo x → SNo y → SNo z → x ≤ z → x + y ≤ z + y
Proof:
Proof not loaded.
L16460
Theorem. (add_SNo_Lt2)
∀x y z, SNo x → SNo y → SNo z → y < z → x + y < x + z
Proof:
Proof not loaded.
L16526
Theorem. (add_SNo_Le2)
∀x y z, SNo x → SNo y → SNo z → y ≤ z → x + y ≤ x + z
Proof:
Proof not loaded.
L16538
Theorem. (add_SNo_Lt3a)
∀x y z w, SNo x → SNo y → SNo z → SNo w → x < z → y ≤ w → x + y < z + w
Proof:
Proof not loaded.
L16551
Theorem. (add_SNo_Lt3b)
∀x y z w, SNo x → SNo y → SNo z → SNo w → x ≤ z → y < w → x + y < z + w
Proof:
Proof not loaded.
L16564
Theorem. (add_SNo_Lt3)
∀x y z w, SNo x → SNo y → SNo z → SNo w → x < z → y < w → x + y < z + w
Proof:
Proof not loaded.
L16579
Theorem. (add_SNo_Le3)
∀x y z w, SNo x → SNo y → SNo z → SNo w → x ≤ z → y ≤ w → x + y ≤ z + w
Proof:
Proof not loaded.
L16592
Theorem. (add_SNo_SNoCutP)
∀x y, SNo x → SNo y → SNoCutP ({w + y|w ∈ SNoL x} ∪ {x + w|w ∈ SNoL y}) ({z + y|z ∈ SNoR x} ∪ {x + z|z ∈ SNoR y})
Proof:
Proof not loaded.
L16600
Theorem. (add_SNo_com)
∀x y, SNo x → SNo y → x + y = y + x
Proof:
Proof not loaded.
L16701
Theorem. (add_SNo_0L)
∀x, SNo x → 0 + x = x
Proof:
Proof not loaded.
L16764
Theorem. (add_SNo_0R)
∀x, SNo x → x + 0 = x
Proof:
Proof not loaded.
L16770
Theorem. (add_SNo_minus_SNo_linv)
∀x, SNo x → - x + x = 0
Proof:
Proof not loaded.
L16945
Theorem. (add_SNo_minus_SNo_rinv)
∀x, SNo x → x + - x = 0
Proof:
Proof not loaded.
L16955
Theorem. (add_SNo_ordinal_SNoCutP)
∀alpha, ordinal alpha → ∀beta, ordinal beta → SNoCutP ({x + beta|x ∈ SNoS_ alpha} ∪ {alpha + x|x ∈ SNoS_ beta}) Empty
Proof:
Proof not loaded.
L16995
Theorem. (add_SNo_ordinal_eq)
∀alpha, ordinal alpha → ∀beta, ordinal beta → alpha + beta = SNoCut ({x + beta|x ∈ SNoS_ alpha} ∪ {alpha + x|x ∈ SNoS_ beta}) Empty
Proof:
Proof not loaded.
L17027
Theorem. (add_SNo_ordinal_ordinal)
∀alpha, ordinal alpha → ∀beta, ordinal beta → ordinal (alpha + beta)
Proof:
Proof not loaded.
L17092
Theorem. (add_SNo_ordinal_SL)
∀alpha, ordinal alpha → ∀beta, ordinal beta → ordsucc alpha + beta = ordsucc (alpha + beta)
Proof:
Proof not loaded.
L17244
Theorem. (add_SNo_ordinal_SR)
∀alpha, ordinal alpha → ∀beta, ordinal beta → alpha + ordsucc beta = ordsucc (alpha + beta)
Proof:
Proof not loaded.
L17265
Theorem. (add_SNo_ordinal_InL)
∀alpha, ordinal alpha → ∀beta, ordinal beta → ∀gamma ∈ alpha, gamma + beta ∈ alpha + beta
Proof:
Proof not loaded.
L17289
Theorem. (add_SNo_ordinal_InR)
∀alpha, ordinal alpha → ∀beta, ordinal beta → ∀gamma ∈ beta, alpha + gamma ∈ alpha + beta
Proof:
Proof not loaded.
L17306
Theorem. (add_nat_add_SNo)
∀n m ∈ ω, add_nat n m = n + m
Proof:
Proof not loaded.
L17335
Theorem. (add_SNo_In_omega)
∀n m ∈ ω, n + m ∈ ω
Proof:
Proof not loaded.
L17344
Theorem. (add_SNo_1_1_2)
1 + 1 = 2
Proof:
Proof not loaded.
L17349
Theorem. (add_SNo_SNoL_interpolate)
∀x y, SNo x → SNo y → ∀u ∈ SNoL (x + y), (∃v ∈ SNoL x, u ≤ v + y) ∨ (∃v ∈ SNoL y, u ≤ x + v)
Proof:
Proof not loaded.
L17506
Theorem. (add_SNo_SNoR_interpolate)
∀x y, SNo x → SNo y → ∀u ∈ SNoR (x + y), (∃v ∈ SNoR x, v + y ≤ u) ∨ (∃v ∈ SNoR y, x + v ≤ u)
Proof:
Proof not loaded.
L17663
Theorem. (add_SNo_assoc)
∀x y z, SNo x → SNo y → SNo z → x + (y + z) = (x + y) + z
Proof:
Proof not loaded.
L18079
Theorem. (add_SNo_minus_R2)
∀x y, SNo x → SNo y → (x + y) + - y = x
Proof:
Proof not loaded.
L18088
Theorem. (add_SNo_minus_R2')
∀x y, SNo x → SNo y → (x + - y) + y = x
Proof:
Proof not loaded.
L18094
Theorem. (add_SNo_minus_L2)
∀x y, SNo x → SNo y → - x + (x + y) = y
Proof:
Proof not loaded.
L18103
Theorem. (add_SNo_minus_L2')
∀x y, SNo x → SNo y → x + (- x + y) = y
Proof:
Proof not loaded.
L18109
Theorem. (add_SNo_cancel_L)
∀x y z, SNo x → SNo y → SNo z → x + y = x + z → y = z
Proof:
Proof not loaded.
L18122
Theorem. (add_SNo_cancel_R)
∀x y z, SNo x → SNo y → SNo z → x + y = z + y → x = z
Proof:
Proof not loaded.
L18136
Theorem. (minus_SNo_0)
- 0 = 0
Proof:
Proof not loaded.
L18144
Theorem. (minus_add_SNo_distr)
∀x y, SNo x → SNo y → - (x + y) = (- x) + (- y)
Proof:
Proof not loaded.
L18174
Theorem. (minus_add_SNo_distr_3)
∀x y z, SNo x → SNo y → SNo z → - (x + y + z) = - x + - y + - z
Proof:
Proof not loaded.
L18182
Theorem. (add_SNo_Lev_bd)
∀x y, SNo x → SNo y → SNoLev (x + y) ⊆ SNoLev x + SNoLev y
Proof:
Proof not loaded.
L18546
Theorem. (add_SNo_SNoS_omega)
∀x y ∈ SNoS_ ω, x + y ∈ SNoS_ ω
Proof:
Proof not loaded.
L18576
Theorem. (add_SNo_Lt1_cancel)
∀x y z, SNo x → SNo y → SNo z → x + y < z + y → x < z
Proof:
Proof not loaded.
L18592
Theorem. (add_SNo_Lt2_cancel)
∀x y z, SNo x → SNo y → SNo z → x + y < x + z → y < z
Proof:
Proof not loaded.
L18599
Theorem. (add_SNo_Le1_cancel)
∀x y z, SNo x → SNo y → SNo z → x + y ≤ z + y → x ≤ z
Proof:
Proof not loaded.
L18615
Theorem. (add_SNo_assoc_4)
∀x y z w, SNo x → SNo y → SNo z → SNo w → x + y + z + w = (x + y + z) + w
Proof:
Proof not loaded.
L18625
Theorem. (add_SNo_com_3_0_1)
∀x y z, SNo x → SNo y → SNo z → x + y + z = y + x + z
Proof:
Proof not loaded.
L18635
Theorem. (add_SNo_com_3b_1_2)
∀x y z, SNo x → SNo y → SNo z → (x + y) + z = (x + z) + y
Proof:
Proof not loaded.
L18645
Theorem. (add_SNo_com_4_inner_mid)
∀x y z w, SNo x → SNo y → SNo z → SNo w → (x + y) + (z + w) = (x + z) + (y + w)
Proof:
Proof not loaded.
L18657
Theorem. (add_SNo_rotate_3_1)
∀x y z, SNo x → SNo y → SNo z → x + y + z = z + x + y
Proof:
Proof not loaded.
L18671
Theorem. (add_SNo_rotate_4_1)
∀x y z w, SNo x → SNo y → SNo z → SNo w → x + y + z + w = w + x + y + z
Proof:
Proof not loaded.
L18679
Theorem. (add_SNo_rotate_5_1)
∀x y z w v, SNo x → SNo y → SNo z → SNo w → SNo v → x + y + z + w + v = v + x + y + z + w
Proof:
Proof not loaded.
L18687
Theorem. (add_SNo_rotate_5_2)
∀x y z w v, SNo x → SNo y → SNo z → SNo w → SNo v → x + y + z + w + v = w + v + x + y + z
Proof:
Proof not loaded.
L18695
Theorem. (add_SNo_minus_SNo_prop2)
∀x y, SNo x → SNo y → x + - x + y = y
Proof:
Proof not loaded.
L18704
Theorem. (add_SNo_minus_SNo_prop3)
∀x y z w, SNo x → SNo y → SNo z → SNo w → (x + y + z) + (- z + w) = x + y + w
Proof:
Proof not loaded.
L18715
Theorem. (add_SNo_minus_SNo_prop5)
∀x y z w, SNo x → SNo y → SNo z → SNo w → (x + y + - z) + (z + w) = x + y + w
Proof:
Proof not loaded.
L18723
Theorem. (add_SNo_minus_Lt1)
∀x y z, SNo x → SNo y → SNo z → x + - y < z → x < z + y
Proof:
Proof not loaded.
L18733
Theorem. (add_SNo_minus_Lt2)
∀x y z, SNo x → SNo y → SNo z → z < x + - y → z + y < x
Proof:
Proof not loaded.
L18744
Theorem. (add_SNo_minus_Lt1b)
∀x y z, SNo x → SNo y → SNo z → x < z + y → x + - y < z
Proof:
Proof not loaded.
L18754
Theorem. (add_SNo_minus_Lt2b)
∀x y z, SNo x → SNo y → SNo z → z + y < x → z < x + - y
Proof:
Proof not loaded.
L18764
Theorem. (add_SNo_minus_Lt1b3)
∀x y z w, SNo x → SNo y → SNo z → SNo w → x + y < w + z → x + y + - z < w
Proof:
Proof not loaded.
L18773
Theorem. (add_SNo_minus_Lt2b3)
∀x y z w, SNo x → SNo y → SNo z → SNo w → w + z < x + y → w < x + y + - z
Proof:
Proof not loaded.
L18782
Theorem. (add_SNo_minus_Lt_lem)
∀x y z u v w, SNo x → SNo y → SNo z → SNo u → SNo v → SNo w → x + y + w < u + v + z → x + y + - z < u + v + - w
Proof:
Proof not loaded.
L18812
Theorem. (add_SNo_minus_Le2)
∀x y z, SNo x → SNo y → SNo z → z ≤ x + - y → z + y ≤ x
Proof:
Proof not loaded.
L18825
Theorem. (add_SNo_minus_Le2b)
∀x y z, SNo x → SNo y → SNo z → z + y ≤ x → z ≤ x + - y
Proof:
Proof not loaded.
L18838
Theorem. (add_SNo_Lt_subprop2)
∀x y z w u v, SNo x → SNo y → SNo z → SNo w → SNo u → SNo v → x + u < z + v → y + v < w + u → x + y < z + w
Proof:
Proof not loaded.
L18869
Theorem. (add_SNo_Lt_subprop3a)
∀x y z w u a, SNo x → SNo y → SNo z → SNo w → SNo u → SNo a → x + z < w + a → y + a < u → x + y + z < w + u
Proof:
Proof not loaded.
L18892
Theorem. (add_SNo_Lt_subprop3b)
∀x y w u v a, SNo x → SNo y → SNo w → SNo u → SNo v → SNo a → x + a < w + v → y < a + u → x + y < w + u + v
Proof:
Proof not loaded.
L18909
Theorem. (add_SNo_Lt_subprop3c)
∀x y z w u a b c, SNo x → SNo y → SNo z → SNo w → SNo u → SNo a → SNo b → SNo c → x + a < b + c → y + c < u → b + z < w + a → x + y + z < w + u
Proof:
Proof not loaded.
L18943
Theorem. (add_SNo_Lt_subprop3d)
∀x y w u v a b c, SNo x → SNo y → SNo w → SNo u → SNo v → SNo a → SNo b → SNo c → x + a < b + v → y < c + u → b + c < w + a → x + y < w + u + v
Proof:
Proof not loaded.
L19003
Theorem. (ordinal_ordsucc_SNo_eq)
∀alpha, ordinal alpha → ordsucc alpha = 1 + alpha
Proof:
Proof not loaded.
L19011
Theorem. (add_SNo_3a_2b)
∀x y z w u, SNo x → SNo y → SNo z → SNo w → SNo u → (x + y + z) + (w + u) = (u + y + z) + (w + x)
Proof:
Proof not loaded.
L19024
Theorem. (add_SNo_1_ordsucc)
∀n ∈ ω, n + 1 = ordsucc n
Proof:
Proof not loaded.
L19034
Theorem. (add_SNo_eps_Lt)
∀x, SNo x → ∀n ∈ ω, x < x + eps_ n
Proof:
Proof not loaded.
L19042
Theorem. (add_SNo_eps_Lt')
∀x y, SNo x → SNo y → ∀n ∈ ω, x < y → x < y + eps_ n
Proof:
Proof not loaded.
L19050
Theorem. (SNoLt_minus_pos)
∀x y, SNo x → SNo y → x < y → 0 < y + - x
Proof:
Proof not loaded.
L19057
Theorem. (add_SNo_omega_In_cases)
∀m, ∀n ∈ ω, ∀k, nat_p k → m ∈ n + k → m ∈ n ∨ m + - n ∈ k
Proof:
Proof not loaded.
L19083
Theorem. (add_SNo_Lt4)
∀x y z w u v, SNo x → SNo y → SNo z → SNo w → SNo u → SNo v → x < w → y < u → z < v → x + y + z < w + u + v
Proof:
Proof not loaded.
L19092
Theorem. (add_SNo_3_3_3_Lt1)
∀x y z w u, SNo x → SNo y → SNo z → SNo w → SNo u → x + y < z + w → x + y + u < z + w + u
Proof:
Proof not loaded.
L19101
Theorem. (add_SNo_3_2_3_Lt1)
∀x y z w u, SNo x → SNo y → SNo z → SNo w → SNo u → y + x < z + w → x + u + y < z + w + u
Proof:
Proof not loaded.
L19109
Theorem. (add_SNo_minus_Lt12b3)
∀x y z w u v, SNo x → SNo y → SNo z → SNo w → SNo u → SNo v → x + y + v < w + u + z → x + y + - z < w + u + - v
Proof:
Proof not loaded.
L19132
Theorem. (add_SNo_minus_Le1b)
∀x y z, SNo x → SNo y → SNo z → x ≤ z + y → x + - y ≤ z
Proof:
Proof not loaded.
L19142
Theorem. (add_SNo_minus_Le1b3)
∀x y z w, SNo x → SNo y → SNo z → SNo w → x + y ≤ w + z → x + y + - z ≤ w
Proof:
Proof not loaded.
L19151
Theorem. (add_SNo_minus_Le12b3)
∀x y z w u v, SNo x → SNo y → SNo z → SNo w → SNo u → SNo v → x + y + v ≤ w + u + z → x + y + - z ≤ w + u + - v
Proof:
Proof not loaded.
End of Section SurrealAdd
Beginning of Section SurrealAbs
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
L19184
Definition. We define abs_SNo to be λx ⇒ if 0 ≤ x then x else - x of type set → set.
L19185
Theorem. (nonneg_abs_SNo)
∀x, 0 ≤ x → abs_SNo x = x
Proof:
Proof not loaded.
L19190
Theorem. (not_nonneg_abs_SNo)
∀x, ¬ (0 ≤ x) → abs_SNo x = - x
Proof:
Proof not loaded.
L19195
Theorem. (pos_abs_SNo)
∀x, 0 < x → abs_SNo x = x
Proof:
Proof not loaded.
L19201
Theorem. (neg_abs_SNo)
∀x, SNo x → x < 0 → abs_SNo x = - x
Proof:
Proof not loaded.
L19211
Theorem. (SNo_abs_SNo)
∀x, SNo x → SNo (abs_SNo x)
Proof:
Proof not loaded.
L19219
Theorem. (abs_SNo_minus)
∀x, SNo x → abs_SNo (- x) = abs_SNo x
Proof:
Proof not loaded.
L19251
Theorem. (abs_SNo_dist_swap)
∀x y, SNo x → SNo y → abs_SNo (x + - y) = abs_SNo (y + - x)
Proof:
Proof not loaded.
End of Section SurrealAbs
Beginning of Section SurrealMul
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
L19278
Definition. We define mul_SNo to be SNo_rec2 (λx y m ⇒ SNoCut ({m (w 0) y + m x (w 1) + - m (w 0) (w 1)|w ∈ SNoL x ⨯ SNoL y} ∪ {m (z 0) y + m x (z 1) + - m (z 0) (z 1)|z ∈ SNoR x ⨯ SNoR y}) ({m (w 0) y + m x (w 1) + - m (w 0) (w 1)|w ∈ SNoL x ⨯ SNoR y} ∪ {m (z 0) y + m x (z 1) + - m (z 0) (z 1)|z ∈ SNoR x ⨯ SNoL y})) of type set → set → set.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
L19289
Theorem. (mul_SNo_eq)
∀x, SNo x → ∀y, SNo y → x * y = SNoCut ({(w 0) * y + x * (w 1) + - (w 0) * (w 1)|w ∈ SNoL x ⨯ SNoL y} ∪ {(z 0) * y + x * (z 1) + - (z 0) * (z 1)|z ∈ SNoR x ⨯ SNoR y}) ({(w 0) * y + x * (w 1) + - (w 0) * (w 1)|w ∈ SNoL x ⨯ SNoR y} ∪ {(z 0) * y + x * (z 1) + - (z 0) * (z 1)|z ∈ SNoR x ⨯ SNoL y})
Proof:
Proof not loaded.
L19449
Theorem. (mul_SNo_eq_2)
∀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
Proof:
Proof not loaded.
L19565
Theorem. (mul_SNo_prop_1)
∀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
Proof:
Proof not loaded.
L20606
Theorem. (SNo_mul_SNo)
∀x y, SNo x → SNo y → SNo (x * y)
Proof:
Proof not loaded.
L20611
Theorem. (SNo_mul_SNo_lem)
∀x y u v, SNo x → SNo y → SNo u → SNo v → SNo (u * y + x * v + - (u * v))
Proof:
Proof not loaded.
L20625
Theorem. (SNo_mul_SNo_3)
∀x y z, SNo x → SNo y → SNo z → SNo (x * y * z)
Proof:
Proof not loaded.
L20634
Theorem. (mul_SNo_eq_3)
∀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
Proof:
Proof not loaded.
L20875
Theorem. (mul_SNo_Lt)
∀x y u v, SNo x → SNo y → SNo u → SNo v → u < x → v < y → u * y + x * v < x * y + u * v
Proof:
Proof not loaded.
L21231
Theorem. (mul_SNo_Le)
∀x y u v, SNo x → SNo y → SNo u → SNo v → u ≤ x → v ≤ y → u * y + x * v ≤ x * y + u * v
Proof:
Proof not loaded.
L21250
Theorem. (mul_SNo_SNoL_interpolate)
∀x y, SNo x → SNo y → ∀u ∈ SNoL (x * y), (∃v ∈ SNoL x, ∃w ∈ SNoL y, u + v * w ≤ v * y + x * w) ∨ (∃v ∈ SNoR x, ∃w ∈ SNoR y, u + v * w ≤ v * y + x * w)
Proof:
Proof not loaded.
L21432
Theorem. (mul_SNo_SNoL_interpolate_impred)
∀x y, SNo x → SNo y → ∀u ∈ SNoL (x * y), ∀p : prop, (∀v ∈ SNoL x, ∀w ∈ SNoL y, u + v * w ≤ v * y + x * w → p) → (∀v ∈ SNoR x, ∀w ∈ SNoR y, u + v * w ≤ v * y + x * w → p) → p
Proof:
Proof not loaded.
L21454
Theorem. (mul_SNo_SNoR_interpolate)
∀x y, SNo x → SNo y → ∀u ∈ SNoR (x * y), (∃v ∈ SNoL x, ∃w ∈ SNoR y, v * y + x * w ≤ u + v * w) ∨ (∃v ∈ SNoR x, ∃w ∈ SNoL y, v * y + x * w ≤ u + v * w)
Proof:
Proof not loaded.
L21636
Theorem. (mul_SNo_SNoR_interpolate_impred)
∀x y, SNo x → SNo y → ∀u ∈ SNoR (x * y), ∀p : prop, (∀v ∈ SNoL x, ∀w ∈ SNoR y, v * y + x * w ≤ u + v * w → p) → (∀v ∈ SNoR x, ∀w ∈ SNoL y, v * y + x * w ≤ u + v * w → p) → p
Proof:
Proof not loaded.
L21658
Theorem. (mul_SNo_Subq_lem)
∀x y X Y Z W, ∀U U', (∀u, u ∈ U → (∀q : prop, (∀w0 ∈ X, ∀w1 ∈ Y, u = w0 * y + x * w1 + - w0 * w1 → q) → (∀z0 ∈ Z, ∀z1 ∈ W, u = z0 * y + x * z1 + - z0 * z1 → q) → q)) → (∀w0 ∈ X, ∀w1 ∈ Y, w0 * y + x * w1 + - w0 * w1 ∈ U') → (∀w0 ∈ Z, ∀w1 ∈ W, w0 * y + x * w1 + - w0 * w1 ∈ U') → U ⊆ U'
Proof:
Proof not loaded.
L21681
Theorem. (mul_SNo_zeroR)
∀x, SNo x → x * 0 = 0
Proof:
Proof not loaded.
L21723
Theorem. (mul_SNo_oneR)
∀x, SNo x → x * 1 = x
Proof:
Proof not loaded.
L21851
Theorem. (mul_SNo_com)
∀x y, SNo x → SNo y → x * y = y * x
Proof:
Proof not loaded.
L22010
Theorem. (mul_SNo_minus_distrL)
∀x y, SNo x → SNo y → (- x) * y = - x * y
Proof:
Proof not loaded.
L22402
Theorem. (mul_SNo_minus_distrR)
∀x y, SNo x → SNo y → x * (- y) = - (x * y)
Proof:
Proof not loaded.
L22409
Theorem. (mul_SNo_distrR)
∀x y z, SNo x → SNo y → SNo z → (x + y) * z = x * z + y * z
Proof:
Proof not loaded.
L23722
Theorem. (mul_SNo_distrL)
∀x y z, SNo x → SNo y → SNo z → x * (y + z) = x * y + x * z
Proof:
Proof not loaded.
Beginning of Section mul_SNo_assoc_lems
L23737
Variable M : set → set → set
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term M.
L23739
Hypothesis SNo_M : ∀x y, SNo x → SNo y → SNo (x * y)
L23740
Hypothesis DL : ∀x y z, SNo x → SNo y → SNo z → x * (y + z) = x * y + x * z
L23741
Hypothesis DR : ∀x y z, SNo x → SNo y → SNo z → (x + y) * z = x * z + y * z
L23742
Hypothesis IL : ∀x y, SNo x → SNo y → ∀u ∈ SNoL (x * y), ∀p : prop, (∀v ∈ SNoL x, ∀w ∈ SNoL y, u + v * w ≤ v * y + x * w → p) → (∀v ∈ SNoR x, ∀w ∈ SNoR y, u + v * w ≤ v * y + x * w → p) → p
L23747
Hypothesis IR : ∀x y, SNo x → SNo y → ∀u ∈ SNoR (x * y), ∀p : prop, (∀v ∈ SNoL x, ∀w ∈ SNoR y, v * y + x * w ≤ u + v * w → p) → (∀v ∈ SNoR x, ∀w ∈ SNoL y, v * y + x * w ≤ u + v * w → p) → p
L23752
Hypothesis M_Lt : ∀x y u v, SNo x → SNo y → SNo u → SNo v → u < x → v < y → u * y + x * v < x * y + u * v
L23754
Hypothesis M_Le : ∀x y u v, SNo x → SNo y → SNo u → SNo v → u ≤ x → v ≤ y → u * y + x * v ≤ x * y + u * v
L23756
Theorem. (mul_SNo_assoc_lem1)
∀x y z, SNo x → SNo y → SNo z → (∀u ∈ SNoS_ (SNoLev x), u * (y * z) = (u * y) * z) → (∀v ∈ SNoS_ (SNoLev y), x * (v * z) = (x * v) * z) → (∀w ∈ SNoS_ (SNoLev z), x * (y * w) = (x * y) * w) → (∀u ∈ SNoS_ (SNoLev x), ∀v ∈ SNoS_ (SNoLev y), u * (v * z) = (u * v) * z) → (∀u ∈ SNoS_ (SNoLev x), ∀w ∈ SNoS_ (SNoLev z), u * (y * w) = (u * y) * w) → (∀v ∈ SNoS_ (SNoLev y), ∀w ∈ SNoS_ (SNoLev z), x * (v * w) = (x * v) * w) → (∀u ∈ SNoS_ (SNoLev x), ∀v ∈ SNoS_ (SNoLev y), ∀w ∈ SNoS_ (SNoLev z), u * (v * w) = (u * v) * w) → ∀L, (∀u ∈ L, ∀q : prop, (∀v ∈ SNoL x, ∀w ∈ SNoL (y * z), u = v * (y * z) + x * w + - v * w → q) → (∀v ∈ SNoR x, ∀w ∈ SNoR (y * z), u = v * (y * z) + x * w + - v * w → q) → q) → ∀u ∈ L, u < (x * y) * z
Proof:
Proof not loaded.
L24216
Theorem. (mul_SNo_assoc_lem2)
∀x y z, SNo x → SNo y → SNo z → (∀u ∈ SNoS_ (SNoLev x), u * (y * z) = (u * y) * z) → (∀v ∈ SNoS_ (SNoLev y), x * (v * z) = (x * v) * z) → (∀w ∈ SNoS_ (SNoLev z), x * (y * w) = (x * y) * w) → (∀u ∈ SNoS_ (SNoLev x), ∀v ∈ SNoS_ (SNoLev y), u * (v * z) = (u * v) * z) → (∀u ∈ SNoS_ (SNoLev x), ∀w ∈ SNoS_ (SNoLev z), u * (y * w) = (u * y) * w) → (∀v ∈ SNoS_ (SNoLev y), ∀w ∈ SNoS_ (SNoLev z), x * (v * w) = (x * v) * w) → (∀u ∈ SNoS_ (SNoLev x), ∀v ∈ SNoS_ (SNoLev y), ∀w ∈ SNoS_ (SNoLev z), u * (v * w) = (u * v) * w) → ∀R, (∀u ∈ R, ∀q : prop, (∀v ∈ SNoL x, ∀w ∈ SNoR (y * z), u = v * (y * z) + x * w + - v * w → q) → (∀v ∈ SNoR x, ∀w ∈ SNoL (y * z), u = v * (y * z) + x * w + - v * w → q) → q) → ∀u ∈ R, (x * y) * z < u
Proof:
Proof not loaded.
End of Section mul_SNo_assoc_lems
L24701
Theorem. (mul_SNo_assoc)
∀x y z, SNo x → SNo y → SNo z → x * (y * z) = (x * y) * z
Proof:
Proof not loaded.
L24916
Theorem. (mul_nat_mul_SNo)
∀n m ∈ ω, mul_nat n m = n * m
Proof:
Proof not loaded.
L24958
Theorem. (mul_SNo_In_omega)
∀n m ∈ ω, n * m ∈ ω
Proof:
Proof not loaded.
L24964
Theorem. (mul_SNo_zeroL)
∀x, SNo x → 0 * x = 0
Proof:
Proof not loaded.
L24970
Theorem. (mul_SNo_oneL)
∀x, SNo x → 1 * x = x
Proof:
Proof not loaded.
L24976
Theorem. (mul_SNo_rotate_3_1)
∀x y z, SNo x → SNo y → SNo z → x * y * z = z * x * y
Proof:
Proof not loaded.
L24990
Theorem. (pos_mul_SNo_Lt)
∀x y z, SNo x → 0 < x → SNo y → SNo z → y < z → x * y < x * z
Proof:
Proof not loaded.
L25008
Theorem. (nonneg_mul_SNo_Le)
∀x y z, SNo x → 0 ≤ x → SNo y → SNo z → y ≤ z → x * y ≤ x * z
Proof:
Proof not loaded.
L25026
Theorem. (neg_mul_SNo_Lt)
∀x y z, SNo x → x < 0 → SNo y → SNo z → z < y → x * y < x * z
Proof:
Proof not loaded.
L25044
Theorem. (pos_mul_SNo_Lt')
∀x y z, SNo x → SNo y → SNo z → 0 < z → x < y → x * z < y * z
Proof:
Proof not loaded.
L25051
Theorem. (mul_SNo_Lt1_pos_Lt)
∀x y, SNo x → SNo y → x < 1 → 0 < y → x * y < y
Proof:
Proof not loaded.
L25058
Theorem. (nonneg_mul_SNo_Le')
∀x y z, SNo x → SNo y → SNo z → 0 ≤ z → x ≤ y → x * z ≤ y * z
Proof:
Proof not loaded.
L25065
Theorem. (mul_SNo_Le1_nonneg_Le)
∀x y, SNo x → SNo y → x ≤ 1 → 0 ≤ y → x * y ≤ y
Proof:
Proof not loaded.
L25072
Theorem. (pos_mul_SNo_Lt2)
∀x y z w, SNo x → SNo y → SNo z → SNo w → 0 < x → 0 < y → x < z → y < w → x * y < z * w
Proof:
Proof not loaded.
L25087
Theorem. (nonneg_mul_SNo_Le2)
∀x y z w, SNo x → SNo y → SNo z → SNo w → 0 ≤ x → 0 ≤ y → x ≤ z → y ≤ w → x * y ≤ z * w
Proof:
Proof not loaded.
L25102
Theorem. (mul_SNo_pos_pos)
∀x y, SNo x → SNo y → 0 < x → 0 < y → 0 < x * y
Proof:
Proof not loaded.
L25118
Theorem. (mul_SNo_pos_neg)
∀x y, SNo x → SNo y → 0 < x → y < 0 → x * y < 0
Proof:
Proof not loaded.
L25132
Theorem. (mul_SNo_neg_pos)
∀x y, SNo x → SNo y → x < 0 → 0 < y → x * y < 0
Proof:
Proof not loaded.
L25146
Theorem. (mul_SNo_neg_neg)
∀x y, SNo x → SNo y → x < 0 → y < 0 → 0 < x * y
Proof:
Proof not loaded.
L25162
Theorem. (mul_SNo_nonneg_nonneg)
∀x y, SNo x → SNo y → 0 ≤ x → 0 ≤ y → 0 ≤ x * y
Proof:
Proof not loaded.
L25178
Theorem. (mul_SNo_nonpos_pos)
∀x y, SNo x → SNo y → x ≤ 0 → 0 < y → x * y ≤ 0
Proof:
Proof not loaded.
L25195
Theorem. (mul_SNo_nonpos_neg)
∀x y, SNo x → SNo y → x ≤ 0 → y < 0 → 0 ≤ x * y
Proof:
Proof not loaded.
L25212
Theorem. (nonpos_mul_SNo_Le)
∀x y z, SNo x → x ≤ 0 → SNo y → SNo z → z ≤ y → x * y ≤ x * z
Proof:
Proof not loaded.
L25240
Theorem. (SNo_zero_or_sqr_pos)
∀x, SNo x → x = 0 ∨ 0 < x * x
Proof:
Proof not loaded.
L25258
Theorem. (SNo_pos_sqr_uniq)
∀x y, SNo x → SNo y → 0 < x → 0 < y → x * x = y * y → x = y
Proof:
Proof not loaded.
L25277
Theorem. (SNo_nonneg_sqr_uniq)
∀x y, SNo x → SNo y → 0 ≤ x → 0 ≤ y → x * x = y * y → x = y
Proof:
Proof not loaded.
L25302
Theorem. (SNo_foil)
∀x y z w, SNo x → SNo y → SNo z → SNo w → (x + y) * (z + w) = x * z + x * w + y * z + y * w
Proof:
Proof not loaded.
L25328
Theorem. (mul_SNo_minus_minus)
∀x y, SNo x → SNo y → (- x) * (- y) = x * y
Proof:
Proof not loaded.
L25337
Theorem. (mul_SNo_com_3_0_1)
∀x y z, SNo x → SNo y → SNo z → x * y * z = y * x * z
Proof:
Proof not loaded.
L25347
Theorem. (mul_SNo_com_3b_1_2)
∀x y z, SNo x → SNo y → SNo z → (x * y) * z = (x * z) * y
Proof:
Proof not loaded.
L25357
Theorem. (mul_SNo_com_4_inner_mid)
∀x y z w, SNo x → SNo y → SNo z → SNo w → (x * y) * (z * w) = (x * z) * (y * w)
Proof:
Proof not loaded.
L25369
Theorem. (SNo_foil_mm)
∀x y z w, SNo x → SNo y → SNo z → SNo w → (x + - y) * (z + - w) = x * z + - x * w + - y * z + y * w
Proof:
Proof not loaded.
L25384
Theorem. (mul_SNo_nonzero_cancel)
∀x y z, SNo x → x ≠ 0 → SNo y → SNo z → x * y = x * z → y = z
Proof:
Proof not loaded.
L25420
Theorem. (mul_SNoCutP_lem)
∀Lx Rx Ly Ry x y, SNoCutP Lx Rx → SNoCutP Ly Ry → x = SNoCut Lx Rx → y = SNoCut Ly Ry → SNoCutP ({w 0 * y + x * w 1 + - w 0 * w 1|w ∈ Lx ⨯ Ly} ∪ {z 0 * y + x * z 1 + - z 0 * z 1|z ∈ Rx ⨯ Ry}) ({w 0 * y + x * w 1 + - w 0 * w 1|w ∈ Lx ⨯ Ry} ∪ {z 0 * y + x * z 1 + - z 0 * z 1|z ∈ Rx ⨯ Ly}) ∧ x * y = SNoCut ({w 0 * y + x * w 1 + - w 0 * w 1|w ∈ Lx ⨯ Ly} ∪ {z 0 * y + x * z 1 + - z 0 * z 1|z ∈ Rx ⨯ Ry}) ({w 0 * y + x * w 1 + - w 0 * w 1|w ∈ Lx ⨯ Ry} ∪ {z 0 * y + x * z 1 + - z 0 * z 1|z ∈ Rx ⨯ Ly}) ∧ ∀q : prop, (∀LxLy' RxRy' LxRy' RxLy', (∀u ∈ LxLy', ∀p : prop, (∀w ∈ Lx, ∀w' ∈ Ly, SNo w → SNo w' → w < x → w' < y → u = w * y + x * w' + - w * w' → p) → p) → (∀w ∈ Lx, ∀w' ∈ Ly, w * y + x * w' + - w * w' ∈ LxLy') → (∀u ∈ RxRy', ∀p : prop, (∀z ∈ Rx, ∀z' ∈ Ry, SNo z → SNo z' → x < z → y < z' → u = z * y + x * z' + - z * z' → p) → p) → (∀z ∈ Rx, ∀z' ∈ Ry, z * y + x * z' + - z * z' ∈ RxRy') → (∀u ∈ LxRy', ∀p : prop, (∀w ∈ Lx, ∀z ∈ Ry, SNo w → SNo z → w < x → y < z → u = w * y + x * z + - w * z → p) → p) → (∀w ∈ Lx, ∀z ∈ Ry, w * y + x * z + - w * z ∈ LxRy') → (∀u ∈ RxLy', ∀p : prop, (∀z ∈ Rx, ∀w ∈ Ly, SNo z → SNo w → x < z → w < y → u = z * y + x * w + - z * w → p) → p) → (∀z ∈ Rx, ∀w ∈ Ly, z * y + x * w + - z * w ∈ RxLy') → SNoCutP (LxLy' ∪ RxRy') (LxRy' ∪ RxLy') → x * y = SNoCut (LxLy' ∪ RxRy') (LxRy' ∪ RxLy') → q) → q
Proof:
Proof not loaded.
L26713
Theorem. (mul_SNoCut_abs)
∀Lx Rx Ly Ry x y, SNoCutP Lx Rx → SNoCutP Ly Ry → x = SNoCut Lx Rx → y = SNoCut Ly Ry → ∀q : prop, (∀LxLy' RxRy' LxRy' RxLy', (∀u ∈ LxLy', ∀p : prop, (∀w ∈ Lx, ∀w' ∈ Ly, SNo w → SNo w' → w < x → w' < y → u = w * y + x * w' + - w * w' → p) → p) → (∀w ∈ Lx, ∀w' ∈ Ly, w * y + x * w' + - w * w' ∈ LxLy') → (∀u ∈ RxRy', ∀p : prop, (∀z ∈ Rx, ∀z' ∈ Ry, SNo z → SNo z' → x < z → y < z' → u = z * y + x * z' + - z * z' → p) → p) → (∀z ∈ Rx, ∀z' ∈ Ry, z * y + x * z' + - z * z' ∈ RxRy') → (∀u ∈ LxRy', ∀p : prop, (∀w ∈ Lx, ∀z ∈ Ry, SNo w → SNo z → w < x → y < z → u = w * y + x * z + - w * z → p) → p) → (∀w ∈ Lx, ∀z ∈ Ry, w * y + x * z + - w * z ∈ LxRy') → (∀u ∈ RxLy', ∀p : prop, (∀z ∈ Rx, ∀w ∈ Ly, SNo z → SNo w → x < z → w < y → u = z * y + x * w + - z * w → p) → p) → (∀z ∈ Rx, ∀w ∈ Ly, z * y + x * w + - z * w ∈ RxLy') → SNoCutP (LxLy' ∪ RxRy') (LxRy' ∪ RxLy') → x * y = SNoCut (LxLy' ∪ RxRy') (LxRy' ∪ RxLy') → q) → q
Proof:
Proof not loaded.
L26738
Theorem. (mul_SNo_SNoCut_SNoL_interpolate)
∀Lx Rx Ly Ry, SNoCutP Lx Rx → SNoCutP Ly Ry → ∀x y, x = SNoCut Lx Rx → y = SNoCut Ly Ry → ∀u ∈ SNoL (x * y), (∃v ∈ Lx, ∃w ∈ Ly, u + v * w ≤ v * y + x * w) ∨ (∃v ∈ Rx, ∃w ∈ Ry, u + v * w ≤ v * y + x * w)
Proof:
Proof not loaded.
L26978
Theorem. (mul_SNo_SNoCut_SNoL_interpolate_impred)
∀Lx Rx Ly Ry, SNoCutP Lx Rx → SNoCutP Ly Ry → ∀x y, x = SNoCut Lx Rx → y = SNoCut Ly Ry → ∀u ∈ SNoL (x * y), ∀p : prop, (∀v ∈ Lx, ∀w ∈ Ly, u + v * w ≤ v * y + x * w → p) → (∀v ∈ Rx, ∀w ∈ Ry, u + v * w ≤ v * y + x * w → p) → p
Proof:
Proof not loaded.
L27004
Theorem. (mul_SNo_SNoCut_SNoR_interpolate)
∀Lx Rx Ly Ry, SNoCutP Lx Rx → SNoCutP Ly Ry → ∀x y, x = SNoCut Lx Rx → y = SNoCut Ly Ry → ∀u ∈ SNoR (x * y), (∃v ∈ Lx, ∃w ∈ Ry, v * y + x * w ≤ u + v * w) ∨ (∃v ∈ Rx, ∃w ∈ Ly, v * y + x * w ≤ u + v * w)
Proof:
Proof not loaded.
L27244
Theorem. (mul_SNo_SNoCut_SNoR_interpolate_impred)
∀Lx Rx Ly Ry, SNoCutP Lx Rx → SNoCutP Ly Ry → ∀x y, x = SNoCut Lx Rx → y = SNoCut Ly Ry → ∀u ∈ SNoR (x * y), ∀p : prop, (∀v ∈ Lx, ∀w ∈ Ry, v * y + x * w ≤ u + v * w → p) → (∀v ∈ Rx, ∀w ∈ Ly, v * y + x * w ≤ u + v * w → p) → p
Proof:
Proof not loaded.
L27270
Theorem. (nonpos_nonneg_0)
∀m n ∈ ω, m = - n → m = 0 ∧ n = 0
Proof:
Proof not loaded.
L27302
Theorem. (mul_minus_SNo_distrR)
∀x y, SNo x → SNo y → x * (- y) = - (x * y)
Proof:
Proof not loaded.
End of Section SurrealMul
Beginning of Section Int
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
L27322
Definition. We define int to be ω ∪ {- n|n ∈ ω} of type set.
L27324
Theorem. (int_SNo_cases)
∀p : set → prop, (∀n ∈ ω, p n) → (∀n ∈ ω, p (- n)) → ∀x ∈ int, p x
Proof:
Proof not loaded.
L27338
Theorem. (int_3_cases)
∀n ∈ int, ∀p : prop, (∀m ∈ ω, n = - ordsucc m → p) → (n = 0 → p) → (∀m ∈ ω, n = ordsucc m → p) → p
Proof:
Proof not loaded.
L27367
Theorem. (int_SNo)
∀x ∈ int, SNo x
Proof:
Proof not loaded.
L27375
Proof:
Proof not loaded.
L27382
Theorem. (int_minus_SNo_omega)
∀n ∈ ω, - n ∈ int
Proof:
Proof not loaded.
L27390
Theorem. (int_add_SNo_lem)
∀n ∈ ω, ∀m, nat_p m → - n + m ∈ int
Proof:
Proof not loaded.
L27446
Theorem. (int_add_SNo)
∀x y ∈ int, x + y ∈ int
Proof:
Proof not loaded.
L27475
Theorem. (int_minus_SNo)
∀x ∈ int, - x ∈ int
Proof:
Proof not loaded.
L27484
Theorem. (int_mul_SNo)
∀x y ∈ int, x * y ∈ int
Proof:
Proof not loaded.
L27553
Theorem. (nonneg_int_nat_p)
∀n ∈ int, 0 ≤ n → nat_p n
Proof:
Proof not loaded.
End of Section Int
Beginning of Section BezoutAndGCD
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_nat.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_nat.
L27591
Theorem. (quotient_remainder_nat)
∀n ∈ ω ∖ {0}, ∀m, nat_p m → ∃q ∈ ω, ∃r ∈ n, m = q * n + r
Proof:
Proof not loaded.
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
Notation. We use ^ as an infix operator with priority 342 and which associates to the right corresponding to applying term exp_SNo_nat.
Notation. We use < as an infix operator with priority 490 and no associativity corresponding to applying term SNoLt.
Notation. We use ≤ as an infix operator with priority 490 and no associativity corresponding to applying term SNoLe.
L27672
Theorem. (mul_SNo_nonpos_nonneg)
∀x y, SNo x → SNo y → x ≤ 0 → 0 ≤ y → x * y ≤ 0
Proof:
Proof not loaded.
L27683
Theorem. (ordinal_0_In_ordsucc)
∀alpha, ordinal alpha → 0 ∈ ordsucc alpha
Proof:
Proof not loaded.
L27692
Theorem. (ordinal_ordsucc_pos)
∀alpha, ordinal alpha → 0 < ordsucc alpha
Proof:
Proof not loaded.
L27699
Theorem. (quotient_remainder_int)
∀n ∈ ω ∖ {0}, ∀m ∈ int, ∃q ∈ int, ∃r ∈ n, m = q * n + r
Proof:
Proof not loaded.
L27842
Definition. We define divides_int to be λm n ⇒ m ∈ int ∧ n ∈ int ∧ ∃k ∈ int, m * k = n of type set → set → prop.
L27844
Proof:
Proof not loaded.
L27859
Proof:
Proof not loaded.
L27876
Theorem. (divides_int_add_SNo)
∀m n k, divides_int m n → divides_int m k → divides_int m (n + k)
Proof:
Proof not loaded.
L27913
Theorem. (divides_int_mul_SNo)
∀m n m' n', divides_int m m' → divides_int n n' → divides_int (m * n) (m' * n')
Proof:
Proof not loaded.
L27951
Theorem. (divides_nat_divides_int)
∀m n, divides_nat m n → divides_int m n
Proof:
Proof not loaded.
L27973
Proof:
Proof not loaded.
L28027
Theorem. (divides_int_minus_SNo)
∀m n, divides_int m n → divides_int m (- n)
Proof:
Proof not loaded.
L28051
Theorem. (divides_int_mul_SNo_L)
∀m n, ∀k ∈ int, divides_int m n → divides_int m (n * k)
Proof:
Proof not loaded.
L28081
Theorem. (divides_int_mul_SNo_R)
∀m n, ∀k ∈ int, divides_int m n → divides_int m (k * n)
Proof:
Proof not loaded.
L28094
Proof:
Proof not loaded.
L28106
Theorem. (divides_int_pos_Le)
∀m n, divides_int m n → 0 < n → m ≤ n
Proof:
Proof not loaded.
L28189
Definition. We define gcd_reln to be λm n d ⇒ divides_int d m ∧ divides_int d n ∧ ∀d', divides_int d' m → divides_int d' n → d' ≤ d of type set → set → set → prop.
L28191
Theorem. (gcd_reln_uniq)
∀a b c d, gcd_reln a b c → gcd_reln a b d → c = d
Proof:
Proof not loaded.
L28218
Definition. We define int_lin_comb to be λa b c ⇒ a ∈ int ∧ b ∈ int ∧ c ∈ int ∧ ∃m n ∈ int, m * a + n * b = c of type set → set → set → prop.
L28220
Theorem. (int_lin_comb_I)
∀a b c ∈ int, (∃m n ∈ int, m * a + n * b = c) → int_lin_comb a b c
Proof:
Proof not loaded.
L28231
Theorem. (int_lin_comb_E)
∀a b c, int_lin_comb a b c → ∀p : prop, (a ∈ int → b ∈ int → c ∈ int → ∀m n ∈ int, m * a + n * b = c → p) → p
Proof:
Proof not loaded.
L28247
Theorem. (int_lin_comb_E1)
∀a b c, int_lin_comb a b c → a ∈ int
Proof:
Proof not loaded.
L28253
Theorem. (int_lin_comb_E2)
∀a b c, int_lin_comb a b c → b ∈ int
Proof:
Proof not loaded.
L28259
Theorem. (int_lin_comb_E3)
∀a b c, int_lin_comb a b c → c ∈ int
Proof:
Proof not loaded.
L28265
Theorem. (int_lin_comb_E4)
∀a b c, int_lin_comb a b c → ∀p : prop, (∀m n ∈ int, m * a + n * b = c → p) → p
Proof:
Proof not loaded.
L28274
Theorem. (least_pos_int_lin_comb_ex)
∀a b ∈ int, ¬ (a = 0 ∧ b = 0) → ∃c, int_lin_comb a b c ∧ 0 < c ∧ ∀c', int_lin_comb a b c' → 0 < c' → c ≤ c'
Proof:
Proof not loaded.
L28474
Theorem. (int_lin_comb_sym)
∀a b d, int_lin_comb a b d → int_lin_comb b a d
Proof:
Proof not loaded.
L28495
Theorem. (least_pos_int_lin_comb_divides_int)
∀a b d, int_lin_comb a b d → 0 < d → (∀c, int_lin_comb a b c → 0 < c → d ≤ c) → divides_int d a
Proof:
Proof not loaded.
L28653
Theorem. (least_pos_int_lin_comb_gcd)
∀a b d, int_lin_comb a b d → 0 < d → (∀c, int_lin_comb a b c → 0 < c → d ≤ c) → gcd_reln a b d
Proof:
Proof not loaded.
L28733
Theorem. (BezoutThm)
∀a b ∈ int, ¬ (a = 0 ∧ b = 0) → ∀d, gcd_reln a b d ↔ int_lin_comb a b d ∧ 0 < d ∧ ∀d', int_lin_comb a b d' → 0 < d' → d ≤ d'
Proof:
Proof not loaded.
L28764
Theorem. (gcd_id)
∀m ∈ ω ∖ {0}, gcd_reln m m m
Proof:
Proof not loaded.
L28863
Theorem. (gcd_0)
Proof:
Proof not loaded.
L28890
Theorem. (gcd_sym)
∀m n d, gcd_reln m n d → gcd_reln n m d
Proof:
Proof not loaded.
L28905
Theorem. (gcd_minus)
∀m n d, gcd_reln m n d → gcd_reln m (- n) d
Proof:
Proof not loaded.
L28928
Theorem. (euclidean_algorithm_prop_1)
∀m n d, n ∈ int → gcd_reln m (n + - m) d → gcd_reln m n d
Proof:
Proof not loaded.
L28964
Theorem. (euclidean_algorithm)
(∀m ∈ ω ∖ {0}, gcd_reln m m m) ∧ (∀m ∈ ω ∖ {0}, gcd_reln 0 m m) ∧ (∀m ∈ ω ∖ {0}, gcd_reln m 0 m) ∧ (∀m n ∈ ω, m < n → ∀d, gcd_reln m (n + - m) d → gcd_reln m n d) ∧ (∀m n ∈ ω, n < m → ∀d, gcd_reln n m d → gcd_reln m n d) ∧ (∀m ∈ ω, ∀n ∈ int, n < 0 → ∀d, gcd_reln m (- n) d → gcd_reln m n d) ∧ (∀m n ∈ int, m < 0 → ∀d, gcd_reln (- m) n d → gcd_reln m n d)
Proof:
Proof not loaded.
L29011
Theorem. (Euclid_lemma)
∀p, prime_nat p → ∀a b ∈ int, divides_int p (a * b) → divides_int p a ∨ divides_int p b
Proof:
Proof not loaded.
End of Section BezoutAndGCD
Beginning of Section PrimeFactorization
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
Notation. We use ^ as an infix operator with priority 342 and which associates to the right corresponding to applying term exp_SNo_nat.
Notation. We use < as an infix operator with priority 490 and no associativity corresponding to applying term SNoLt.
Notation. We use ≤ as an infix operator with priority 490 and no associativity corresponding to applying term SNoLe.
L29133
Proof:
Proof not loaded.
L29157
Definition. We define Pi_SNo to be λf n ⇒ nat_primrec 1 (λi r ⇒ r * f i) n of type (set → set) → set → set.
L29160
Theorem. (Pi_SNo_0)
∀f : set → set, Pi_SNo f 0 = 1
Proof:
Proof not loaded.
L29165
Theorem. (Pi_SNo_S)
∀f : set → set, ∀n, nat_p n → Pi_SNo f (ordsucc n) = Pi_SNo f n * f n
Proof:
Proof not loaded.
L29171
Theorem. (Pi_SNo_In_omega)
∀f : set → set, ∀n, nat_p n → (∀i ∈ n, f i ∈ ω) → Pi_SNo f n ∈ ω
Proof:
Proof not loaded.
L29196
Theorem. (Pi_SNo_In_int)
∀f : set → set, ∀n, nat_p n → (∀i ∈ n, f i ∈ int) → Pi_SNo f n ∈ int
Proof:
Proof not loaded.
L29221
Theorem. (divides_int_prime_nat_eq)
∀p q, prime_nat p → prime_nat q → divides_int p q → p = q
Proof:
Proof not loaded.
L29246
Theorem. (Euclid_lemma_Pi_SNo)
∀f : set → set, ∀p, prime_nat p → ∀n, nat_p n → (∀i ∈ n, f i ∈ int) → divides_int p (Pi_SNo f n) → ∃i ∈ n, divides_int p (f i)
Proof:
Proof not loaded.
L29287
Theorem. (divides_nat_mul_SNo_R)
∀m n ∈ ω, divides_nat m (m * n)
Proof:
Proof not loaded.
L29301
Theorem. (divides_nat_mul_SNo_L)
∀m n ∈ ω, divides_nat n (m * n)
Proof:
Proof not loaded.
L29308
Theorem. (Pi_SNo_divides)
∀f : set → set, ∀n, nat_p n → (∀i ∈ n, f i ∈ ω) → (∀i ∈ n, divides_nat (f i) (Pi_SNo f n))
Proof:
Proof not loaded.
L29340
Definition. We define nonincrfinseq to be λA n f ⇒ ∀i ∈ n, A (f i) ∧ ∀j ∈ i, f i ≤ f j of type (set → prop) → set → (set → set) → prop.
L29342
Theorem. (Pi_SNo_eq)
∀f g : set → set, ∀m, nat_p m → (∀i ∈ m, f i = g i) → Pi_SNo f m = Pi_SNo g m
Proof:
Proof not loaded.
L29365
Theorem. (prime_factorization_ex_uniq)
∀n, nat_p n → 0 ∈ n → ∃k ∈ ω, ∃f : set → set, nonincrfinseq prime_nat k f ∧ Pi_SNo f k = n ∧ ∀k' ∈ ω, ∀f' : set → set, nonincrfinseq prime_nat k' f' → Pi_SNo f' k' = n → k' = k ∧ ∀i ∈ k, f' i = f i
Proof:
Proof not loaded.
End of Section PrimeFactorization
Beginning of Section SurrealExp
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
L29865
Definition. We define exp_SNo_nat to be λn m : set ⇒ nat_primrec 1 (λ_ r ⇒ n * r) m of type set → set → set.
Notation. We use ^ as an infix operator with priority 342 and which associates to the right corresponding to applying term exp_SNo_nat.
L29867
Theorem. (exp_SNo_nat_0)
∀x, SNo x → x ^ 0 = 1
Proof:
Proof not loaded.
L29872
Theorem. (exp_SNo_nat_S)
∀x, SNo x → ∀n, nat_p n → x ^ (ordsucc n) = x * x ^ n
Proof:
Proof not loaded.
L29877
Theorem. (exp_SNo_nat_1)
∀x, SNo x → x ^ 1 = x
Proof:
Proof not loaded.
L29886
Theorem. (SNo_exp_SNo_nat)
∀x, SNo x → ∀n, nat_p n → SNo (x ^ n)
Proof:
Proof not loaded.
L29896
Theorem. (nat_exp_SNo_nat)
∀x, nat_p x → ∀n, nat_p n → nat_p (x ^ n)
Proof:
Proof not loaded.
L29911
Theorem. (eps_ordsucc_half_add)
∀n, nat_p n → eps_ (ordsucc n) + eps_ (ordsucc n) = eps_ n
Proof:
Proof not loaded.
L30071
Theorem. (eps_1_half_eq1)
Proof:
Proof not loaded.
L30077
Theorem. (eps_1_half_eq2)
Proof:
Proof not loaded.
L30086
Theorem. (double_eps_1)
∀x y z, SNo x → SNo y → SNo z → x + x = y + z → x = eps_ 1 * (y + z)
Proof:
Proof not loaded.
L30107
Theorem. (exp_SNo_1_bd)
∀x, SNo x → 1 ≤ x → ∀n, nat_p n → 1 ≤ x ^ n
Proof:
Proof not loaded.
L30127
Theorem. (exp_SNo_2_bd)
∀n, nat_p n → n < 2 ^ n
Proof:
Proof not loaded.
L30161
Theorem. (mul_SNo_eps_power_2)
∀n, nat_p n → eps_ n * 2 ^ n = 1
Proof:
Proof not loaded.
L30186
Theorem. (eps_bd_1)
∀n ∈ ω, eps_ n ≤ 1
Proof:
Proof not loaded.
L30204
Theorem. (mul_SNo_eps_power_2')
∀n, nat_p n → 2 ^ n * eps_ n = 1
Proof:
Proof not loaded.
L30213
Theorem. (exp_SNo_nat_mul_add)
∀x, SNo x → ∀m, nat_p m → ∀n, nat_p n → x ^ m * x ^ n = x ^ (m + n)
Proof:
Proof not loaded.
L30245
Theorem. (exp_SNo_nat_mul_add')
∀x, SNo x → ∀m n ∈ ω, x ^ m * x ^ n = x ^ (m + n)
Proof:
Proof not loaded.
L30250
Theorem. (exp_SNo_nat_pos)
∀x, SNo x → 0 < x → ∀n, nat_p n → 0 < x ^ n
Proof:
Proof not loaded.
L30264
Theorem. (mul_SNo_eps_eps_add_SNo)
∀m n ∈ ω, eps_ m * eps_ n = eps_ (m + n)
Proof:
Proof not loaded.
L30314
Theorem. (SNoS_omega_Lev_equip)
∀n, nat_p n → equip {x ∈ SNoS_ ω|SNoLev x = n} (2 ^ n)
Proof:
Proof not loaded.
L30711
Theorem. (SNoS_finite)
Proof:
Proof not loaded.
L30763
Proof:
Proof not loaded.
L30783
Proof:
Proof not loaded.
End of Section SurrealExp
Beginning of Section SNoMaxMin
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
Notation. We use ^ as an infix operator with priority 342 and which associates to the right corresponding to applying term exp_SNo_nat.
Notation. We use < as an infix operator with priority 490 and no associativity corresponding to applying term SNoLt.
Notation. We use ≤ as an infix operator with priority 490 and no associativity corresponding to applying term SNoLe.
L30816
Definition. We define SNo_max_of to be λX x ⇒ x ∈ X ∧ SNo x ∧ ∀y ∈ X, SNo y → y ≤ x of type set → set → prop.
L30817
Definition. We define SNo_min_of to be λX x ⇒ x ∈ X ∧ SNo x ∧ ∀y ∈ X, SNo y → x ≤ y of type set → set → prop.
L30818
Theorem. (minus_SNo_max_min)
∀X y, (∀x ∈ X, SNo x) → SNo_max_of X y → SNo_min_of {- x|x ∈ X} (- y)
Proof:
Proof not loaded.
L30839
Theorem. (minus_SNo_max_min')
∀X y, (∀x ∈ X, SNo x) → SNo_max_of {- x|x ∈ X} y → SNo_min_of X (- y)
Proof:
Proof not loaded.
L30858
Theorem. (minus_SNo_min_max)
∀X y, (∀x ∈ X, SNo x) → SNo_min_of X y → SNo_max_of {- x|x ∈ X} (- y)
Proof:
Proof not loaded.
L30879
Theorem. (double_SNo_max_1)
∀x y, SNo x → SNo_max_of (SNoL x) y → ∀z, SNo z → x < z → y + z < x + x → ∃w ∈ SNoR z, y + w = x + x
Proof:
Proof not loaded.
L31071
Theorem. (double_SNo_min_1)
∀x y, SNo x → SNo_min_of (SNoR x) y → ∀z, SNo z → z < x → x + x < y + z → ∃w ∈ SNoL z, y + w = x + x
Proof:
Proof not loaded.
L31141
Theorem. (finite_max_exists)
∀X, (∀x ∈ X, SNo x) → finite X → X ≠ 0 → ∃x, SNo_max_of X x
Proof:
Proof not loaded.
L31287
Theorem. (finite_min_exists)
∀X, (∀x ∈ X, SNo x) → finite X → X ≠ 0 → ∃x, SNo_min_of X x
Proof:
Proof not loaded.
L31355
Proof:
Proof not loaded.
L31370
Proof:
Proof not loaded.
End of Section SNoMaxMin
Beginning of Section DiadicRationals
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
Notation. We use < as an infix operator with priority 490 and no associativity corresponding to applying term SNoLt.
Notation. We use ≤ as an infix operator with priority 490 and no associativity corresponding to applying term SNoLe.
Notation. We use ^ as an infix operator with priority 342 and which associates to the right corresponding to applying term exp_SNo_nat.
L31396
Proof:
Proof not loaded.
L31420
Definition. We define diadic_rational_p to be λx ⇒ ∃k ∈ ω, ∃m ∈ int, x = eps_ k * m of type set → prop.
L31422
Proof:
Proof not loaded.
L31447
Proof:
Proof not loaded.
L31458
Proof:
Proof not loaded.
L31463
Proof:
Proof not loaded.
L31475
Proof:
Proof not loaded.
L31501
Proof:
Proof not loaded.
L31543
Proof:
Proof not loaded.
L31621
Theorem. (SNoS_omega_diadic_rational_p_lem)
∀n, nat_p n → ∀x, SNo x → SNoLev x = n → diadic_rational_p x
Proof:
Proof not loaded.
L31826
Proof:
Proof not loaded.
L31839
Theorem. (mul_SNo_SNoS_omega)
∀x y ∈ SNoS_ ω, x * y ∈ SNoS_ ω
Proof:
Proof not loaded.
End of Section DiadicRationals
Beginning of Section SurrealDiv
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
Notation. We use < as an infix operator with priority 490 and no associativity corresponding to applying term SNoLt.
Notation. We use ≤ as an infix operator with priority 490 and no associativity corresponding to applying term SNoLe.
Notation. We use ^ as an infix operator with priority 342 and which associates to the right corresponding to applying term exp_SNo_nat.
L31860
Definition. We define SNoL_pos to be λx ⇒ {w ∈ SNoL x|0 < w} of type set → set.
L31861
Theorem. (SNo_recip_pos_pos)
∀x xi, SNo x → SNo xi → 0 < x → x * xi = 1 → 0 < xi
Proof:
Proof not loaded.
L31883
Theorem. (SNo_recip_lem1)
∀x x' x'i y y', SNo x → 0 < x → x' ∈ SNoL_pos x → SNo x'i → x' * x'i = 1 → SNo y → x * y < 1 → SNo y' → 1 + - x * y' = (1 + - x * y) * (x' + - x) * x'i → 1 < x * y'
Proof:
Proof not loaded.
L31929
Theorem. (SNo_recip_lem2)
∀x x' x'i y y', SNo x → 0 < x → x' ∈ SNoL_pos x → SNo x'i → x' * x'i = 1 → SNo y → 1 < x * y → SNo y' → 1 + - x * y' = (1 + - x * y) * (x' + - x) * x'i → x * y' < 1
Proof:
Proof not loaded.
L31975
Theorem. (SNo_recip_lem3)
∀x x' x'i y y', SNo x → 0 < x → x' ∈ SNoR x → SNo x'i → x' * x'i = 1 → SNo y → x * y < 1 → SNo y' → 1 + - x * y' = (1 + - x * y) * (x' + - x) * x'i → x * y' < 1
Proof:
Proof not loaded.
L32020
Theorem. (SNo_recip_lem4)
∀x x' x'i y y', SNo x → 0 < x → x' ∈ SNoR x → SNo x'i → x' * x'i = 1 → SNo y → 1 < x * y → SNo y' → 1 + - x * y' = (1 + - x * y) * (x' + - x) * x'i → 1 < x * y'
Proof:
Proof not loaded.
L32065
Definition. We define SNo_recipauxset to be λY x X g ⇒ ⋃y ∈ Y{(1 + (x' + - x) * y) * g x'|x' ∈ X} of type set → set → set → (set → set) → set.
L32067
Theorem. (SNo_recipauxset_I)
∀Y x X, ∀g : set → set, ∀y ∈ Y, ∀x' ∈ X, (1 + (x' + - x) * y) * g x' ∈ SNo_recipauxset Y x X g
Proof:
Proof not loaded.
L32076
Theorem. (SNo_recipauxset_E)
∀Y x X, ∀g : set → set, ∀z ∈ SNo_recipauxset Y x X g, ∀p : prop, (∀y ∈ Y, ∀x' ∈ X, z = (1 + (x' + - x) * y) * g x' → p) → p
Proof:
Proof not loaded.
L32088
Theorem. (SNo_recipauxset_ext)
∀Y x X, ∀g h : set → set, (∀x' ∈ X, g x' = h x') → SNo_recipauxset Y x X g = SNo_recipauxset Y x X h
Proof:
Proof not loaded.
L32102
Definition. We define SNo_recipaux to be λx g ⇒ nat_primrec ({0},0) (λk p ⇒ (p 0 ∪ SNo_recipauxset (p 0) x (SNoR x) g ∪ SNo_recipauxset (p 1) x (SNoL_pos x) g,p 1 ∪ SNo_recipauxset (p 0) x (SNoL_pos x) g ∪ SNo_recipauxset (p 1) x (SNoR x) g)) of type set → (set → set) → set → set.
L32110
Theorem. (SNo_recipaux_0)
∀x, ∀g : set → set, SNo_recipaux x g 0 = ({0},0)
Proof:
Proof not loaded.
L32119
Theorem. (SNo_recipaux_S)
∀x, ∀g : set → set, ∀n, nat_p n → SNo_recipaux x g (ordsucc n) = (SNo_recipaux x g n 0 ∪ SNo_recipauxset (SNo_recipaux x g n 0) x (SNoR x) g ∪ SNo_recipauxset (SNo_recipaux x g n 1) x (SNoL_pos x) g,SNo_recipaux x g n 1 ∪ SNo_recipauxset (SNo_recipaux x g n 0) x (SNoL_pos x) g ∪ SNo_recipauxset (SNo_recipaux x g n 1) x (SNoR x) g)
Proof:
Proof not loaded.
L32133
Theorem. (SNo_recipaux_lem1)
∀x, SNo x → 0 < x → ∀g : set → set, (∀x' ∈ SNoS_ (SNoLev x), 0 < x' → SNo (g x') ∧ x' * g x' = 1) → ∀k, nat_p k → (∀y ∈ SNo_recipaux x g k 0, SNo y ∧ x * y < 1) ∧ (∀y ∈ SNo_recipaux x g k 1, SNo y ∧ 1 < x * y)
Proof:
Proof not loaded.
L32376
Theorem. (SNo_recipaux_lem2)
∀x, SNo x → 0 < x → ∀g : set → set, (∀x' ∈ SNoS_ (SNoLev x), 0 < x' → SNo (g x') ∧ x' * g x' = 1) → SNoCutP (⋃k ∈ ωSNo_recipaux x g k 0) (⋃k ∈ ωSNo_recipaux x g k 1)
Proof:
Proof not loaded.
L32437
Theorem. (SNo_recipaux_ext)
∀x, SNo x → ∀g h : set → set, (∀x' ∈ SNoS_ (SNoLev x), g x' = h x') → ∀k, nat_p k → SNo_recipaux x g k = SNo_recipaux x h k
Proof:
Proof not loaded.
Beginning of Section recip_SNo_pos
L32527
Let G : set → (set → set) → set ≝ λx g ⇒ SNoCut (⋃k ∈ ωSNo_recipaux x g k 0) (⋃k ∈ ωSNo_recipaux x g k 1)
L32528
Definition. We define recip_SNo_pos to be SNo_rec_i G of type set → set.
L32529
Theorem. (recip_SNo_pos_eq)
∀x, SNo x → recip_SNo_pos x = G x recip_SNo_pos
Proof:
Proof not loaded.
L32554
Theorem. (recip_SNo_pos_prop1)
∀x, SNo x → 0 < x → SNo (recip_SNo_pos x) ∧ x * recip_SNo_pos x = 1
Proof:
Proof not loaded.
L33177
Theorem. (SNo_recip_SNo_pos)
∀x, SNo x → 0 < x → SNo (recip_SNo_pos x)
Proof:
Proof not loaded.
L33182
Theorem. (recip_SNo_pos_invR)
∀x, SNo x → 0 < x → x * recip_SNo_pos x = 1
Proof:
Proof not loaded.
L33187
Theorem. (recip_SNo_pos_is_pos)
∀x, SNo x → 0 < x → 0 < recip_SNo_pos x
Proof:
Proof not loaded.
L33212
Theorem. (recip_SNo_pos_invol)
∀x, SNo x → 0 < x → recip_SNo_pos (recip_SNo_pos x) = x
Proof:
Proof not loaded.
L33235
Theorem. (recip_SNo_pos_eps_)
∀n, nat_p n → recip_SNo_pos (eps_ n) = 2 ^ n
Proof:
Proof not loaded.
L33256
Theorem. (recip_SNo_pos_pow_2)
∀n, nat_p n → recip_SNo_pos (2 ^ n) = eps_ n
Proof:
Proof not loaded.
L33262
Proof:
Proof not loaded.
End of Section recip_SNo_pos
L33269
Definition. We define recip_SNo to be λx ⇒ if 0 < x then recip_SNo_pos x else if x < 0 then - recip_SNo_pos (- x) else 0 of type set → set.
L33270
Theorem. (recip_SNo_poscase)
∀x, 0 < x → recip_SNo x = recip_SNo_pos x
Proof:
Proof not loaded.
L33275
Theorem. (recip_SNo_negcase)
∀x, SNo x → x < 0 → recip_SNo x = - recip_SNo_pos (- x)
Proof:
Proof not loaded.
L33287
Proof:
Proof not loaded.
L33294
Theorem. (SNo_recip_SNo)
∀x, SNo x → SNo (recip_SNo x)
Proof:
Proof not loaded.
L33314
Theorem. (recip_SNo_invR)
∀x, SNo x → x ≠ 0 → x * recip_SNo x = 1
Proof:
Proof not loaded.
L33336
Theorem. (recip_SNo_invL)
∀x, SNo x → x ≠ 0 → recip_SNo x * x = 1
Proof:
Proof not loaded.
L33343
Theorem. (mul_SNo_nonzero_cancel_L)
∀x y z, SNo x → x ≠ 0 → SNo y → SNo z → x * y = x * z → y = z
Proof:
Proof not loaded.
L33359
Theorem. (recip_SNo_pow_2)
∀n, nat_p n → recip_SNo (2 ^ n) = eps_ n
Proof:
Proof not loaded.
L33367
Theorem. (recip_SNo_of_pos_is_pos)
∀x, SNo x → 0 < x → 0 < recip_SNo x
Proof:
Proof not loaded.
L33373
Definition. We define div_SNo to be λx y ⇒ x * recip_SNo y of type set → set → set.
Notation. We use :/: as an infix operator with priority 353 and no associativity corresponding to applying term div_SNo.
L33377
Theorem. (SNo_div_SNo)
∀x y, SNo x → SNo y → SNo (x :/: y)
Proof:
Proof not loaded.
L33383
Theorem. (div_SNo_0_num)
∀x, SNo x → 0 :/: x = 0
Proof:
Proof not loaded.
L33388
Theorem. (div_SNo_0_denum)
∀x, SNo x → x :/: 0 = 0
Proof:
Proof not loaded.
L33395
Theorem. (mul_div_SNo_invL)
∀x y, SNo x → SNo y → y ≠ 0 → (x :/: y) * y = x
Proof:
Proof not loaded.
L33405
Theorem. (mul_div_SNo_invR)
∀x y, SNo x → SNo y → y ≠ 0 → y * (x :/: y) = x
Proof:
Proof not loaded.
L33411
Theorem. (mul_div_SNo_R)
∀x y z, SNo x → SNo y → SNo z → (x :/: y) * z = (x * z) :/: y
Proof:
Proof not loaded.
L33432
Theorem. (mul_div_SNo_L)
∀x y z, SNo x → SNo y → SNo z → z * (x :/: y) = (z * x) :/: y
Proof:
Proof not loaded.
L33440
Theorem. (div_mul_SNo_invL)
∀x y, SNo x → SNo y → y ≠ 0 → (x * y) :/: y = x
Proof:
Proof not loaded.
L33447
Theorem. (div_div_SNo)
∀x y z, SNo x → SNo y → SNo z → (x :/: y) :/: z = x :/: (y * z)
Proof:
Proof not loaded.
L33497
Theorem. (mul_div_SNo_both)
∀x y z w, SNo x → SNo y → SNo z → SNo w → (x :/: y) * (z :/: w) = (x * z) :/: (y * w)
Proof:
Proof not loaded.
L33506
Theorem. (recip_SNo_pos_pos)
∀x, SNo x → 0 < x → 0 < recip_SNo_pos x
Proof:
Proof not loaded.
L33522
Theorem. (div_SNo_pos_pos)
∀x y, SNo x → SNo y → 0 < x → 0 < y → 0 < x :/: y
Proof:
Proof not loaded.
L33530
Theorem. (div_SNo_neg_pos)
∀x y, SNo x → SNo y → x < 0 → 0 < y → x :/: y < 0
Proof:
Proof not loaded.
L33538
Theorem. (div_SNo_pos_LtL)
∀x y z, SNo x → SNo y → SNo z → 0 < y → x < z * y → x :/: y < z
Proof:
Proof not loaded.
L33559
Theorem. (div_SNo_pos_LtR)
∀x y z, SNo x → SNo y → SNo z → 0 < y → z * y < x → z < x :/: y
Proof:
Proof not loaded.
L33580
Theorem. (div_SNo_pos_LtL')
∀x y z, SNo x → SNo y → SNo z → 0 < y → x :/: y < z → x < z * y
Proof:
Proof not loaded.
L33599
Theorem. (div_SNo_pos_LtR')
∀x y z, SNo x → SNo y → SNo z → 0 < y → z < x :/: y → z * y < x
Proof:
Proof not loaded.
L33618
Theorem. (mul_div_SNo_nonzero_eq)
∀x y z, SNo x → SNo y → SNo z → y ≠ 0 → x = y * z → x :/: y = z
Proof:
Proof not loaded.
End of Section SurrealDiv
Beginning of Section Reals
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
Notation. We use :/: as an infix operator with priority 353 and no associativity corresponding to applying term div_SNo.
Notation. We use ^ as an infix operator with priority 342 and which associates to the right corresponding to applying term exp_SNo_nat.
Notation. We use < as an infix operator with priority 490 and no associativity corresponding to applying term SNoLt.
Notation. We use ≤ as an infix operator with priority 490 and no associativity corresponding to applying term SNoLe.
L33641
Theorem. (SNoS_omega_drat_intvl)
∀x ∈ SNoS_ ω, ∀k ∈ ω, ∃q ∈ SNoS_ ω, q < x ∧ x < q + eps_ k
Proof:
Proof not loaded.
L33669
Theorem. (SNoS_ordsucc_omega_bdd_above)
∀x ∈ SNoS_ (ordsucc ω), x < ω → ∃N ∈ ω, x < N
Proof:
Proof not loaded.
L33716
Theorem. (SNoS_ordsucc_omega_bdd_below)
∀x ∈ SNoS_ (ordsucc ω), - ω < x → ∃N ∈ ω, - N < x
Proof:
Proof not loaded.
L33737
Theorem. (SNoS_ordsucc_omega_bdd_drat_intvl)
∀x ∈ SNoS_ (ordsucc ω), - ω < x → x < ω → ∀k ∈ ω, ∃q ∈ SNoS_ ω, q < x ∧ x < q + eps_ k
Proof:
Proof not loaded.
L33875
Definition. We define real to be {x ∈ SNoS_ (ordsucc ω)|x ≠ ω ∧ x ≠ - ω ∧ (∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - x) < eps_ k) → q = x)} of type set.
L33877
Theorem. (real_I)
∀x ∈ SNoS_ (ordsucc ω), x ≠ ω → x ≠ - ω → (∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - x) < eps_ k) → q = x) → x ∈ real
Proof:
Proof not loaded.
L33893
Theorem. (real_E)
∀x ∈ real, ∀p : prop, (SNo x → SNoLev x ∈ ordsucc ω → x ∈ SNoS_ (ordsucc ω) → - ω < x → x < ω → (∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - x) < eps_ k) → q = x) → (∀k ∈ ω, ∃q ∈ SNoS_ ω, q < x ∧ x < q + eps_ k) → p) → p
Proof:
Proof not loaded.
L33936
Theorem. (real_SNo)
∀x ∈ real, SNo x
Proof:
Proof not loaded.
L33941
Theorem. (real_SNoS_omega_prop)
∀x ∈ real, ∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - x) < eps_ k) → q = x
Proof:
Proof not loaded.
L33946
Proof:
Proof not loaded.
L34037
Theorem. (real_0)
Proof:
Proof not loaded.
L34041
Theorem. (real_1)
Proof:
Proof not loaded.
L34045
Theorem. (SNoLev_In_real_SNoS_omega)
∀x ∈ real, ∀w, SNo w → SNoLev w ∈ SNoLev x → w ∈ SNoS_ ω
Proof:
Proof not loaded.
L34062
Theorem. (real_SNoCut_SNoS_omega)
∀L R ⊆ SNoS_ ω, SNoCutP L R → L ≠ 0 → R ≠ 0 → (∀w ∈ L, ∃w' ∈ L, w < w') → (∀z ∈ R, ∃z' ∈ R, z' < z) → SNoCut L R ∈ real
Proof:
Proof not loaded.
L34311
Theorem. (real_SNoCut)
∀L R ⊆ real, SNoCutP L R → L ≠ 0 → R ≠ 0 → (∀w ∈ L, ∃w' ∈ L, w < w') → (∀z ∈ R, ∃z' ∈ R, z' < z) → SNoCut L R ∈ real
Proof:
Proof not loaded.
L34708
Theorem. (minus_SNo_prereal_1)
∀x, SNo x → (∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - x) < eps_ k) → q = x) → (∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - - x) < eps_ k) → q = - x)
Proof:
Proof not loaded.
L34734
Theorem. (minus_SNo_prereal_2)
∀x, SNo x → (∀k ∈ ω, ∃q ∈ SNoS_ ω, q < x ∧ x < q + eps_ k) → (∀k ∈ ω, ∃q ∈ SNoS_ ω, q < - x ∧ - x < q + eps_ k)
Proof:
Proof not loaded.
L34764
Theorem. (SNo_prereal_incr_lower_pos)
∀x, SNo x → 0 < x → (∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - x) < eps_ k) → q = x) → (∀k ∈ ω, ∃q ∈ SNoS_ ω, q < x ∧ x < q + eps_ k) → ∀k ∈ ω, ∀p : prop, (∀q ∈ SNoS_ ω, 0 < q → q < x → x < q + eps_ k → p) → p
Proof:
Proof not loaded.
L34850
Theorem. (real_minus_SNo)
Proof:
Proof not loaded.
L34877
Theorem. (SNo_prereal_incr_lower_approx)
∀x, SNo x → (∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - x) < eps_ k) → q = x) → (∀k ∈ ω, ∃q ∈ SNoS_ ω, q < x ∧ x < q + eps_ k) → ∃f ∈ SNoS_ ωω, ∀n ∈ ω, f n < x ∧ x < f n + eps_ n ∧ ∀i ∈ n, f i < f n
Proof:
Proof not loaded.
L35093
Theorem. (SNo_prereal_decr_upper_approx)
∀x, SNo x → (∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - x) < eps_ k) → q = x) → (∀k ∈ ω, ∃q ∈ SNoS_ ω, q < x ∧ x < q + eps_ k) → ∃g ∈ SNoS_ ωω, ∀n ∈ ω, g n + - eps_ n < x ∧ x < g n ∧ ∀i ∈ n, g n < g i
Proof:
Proof not loaded.
L35156
Theorem. (SNoCutP_SNoCut_lim)
∀lambda, ordinal lambda → (∀alpha ∈ lambda, ordsucc alpha ∈ lambda) → ∀L R ⊆ SNoS_ lambda, SNoCutP L R → SNoLev (SNoCut L R) ∈ ordsucc lambda
Proof:
Proof not loaded.
L35222
Proof:
Proof not loaded.
L35227
Theorem. (SNo_approx_real_lem)
∀f g ∈ SNoS_ ωω, (∀n m ∈ ω, f n < g m) → ∀p : prop, (SNoCutP {f n|n ∈ ω} {g n|n ∈ ω} → SNo (SNoCut {f n|n ∈ ω} {g n|n ∈ ω}) → SNoLev (SNoCut {f n|n ∈ ω} {g n|n ∈ ω}) ∈ ordsucc ω → SNoCut {f n|n ∈ ω} {g n|n ∈ ω} ∈ SNoS_ (ordsucc ω) → (∀n ∈ ω, f n < SNoCut {f n|n ∈ ω} {g n|n ∈ ω}) → (∀n ∈ ω, SNoCut {f n|n ∈ ω} {g n|n ∈ ω} < g n) → p) → p
Proof:
Proof not loaded.
L35328
Theorem. (SNo_approx_real)
∀x, SNo x → ∀f g ∈ SNoS_ ωω, (∀n ∈ ω, f n < x) → (∀n ∈ ω, x < f n + eps_ n) → (∀n ∈ ω, ∀i ∈ n, f i < f n) → (∀n ∈ ω, x < g n) → (∀n ∈ ω, ∀i ∈ n, g n < g i) → x = SNoCut {f n|n ∈ ω} {g n|n ∈ ω} → x ∈ real
Proof:
Proof not loaded.
L35545
Theorem. (SNo_approx_real_rep)
∀x ∈ real, ∀p : prop, (∀f g ∈ SNoS_ ωω, (∀n ∈ ω, f n < x) → (∀n ∈ ω, x < f n + eps_ n) → (∀n ∈ ω, ∀i ∈ n, f i < f n) → (∀n ∈ ω, g n + - eps_ n < x) → (∀n ∈ ω, x < g n) → (∀n ∈ ω, ∀i ∈ n, g n < g i) → SNoCutP {f n|n ∈ ω} {g n|n ∈ ω} → x = SNoCut {f n|n ∈ ω} {g n|n ∈ ω} → p) → p
Proof:
Proof not loaded.
L35728
Theorem. (real_add_SNo)
∀x y ∈ real, x + y ∈ real
Proof:
Proof not loaded.
L36204
Theorem. (SNoS_ordsucc_omega_bdd_eps_pos)
∀x ∈ SNoS_ (ordsucc ω), 0 < x → x < ω → ∃N ∈ ω, eps_ N * x < 1
Proof:
Proof not loaded.
L36255
Theorem. (real_mul_SNo_pos)
∀x y ∈ real, 0 < x → 0 < y → x * y ∈ real
Proof:
Proof not loaded.
L37620
Theorem. (real_mul_SNo)
∀x y ∈ real, x * y ∈ real
Proof:
Proof not loaded.
L37678
Theorem. (nonneg_real_nat_interval)
∀x ∈ real, 0 ≤ x → ∃n ∈ ω, n ≤ x ∧ x < ordsucc n
Proof:
Proof not loaded.
L37757
Theorem. (pos_real_left_approx_double)
∀x ∈ real, 0 < x → x ≠ 2 → (∀m ∈ ω, x ≠ eps_ m) → ∃w ∈ SNoL_pos x, x < 2 * w
Proof:
Proof not loaded.
L38122
Proof:
Proof not loaded.
L38866
Proof:
Proof not loaded.
L38872
Proof:
Proof not loaded.
L38898
Theorem. (real_div_SNo)
∀x y ∈ real, x :/: y ∈ real
Proof:
Proof not loaded.
End of Section Reals
Beginning of Section even_odd
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_nat.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_nat.
L38915
Theorem. (nat_le2_cases)
∀m, nat_p m → m ⊆ 2 → m = 0 ∨ m = 1 ∨ m = 2
Proof:
Proof not loaded.
L38936
Theorem. (prime_nat_2_lem)
∀m, nat_p m → ∀n, nat_p n → m * n = 2 → m = 1 ∨ m = 2
Proof:
Proof not loaded.
L38967
Proof:
Proof not loaded.
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
L38987
Theorem. (not_eq_2m_2n1)
∀m n ∈ int, 2 * m ≠ 2 * n + 1
Proof:
Proof not loaded.
End of Section even_odd
Beginning of Section form100_22b
L39029
Let tag : set → set ≝ λalpha ⇒ SetAdjoin alpha {1}
Notation. We use ' as a postfix operator with priority 100 corresponding to applying term tag.
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
L39036
Proof:
Proof not loaded.
L39203
Theorem. (Repl_finite)
∀f : set → set, ∀X, finite X → finite {f x|x ∈ X}
Proof:
Proof not loaded.
L39256
Theorem. (infinite_bigger)
∀X ⊆ ω, infinite X → ∀m ∈ ω, ∃n ∈ X, m ∈ n
Proof:
Proof not loaded.
L39285
Proof:
Proof not loaded.
L41035
Proof:
Proof not loaded.
L41048
Proof:
Proof not loaded.
L41056
Proof:
Proof not loaded.
End of Section form100_22b
Beginning of Section rational
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
Notation. We use ^ as an infix operator with priority 342 and which associates to the right corresponding to applying term exp_SNo_nat.
Notation. We use :/: as an infix operator with priority 353 and no associativity corresponding to applying term div_SNo.
Notation. We use < as an infix operator with priority 490 and no associativity corresponding to applying term SNoLt.
Notation. We use ≤ as an infix operator with priority 490 and no associativity corresponding to applying term SNoLe.
L41082
Definition. We define rational to be {x ∈ real|∃m ∈ int, ∃n ∈ ω ∖ {0}, x = m :/: n} of type set.
End of Section rational
Beginning of Section form100_3
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
Notation. We use :/: as an infix operator with priority 353 and no associativity corresponding to applying term div_SNo.
Notation. We use ^ as an infix operator with priority 342 and which associates to the right corresponding to applying term exp_SNo_nat.
(*** The Denumerability of the Rational Numbers ***)
L41096
Proof:
Proof not loaded.
L41105
Proof:
Proof not loaded.
L41153
Proof:
Proof not loaded.
L41157
Proof:
Proof not loaded.
L41216
Definition. We define nat_pair to be λm n ⇒ 2 ^ m * (2 * n + 1) of type set → set → set.
L41218
Theorem. (nat_pair_In_omega)
∀m n ∈ ω, nat_pair m n ∈ ω
Proof:
Proof not loaded.
L41230
Theorem. (nat_pair_0)
∀m n m' n' ∈ ω, nat_pair m n = nat_pair m' n' → m = m'
Proof:
Proof not loaded.
L41439
Theorem. (nat_pair_1)
∀m n m' n' ∈ ω, nat_pair m n = nat_pair m' n' → n = n'
Proof:
Proof not loaded.
L41476
Proof:
Proof not loaded.
End of Section form100_3
Beginning of Section SurrealSqrt
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
Notation. We use :/: as an infix operator with priority 353 and no associativity corresponding to applying term div_SNo.
Notation. We use < as an infix operator with priority 490 and no associativity corresponding to applying term SNoLt.
Notation. We use ≤ as an infix operator with priority 490 and no associativity corresponding to applying term SNoLe.
Notation. We use ^ as an infix operator with priority 342 and which associates to the right corresponding to applying term exp_SNo_nat.
L41810
Definition. We define SNoL_nonneg to be λx ⇒ {w ∈ SNoL x|0 ≤ w} of type set → set.
L41811
Proof:
Proof not loaded.
L41817
Proof:
Proof not loaded.
L41831
Definition. We define SNo_sqrtauxset to be λY Z x ⇒ ⋃y ∈ Y{(x + y * z) :/: (y + z)|z ∈ Z, 0 < y + z} of type set → set → set → set.
L41833
Theorem. (SNo_sqrtauxset_I)
∀Y Z x, ∀y ∈ Y, ∀z ∈ Z, 0 < y + z → (x + y * z) :/: (y + z) ∈ SNo_sqrtauxset Y Z x
Proof:
Proof not loaded.
L41843
Theorem. (SNo_sqrtauxset_E)
∀Y Z x, ∀u ∈ SNo_sqrtauxset Y Z x, ∀p : prop, (∀y ∈ Y, ∀z ∈ Z, 0 < y + z → u = (x + y * z) :/: (y + z) → p) → p
Proof:
Proof not loaded.
L41857
Theorem. (SNo_sqrtauxset_0)
∀Z x, SNo_sqrtauxset 0 Z x = 0
Proof:
Proof not loaded.
L41865
Theorem. (SNo_sqrtauxset_0')
∀Y x, SNo_sqrtauxset Y 0 x = 0
Proof:
Proof not loaded.
L41874
Definition. We define SNo_sqrtaux to be λx g ⇒ nat_primrec ({g w|w ∈ SNoL_nonneg x},{g z|z ∈ SNoR x}) (λk p ⇒ (p 0 ∪ SNo_sqrtauxset (p 0) (p 1) x,p 1 ∪ SNo_sqrtauxset (p 0) (p 0) x ∪ SNo_sqrtauxset (p 1) (p 1) x)) of type set → (set → set) → set → set.
L41881
Theorem. (SNo_sqrtaux_0)
∀x, ∀g : set → set, SNo_sqrtaux x g 0 = ({g w|w ∈ SNoL_nonneg x},{g z|z ∈ SNoR x})
Proof:
Proof not loaded.
L41889
Theorem. (SNo_sqrtaux_S)
∀x, ∀g : set → set, ∀n, nat_p n → SNo_sqrtaux x g (ordsucc n) = (SNo_sqrtaux x g n 0 ∪ SNo_sqrtauxset (SNo_sqrtaux x g n 0) (SNo_sqrtaux x g n 1) x,SNo_sqrtaux x g n 1 ∪ SNo_sqrtauxset (SNo_sqrtaux x g n 0) (SNo_sqrtaux x g n 0) x ∪ SNo_sqrtauxset (SNo_sqrtaux x g n 1) (SNo_sqrtaux x g n 1) x)
Proof:
Proof not loaded.
L41903
Theorem. (SNo_sqrtaux_mon_lem)
∀x, ∀g : set → set, ∀m, nat_p m → ∀n, nat_p n → SNo_sqrtaux x g m 0 ⊆ SNo_sqrtaux x g (add_nat m n) 0 ∧ SNo_sqrtaux x g m 1 ⊆ SNo_sqrtaux x g (add_nat m n) 1
Proof:
Proof not loaded.
L41945
Theorem. (SNo_sqrtaux_mon)
∀x, ∀g : set → set, ∀m, nat_p m → ∀n, nat_p n → m ⊆ n → SNo_sqrtaux x g m 0 ⊆ SNo_sqrtaux x g n 0 ∧ SNo_sqrtaux x g m 1 ⊆ SNo_sqrtaux x g n 1
Proof:
Proof not loaded.
L41959
Theorem. (SNo_sqrtaux_ext)
∀x, SNo x → ∀g h : set → set, (∀x' ∈ SNoS_ (SNoLev x), g x' = h x') → ∀k, nat_p k → SNo_sqrtaux x g k = SNo_sqrtaux x h k
Proof:
Proof not loaded.
Beginning of Section sqrt_SNo_nonneg
L42000
Let G : set → (set → set) → set ≝ λx g ⇒ SNoCut (⋃k ∈ ωSNo_sqrtaux x g k 0) (⋃k ∈ ωSNo_sqrtaux x g k 1)
L42001
Definition. We define sqrt_SNo_nonneg to be SNo_rec_i G of type set → set.
L42002
Proof:
Proof not loaded.
L42027
Theorem. (sqrt_SNo_nonneg_prop1a)
∀x, SNo x → 0 ≤ x → (∀w ∈ SNoS_ (SNoLev x), 0 ≤ w → SNo (sqrt_SNo_nonneg w) ∧ 0 ≤ sqrt_SNo_nonneg w ∧ sqrt_SNo_nonneg w * sqrt_SNo_nonneg w = w) → ∀k, nat_p k → (∀y ∈ SNo_sqrtaux x sqrt_SNo_nonneg k 0, SNo y ∧ 0 ≤ y ∧ y * y < x) ∧ (∀y ∈ SNo_sqrtaux x sqrt_SNo_nonneg k 1, SNo y ∧ 0 ≤ y ∧ x < y * y)
Proof:
Proof not loaded.
L42465
Proof:
Proof not loaded.
L42534
Theorem. (sqrt_SNo_nonneg_prop1c)
∀x, SNo x → 0 ≤ x → SNoCutP (⋃k ∈ ωSNo_sqrtaux x sqrt_SNo_nonneg k 0) (⋃k ∈ ωSNo_sqrtaux x sqrt_SNo_nonneg k 1) → (∀z ∈ (⋃k ∈ ωSNo_sqrtaux x sqrt_SNo_nonneg k 1), ∀p : prop, (SNo z → 0 ≤ z → x < z * z → p) → p) → 0 ≤ G x sqrt_SNo_nonneg
Proof:
Proof not loaded.
L42570
Proof:
Proof not loaded.
L42853
Proof:
Proof not loaded.
L43237
Proof:
Proof not loaded.
End of Section sqrt_SNo_nonneg
L43320
Theorem. (SNo_sqrtaux_0_1_prop)
∀x, SNo x → 0 ≤ x → ∀k, nat_p k → (∀y ∈ SNo_sqrtaux x sqrt_SNo_nonneg k 0, SNo y ∧ 0 ≤ y ∧ y * y < x) ∧ (∀y ∈ SNo_sqrtaux x sqrt_SNo_nonneg k 1, SNo y ∧ 0 ≤ y ∧ x < y * y)
Proof:
Proof not loaded.
L43331
Theorem. (SNo_sqrtaux_0_prop)
∀x, SNo x → 0 ≤ x → ∀k, nat_p k → ∀y ∈ SNo_sqrtaux x sqrt_SNo_nonneg k 0, SNo y ∧ 0 ≤ y ∧ y * y < x
Proof:
Proof not loaded.
L43340
Theorem. (SNo_sqrtaux_1_prop)
∀x, SNo x → 0 ≤ x → ∀k, nat_p k → ∀y ∈ SNo_sqrtaux x sqrt_SNo_nonneg k 1, SNo y ∧ 0 ≤ y ∧ x < y * y
Proof:
Proof not loaded.
L43349
Proof:
Proof not loaded.
L43357
Theorem. (SNo_sqrt_SNo_nonneg)
∀x, SNo x → 0 ≤ x → SNo (sqrt_SNo_nonneg x)
Proof:
Proof not loaded.
L43363
Theorem. (sqrt_SNo_nonneg_nonneg)
∀x, SNo x → 0 ≤ x → 0 ≤ sqrt_SNo_nonneg x
Proof:
Proof not loaded.
L43369
Theorem. (sqrt_SNo_nonneg_sqr)
∀x, SNo x → 0 ≤ x → sqrt_SNo_nonneg x * sqrt_SNo_nonneg x = x
Proof:
Proof not loaded.
L43375
Proof:
Proof not loaded.
L43455
Proof:
Proof not loaded.
L43579
Theorem. (sqrt_SNo_nonneg_0inL0)
∀x, SNo x → 0 ≤ x → 0 ∈ SNoLev x → 0 ∈ SNo_sqrtaux x sqrt_SNo_nonneg 0 0
Proof:
Proof not loaded.
L43607
Proof:
Proof not loaded.
L43625
Proof:
Proof not loaded.
L43699
Theorem. (SNo_sqrtauxset_real)
∀Y Z x, Y ⊆ real → Z ⊆ real → x ∈ real → SNo_sqrtauxset Y Z x ⊆ real
Proof:
Proof not loaded.
L43726
Theorem. (SNo_sqrtauxset_real_nonneg)
∀Y Z x, Y ⊆ {w ∈ real|0 ≤ w} → Z ⊆ {z ∈ real|0 ≤ z} → x ∈ real → 0 ≤ x → SNo_sqrtauxset Y Z x ⊆ {w ∈ real|0 ≤ w}
Proof:
Proof not loaded.
L43797
Proof:
Proof not loaded.
L44221
Proof:
Proof not loaded.
End of Section SurrealSqrt
Beginning of Section form100_1
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
Notation. We use :/: as an infix operator with priority 353 and no associativity corresponding to applying term div_SNo.
L44647
Theorem. (divides_int_div_SNo_int)
∀m n, divides_int m n → n :/: m ∈ int
Proof:
Proof not loaded.
L44684
Theorem. (form100_1_lem1)
∀m, nat_p m → ∀n, nat_p n → m * m = 2 * n * n → n = 0
Proof:
Proof not loaded.
L44847
Theorem. (form100_1_lem2)
∀m ∈ ω, ∀n ∈ ω ∖ 1, m * m ≠ 2 * n * n
Proof:
Proof not loaded.
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
Notation. We use :/: as an infix operator with priority 353 and no associativity corresponding to applying term div_SNo.
L44869
Proof:
Proof not loaded.
End of Section form100_1