Beginning of Section TaggedSets
L4
Let tag : set → set ≝ λalpha ⇒ SetAdjoin alpha {1}
Notation. We use ' as a postfix operator with priority 100 corresponding to applying term tag.
L6
Axiom. (not_TransSet_Sing1) We take the following as an axiom:
¬ TransSet {1}
In Proofgold the corresponding term root is 8f2d67... and proposition id is be9a70...
L7
Axiom. (not_ordinal_Sing1) We take the following as an axiom:
¬ ordinal {1}
In Proofgold the corresponding term root is 99a3f6... and proposition id is db7977...
L8
Axiom. (tagged_not_ordinal) We take the following as an axiom:
∀y, ¬ ordinal (y ')
In Proofgold the corresponding term root is f9488c... and proposition id is aaf6e4...
L9
Axiom. (tagged_notin_ordinal) We take the following as an axiom:
∀alpha y, ordinal alpha → (y ') ∉ alpha
In Proofgold the corresponding term root is b603ba... and proposition id is c0e2c3...
L10
Axiom. (tagged_eqE_Subq) We take the following as an axiom:
∀alpha beta, ordinal alpha → alpha ' = beta ' → alpha ⊆ beta
In Proofgold the corresponding term root is cf032f... and proposition id is ef37f5...
L11
Axiom. (tagged_eqE_eq) We take the following as an axiom:
∀alpha beta, ordinal alpha → ordinal beta → alpha ' = beta ' → alpha = beta
In Proofgold the corresponding term root is 1f7dc9... and proposition id is ec1608...
L12
Axiom. (tagged_ReplE) We take the following as an axiom:
∀alpha beta, ordinal alpha → ordinal beta → beta ' ∈ {gamma '|gamma ∈ alpha} → beta ∈ alpha
In Proofgold the corresponding term root is a1d43c... and proposition id is 70c250...
L13
Axiom. (ordinal_notin_tagged_Repl) We take the following as an axiom:
∀alpha Y, ordinal alpha → alpha ∉ {y '|y ∈ Y}
In Proofgold the corresponding term root is 7f35b5... and proposition id is e7ff3b...
L14
Definition. We define SNoElts_ to be λalpha ⇒ alpha ∪ {beta '|beta ∈ alpha} of type set → set.
In Proofgold the corresponding term root is c0ec73... and object id is 6f0c36...
L15
Axiom. (SNoElts_mon) We take the following as an axiom:
∀alpha beta, alpha ⊆ beta → SNoElts_ alpha ⊆ SNoElts_ beta
In Proofgold the corresponding term root is 49a08e... and proposition id is 859611...
L16
Definition. We define SNo_ to be λalpha x ⇒ x ⊆ SNoElts_ alpha ∧ ∀beta ∈ alpha, exactly1of2 (beta ' ∈ x) (beta ∈ x) of type set → set → prop.
In Proofgold the corresponding term root is 4ab7e4... and object id is c16a73...
L17
Definition. We define PSNo to be λalpha p ⇒ {beta ∈ alpha|p beta} ∪ {beta '|beta ∈ alpha, ¬ p beta} of type set → (set → prop) → set.
In Proofgold the corresponding term root is 3657ae... and object id is 0a8351...
L18
Axiom. (PNoEq_PSNo) We take the following as an axiom:
∀alpha, ordinal alpha → ∀p : set → prop, PNoEq_ alpha (λbeta ⇒ beta ∈ PSNo alpha p) p
In Proofgold the corresponding term root is c12e02... and proposition id is 688518...
L19
Axiom. (SNo_PSNo) We take the following as an axiom:
∀alpha, ordinal alpha → ∀p : set → prop, SNo_ alpha (PSNo alpha p)
In Proofgold the corresponding term root is 96e4e2... and proposition id is f03db0...
L20
Axiom. (SNo_PSNo_eta_) We take the following as an axiom:
∀alpha x, ordinal alpha → SNo_ alpha x → x = PSNo alpha (λbeta ⇒ beta ∈ x)
In Proofgold the corresponding term root is 1642af... and proposition id is 630119...
Primitive. The name SNo is a term of type set → prop.
In Proofgold the corresponding term root is 11faa7... and object id is 116b76...
L23
Axiom. (SNo_SNo) We take the following as an axiom:
∀alpha, ordinal alpha → ∀z, SNo_ alpha z → SNo z
In Proofgold the corresponding term root is 929b7a... and proposition id is a59341...
Primitive. The name SNoLev is a term of type set → set.
In Proofgold the corresponding term root is 293b77... and object id is 83dce3...
L26
Axiom. (SNoLev_uniq_Subq) We take the following as an axiom:
∀x alpha beta, ordinal alpha → ordinal beta → SNo_ alpha x → SNo_ beta x → alpha ⊆ beta
In Proofgold the corresponding term root is 2ca114... and proposition id is 65843d...
L27
Axiom. (SNoLev_uniq) We take the following as an axiom:
∀x alpha beta, ordinal alpha → ordinal beta → SNo_ alpha x → SNo_ beta x → alpha = beta
In Proofgold the corresponding term root is 68f71d... and proposition id is 5d96d4...
L28
Axiom. (SNoLev_prop) We take the following as an axiom:
∀x, SNo x → ordinal (SNoLev x) ∧ SNo_ (SNoLev x) x
In Proofgold the corresponding term root is a8afcc... and proposition id is 21761c...
L29
Axiom. (SNoLev_ordinal) We take the following as an axiom:
∀x, SNo x → ordinal (SNoLev x)
In Proofgold the corresponding term root is 7cacc5... and proposition id is f0e9f7...
L30
Axiom. (SNoLev_) We take the following as an axiom:
∀x, SNo x → SNo_ (SNoLev x) x
In Proofgold the corresponding term root is 4a1033... and proposition id is 49cd5a...
L31
Axiom. (SNo_PSNo_eta) We take the following as an axiom:
∀x, SNo x → x = PSNo (SNoLev x) (λbeta ⇒ beta ∈ x)
In Proofgold the corresponding term root is 6ffefe... and proposition id is 8c7870...
L32
Axiom. (SNoLev_PSNo) We take the following as an axiom:
∀alpha, ordinal alpha → ∀p : set → prop, SNoLev (PSNo alpha p) = alpha
In Proofgold the corresponding term root is 07f1eb... and proposition id is 9c4890...
L33
Axiom. (SNo_Subq) We take the following as an axiom:
∀x y, SNo x → SNo y → SNoLev x ⊆ SNoLev y → (∀alpha ∈ SNoLev x, alpha ∈ x ↔ alpha ∈ y) → x ⊆ y
In Proofgold the corresponding term root is a244d7... and proposition id is a428af...
L34
Definition. We define SNoEq_ to be λalpha x y ⇒ PNoEq_ alpha (λbeta ⇒ beta ∈ x) (λbeta ⇒ beta ∈ y) of type set → set → set → prop.
In Proofgold the corresponding term root is 5f11e2... and object id is 12b5f6...
L35
Axiom. (SNoEq_I) We take the following as an axiom:
∀alpha x y, (∀beta ∈ alpha, beta ∈ x ↔ beta ∈ y) → SNoEq_ alpha x y
In Proofgold the corresponding term root is a718b1... and proposition id is fdcb78...
L36
Axiom. (SNo_eq) We take the following as an axiom:
∀x y, SNo x → SNo y → SNoLev x = SNoLev y → SNoEq_ (SNoLev x) x y → x = y
In Proofgold the corresponding term root is b08bdc... and proposition id is bf4ac3...
End of Section TaggedSets
L38
Definition. We define SNoLt to be λx y ⇒ PNoLt (SNoLev x) (λbeta ⇒ beta ∈ x) (SNoLev y) (λbeta ⇒ beta ∈ y) of type set → set → prop.
In Proofgold the corresponding term root is 46e7ed... and object id is 8c8aa9...
Notation. We use < as an infix operator with priority 490 and no associativity corresponding to applying term SNoLt.
L40
Definition. We define SNoLe to be λx y ⇒ PNoLe (SNoLev x) (λbeta ⇒ beta ∈ x) (SNoLev y) (λbeta ⇒ beta ∈ y) of type set → set → prop.
In Proofgold the corresponding term root is ddf7d3... and object id is 54f405...
Notation. We use ≤ as an infix operator with priority 490 and no associativity corresponding to applying term SNoLe.
L43
Axiom. (SNoLtLe) We take the following as an axiom:
∀x y, x < y → x ≤ y
In Proofgold the corresponding term root is c0fef1... and proposition id is f09833...
L44
Axiom. (SNoLeE) We take the following as an axiom:
∀x y, SNo x → SNo y → x ≤ y → x < y ∨ x = y
In Proofgold the corresponding term root is 1c9c62... and proposition id is 23cc47...
L45
Axiom. (SNoEq_sym_) We take the following as an axiom:
∀alpha x y, SNoEq_ alpha x y → SNoEq_ alpha y x
In Proofgold the corresponding term root is f8c61d... and proposition id is f756d2...
L46
Axiom. (SNoEq_tra_) We take the following as an axiom:
∀alpha x y z, SNoEq_ alpha x y → SNoEq_ alpha y z → SNoEq_ alpha x z
In Proofgold the corresponding term root is 0fff96... and proposition id is 246d04...
L47
Axiom. (SNoLtE) We take the following as an axiom:
∀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
In Proofgold the corresponding term root is 958711... and proposition id is d12fc6...
L48
Axiom. (SNoLtI2) We take the following as an axiom:
∀x y, SNoLev x ∈ SNoLev y → SNoEq_ (SNoLev x) x y → SNoLev x ∈ y → x < y
In Proofgold the corresponding term root is 282b01... and proposition id is 82b82c...
L49
Axiom. (SNoLtI3) We take the following as an axiom:
∀x y, SNoLev y ∈ SNoLev x → SNoEq_ (SNoLev y) x y → SNoLev y ∉ x → x < y
In Proofgold the corresponding term root is 006afc... and proposition id is 938f67...
L50
Axiom. (SNoLt_irref) We take the following as an axiom:
∀x, ¬ SNoLt x x
In Proofgold the corresponding term root is d5ecf9... and proposition id is 06fac5...
L51
Axiom. (SNoLt_trichotomy_or) We take the following as an axiom:
∀x y, SNo x → SNo y → x < y ∨ x = y ∨ y < x
In Proofgold the corresponding term root is 35a4c8... and proposition id is 8ad056...
L52
Axiom. (SNoLt_trichotomy_or_impred) We take the following as an axiom:
∀x y, SNo x → SNo y → ∀p : prop, (x < y → p) → (x = y → p) → (y < x → p) → p
In Proofgold the corresponding term root is ba04ef... and proposition id is 7588e3...
L53
Axiom. (SNoLt_tra) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x < y → y < z → x < z
In Proofgold the corresponding term root is ac0e24... and proposition id is ccfdf7...
L54
Axiom. (SNoLe_ref) We take the following as an axiom:
∀x, SNoLe x x
In Proofgold the corresponding term root is c940c8... and proposition id is 83bd2d...
L55
Axiom. (SNoLe_antisym) We take the following as an axiom:
∀x y, SNo x → SNo y → x ≤ y → y ≤ x → x = y
In Proofgold the corresponding term root is f9f757... and proposition id is 3abee4...
L56
Axiom. (SNoLtLe_tra) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x < y → y ≤ z → x < z
In Proofgold the corresponding term root is 3bc661... and proposition id is ba8545...
L57
Axiom. (SNoLeLt_tra) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x ≤ y → y < z → x < z
In Proofgold the corresponding term root is b2178f... and proposition id is 4a77a2...
L58
Axiom. (SNoLe_tra) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x ≤ y → y ≤ z → x ≤ z
In Proofgold the corresponding term root is a0c5c6... and proposition id is 031989...
L59
Axiom. (SNoLtLe_or) We take the following as an axiom:
∀x y, SNo x → SNo y → x < y ∨ y ≤ x
In Proofgold the corresponding term root is f595ac... and proposition id is 8965d2...
L60
Axiom. (SNoLt_PSNo_PNoLt) We take the following as an axiom:
∀alpha beta, ∀p q : set → prop, ordinal alpha → ordinal beta → PSNo alpha p < PSNo beta q → PNoLt alpha p beta q
In Proofgold the corresponding term root is 6e122d... and proposition id is 535161...
L61
Axiom. (PNoLt_SNoLt_PSNo) We take the following as an axiom:
∀alpha beta, ∀p q : set → prop, ordinal alpha → ordinal beta → PNoLt alpha p beta q → PSNo alpha p < PSNo beta q
In Proofgold the corresponding term root is 11b6ed... and proposition id is 6196d9...
L62
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.
In Proofgold the corresponding term root is ec849e... and object id is 295bc4...
L63
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.
In Proofgold the corresponding term root is c083d8... and object id is 775127...
L64
Axiom. (SNoCutP_SNoCut) We take the following as an axiom:
∀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)
In Proofgold the corresponding term root is 9398b7... and proposition id is 66456c...
L65
Axiom. (SNoCutP_SNoCut_impred) We take the following as an axiom:
∀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
In Proofgold the corresponding term root is 02c4ae... and proposition id is 5bcc8f...
L66
Axiom. (SNoCutP_L_0) We take the following as an axiom:
∀L, (∀x ∈ L, SNo x) → SNoCutP L 0
In Proofgold the corresponding term root is 47329c... and proposition id is ba61e1...
L67
Axiom. (SNoCutP_0_R) We take the following as an axiom:
∀R, (∀x ∈ R, SNo x) → SNoCutP 0 R
In Proofgold the corresponding term root is 54eb82... and proposition id is a06bcd...
L68
Axiom. (SNoCutP_0_0) We take the following as an axiom:
SNoCutP 0 0
In Proofgold the corresponding term root is 3b144e... and proposition id is a5144d...
L69
Definition. We define SNoS_ to be λalpha ⇒ {x ∈ 𝒫 (SNoElts_ alpha)|∃beta ∈ alpha, SNo_ beta x} of type set → set.
In Proofgold the corresponding term root is d5069a... and object id is 4680ce...
L70
Axiom. (SNoS_E) We take the following as an axiom:
∀alpha, ordinal alpha → ∀x ∈ SNoS_ alpha, ∃beta ∈ alpha, SNo_ beta x
In Proofgold the corresponding term root is 970ce2... and proposition id is bb731c...
Beginning of Section TaggedSets2
L72
Let tag : set → set ≝ λalpha ⇒ SetAdjoin alpha {1}
Notation. We use ' as a postfix operator with priority 100 corresponding to applying term tag.
L74
Axiom. (SNoS_I) We take the following as an axiom:
∀alpha, ordinal alpha → ∀x, ∀beta ∈ alpha, SNo_ beta x → x ∈ SNoS_ alpha
In Proofgold the corresponding term root is f5227d... and proposition id is 04f24b...
L75
Axiom. (SNoS_I2) We take the following as an axiom:
∀x y, SNo x → SNo y → SNoLev x ∈ SNoLev y → x ∈ SNoS_ (SNoLev y)
In Proofgold the corresponding term root is 7a14c7... and proposition id is b4042d...
L76
Axiom. (SNoS_Subq) We take the following as an axiom:
∀alpha beta, ordinal alpha → ordinal beta → alpha ⊆ beta → SNoS_ alpha ⊆ SNoS_ beta
In Proofgold the corresponding term root is 6828e7... and proposition id is d928b8...
L77
Axiom. (SNoLev_uniq2) We take the following as an axiom:
∀alpha, ordinal alpha → ∀x, SNo_ alpha x → SNoLev x = alpha
In Proofgold the corresponding term root is fbb461... and proposition id is f48d47...
L78
Axiom. (SNoS_E2) We take the following as an axiom:
∀alpha, ordinal alpha → ∀x ∈ SNoS_ alpha, ∀p : prop, (SNoLev x ∈ alpha → ordinal (SNoLev x) → SNo x → SNo_ (SNoLev x) x → p) → p
In Proofgold the corresponding term root is deb031... and proposition id is 62b490...
L79
Axiom. (SNoS_In_neq) We take the following as an axiom:
∀w, SNo w → ∀x ∈ SNoS_ (SNoLev w), x ≠ w
In Proofgold the corresponding term root is ab85fd... and proposition id is d5dbd7...
L80
Axiom. (SNoS_SNoLev) We take the following as an axiom:
∀z, SNo z → z ∈ SNoS_ (ordsucc (SNoLev z))
In Proofgold the corresponding term root is a9ba1f... and proposition id is 8efb88...
L81
Definition. We define SNoL to be λz ⇒ {x ∈ SNoS_ (SNoLev z)|x < z} of type set → set.
In Proofgold the corresponding term root is 8cd812... and object id is 48bcf8...
L82
Definition. We define SNoR to be λz ⇒ {y ∈ SNoS_ (SNoLev z)|z < y} of type set → set.
In Proofgold the corresponding term root is 73b2b9... and object id is 0cfe87...
L83
Axiom. (SNoCutP_SNoL_SNoR) We take the following as an axiom:
∀z, SNo z → SNoCutP (SNoL z) (SNoR z)
In Proofgold the corresponding term root is 524866... and proposition id is 7aba57...
L84
Axiom. (SNoL_E) We take the following as an axiom:
∀x, SNo x → ∀w ∈ SNoL x, ∀p : prop, (SNo w → SNoLev w ∈ SNoLev x → w < x → p) → p
In Proofgold the corresponding term root is cead4f... and proposition id is 7ccd8b...
L85
Axiom. (SNoR_E) We take the following as an axiom:
∀x, SNo x → ∀z ∈ SNoR x, ∀p : prop, (SNo z → SNoLev z ∈ SNoLev x → x < z → p) → p
In Proofgold the corresponding term root is efca05... and proposition id is 7dca04...
L86
Axiom. (SNoL_SNoS_) We take the following as an axiom:
∀z, SNoL z ⊆ SNoS_ (SNoLev z)
In Proofgold the corresponding term root is 73f5b2... and proposition id is 409713...
L87
Axiom. (SNoR_SNoS_) We take the following as an axiom:
∀z, SNoR z ⊆ SNoS_ (SNoLev z)
In Proofgold the corresponding term root is 16bdfc... and proposition id is 2fe1c0...
L88
Axiom. (SNoL_SNoS) We take the following as an axiom:
∀x, SNo x → ∀w ∈ SNoL x, w ∈ SNoS_ (SNoLev x)
In Proofgold the corresponding term root is 6e3a22... and proposition id is ded78a...
L89
Axiom. (SNoR_SNoS) We take the following as an axiom:
∀x, SNo x → ∀z ∈ SNoR x, z ∈ SNoS_ (SNoLev x)
In Proofgold the corresponding term root is 98051c... and proposition id is e13f49...
L90
Axiom. (SNoL_I) We take the following as an axiom:
∀z, SNo z → ∀x, SNo x → SNoLev x ∈ SNoLev z → x < z → x ∈ SNoL z
In Proofgold the corresponding term root is ddd91b... and proposition id is 4f3d04...
L91
Axiom. (SNoR_I) We take the following as an axiom:
∀z, SNo z → ∀y, SNo y → SNoLev y ∈ SNoLev z → z < y → y ∈ SNoR z
In Proofgold the corresponding term root is 97693c... and proposition id is 383e88...
L92
Axiom. (SNo_eta) We take the following as an axiom:
∀z, SNo z → z = SNoCut (SNoL z) (SNoR z)
In Proofgold the corresponding term root is 3cc369... and proposition id is dc9273...
L93
Axiom. (SNoCutP_SNo_SNoCut) We take the following as an axiom:
∀L R, SNoCutP L R → SNo (SNoCut L R)
In Proofgold the corresponding term root is 9621aa... and proposition id is ae46e8...
L94
Axiom. (SNoCutP_SNoCut_L) We take the following as an axiom:
∀L R, SNoCutP L R → ∀x ∈ L, x < SNoCut L R
In Proofgold the corresponding term root is 984a30... and proposition id is 4bca14...
L95
Axiom. (SNoCutP_SNoCut_R) We take the following as an axiom:
∀L R, SNoCutP L R → ∀y ∈ R, SNoCut L R < y
In Proofgold the corresponding term root is 9161db... and proposition id is 7c3d12...
L96
Axiom. (SNoCutP_SNoCut_fst) We take the following as an axiom:
∀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
In Proofgold the corresponding term root is b52eb7... and proposition id is 8362f8...
L97
Axiom. (SNoCut_Le) We take the following as an axiom:
∀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
In Proofgold the corresponding term root is bb8cdc... and proposition id is 423731...
L98
Axiom. (SNoCut_ext) We take the following as an axiom:
∀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
In Proofgold the corresponding term root is c1078e... and proposition id is f66618...
L99
Axiom. (SNoLt_SNoL_or_SNoR_impred) We take the following as an axiom:
∀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
In Proofgold the corresponding term root is f3b15a... and proposition id is ffc0bf...
L100
Axiom. (SNoL_or_SNoR_impred) We take the following as an axiom:
∀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
In Proofgold the corresponding term root is f8a5e2... and proposition id is 68ba98...
L101
Axiom. (SNoL_SNoCutP_ex) We take the following as an axiom:
∀L R, SNoCutP L R → ∀w ∈ SNoL (SNoCut L R), ∃w' ∈ L, w ≤ w'
In Proofgold the corresponding term root is 3b4695... and proposition id is 6d8af6...
L102
Axiom. (SNoR_SNoCutP_ex) We take the following as an axiom:
∀L R, SNoCutP L R → ∀z ∈ SNoR (SNoCut L R), ∃z' ∈ R, z' ≤ z
In Proofgold the corresponding term root is ca7be2... and proposition id is bb0b53...
L103
Axiom. (ordinal_SNo_) We take the following as an axiom:
∀alpha, ordinal alpha → SNo_ alpha alpha
In Proofgold the corresponding term root is 4731fd... and proposition id is 7754e5...
L104
Axiom. (ordinal_SNo) We take the following as an axiom:
∀alpha, ordinal alpha → SNo alpha
In Proofgold the corresponding term root is ac39bc... and proposition id is 1eea33...
L105
Axiom. (ordinal_SNoLev) We take the following as an axiom:
∀alpha, ordinal alpha → SNoLev alpha = alpha
In Proofgold the corresponding term root is 56f8b0... and proposition id is fea5fc...
L106
Axiom. (ordinal_SNoLev_max) We take the following as an axiom:
∀alpha, ordinal alpha → ∀z, SNo z → SNoLev z ∈ alpha → z < alpha
In Proofgold the corresponding term root is 945794... and proposition id is 51ee47...
L107
Axiom. (ordinal_SNoL) We take the following as an axiom:
∀alpha, ordinal alpha → SNoL alpha = SNoS_ alpha
In Proofgold the corresponding term root is fef608... and proposition id is 95823e...
L108
Axiom. (ordinal_SNoR) We take the following as an axiom:
∀alpha, ordinal alpha → SNoR alpha = Empty
In Proofgold the corresponding term root is 07c69a... and proposition id is f853d9...
L109
Axiom. (nat_p_SNo) We take the following as an axiom:
∀n, nat_p n → SNo n
In Proofgold the corresponding term root is 0644f3... and proposition id is 5fd930...
L110
Axiom. (omega_SNo) We take the following as an axiom:
∀n ∈ ω, SNo n
In Proofgold the corresponding term root is d32269... and proposition id is d0f9c6...
L111
Axiom. (omega_SNoS_omega) We take the following as an axiom:
ω ⊆ SNoS_ ω
In Proofgold the corresponding term root is 4ba265... and proposition id is 2ccf7a...
L112
Axiom. (ordinal_In_SNoLt) We take the following as an axiom:
∀alpha, ordinal alpha → ∀beta ∈ alpha, beta < alpha
In Proofgold the corresponding term root is e37d00... and proposition id is ced78e...
L113
Axiom. (ordinal_SNoLev_max_2) We take the following as an axiom:
∀alpha, ordinal alpha → ∀z, SNo z → SNoLev z ∈ ordsucc alpha → z ≤ alpha
In Proofgold the corresponding term root is 72c5eb... and proposition id is c9a731...
L114
Axiom. (ordinal_Subq_SNoLe) We take the following as an axiom:
∀alpha beta, ordinal alpha → ordinal beta → alpha ⊆ beta → alpha ≤ beta
In Proofgold the corresponding term root is 7558ba... and proposition id is 15c58a...
L115
Axiom. (ordinal_SNoLt_In) We take the following as an axiom:
∀alpha beta, ordinal alpha → ordinal beta → alpha < beta → alpha ∈ beta
In Proofgold the corresponding term root is d6f066... and proposition id is de775b...
L116
Axiom. (omega_nonneg) We take the following as an axiom:
∀m ∈ ω, 0 ≤ m
In Proofgold the corresponding term root is ee67c9... and proposition id is eaf06b...
L117
Axiom. (SNo_0) We take the following as an axiom:
SNo 0
In Proofgold the corresponding term root is c8204b... and proposition id is 94a310...
L118
Axiom. (SNo_1) We take the following as an axiom:
SNo 1
In Proofgold the corresponding term root is ac50d7... and proposition id is 9a733a...
L119
Axiom. (SNo_2) We take the following as an axiom:
SNo 2
In Proofgold the corresponding term root is 487591... and proposition id is c524a4...
L120
Axiom. (SNoLev_0) We take the following as an axiom:
SNoLev 0 = 0
In Proofgold the corresponding term root is 45a0f7... and proposition id is 3527a4...
L121
Axiom. (SNoCut_0_0) We take the following as an axiom:
SNoCut 0 0 = 0
In Proofgold the corresponding term root is 6a1f81... and proposition id is abbffb...
L122
Axiom. (SNoL_0) We take the following as an axiom:
SNoL 0 = 0
In Proofgold the corresponding term root is c01c2b... and proposition id is fdaa69...
L123
Axiom. (SNoR_0) We take the following as an axiom:
SNoR 0 = 0
In Proofgold the corresponding term root is 7329c7... and proposition id is 510751...
L124
Axiom. (SNoL_1) We take the following as an axiom:
SNoL 1 = 1
In Proofgold the corresponding term root is 84d688... and proposition id is 15aa79...
L125
Axiom. (SNoR_1) We take the following as an axiom:
SNoR 1 = 0
In Proofgold the corresponding term root is e6a83a... and proposition id is 8da427...
L126
Axiom. (SNo_max_SNoLev) We take the following as an axiom:
∀x, SNo x → (∀y ∈ SNoS_ (SNoLev x), y < x) → SNoLev x = x
In Proofgold the corresponding term root is ff019e... and proposition id is 3be246...
L127
Axiom. (SNo_max_ordinal) We take the following as an axiom:
∀x, SNo x → (∀y ∈ SNoS_ (SNoLev x), y < x) → ordinal x
In Proofgold the corresponding term root is 0b230c... and proposition id is f28b9a...
L128
Axiom. (pos_low_eq_one) We take the following as an axiom:
∀x, SNo x → 0 < x → SNoLev x ⊆ 1 → x = 1
In Proofgold the corresponding term root is 7c84ef... and proposition id is db40ad...
L129
Definition. We define SNo_extend0 to be λx ⇒ PSNo (ordsucc (SNoLev x)) (λdelta ⇒ delta ∈ x ∧ delta ≠ SNoLev x) of type set → set.
In Proofgold the corresponding term root is 997d91... and object id is ff4161...
L130
Definition. We define SNo_extend1 to be λx ⇒ PSNo (ordsucc (SNoLev x)) (λdelta ⇒ delta ∈ x ∨ delta = SNoLev x) of type set → set.
In Proofgold the corresponding term root is 464e47... and object id is 8c551b...
L131
Axiom. (SNo_extend0_SNo_) We take the following as an axiom:
∀x, SNo x → SNo_ (ordsucc (SNoLev x)) (SNo_extend0 x)
In Proofgold the corresponding term root is d41d3e... and proposition id is c8f8ea...
L132
Axiom. (SNo_extend1_SNo_) We take the following as an axiom:
∀x, SNo x → SNo_ (ordsucc (SNoLev x)) (SNo_extend1 x)
In Proofgold the corresponding term root is b7b866... and proposition id is 73bbf2...
L133
Axiom. (SNo_extend0_SNo) We take the following as an axiom:
∀x, SNo x → SNo (SNo_extend0 x)
In Proofgold the corresponding term root is b353a2... and proposition id is 76562c...
L134
Axiom. (SNo_extend1_SNo) We take the following as an axiom:
∀x, SNo x → SNo (SNo_extend1 x)
In Proofgold the corresponding term root is fa323a... and proposition id is 5345a7...
L135
Axiom. (SNo_extend0_SNoLev) We take the following as an axiom:
∀x, SNo x → SNoLev (SNo_extend0 x) = ordsucc (SNoLev x)
In Proofgold the corresponding term root is 26efcd... and proposition id is 5aa0af...
L136
Axiom. (SNo_extend1_SNoLev) We take the following as an axiom:
∀x, SNo x → SNoLev (SNo_extend1 x) = ordsucc (SNoLev x)
In Proofgold the corresponding term root is 33cf60... and proposition id is 529347...
L137
Axiom. (SNo_extend0_nIn) We take the following as an axiom:
∀x, SNo x → SNoLev x ∉ SNo_extend0 x
In Proofgold the corresponding term root is 217cff... and proposition id is 0dfd17...
L138
Axiom. (SNo_extend1_In) We take the following as an axiom:
∀x, SNo x → SNoLev x ∈ SNo_extend1 x
In Proofgold the corresponding term root is ac9570... and proposition id is 8ca372...
L139
Axiom. (SNo_extend0_SNoEq) We take the following as an axiom:
∀x, SNo x → SNoEq_ (SNoLev x) (SNo_extend0 x) x
In Proofgold the corresponding term root is bd4a27... and proposition id is 129986...
L140
Axiom. (SNo_extend1_SNoEq) We take the following as an axiom:
∀x, SNo x → SNoEq_ (SNoLev x) (SNo_extend1 x) x
In Proofgold the corresponding term root is ba974f... and proposition id is d6f8bb...
L141
Axiom. (SNoLev_0_eq_0) We take the following as an axiom:
∀x, SNo x → SNoLev x = 0 → x = 0
In Proofgold the corresponding term root is fe0bc4... and proposition id is dfcf39...
L142
Axiom. (SNo_0_eq_0) We take the following as an axiom:
∀q, SNo_ 0 q → q = 0
In Proofgold the corresponding term root is 72efa8... and proposition id is 7bd751...
L143
Definition. We define eps_ to be λn ⇒ {0} ∪ {(ordsucc m) '|m ∈ n} of type set → set.
In Proofgold the corresponding term root is 5e992a... and object id is ffee2b...
L144
Axiom. (eps_ordinal_In_eq_0) We take the following as an axiom:
∀n alpha, ordinal alpha → alpha ∈ eps_ n → alpha = 0
In Proofgold the corresponding term root is 3046fd... and proposition id is 1190f3...
L145
Axiom. (eps_0_1) We take the following as an axiom:
eps_ 0 = 1
In Proofgold the corresponding term root is 5bbce1... and proposition id is d073f0...
L146
Axiom. (SNo__eps_) We take the following as an axiom:
∀n ∈ ω, SNo_ (ordsucc n) (eps_ n)
In Proofgold the corresponding term root is e9c4d9... and proposition id is 1c1428...
L147
Axiom. (SNo_eps_) We take the following as an axiom:
∀n ∈ ω, SNo (eps_ n)
In Proofgold the corresponding term root is 9fb700... and proposition id is 006b0f...
L148
Axiom. (SNo_eps_1) We take the following as an axiom:
SNo (eps_ 1)
In Proofgold the corresponding term root is 17c276... and proposition id is 8b78d7...
L149
Axiom. (SNoLev_eps_) We take the following as an axiom:
∀n ∈ ω, SNoLev (eps_ n) = ordsucc n
In Proofgold the corresponding term root is 6891e3... and proposition id is 75efd1...
L150
Axiom. (SNo_eps_SNoS_omega) We take the following as an axiom:
∀n ∈ ω, eps_ n ∈ SNoS_ ω
In Proofgold the corresponding term root is 736d2a... and proposition id is 52da18...
L151
Axiom. (SNo_eps_decr) We take the following as an axiom:
∀n ∈ ω, ∀m ∈ n, eps_ n < eps_ m
In Proofgold the corresponding term root is d6a46a... and proposition id is 67c76a...
L152
Axiom. (SNo_eps_pos) We take the following as an axiom:
∀n ∈ ω, 0 < eps_ n
In Proofgold the corresponding term root is 8b75de... and proposition id is 760b4a...
L153
Axiom. (SNo_pos_eps_Lt) We take the following as an axiom:
∀n, nat_p n → ∀x ∈ SNoS_ (ordsucc n), 0 < x → eps_ n < x
In Proofgold the corresponding term root is 72974f... and proposition id is 771b0e...
L154
Axiom. (SNo_pos_eps_Le) We take the following as an axiom:
∀n, nat_p n → ∀x ∈ SNoS_ (ordsucc (ordsucc n)), 0 < x → eps_ n ≤ x
In Proofgold the corresponding term root is f1e297... and proposition id is 6658de...
L155
Axiom. (eps_SNo_eq) We take the following as an axiom:
∀n, nat_p n → ∀x ∈ SNoS_ (ordsucc n), 0 < x → SNoEq_ (SNoLev x) (eps_ n) x → ∃m ∈ n, x = eps_ m
In Proofgold the corresponding term root is 8c2587... and proposition id is 8515ac...
L156
Axiom. (eps_SNoCutP) We take the following as an axiom:
∀n ∈ ω, SNoCutP {0} {eps_ m|m ∈ n}
In Proofgold the corresponding term root is 545873... and proposition id is 30edf9...
L157
Axiom. (eps_SNoCut) We take the following as an axiom:
∀n ∈ ω, eps_ n = SNoCut {0} {eps_ m|m ∈ n}
In Proofgold the corresponding term root is 06d6c5... and proposition id is eba0c6...
End of Section TaggedSets2
L159
Axiom. (SNo_etaE) We take the following as an axiom:
∀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
In Proofgold the corresponding term root is c24473... and proposition id is 109f1d...
L160
Axiom. (SNo_ind) We take the following as an axiom:
∀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
In Proofgold the corresponding term root is 5b4c39... and proposition id is 94cbe6...
Beginning of Section SurrealRecI
L162
Variable F : set → (set → set) → set
L163
Let default : set ≝ Eps_i (λ_ ⇒ True)
L164
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)
Primitive. The name SNo_rec_i is a term of type set → set.
In Proofgold the corresponding term root is be45df... and object id is 230ba8...
L167
Hypothesis Fr : ∀z, SNo z → ∀g h : set → set, (∀w ∈ SNoS_ (SNoLev z), g w = h w) → F z g = F z h
L168
Axiom. (SNo_rec_i_eq) We take the following as an axiom:
∀z, SNo z → SNo_rec_i z = F z SNo_rec_i
In Proofgold the corresponding term root is d5ffa8... and proposition id is f547c8...
End of Section SurrealRecI
Beginning of Section SurrealRecII
L171
Variable F : set → (set → (set → set)) → (set → set)
L172
Let default : (set → set) ≝ Descr_ii (λ_ ⇒ True)
L173
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)
Primitive. The name SNo_rec_ii is a term of type set → (set → set).
In Proofgold the corresponding term root is e148e6... and object id is c3f218...
L176
Hypothesis Fr : ∀z, SNo z → ∀g h : set → (set → set), (∀w ∈ SNoS_ (SNoLev z), g w = h w) → F z g = F z h
L177
Axiom. (SNo_rec_ii_eq) We take the following as an axiom:
∀z, SNo z → SNo_rec_ii z = F z SNo_rec_ii
In Proofgold the corresponding term root is 39e866... and proposition id is 1c5373...
End of Section SurrealRecII
Beginning of Section SurrealRec2
L180
Variable F : set → set → (set → set → set) → set
L181
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)
L182
Let H : set → (set → set → set) → set → set ≝ λw f z ⇒ if SNo z then SNo_rec_i (G w f) z else Empty
Primitive. The name SNo_rec2 is a term of type set → set → set.
In Proofgold the corresponding term root is 7d10ab... and object id is 951110...
L185
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
L186
Axiom. (SNo_rec2_G_prop) We take the following as an axiom:
∀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
In Proofgold the corresponding term root is 0f875d... and proposition id is de8737...
L187
Axiom. (SNo_rec2_eq_1) We take the following as an axiom:
∀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))
In Proofgold the corresponding term root is 12a51a... and proposition id is 0dc50e...
L188
Axiom. (SNo_rec2_eq) We take the following as an axiom:
∀w, SNo w → ∀z, SNo z → SNo_rec2 w z = F w z SNo_rec2
In Proofgold the corresponding term root is e9ea41... and proposition id is ac9f2b...
End of Section SurrealRec2
L190
Axiom. (SNo_ordinal_ind) We take the following as an axiom:
∀P : set → prop, (∀alpha, ordinal alpha → ∀x ∈ SNoS_ alpha, P x) → (∀x, SNo x → P x)
In Proofgold the corresponding term root is 5b75fb... and proposition id is dc2c6d...
L191
Axiom. (SNo_ordinal_ind2) We take the following as an axiom:
∀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)
In Proofgold the corresponding term root is ba3315... and proposition id is 4cd5ac...
L192
Axiom. (SNo_ordinal_ind3) We take the following as an axiom:
∀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)
In Proofgold the corresponding term root is fccdb6... and proposition id is dece8c...
L193
Axiom. (SNoLev_ind) We take the following as an axiom:
∀P : set → prop, (∀x, SNo x → (∀w ∈ SNoS_ (SNoLev x), P w) → P x) → (∀x, SNo x → P x)
In Proofgold the corresponding term root is 8b2b42... and proposition id is 851a88...
L194
Axiom. (SNoLev_ind2) We take the following as an axiom:
∀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
In Proofgold the corresponding term root is 87eb9a... and proposition id is 800d4c...
L195
Axiom. (SNoLev_ind3) We take the following as an axiom:
∀P : set → set → set → prop, (∀x y z, SNo x → SNo y → SNo z → (∀u ∈ SNoS_ (SNoLev x), P u y z) → (∀v ∈ SNoS_ (SNoLev y), P x v z) → (∀w ∈ SNoS_ (SNoLev z), P x y w) → (∀u ∈ SNoS_ (SNoLev x), ∀v ∈ SNoS_ (SNoLev y), P u v z) → (∀u ∈ SNoS_ (SNoLev x), ∀w ∈ SNoS_ (SNoLev z), P u y w) → (∀v ∈ SNoS_ (SNoLev y), ∀w ∈ SNoS_ (SNoLev z), P x v w) → (∀u ∈ SNoS_ (SNoLev x), ∀v ∈ SNoS_ (SNoLev y), ∀w ∈ SNoS_ (SNoLev z), P u v w) → P x y z) → ∀x y z, SNo x → SNo y → SNo z → P x y z
In Proofgold the corresponding term root is f1d779... and proposition id is ee16b9...
L196
Axiom. (SNo_omega) We take the following as an axiom:
SNo ω
In Proofgold the corresponding term root is f65848... and proposition id is db7b5f...
L197
Axiom. (SNoLt_0_1) We take the following as an axiom:
0 < 1
In Proofgold the corresponding term root is dd6047... and proposition id is cb6392...
L198
Axiom. (SNoLt_0_2) We take the following as an axiom:
0 < 2
In Proofgold the corresponding term root is 7be36f... and proposition id is f46934...
L199
Axiom. (SNoLt_1_2) We take the following as an axiom:
1 < 2
In Proofgold the corresponding term root is cc44e8... and proposition id is 19d5e1...
L200
Axiom. (restr_SNo_) We take the following as an axiom:
∀x, SNo x → ∀alpha ∈ SNoLev x, SNo_ alpha (x ∩ SNoElts_ alpha)
In Proofgold the corresponding term root is d78444... and proposition id is e0eca8...
L201
Axiom. (restr_SNo) We take the following as an axiom:
∀x, SNo x → ∀alpha ∈ SNoLev x, SNo (x ∩ SNoElts_ alpha)
In Proofgold the corresponding term root is 930b56... and proposition id is d141ed...
L202
Axiom. (restr_SNoLev) We take the following as an axiom:
∀x, SNo x → ∀alpha ∈ SNoLev x, SNoLev (x ∩ SNoElts_ alpha) = alpha
In Proofgold the corresponding term root is cae8b5... and proposition id is 8b1853...
L203
Axiom. (restr_SNoEq) We take the following as an axiom:
∀x, SNo x → ∀alpha ∈ SNoLev x, SNoEq_ alpha (x ∩ SNoElts_ alpha) x
In Proofgold the corresponding term root is 829f8b... and proposition id is 704f5a...
L204
Axiom. (SNo_extend0_restr_eq) We take the following as an axiom:
∀x, SNo x → x = SNo_extend0 x ∩ SNoElts_ (SNoLev x)
In Proofgold the corresponding term root is 2c202e... and proposition id is 9827a9...
L205
Axiom. (SNo_extend1_restr_eq) We take the following as an axiom:
∀x, SNo x → x = SNo_extend1 x ∩ SNoElts_ (SNoLev x)
In Proofgold the corresponding term root is 75bbe8... and proposition id is 275196...