Beginning of Section TaggedSets

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

Notation. We use ' as a postfix operator with priority 100 corresponding to applying term tag.

Theorem. (not_TransSet_Sing1)

¬ TransSet {1}

In Proofgold the corresponding term root is 8f2d67... and proposition id is be9a70...

Proof:
Proof not loaded.

Theorem. (not_ordinal_Sing1)

¬ ordinal {1}

In Proofgold the corresponding term root is 99a3f6... and proposition id is db7977...

Proof:
Proof not loaded.

Theorem. (tagged_not_ordinal)

∀y, ¬ ordinal (y ')

In Proofgold the corresponding term root is f9488c... and proposition id is aaf6e4...

Proof:
Proof not loaded.

Theorem. (tagged_notin_ordinal)

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

In Proofgold the corresponding term root is b603ba... and proposition id is c0e2c3...

Proof:
Proof not loaded.

Theorem. (tagged_eqE_Subq)

∀alpha beta, ordinal alpha → alpha ' = beta ' → alpha ⊆ beta

In Proofgold the corresponding term root is cf032f... and proposition id is ef37f5...

Proof:
Proof not loaded.

Theorem. (tagged_eqE_eq)

∀alpha beta, ordinal alpha → ordinal beta → alpha ' = beta ' → alpha = beta

In Proofgold the corresponding term root is 1f7dc9... and proposition id is ec1608...

Proof:
Proof not loaded.

Theorem. (tagged_ReplE)

∀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...

Proof:
Proof not loaded.

Theorem. (ordinal_notin_tagged_Repl)

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

In Proofgold the corresponding term root is 7f35b5... and proposition id is e7ff3b...

Proof:
Proof not loaded.

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

Theorem. (SNoElts_mon)

∀alpha beta, alpha ⊆ beta → SNoElts_ alpha ⊆ SNoElts_ beta

In Proofgold the corresponding term root is 49a08e... and proposition id is 859611...

Proof:
Proof not loaded.

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

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

Theorem. (PNoEq_PSNo)

∀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...

Proof:
Proof not loaded.

Theorem. (SNo_PSNo)

∀alpha, ordinal alpha → ∀p : set → prop, SNo_ alpha (PSNo alpha p)

In Proofgold the corresponding term root is 96e4e2... and proposition id is f03db0...

Proof:
Proof not loaded.

Theorem. (SNo_PSNo_eta_)

∀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...

Proof:
Proof not loaded.

Definition. We define SNo to be λx ⇒ ∃alpha, ordinal alpha ∧ SNo_ alpha x of type set → prop.

In Proofgold the corresponding term root is 11faa7... and object id is 116b76...

Theorem. (SNo_SNo)

∀alpha, ordinal alpha → ∀z, SNo_ alpha z → SNo z

In Proofgold the corresponding term root is 929b7a... and proposition id is a59341...

Proof:
Proof not loaded.

Definition. We define SNoLev to be λx ⇒ Eps_i (λalpha ⇒ ordinal alpha ∧ SNo_ alpha x) of type set → set.

In Proofgold the corresponding term root is 293b77... and object id is 83dce3...

Theorem. (SNoLev_uniq_Subq)

∀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...

Proof:
Proof not loaded.

Theorem. (SNoLev_uniq)

∀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...

Proof:
Proof not loaded.

Theorem. (SNoLev_prop)

∀x, SNo x → ordinal (SNoLev x) ∧ SNo_ (SNoLev x) x

In Proofgold the corresponding term root is a8afcc... and proposition id is 21761c...

Proof:
Proof not loaded.

Theorem. (SNoLev_ordinal)

∀x, SNo x → ordinal (SNoLev x)

In Proofgold the corresponding term root is 7cacc5... and proposition id is f0e9f7...

Proof:
Proof not loaded.

Theorem. (SNoLev_)

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

In Proofgold the corresponding term root is 4a1033... and proposition id is 49cd5a...

Proof:
Proof not loaded.

Theorem. (SNo_PSNo_eta)

∀x, SNo x → x = PSNo (SNoLev x) (λbeta ⇒ beta ∈ x)

In Proofgold the corresponding term root is 6ffefe... and proposition id is 8c7870...

Proof:
Proof not loaded.

Theorem. (SNoLev_PSNo)

∀alpha, ordinal alpha → ∀p : set → prop, SNoLev (PSNo alpha p) = alpha

In Proofgold the corresponding term root is 07f1eb... and proposition id is 9c4890...

Proof:
Proof not loaded.

Theorem. (SNo_Subq)

∀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...

Proof:
Proof not loaded.

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

Theorem. (SNoEq_I)

∀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...

Proof:
Proof not loaded.

Theorem. (SNo_eq)

∀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...

Proof:
Proof not loaded.

End of Section TaggedSets

Beginning of Section TaggedSets2

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

Notation. We use ' as a postfix operator with priority 100 corresponding to applying term tag.

Theorem. (SNoS_I)

∀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...

Proof:
Proof not loaded.

Theorem. (SNoS_I2)

∀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...

Proof:
Proof not loaded.

Theorem. (SNoS_Subq)

∀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...

Proof:
Proof not loaded.

Theorem. (SNoLev_uniq2)

∀alpha, ordinal alpha → ∀x, SNo_ alpha x → SNoLev x = alpha

In Proofgold the corresponding term root is fbb461... and proposition id is f48d47...

Proof:
Proof not loaded.

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

In Proofgold the corresponding term root is deb031... and proposition id is 62b490...

Proof:
Proof not loaded.

Theorem. (SNoS_In_neq)

∀w, SNo w → ∀x ∈ SNoS_ (SNoLev w), x ≠ w

In Proofgold the corresponding term root is ab85fd... and proposition id is d5dbd7...

Proof:
Proof not loaded.

Theorem. (SNoS_SNoLev)

∀z, SNo z → z ∈ SNoS_ (ordsucc (SNoLev z))

In Proofgold the corresponding term root is a9ba1f... and proposition id is 8efb88...

Proof:
Proof not loaded.

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

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

Theorem. (SNoCutP_SNoL_SNoR)

∀z, SNo z → SNoCutP (SNoL z) (SNoR z)

In Proofgold the corresponding term root is 524866... and proposition id is 7aba57...

Proof:
Proof not loaded.

Theorem. (SNoL_E)

∀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...

Proof:
Proof not loaded.

Theorem. (SNoR_E)

∀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...

Proof:
Proof not loaded.

Theorem. (SNoL_SNoS_)

∀z, SNoL z ⊆ SNoS_ (SNoLev z)

In Proofgold the corresponding term root is 73f5b2... and proposition id is 409713...

Proof:
Proof not loaded.

Theorem. (SNoR_SNoS_)

∀z, SNoR z ⊆ SNoS_ (SNoLev z)

In Proofgold the corresponding term root is 16bdfc... and proposition id is 2fe1c0...

Proof:
Proof not loaded.

Theorem. (SNoL_SNoS)

∀x, SNo x → ∀w ∈ SNoL x, w ∈ SNoS_ (SNoLev x)

In Proofgold the corresponding term root is 6e3a22... and proposition id is ded78a...

Proof:
Proof not loaded.

Theorem. (SNoR_SNoS)

∀x, SNo x → ∀z ∈ SNoR x, z ∈ SNoS_ (SNoLev x)

In Proofgold the corresponding term root is 98051c... and proposition id is e13f49...

Proof:
Proof not loaded.

Theorem. (SNoL_I)

∀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...

Proof:
Proof not loaded.

Theorem. (SNoR_I)

∀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...

Proof:
Proof not loaded.

Theorem. (SNo_eta)

∀z, SNo z → z = SNoCut (SNoL z) (SNoR z)

In Proofgold the corresponding term root is 3cc369... and proposition id is dc9273...

Proof:
Proof not loaded.

Theorem. (SNoCutP_SNo_SNoCut)

∀L R, SNoCutP L R → SNo (SNoCut L R)

In Proofgold the corresponding term root is 9621aa... and proposition id is ae46e8...

Proof:
Proof not loaded.

Theorem. (SNoCutP_SNoCut_L)

∀L R, SNoCutP L R → ∀x ∈ L, x < SNoCut L R

In Proofgold the corresponding term root is 984a30... and proposition id is 4bca14...

Proof:
Proof not loaded.

Theorem. (SNoCutP_SNoCut_R)

∀L R, SNoCutP L R → ∀y ∈ R, SNoCut L R < y

In Proofgold the corresponding term root is 9161db... and proposition id is 7c3d12...

Proof:
Proof not loaded.

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

In Proofgold the corresponding term root is b52eb7... and proposition id is 8362f8...

Proof:
Proof not loaded.

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

In Proofgold the corresponding term root is bb8cdc... and proposition id is 423731...

Proof:
Proof not loaded.

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

In Proofgold the corresponding term root is c1078e... and proposition id is f66618...

Proof:
Proof not loaded.

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

In Proofgold the corresponding term root is f3b15a... and proposition id is ffc0bf...

Proof:
Proof not loaded.

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

In Proofgold the corresponding term root is f8a5e2... and proposition id is 68ba98...

Proof:
Proof not loaded.

Theorem. (SNoL_SNoCutP_ex)

∀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...

Proof:
Proof not loaded.

Theorem. (SNoR_SNoCutP_ex)

∀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...

Proof:
Proof not loaded.

Theorem. (ordinal_SNo_)

∀alpha, ordinal alpha → SNo_ alpha alpha

In Proofgold the corresponding term root is 4731fd... and proposition id is 7754e5...

Proof:
Proof not loaded.

Theorem. (ordinal_SNo)

∀alpha, ordinal alpha → SNo alpha

In Proofgold the corresponding term root is ac39bc... and proposition id is 1eea33...

Proof:
Proof not loaded.

Theorem. (ordinal_SNoLev)

∀alpha, ordinal alpha → SNoLev alpha = alpha

In Proofgold the corresponding term root is 56f8b0... and proposition id is fea5fc...

Proof:
Proof not loaded.

Theorem. (ordinal_SNoLev_max)

∀alpha, ordinal alpha → ∀z, SNo z → SNoLev z ∈ alpha → z < alpha

In Proofgold the corresponding term root is 945794... and proposition id is 51ee47...

Proof:
Proof not loaded.

Theorem. (ordinal_SNoL)

∀alpha, ordinal alpha → SNoL alpha = SNoS_ alpha

In Proofgold the corresponding term root is fef608... and proposition id is 95823e...

Proof:
Proof not loaded.

Theorem. (ordinal_SNoR)

∀alpha, ordinal alpha → SNoR alpha = Empty

In Proofgold the corresponding term root is 07c69a... and proposition id is f853d9...

Proof:
Proof not loaded.

Theorem. (nat_p_SNo)

∀n, nat_p n → SNo n

In Proofgold the corresponding term root is 0644f3... and proposition id is 5fd930...

Proof:
Proof not loaded.

Theorem. (omega_SNo)

∀n ∈ ω, SNo n

In Proofgold the corresponding term root is d32269... and proposition id is d0f9c6...

Proof:
Proof not loaded.

Theorem. (omega_SNoS_omega)

ω ⊆ SNoS_ ω

In Proofgold the corresponding term root is 4ba265... and proposition id is 2ccf7a...

Proof:
Proof not loaded.

Theorem. (ordinal_In_SNoLt)

∀alpha, ordinal alpha → ∀beta ∈ alpha, beta < alpha

In Proofgold the corresponding term root is e37d00... and proposition id is ced78e...

Proof:
Proof not loaded.

Theorem. (ordinal_SNoLev_max_2)

∀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...

Proof:
Proof not loaded.

Theorem. (ordinal_Subq_SNoLe)

∀alpha beta, ordinal alpha → ordinal beta → alpha ⊆ beta → alpha ≤ beta

In Proofgold the corresponding term root is 7558ba... and proposition id is 15c58a...

Proof:
Proof not loaded.

Theorem. (ordinal_SNoLt_In)

∀alpha beta, ordinal alpha → ordinal beta → alpha < beta → alpha ∈ beta

In Proofgold the corresponding term root is d6f066... and proposition id is de775b...

Proof:
Proof not loaded.

Theorem. (omega_nonneg)

∀m ∈ ω, 0 ≤ m

In Proofgold the corresponding term root is ee67c9... and proposition id is eaf06b...

Proof:
Proof not loaded.

Theorem. (SNo_0)

SNo 0

In Proofgold the corresponding term root is c8204b... and proposition id is 94a310...

Proof:
Proof not loaded.

Theorem. (SNo_1)

SNo 1

In Proofgold the corresponding term root is ac50d7... and proposition id is 9a733a...

Proof:
Proof not loaded.

Theorem. (SNo_2)

SNo 2

In Proofgold the corresponding term root is 487591... and proposition id is c524a4...

Proof:
Proof not loaded.

Theorem. (SNoLev_0)

SNoLev 0 = 0

In Proofgold the corresponding term root is 45a0f7... and proposition id is 3527a4...

Proof:
Proof not loaded.

Theorem. (SNoCut_0_0)

SNoCut 0 0 = 0

In Proofgold the corresponding term root is 6a1f81... and proposition id is abbffb...

Proof:
Proof not loaded.

Theorem. (SNoL_0)

SNoL 0 = 0

In Proofgold the corresponding term root is c01c2b... and proposition id is fdaa69...

Proof:
Proof not loaded.

Theorem. (SNoR_0)

SNoR 0 = 0

In Proofgold the corresponding term root is 7329c7... and proposition id is 510751...

Proof:
Proof not loaded.

Theorem. (SNoL_1)

SNoL 1 = 1

In Proofgold the corresponding term root is 84d688... and proposition id is 15aa79...

Proof:
Proof not loaded.

Theorem. (SNoR_1)

SNoR 1 = 0

In Proofgold the corresponding term root is e6a83a... and proposition id is 8da427...

Proof:
Proof not loaded.

Theorem. (SNo_max_SNoLev)

∀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...

Proof:
Proof not loaded.

Theorem. (SNo_max_ordinal)

∀x, SNo x → (∀y ∈ SNoS_ (SNoLev x), y < x) → ordinal x

In Proofgold the corresponding term root is 0b230c... and proposition id is f28b9a...

Proof:
Proof not loaded.

Theorem. (pos_low_eq_one)

∀x, SNo x → 0 < x → SNoLev x ⊆ 1 → x = 1

In Proofgold the corresponding term root is 7c84ef... and proposition id is db40ad...

Proof:
Proof not loaded.

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

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

Theorem. (SNo_extend0_SNo_)

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

In Proofgold the corresponding term root is d41d3e... and proposition id is c8f8ea...

Proof:
Proof not loaded.

Theorem. (SNo_extend1_SNo_)

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

In Proofgold the corresponding term root is b7b866... and proposition id is 73bbf2...

Proof:
Proof not loaded.

Theorem. (SNo_extend0_SNo)

∀x, SNo x → SNo (SNo_extend0 x)

In Proofgold the corresponding term root is b353a2... and proposition id is 76562c...

Proof:
Proof not loaded.

Theorem. (SNo_extend1_SNo)

∀x, SNo x → SNo (SNo_extend1 x)

In Proofgold the corresponding term root is fa323a... and proposition id is 5345a7...

Proof:
Proof not loaded.

Theorem. (SNo_extend0_SNoLev)

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

In Proofgold the corresponding term root is 26efcd... and proposition id is 5aa0af...

Proof:
Proof not loaded.

Theorem. (SNo_extend1_SNoLev)

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

In Proofgold the corresponding term root is 33cf60... and proposition id is 529347...

Proof:
Proof not loaded.

Theorem. (SNo_extend0_nIn)

∀x, SNo x → SNoLev x ∉ SNo_extend0 x

In Proofgold the corresponding term root is 217cff... and proposition id is 0dfd17...

Proof:
Proof not loaded.

Theorem. (SNo_extend1_In)

∀x, SNo x → SNoLev x ∈ SNo_extend1 x

In Proofgold the corresponding term root is ac9570... and proposition id is 8ca372...

Proof:
Proof not loaded.

Theorem. (SNo_extend0_SNoEq)

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

In Proofgold the corresponding term root is bd4a27... and proposition id is 129986...

Proof:
Proof not loaded.

Theorem. (SNo_extend1_SNoEq)

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

In Proofgold the corresponding term root is ba974f... and proposition id is d6f8bb...

Proof:
Proof not loaded.

Theorem. (SNoLev_0_eq_0)

∀x, SNo x → SNoLev x = 0 → x = 0

In Proofgold the corresponding term root is fe0bc4... and proposition id is dfcf39...

Proof:
Proof not loaded.

Theorem. (SNo_0_eq_0)

∀q, SNo_ 0 q → q = 0

In Proofgold the corresponding term root is 72efa8... and proposition id is 7bd751...

Proof:
Proof not loaded.

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

Theorem. (eps_ordinal_In_eq_0)

∀n alpha, ordinal alpha → alpha ∈ eps_ n → alpha = 0

In Proofgold the corresponding term root is 3046fd... and proposition id is 1190f3...

Proof:
Proof not loaded.

Theorem. (eps_0_1)

eps_ 0 = 1

In Proofgold the corresponding term root is 5bbce1... and proposition id is d073f0...

Proof:
Proof not loaded.

Theorem. (SNo__eps_)

∀n ∈ ω, SNo_ (ordsucc n) (eps_ n)

In Proofgold the corresponding term root is e9c4d9... and proposition id is 1c1428...

Proof:
Proof not loaded.

Theorem. (SNo_eps_)

∀n ∈ ω, SNo (eps_ n)

In Proofgold the corresponding term root is 9fb700... and proposition id is 006b0f...

Proof:
Proof not loaded.

Theorem. (SNo_eps_1)

SNo (eps_ 1)

In Proofgold the corresponding term root is 17c276... and proposition id is 8b78d7...

Proof:
Proof not loaded.

Theorem. (SNoLev_eps_)

∀n ∈ ω, SNoLev (eps_ n) = ordsucc n

In Proofgold the corresponding term root is 6891e3... and proposition id is 75efd1...

Proof:
Proof not loaded.

Theorem. (SNo_eps_SNoS_omega)

∀n ∈ ω, eps_ n ∈ SNoS_ ω

In Proofgold the corresponding term root is 736d2a... and proposition id is 52da18...

Proof:
Proof not loaded.

Theorem. (SNo_eps_decr)

∀n ∈ ω, ∀m ∈ n, eps_ n < eps_ m

In Proofgold the corresponding term root is d6a46a... and proposition id is 67c76a...

Proof:
Proof not loaded.

Theorem. (SNo_eps_pos)

∀n ∈ ω, 0 < eps_ n

In Proofgold the corresponding term root is 8b75de... and proposition id is 760b4a...

Proof:
Proof not loaded.

Theorem. (SNo_pos_eps_Lt)

∀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...

Proof:
Proof not loaded.

Theorem. (SNo_pos_eps_Le)

∀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...

Proof:
Proof not loaded.

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

In Proofgold the corresponding term root is 8c2587... and proposition id is 8515ac...

Proof:
Proof not loaded.

Theorem. (eps_SNoCutP)

∀n ∈ ω, SNoCutP {0} {eps_ m|m ∈ n}

In Proofgold the corresponding term root is 545873... and proposition id is 30edf9...

Proof:
Proof not loaded.

Theorem. (eps_SNoCut)

∀n ∈ ω, eps_ n = SNoCut {0} {eps_ m|m ∈ n}

In Proofgold the corresponding term root is 06d6c5... and proposition id is eba0c6...

Proof:
Proof not loaded.

End of Section TaggedSets2