Beginning of Section Conj_ZF_UPair_closed__1__1

Variable x : set

Variable y : set

Variable z : set

Hypothesis H0 : z ∈ UPair x y

Theorem. (Conj_ZF_UPair_closed__1__1)

If_i (x ∈ Empty) x y ∈ Repl (𝒫 (𝒫 x)) (λw : set ⇒ If_i (x ∈ w) x y) → z ∈ Repl (𝒫 (𝒫 x)) (λw : set ⇒ If_i (x ∈ w) x y)

In Proofgold the corresponding term root is f6cddc... and proposition id is d27324...

Proof:

The rest of the proof is missing.

End of Section Conj_ZF_UPair_closed__1__1

Beginning of Section Conj_ZF_UPair_closed__5__1

Variable x : set

Variable y : set

Variable z : set

Hypothesis H0 : ZF_closed x

Hypothesis H2 : z ∈ x

Theorem. (Conj_ZF_UPair_closed__5__1)

Repl (𝒫 (𝒫 y)) (λw : set ⇒ If_i (y ∈ w) y z) = UPair y z → UPair y z ∈ x

In Proofgold the corresponding term root is d1689a... and proposition id is 736fe9...

Proof:

The rest of the proof is missing.

End of Section Conj_ZF_UPair_closed__5__1

Beginning of Section Conj_ordinal_ordsucc_In_eq__1__1

Variable x : set

Variable y : set

Hypothesis H0 : ordinal x

Theorem. (Conj_ordinal_ordsucc_In_eq__1__1)

ordinal (ordsucc y) → ordsucc y ∈ x ∨ x = ordsucc y

In Proofgold the corresponding term root is 19571a... and proposition id is 572d45...

Proof:

The rest of the proof is missing.

End of Section Conj_ordinal_ordsucc_In_eq__1__1

Beginning of Section Conj_ordinal_famunion__2__0

Variable x : set

Variable f : (set → set)

Variable y : set

Variable z : set

Hypothesis H1 : z ∈ x

Hypothesis H2 : y ∈ f z

Theorem. (Conj_ordinal_famunion__2__0)

ordinal (f z) → TransSet y

In Proofgold the corresponding term root is 1cb0d5... and proposition id is 8a79f7...

Proof:

The rest of the proof is missing.

End of Section Conj_ordinal_famunion__2__0

Beginning of Section Conj_KnasterTarski_set__3__0

Variable x : set

Variable f : (set → set)

Hypothesis H1 : Sep x (λy : set ⇒ ∀z : set, z ∈ 𝒫 x → Subq (f z) z → y ∈ z) ∈ 𝒫 x

Hypothesis H2 : f (Sep x (λy : set ⇒ ∀z : set, z ∈ 𝒫 x → Subq (f z) z → y ∈ z)) ∈ 𝒫 x

Hypothesis H3 : (∀y : set, y ∈ 𝒫 x → Subq (f y) y → Subq (Sep x (λz : set ⇒ ∀w : set, w ∈ 𝒫 x → Subq (f w) w → z ∈ w)) y)

Hypothesis H4 : Subq (f (Sep x (λy : set ⇒ ∀z : set, z ∈ 𝒫 x → Subq (f z) z → y ∈ z))) (Sep x (λy : set ⇒ ∀z : set, z ∈ 𝒫 x → Subq (f z) z → y ∈ z))

Theorem. (Conj_KnasterTarski_set__3__0)

Subq (f (f (Sep x (λy : set ⇒ ∀z : set, z ∈ 𝒫 x → Subq (f z) z → y ∈ z)))) (f (Sep x (λy : set ⇒ ∀z : set, z ∈ 𝒫 x → Subq (f z) z → y ∈ z))) → (∃y : set, y ∈ 𝒫 x ∧ f y = y)

In Proofgold the corresponding term root is dfd671... and proposition id is 98ac0f...

Proof:

The rest of the proof is missing.

End of Section Conj_KnasterTarski_set__3__0

Beginning of Section Conj_KnasterTarski_set__4__0

Variable x : set

Variable f : (set → set)

Hypothesis H1 : Sep x (λy : set ⇒ ∀z : set, z ∈ 𝒫 x → Subq (f z) z → y ∈ z) ∈ 𝒫 x

Hypothesis H2 : f (Sep x (λy : set ⇒ ∀z : set, z ∈ 𝒫 x → Subq (f z) z → y ∈ z)) ∈ 𝒫 x

Hypothesis H3 : (∀y : set, y ∈ 𝒫 x → Subq (f y) y → Subq (Sep x (λz : set ⇒ ∀w : set, w ∈ 𝒫 x → Subq (f w) w → z ∈ w)) y)

Theorem. (Conj_KnasterTarski_set__4__0)

Subq (f (Sep x (λy : set ⇒ ∀z : set, z ∈ 𝒫 x → Subq (f z) z → y ∈ z))) (Sep x (λy : set ⇒ ∀z : set, z ∈ 𝒫 x → Subq (f z) z → y ∈ z)) → (∃y : set, y ∈ 𝒫 x ∧ f y = y)

In Proofgold the corresponding term root is 11da76... and proposition id is 16e542...

Proof:

The rest of the proof is missing.

End of Section Conj_KnasterTarski_set__4__0

Beginning of Section Conj_SchroederBernstein__3__3

Variable x : set

Variable y : set

Variable f : (set → set)

Variable f2 : (set → set)

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Hypothesis H0 : (∀x2 : set, x2 ∈ y → (∀y2 : set, y2 ∈ y → f2 x2 = f2 y2 → x2 = y2))

Hypothesis H1 : (λx2 : set ⇒ Repl (setminus y (Repl (setminus x x2) (λy2 : set ⇒ f y2))) (λy2 : set ⇒ f2 y2)) z = z

Hypothesis H2 : w = f2 v

Hypothesis H4 : u ∈ z

Theorem. (Conj_SchroederBernstein__3__3)

u ∈ Repl (setminus y (Repl (setminus x z) f)) f2 → inv y f2 w = inv y f2 u → w = u

In Proofgold the corresponding term root is c39df2... and proposition id is 527b2f...

Proof:

The rest of the proof is missing.

End of Section Conj_SchroederBernstein__3__3

Beginning of Section Conj_PigeonHole_nat__1__0

Variable x : set

Variable f : (set → set)

Variable y : set

Variable z : set

Variable w : set

Hypothesis H1 : z ∈ ordsucc (ordsucc x)

Hypothesis H2 : ordsucc w ∈ ordsucc (ordsucc x)

Hypothesis H3 : ¬ Subq y z

Hypothesis H4 : Subq y w

Hypothesis H5 : f z = f (ordsucc w)

Theorem. (Conj_PigeonHole_nat__1__0)

z ≠ ordsucc w

In Proofgold the corresponding term root is d0c8d7... and proposition id is 24d2cf...

Proof:

The rest of the proof is missing.

End of Section Conj_PigeonHole_nat__1__0

Beginning of Section Conj_PigeonHole_nat__5__1

Variable x : set

Variable f : (set → set)

Variable y : set

Variable z : set

Variable w : set

Hypothesis H0 : nat_p x

Hypothesis H2 : z ∈ ordsucc x

Hypothesis H3 : w ∈ ordsucc x

Hypothesis H4 : z ∈ ordsucc (ordsucc x)

Theorem. (Conj_PigeonHole_nat__5__1)

ordsucc z ∈ ordsucc (ordsucc x) → If_i (Subq y z) (f (ordsucc z)) (f z) = If_i (Subq y w) (f (ordsucc w)) (f w) → z = w

In Proofgold the corresponding term root is 69463d... and proposition id is a8682a...

Proof:

The rest of the proof is missing.

End of Section Conj_PigeonHole_nat__5__1

Beginning of Section Conj_PigeonHole_nat_bij__2__2

Variable x : set

Variable f : (set → set)

Variable y : set

Variable z : set

Variable w : set

Hypothesis H0 : (∀u : set, u ∈ x → (∀v : set, v ∈ x → f u = f v → u = v))

Hypothesis H1 : ¬ (∃u : set, u ∈ x ∧ f u = y)

Hypothesis H3 : w ∈ ordsucc x

Theorem. (Conj_PigeonHole_nat_bij__2__2)

(z ≠ x → z ∈ x) → If_i (z = x) y (f z) = If_i (w = x) y (f w) → z = w

In Proofgold the corresponding term root is de293d... and proposition id is 814b84...

Proof:

The rest of the proof is missing.

End of Section Conj_PigeonHole_nat_bij__2__2

Beginning of Section Conj_finite_ind__2__4

Variable p : (set → prop)

Variable x : set

Variable y : set

Variable f : (set → set)

Hypothesis H0 : (∀z : set, ∀w : set, finite z → nIn w z → p z → p (binunion z (Sing w)))

Hypothesis H1 : nat_p x

Hypothesis H2 : (∀z : set, equip z x → p z)

Hypothesis H3 : (∀z : set, z ∈ ordsucc x → f z ∈ y)

Hypothesis H5 : (∀z : set, z ∈ y → (∃w : set, w ∈ ordsucc x ∧ f w = z))

Theorem. (Conj_finite_ind__2__4)

y = binunion (Repl x f) (Sing (f x)) → p y

In Proofgold the corresponding term root is 4ee808... and proposition id is 71cb45...

Proof:

The rest of the proof is missing.

End of Section Conj_finite_ind__2__4

Beginning of Section Conj_Descr_Vo1_prop__1__1

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

Variable p : (set → prop)

Hypothesis H0 : (∀q : set → prop, ∀p2 : set → prop, P q → P p2 → q = p2)

Theorem. (Conj_Descr_Vo1_prop__1__1)

p = Descr_Vo1 P → P (Descr_Vo1 P)

In Proofgold the corresponding term root is 5a51b6... and proposition id is 150974...

Proof:

The rest of the proof is missing.

End of Section Conj_Descr_Vo1_prop__1__1

Beginning of Section Conj_nat_setsum1_ordsucc__1__0

Variable x : set

Variable y : set

Hypothesis H1 : x = ordsucc y

Theorem. (Conj_nat_setsum1_ordsucc__1__0)

y ∈ x → ordsucc y ∈ Inj1 x

In Proofgold the corresponding term root is 329db4... and proposition id is 01b082...

Proof:

The rest of the proof is missing.

End of Section Conj_nat_setsum1_ordsucc__1__0

Beginning of Section Conj_PNoLt_trichotomy_or__6__2

Variable x : set

Variable y : set

Variable p : (set → prop)

Variable q : (set → prop)

Hypothesis H0 : TransSet y

Hypothesis H1 : PNoEq_ (binintersect x y) p q

Theorem. (Conj_PNoLt_trichotomy_or__6__2)

binintersect x y = x → PNoLt x p y q ∨ x = y ∧ PNoEq_ x p q ∨ PNoLt y q x p

In Proofgold the corresponding term root is 5fbb6c... and proposition id is 21717c...

Proof:

The rest of the proof is missing.

End of Section Conj_PNoLt_trichotomy_or__6__2

Beginning of Section Conj_PNoLt_trichotomy_or__7__2

Variable x : set

Variable y : set

Variable p : (set → prop)

Variable q : (set → prop)

Hypothesis H0 : ordinal x

Hypothesis H1 : ordinal y

Hypothesis H3 : TransSet y

Theorem. (Conj_PNoLt_trichotomy_or__7__2)

ordinal (binintersect x y) → PNoLt x p y q ∨ x = y ∧ PNoEq_ x p q ∨ PNoLt y q x p

In Proofgold the corresponding term root is 1bc7a3... and proposition id is 070102...

Proof:

The rest of the proof is missing.

End of Section Conj_PNoLt_trichotomy_or__7__2

Beginning of Section Conj_PNoLt_tra__1__0

Variable x : set

Variable y : set

Variable z : set

Variable p : (set → prop)

Variable q : (set → prop)

Variable p2 : (set → prop)

Variable w : set

Hypothesis H1 : ordinal y

Hypothesis H2 : TransSet z

Hypothesis H3 : PNoEq_ x p q

Hypothesis H4 : q x

Hypothesis H5 : w ∈ y

Hypothesis H6 : w ∈ z

Hypothesis H7 : PNoEq_ w q p2

Hypothesis H8 : ¬ q w

Hypothesis H9 : p2 w

Theorem. (Conj_PNoLt_tra__1__0)

ordinal w → PNoLt x p z p2

In Proofgold the corresponding term root is 64613e... and proposition id is 2ffa11...

Proof:

The rest of the proof is missing.

End of Section Conj_PNoLt_tra__1__0

Beginning of Section Conj_PNoLt_tra__2__12

Variable x : set

Variable y : set

Variable z : set

Variable p : (set → prop)

Variable q : (set → prop)

Variable p2 : (set → prop)

Variable w : set

Variable u : set

Hypothesis H0 : ordinal y

Hypothesis H1 : TransSet x

Hypothesis H2 : TransSet z

Hypothesis H3 : w ∈ x

Hypothesis H4 : PNoEq_ w p q

Hypothesis H5 : ¬ p w

Hypothesis H6 : q w

Hypothesis H7 : ordinal w

Hypothesis H8 : u ∈ y

Hypothesis H9 : u ∈ z

Hypothesis H10 : PNoEq_ u q p2

Hypothesis H11 : ¬ q u

Theorem. (Conj_PNoLt_tra__2__12)

ordinal u → PNoLt x p z p2

In Proofgold the corresponding term root is 068007... and proposition id is cced19...

Proof:

The rest of the proof is missing.

End of Section Conj_PNoLt_tra__2__12

Beginning of Section Conj_PNoLe_tra__1__0

Variable x : set

Variable y : set

Variable z : set

Variable p : (set → prop)

Variable q : (set → prop)

Variable p2 : (set → prop)

Hypothesis H1 : ordinal z

Hypothesis H2 : PNoLe y q z p2

Hypothesis H3 : x = y

Hypothesis H4 : PNoEq_ x p q

Theorem. (Conj_PNoLe_tra__1__0)

PNoEq_ y p q → PNoLe y p z p2

In Proofgold the corresponding term root is 6e0b08... and proposition id is 7337bf...

Proof:

The rest of the proof is missing.

End of Section Conj_PNoLe_tra__1__0

Beginning of Section Conj_PNo_rel_strict_upperbd_antimon__6__1

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

Variable x : set

Variable p : (set → prop)

Variable y : set

Hypothesis H0 : ordinal x

Hypothesis H2 : TransSet x

Theorem. (Conj_PNo_rel_strict_upperbd_antimon__6__1)

ordinal y → (∀z : set, z ∈ x → (∀q : set → prop, PNo_downc P z q → PNoLt z q x p)) → (∀z : set, z ∈ y → (∀q : set → prop, PNo_downc P z q → PNoLt z q y p))

In Proofgold the corresponding term root is 8f263d... and proposition id is 3d21a9...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_rel_strict_upperbd_antimon__6__1

Beginning of Section Conj_PNo_rel_strict_upperbd_antimon__6__2

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

Variable x : set

Variable p : (set → prop)

Variable y : set

Hypothesis H0 : ordinal x

Hypothesis H1 : y ∈ x

Theorem. (Conj_PNo_rel_strict_upperbd_antimon__6__2)

ordinal y → (∀z : set, z ∈ x → (∀q : set → prop, PNo_downc P z q → PNoLt z q x p)) → (∀z : set, z ∈ y → (∀q : set → prop, PNo_downc P z q → PNoLt z q y p))

In Proofgold the corresponding term root is 6b0317... and proposition id is 4772a3...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_rel_strict_upperbd_antimon__6__2

Beginning of Section Conj_PNo_rel_strict_lowerbd_antimon__4__0

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

Variable x : set

Variable p : (set → prop)

Variable y : set

Variable z : set

Variable q : (set → prop)

Hypothesis H1 : TransSet x

Hypothesis H2 : TransSet y

Hypothesis H3 : (∀w : set, w ∈ x → (∀p2 : set → prop, PNo_upc P w p2 → PNoLt x p w p2))

Hypothesis H4 : z ∈ y

Hypothesis H5 : PNo_upc P z q

Theorem. (Conj_PNo_rel_strict_lowerbd_antimon__4__0)

z ∈ x → PNoLt y p z q

In Proofgold the corresponding term root is b0eccf... and proposition id is deba05...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_rel_strict_lowerbd_antimon__4__0

Beginning of Section Conj_PNo_rel_imv_ex__4__9

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

Variable x : set

Variable p : (set → prop)

Variable y : set

Variable q : (set → prop)

Variable z : set

Hypothesis H0 : ordinal x

Hypothesis H1 : (∀w : set, w ∈ x → (∀p2 : set → prop, PNo_upc P w p2 → PNoLt x p w p2))

Hypothesis H2 : PNoEq_ x p (λw : set ⇒ p w ∨ w = x)

Hypothesis H3 : PNo_upc P y q

Hypothesis H4 : ordinal y

Hypothesis H5 : y = x

Hypothesis H6 : z ∈ x

Hypothesis H7 : PNoEq_ z q (λw : set ⇒ p w ∨ w = x)

Hypothesis H8 : ¬ q z

Theorem. (Conj_PNo_rel_imv_ex__4__9)

ordinal z → PNoLt (ordsucc x) (λw : set ⇒ p w ∨ w = x) x q

In Proofgold the corresponding term root is 5ab3cf... and proposition id is 24c2fe...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_rel_imv_ex__4__9

Beginning of Section Conj_PNo_rel_imv_ex__7__0

Variable x : set

Variable p : (set → prop)

Variable q : (set → prop)

Variable y : set

Hypothesis H1 : PNoEq_ x p (λz : set ⇒ p z ∨ z = x)

Hypothesis H2 : y ∈ x

Hypothesis H3 : PNoEq_ y (λz : set ⇒ p z ∨ z = x) q

Hypothesis H4 : ¬ (p y ∨ y = x)

Hypothesis H5 : ordinal y

Hypothesis H6 : PNoLt y q x p

Theorem. (Conj_PNo_rel_imv_ex__7__0)

¬ PNoLt x p y q

In Proofgold the corresponding term root is d9bff3... and proposition id is eb8531...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_rel_imv_ex__7__0

Beginning of Section Conj_PNo_rel_imv_ex__7__3

Variable x : set

Variable p : (set → prop)

Variable q : (set → prop)

Variable y : set

Hypothesis H0 : ordinal x

Hypothesis H1 : PNoEq_ x p (λz : set ⇒ p z ∨ z = x)

Hypothesis H2 : y ∈ x

Hypothesis H4 : ¬ (p y ∨ y = x)

Hypothesis H5 : ordinal y

Hypothesis H6 : PNoLt y q x p

Theorem. (Conj_PNo_rel_imv_ex__7__3)

¬ PNoLt x p y q

In Proofgold the corresponding term root is cb3490... and proposition id is e94bd7...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_rel_imv_ex__7__3

Beginning of Section Conj_PNo_rel_imv_ex__7__4

Variable x : set

Variable p : (set → prop)

Variable q : (set → prop)

Variable y : set

Hypothesis H0 : ordinal x

Hypothesis H1 : PNoEq_ x p (λz : set ⇒ p z ∨ z = x)

Hypothesis H2 : y ∈ x

Hypothesis H3 : PNoEq_ y (λz : set ⇒ p z ∨ z = x) q

Hypothesis H5 : ordinal y

Hypothesis H6 : PNoLt y q x p

Theorem. (Conj_PNo_rel_imv_ex__7__4)

¬ PNoLt x p y q

In Proofgold the corresponding term root is 9eefe4... and proposition id is e1d832...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_rel_imv_ex__7__4

Beginning of Section Conj_PNo_rel_imv_ex__15__3

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

Variable Q : (set → ((set → prop) → prop))

Variable x : set

Variable y : set

Variable p : (set → prop)

Hypothesis H0 : ¬ (∃q : set → prop, PNo_rel_strict_uniq_imv P Q x q)

Hypothesis H1 : x = ordsucc y

Hypothesis H2 : ordinal y

Hypothesis H4 : binintersect y (ordsucc y) = y

Hypothesis H5 : binintersect (ordsucc y) y = y

Hypothesis H6 : (∀z : set, z ∈ y → (∀q : set → prop, PNo_downc P z q → PNoLt z q y p))

Hypothesis H7 : (∀z : set, z ∈ y → (∀q : set → prop, PNo_upc Q z q → PNoLt y p z q))

Hypothesis H8 : (∀q : set → prop, PNo_rel_strict_imv P Q y q → PNoEq_ y p q)

Hypothesis H9 : PNoEq_ y p (λz : set ⇒ p z ∨ z = y)

Hypothesis H10 : PNoLt y p (ordsucc y) (λz : set ⇒ p z ∨ z = y)

Hypothesis H11 : ¬ (PNo_rel_strict_imv P Q x (λz : set ⇒ p z ∧ z ≠ y) ∧ PNo_rel_strict_imv P Q x (λz : set ⇒ p z ∨ z = y))

Hypothesis H12 : (∀q : set → prop, PNo_upc Q y q → ¬ PNoEq_ y p q)

Theorem. (Conj_PNo_rel_imv_ex__15__3)

¬ PNo_rel_strict_imv P Q (ordsucc y) (λz : set ⇒ p z ∨ z = y)

In Proofgold the corresponding term root is a231b3... and proposition id is eef5ef...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_rel_imv_ex__15__3

Beginning of Section Conj_PNo_rel_imv_ex__15__11

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

Variable Q : (set → ((set → prop) → prop))

Variable x : set

Variable y : set

Variable p : (set → prop)

Hypothesis H0 : ¬ (∃q : set → prop, PNo_rel_strict_uniq_imv P Q x q)

Hypothesis H1 : x = ordsucc y

Hypothesis H2 : ordinal y

Hypothesis H3 : ordinal (ordsucc y)

Hypothesis H4 : binintersect y (ordsucc y) = y

Hypothesis H5 : binintersect (ordsucc y) y = y

Hypothesis H6 : (∀z : set, z ∈ y → (∀q : set → prop, PNo_downc P z q → PNoLt z q y p))

Hypothesis H7 : (∀z : set, z ∈ y → (∀q : set → prop, PNo_upc Q z q → PNoLt y p z q))

Hypothesis H8 : (∀q : set → prop, PNo_rel_strict_imv P Q y q → PNoEq_ y p q)

Hypothesis H9 : PNoEq_ y p (λz : set ⇒ p z ∨ z = y)

Hypothesis H10 : PNoLt y p (ordsucc y) (λz : set ⇒ p z ∨ z = y)

Hypothesis H12 : (∀q : set → prop, PNo_upc Q y q → ¬ PNoEq_ y p q)

Theorem. (Conj_PNo_rel_imv_ex__15__11)

¬ PNo_rel_strict_imv P Q (ordsucc y) (λz : set ⇒ p z ∨ z = y)

In Proofgold the corresponding term root is a9afe8... and proposition id is b8cd09...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_rel_imv_ex__15__11

Beginning of Section Conj_PNo_rel_imv_ex__16__2

Variable x : set

Variable p : (set → prop)

Variable q : (set → prop)

Variable y : set

Hypothesis H0 : ordinal x

Hypothesis H1 : PNoEq_ x (λz : set ⇒ p z ∧ z ≠ x) p

Hypothesis H3 : PNoEq_ y q (λz : set ⇒ p z ∧ z ≠ x)

Hypothesis H4 : p y ∧ y ≠ x

Hypothesis H5 : ordinal y

Hypothesis H6 : PNoLt x p y q

Theorem. (Conj_PNo_rel_imv_ex__16__2)

¬ PNoLt y q x p

In Proofgold the corresponding term root is bb97e9... and proposition id is ec2d3f...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_rel_imv_ex__16__2

Beginning of Section Conj_PNo_rel_imv_ex__17__0

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

Variable x : set

Variable p : (set → prop)

Variable y : set

Variable q : (set → prop)

Variable z : set

Hypothesis H1 : (∀w : set, w ∈ x → (∀p2 : set → prop, PNo_upc P w p2 → PNoLt x p w p2))

Hypothesis H2 : PNoEq_ x (λw : set ⇒ p w ∧ w ≠ x) p

Hypothesis H3 : PNo_upc P y q

Hypothesis H4 : ordinal y

Hypothesis H5 : y = x

Hypothesis H6 : z ∈ x

Hypothesis H7 : PNoEq_ z q (λw : set ⇒ p w ∧ w ≠ x)

Hypothesis H8 : ¬ q z

Hypothesis H9 : p z ∧ z ≠ x

Hypothesis H10 : ordinal z

Theorem. (Conj_PNo_rel_imv_ex__17__0)

¬ PNoLt x p z q

In Proofgold the corresponding term root is b0e8ab... and proposition id is 5a9ced...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_rel_imv_ex__17__0

Beginning of Section Conj_PNo_rel_imv_ex__19__3

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

Variable x : set

Variable p : (set → prop)

Variable y : set

Variable q : (set → prop)

Hypothesis H0 : ordinal x

Hypothesis H1 : ordinal (ordsucc x)

Hypothesis H2 : binintersect x (ordsucc x) = x

Hypothesis H4 : PNoEq_ x (λz : set ⇒ p z ∧ z ≠ x) p

Hypothesis H5 : PNoLt (ordsucc x) (λz : set ⇒ p z ∧ z ≠ x) x p

Hypothesis H6 : y ∈ ordsucc x

Hypothesis H7 : PNo_upc P y q

Theorem. (Conj_PNo_rel_imv_ex__19__3)

ordinal y → PNoLt (ordsucc x) (λz : set ⇒ p z ∧ z ≠ x) y q

In Proofgold the corresponding term root is 233b53... and proposition id is 8d1209...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_rel_imv_ex__19__3

Beginning of Section Conj_PNo_rel_imv_ex__20__5

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

Variable x : set

Variable p : (set → prop)

Variable y : set

Variable q : (set → prop)

Variable z : set

Hypothesis H0 : ordinal x

Hypothesis H1 : (∀w : set, w ∈ x → (∀p2 : set → prop, PNo_downc P w p2 → PNoLt w p2 x p))

Hypothesis H2 : PNo_downc P y q

Hypothesis H3 : ordinal y

Hypothesis H4 : y = x

Hypothesis H6 : q z

Hypothesis H7 : ordinal z

Hypothesis H8 : PNoLt x p z q

Theorem. (Conj_PNo_rel_imv_ex__20__5)

PNoLt z q x p → PNoLt x q (ordsucc x) (λw : set ⇒ p w ∧ w ≠ x)

In Proofgold the corresponding term root is 23c728... and proposition id is b05661...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_rel_imv_ex__20__5

Beginning of Section Conj_PNo_rel_imv_ex__22__6

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

Variable x : set

Variable p : (set → prop)

Variable y : set

Variable q : (set → prop)

Variable z : set

Hypothesis H0 : ordinal x

Hypothesis H1 : (∀w : set, w ∈ x → (∀p2 : set → prop, PNo_downc P w p2 → PNoLt w p2 x p))

Hypothesis H2 : PNoEq_ x (λw : set ⇒ p w ∧ w ≠ x) p

Hypothesis H3 : PNo_downc P y q

Hypothesis H4 : ordinal y

Hypothesis H5 : y = x

Hypothesis H7 : PNoEq_ z (λw : set ⇒ p w ∧ w ≠ x) q

Hypothesis H8 : ¬ (p z ∧ z ≠ x)

Hypothesis H9 : q z

Theorem. (Conj_PNo_rel_imv_ex__22__6)

ordinal z → PNoLt x q (ordsucc x) (λw : set ⇒ p w ∧ w ≠ x)

In Proofgold the corresponding term root is e3f4d2... and proposition id is 0ef788...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_rel_imv_ex__22__6

Beginning of Section Conj_PNo_rel_imv_ex__29__1

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

Variable Q : (set → ((set → prop) → prop))

Variable x : set

Variable y : set

Variable p : (set → prop)

Hypothesis H0 : ¬ (∃q : set → prop, PNo_rel_strict_uniq_imv P Q x q)

Hypothesis H2 : ordinal y

Hypothesis H3 : ordinal (ordsucc y)

Hypothesis H4 : binintersect y (ordsucc y) = y

Hypothesis H5 : binintersect (ordsucc y) y = y

Hypothesis H6 : (∀z : set, z ∈ y → (∀q : set → prop, PNo_downc P z q → PNoLt z q y p))

Hypothesis H7 : (∀z : set, z ∈ y → (∀q : set → prop, PNo_upc Q z q → PNoLt y p z q))

Hypothesis H8 : (∀q : set → prop, PNo_rel_strict_imv P Q y q → PNoEq_ y p q)

Hypothesis H9 : PNoEq_ y (λz : set ⇒ p z ∧ z ≠ y) p

Hypothesis H10 : PNoLt (ordsucc y) (λz : set ⇒ p z ∧ z ≠ y) y p

Hypothesis H11 : ¬ (PNo_rel_strict_imv P Q x (λz : set ⇒ p z ∧ z ≠ y) ∧ PNo_rel_strict_imv P Q x (λz : set ⇒ p z ∨ z = y))

Hypothesis H12 : (∀q : set → prop, PNo_downc P y q → ¬ PNoEq_ y p q)

Theorem. (Conj_PNo_rel_imv_ex__29__1)

¬ PNo_rel_strict_imv P Q (ordsucc y) (λz : set ⇒ p z ∧ z ≠ y)

In Proofgold the corresponding term root is 8cba16... and proposition id is e00566...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_rel_imv_ex__29__1

Beginning of Section Conj_PNo_rel_imv_ex__32__9

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

Variable Q : (set → ((set → prop) → prop))

Variable x : set

Variable y : set

Variable p : (set → prop)

Hypothesis H0 : PNoLt_pwise (PNo_downc P) (PNo_upc Q)

Hypothesis H1 : ¬ (∃q : set → prop, PNo_rel_strict_uniq_imv P Q x q)

Hypothesis H2 : ¬ (∃z : set, z ∈ x ∧ (∃q : set → prop, PNo_rel_strict_split_imv P Q z q))

Hypothesis H3 : y ∈ x

Hypothesis H4 : x = ordsucc y

Hypothesis H5 : ordinal y

Hypothesis H6 : ordinal (ordsucc y)

Hypothesis H7 : binintersect y (ordsucc y) = y

Hypothesis H8 : binintersect (ordsucc y) y = y

Hypothesis H10 : (∀z : set, z ∈ y → (∀q : set → prop, PNo_upc Q z q → PNoLt y p z q))

Hypothesis H11 : (∀q : set → prop, PNo_rel_strict_imv P Q y q → PNoEq_ y p q)

Hypothesis H12 : PNoEq_ y (λz : set ⇒ p z ∧ z ≠ y) p

Hypothesis H13 : PNoLt (ordsucc y) (λz : set ⇒ p z ∧ z ≠ y) y p

Hypothesis H14 : PNoEq_ y p (λz : set ⇒ p z ∨ z = y)

Hypothesis H15 : p y ∨ y = y

Theorem. (Conj_PNo_rel_imv_ex__32__9)

¬ PNoLt y p (ordsucc y) (λz : set ⇒ p z ∨ z = y)

In Proofgold the corresponding term root is b4e1a0... and proposition id is 9bc844...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_rel_imv_ex__32__9

Beginning of Section Conj_PNo_rel_imv_ex__32__11

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

Variable Q : (set → ((set → prop) → prop))

Variable x : set

Variable y : set

Variable p : (set → prop)

Hypothesis H0 : PNoLt_pwise (PNo_downc P) (PNo_upc Q)

Hypothesis H1 : ¬ (∃q : set → prop, PNo_rel_strict_uniq_imv P Q x q)

Hypothesis H2 : ¬ (∃z : set, z ∈ x ∧ (∃q : set → prop, PNo_rel_strict_split_imv P Q z q))

Hypothesis H3 : y ∈ x

Hypothesis H4 : x = ordsucc y

Hypothesis H5 : ordinal y

Hypothesis H6 : ordinal (ordsucc y)

Hypothesis H7 : binintersect y (ordsucc y) = y

Hypothesis H8 : binintersect (ordsucc y) y = y

Hypothesis H9 : (∀z : set, z ∈ y → (∀q : set → prop, PNo_downc P z q → PNoLt z q y p))

Hypothesis H10 : (∀z : set, z ∈ y → (∀q : set → prop, PNo_upc Q z q → PNoLt y p z q))

Hypothesis H12 : PNoEq_ y (λz : set ⇒ p z ∧ z ≠ y) p

Hypothesis H13 : PNoLt (ordsucc y) (λz : set ⇒ p z ∧ z ≠ y) y p

Hypothesis H14 : PNoEq_ y p (λz : set ⇒ p z ∨ z = y)

Hypothesis H15 : p y ∨ y = y

Theorem. (Conj_PNo_rel_imv_ex__32__11)

¬ PNoLt y p (ordsucc y) (λz : set ⇒ p z ∨ z = y)

In Proofgold the corresponding term root is bf03ed... and proposition id is 414ac4...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_rel_imv_ex__32__11

Beginning of Section Conj_PNo_rel_imv_ex__37__7

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

Variable Q : (set → ((set → prop) → prop))

Variable x : set

Variable y : set

Variable p : (set → prop)

Hypothesis H0 : PNoLt_pwise (PNo_downc P) (PNo_upc Q)

Hypothesis H1 : ¬ (∃q : set → prop, PNo_rel_strict_uniq_imv P Q x q)

Hypothesis H2 : ¬ (∃z : set, z ∈ x ∧ (∃q : set → prop, PNo_rel_strict_split_imv P Q z q))

Hypothesis H3 : y ∈ x

Hypothesis H4 : x = ordsucc y

Hypothesis H5 : ordinal y

Hypothesis H6 : ordinal (ordsucc y)

Hypothesis H8 : binintersect (ordsucc y) y = y

Hypothesis H9 : (∀z : set, z ∈ y → (∀q : set → prop, PNo_downc P z q → PNoLt z q y p))

Hypothesis H10 : (∀z : set, z ∈ y → (∀q : set → prop, PNo_upc Q z q → PNoLt y p z q))

Hypothesis H11 : (∀q : set → prop, PNo_rel_strict_imv P Q y q → PNoEq_ y p q)

Theorem. (Conj_PNo_rel_imv_ex__37__7)

¬ PNoEq_ y (λz : set ⇒ p z ∧ z ≠ y) p

In Proofgold the corresponding term root is 0fe916... and proposition id is 905ede...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_rel_imv_ex__37__7

Beginning of Section Conj_PNo_rel_imv_ex__38__8

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

Variable Q : (set → ((set → prop) → prop))

Variable x : set

Variable y : set

Hypothesis H0 : PNoLt_pwise (PNo_downc P) (PNo_upc Q)

Hypothesis H1 : ¬ (∃p : set → prop, PNo_rel_strict_uniq_imv P Q x p)

Hypothesis H2 : ¬ (∃z : set, z ∈ x ∧ (∃p : set → prop, PNo_rel_strict_split_imv P Q z p))

Hypothesis H3 : (∀z : set, z ∈ x → (∃p : set → prop, PNo_rel_strict_uniq_imv P Q z p))

Hypothesis H4 : y ∈ x

Hypothesis H5 : x = ordsucc y

Hypothesis H6 : ordinal y

Hypothesis H7 : ordinal (ordsucc y)

Theorem. (Conj_PNo_rel_imv_ex__38__8)

binintersect (ordsucc y) y ≠ y

In Proofgold the corresponding term root is da8890... and proposition id is d9c8fe...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_rel_imv_ex__38__8

Beginning of Section Conj_PNo_rel_imv_ex__39__1

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

Variable Q : (set → ((set → prop) → prop))

Variable x : set

Variable y : set

Hypothesis H0 : PNoLt_pwise (PNo_downc P) (PNo_upc Q)

Hypothesis H2 : ¬ (∃z : set, z ∈ x ∧ (∃p : set → prop, PNo_rel_strict_split_imv P Q z p))

Hypothesis H3 : (∀z : set, z ∈ x → (∃p : set → prop, PNo_rel_strict_uniq_imv P Q z p))

Hypothesis H4 : y ∈ x

Hypothesis H5 : x = ordsucc y

Hypothesis H6 : ordinal y

Hypothesis H7 : ordinal (ordsucc y)

Theorem. (Conj_PNo_rel_imv_ex__39__1)

binintersect y (ordsucc y) ≠ y

In Proofgold the corresponding term root is b70e25... and proposition id is b66192...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_rel_imv_ex__39__1

Beginning of Section Conj_PNo_rel_imv_ex__40__5

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

Variable Q : (set → ((set → prop) → prop))

Variable x : set

Variable y : set

Hypothesis H0 : PNoLt_pwise (PNo_downc P) (PNo_upc Q)

Hypothesis H1 : ordinal x

Hypothesis H2 : ¬ (∃p : set → prop, PNo_rel_strict_uniq_imv P Q x p)

Hypothesis H3 : ¬ (∃z : set, z ∈ x ∧ (∃p : set → prop, PNo_rel_strict_split_imv P Q z p))

Hypothesis H4 : (∀z : set, z ∈ x → (∃p : set → prop, PNo_rel_strict_uniq_imv P Q z p))

Hypothesis H6 : x = ordsucc y

Hypothesis H7 : ordinal y

Theorem. (Conj_PNo_rel_imv_ex__40__5)

¬ ordinal (ordsucc y)

In Proofgold the corresponding term root is 335ad9... and proposition id is 51980f...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_rel_imv_ex__40__5

Beginning of Section Conj_PNo_rel_imv_ex__45__7

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

Variable Q : (set → ((set → prop) → prop))

Variable x : set

Variable y : set

Variable p : (set → prop)

Hypothesis H0 : TransSet x

Hypothesis H1 : ordinal y

Hypothesis H2 : (∀z : set, z ∈ y → z ∈ x → PNo_rel_strict_uniq_imv P Q z (λw : set ⇒ ∀q : set → prop, PNo_rel_strict_imv P Q (ordsucc w) q → q w))

Hypothesis H3 : y ∈ x

Hypothesis H4 : PNo_rel_strict_imv P Q y p

Hypothesis H5 : PNo_rel_strict_upperbd P y p

Hypothesis H6 : PNo_rel_strict_lowerbd Q y p

Theorem. (Conj_PNo_rel_imv_ex__45__7)

PNoEq_ y (λz : set ⇒ ∀q : set → prop, PNo_rel_strict_imv P Q (ordsucc z) q → q z) p → PNo_rel_strict_imv P Q y (λz : set ⇒ ∀q : set → prop, PNo_rel_strict_imv P Q (ordsucc z) q → q z) ∧ (∀q : set → prop, PNo_rel_strict_imv P Q y q → PNoEq_ y (λz : set ⇒ ∀p2 : set → prop, PNo_rel_strict_imv P Q (ordsucc z) p2 → p2 z) q)

In Proofgold the corresponding term root is 24ce4f... and proposition id is 8a635d...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_rel_imv_ex__45__7

Beginning of Section Conj_PNo_rel_imv_ex__49__2

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

Variable Q : (set → ((set → prop) → prop))

Variable x : set

Variable y : set

Variable p : (set → prop)

Hypothesis H0 : PNo_upc Q y p

Hypothesis H1 : ordinal y

Hypothesis H3 : PNoEq_ y p (λz : set ⇒ ∀q : set → prop, PNo_rel_strict_imv P Q (ordsucc z) q → q z)

Hypothesis H4 : (∀q : set → prop, PNo_rel_strict_imv P Q (ordsucc y) q → q y)

Hypothesis H5 : PNo_rel_strict_lowerbd Q (ordsucc y) (λz : set ⇒ ∀q : set → prop, PNo_rel_strict_imv P Q (ordsucc z) q → q z)

Theorem. (Conj_PNo_rel_imv_ex__49__2)

PNoLt (ordsucc y) (λz : set ⇒ ∀q : set → prop, PNo_rel_strict_imv P Q (ordsucc z) q → q z) y p → PNoLt x (λz : set ⇒ ∀q : set → prop, PNo_rel_strict_imv P Q (ordsucc z) q → q z) y p

In Proofgold the corresponding term root is e39ce0... and proposition id is 4434ae...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_rel_imv_ex__49__2

Beginning of Section Conj_PNo_rel_imv_ex__54__4

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

Variable Q : (set → ((set → prop) → prop))

Variable x : set

Variable y : set

Variable p : (set → prop)

Variable z : set

Hypothesis H0 : (∀w : set, w ∈ x → ordsucc w ∈ x)

Hypothesis H1 : (∀w : set, w ∈ x → PNo_rel_strict_uniq_imv P Q w (λu : set ⇒ ∀q : set → prop, PNo_rel_strict_imv P Q (ordsucc u) q → q u))

Hypothesis H2 : PNo_upc Q y p

Hypothesis H3 : ordinal y

Hypothesis H5 : z ∈ x

Hypothesis H6 : PNoEq_ z p (λw : set ⇒ ∀q : set → prop, PNo_rel_strict_imv P Q (ordsucc w) q → q w)

Hypothesis H7 : ¬ p z

Hypothesis H8 : (∀q : set → prop, PNo_rel_strict_imv P Q (ordsucc z) q → q z)

Theorem. (Conj_PNo_rel_imv_ex__54__4)

ordinal z → PNoLt x (λw : set ⇒ ∀q : set → prop, PNo_rel_strict_imv P Q (ordsucc w) q → q w) y p

In Proofgold the corresponding term root is 812c2a... and proposition id is c8cd71...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_rel_imv_ex__54__4

Beginning of Section Conj_PNo_rel_imv_ex__58__3

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

Variable Q : (set → ((set → prop) → prop))

Variable x : set

Variable p : (set → prop)

Variable y : set

Hypothesis H0 : ordinal x

Hypothesis H1 : ordinal (ordsucc x)

Hypothesis H2 : PNo_rel_strict_imv P Q (ordsucc x) p

Hypothesis H4 : p y

Hypothesis H5 : (∀q : set → prop, PNo_rel_strict_imv P Q (ordsucc y) q → PNoEq_ (ordsucc y) (λz : set ⇒ ∀p2 : set → prop, PNo_rel_strict_imv P Q (ordsucc z) p2 → p2 z) q)

Theorem. (Conj_PNo_rel_imv_ex__58__3)

PNoEq_ (ordsucc y) (λz : set ⇒ ∀q : set → prop, PNo_rel_strict_imv P Q (ordsucc z) q → q z) p → (∀q : set → prop, PNo_rel_strict_imv P Q (ordsucc y) q → q y)

In Proofgold the corresponding term root is 8c96ea... and proposition id is 8b768a...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_rel_imv_ex__58__3

Beginning of Section Conj_PNo_rel_imv_ex__62__6

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

Variable Q : (set → ((set → prop) → prop))

Variable x : set

Variable y : set

Variable p : (set → prop)

Variable q : (set → prop)

Variable z : set

Hypothesis H0 : TransSet x

Hypothesis H1 : (∀w : set, w ∈ x → ordsucc w ∈ x)

Hypothesis H2 : (∀w : set, w ∈ x → PNo_rel_strict_uniq_imv P Q w (λu : set ⇒ ∀p2 : set → prop, PNo_rel_strict_imv P Q (ordsucc u) p2 → p2 u))

Hypothesis H3 : y ∈ x

Hypothesis H4 : ordinal y

Hypothesis H5 : ordinal (ordsucc y)

Hypothesis H7 : PNo_rel_strict_imv P Q (ordsucc y) q

Hypothesis H8 : z ∈ y

Hypothesis H9 : ¬ p z

Hypothesis H10 : q z

Theorem. (Conj_PNo_rel_imv_ex__62__6)

z ∈ x → q y

In Proofgold the corresponding term root is 9d3f53... and proposition id is d094cd...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_rel_imv_ex__62__6

Beginning of Section Conj_PNo_rel_imv_ex__64__8

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

Variable Q : (set → ((set → prop) → prop))

Variable x : set

Variable y : set

Variable p : (set → prop)

Variable q : (set → prop)

Hypothesis H0 : TransSet x

Hypothesis H1 : (∀z : set, z ∈ x → ordsucc z ∈ x)

Hypothesis H2 : (∀z : set, z ∈ x → PNo_rel_strict_uniq_imv P Q z (λw : set ⇒ ∀p2 : set → prop, PNo_rel_strict_imv P Q (ordsucc w) p2 → p2 w))

Hypothesis H3 : y ∈ x

Hypothesis H4 : PNo_downc P y p

Hypothesis H5 : ordinal y

Hypothesis H6 : ordinal (ordsucc y)

Hypothesis H7 : PNoEq_ y (λz : set ⇒ ∀p2 : set → prop, PNo_rel_strict_imv P Q (ordsucc z) p2 → p2 z) p

Hypothesis H9 : PNo_rel_strict_upperbd P (ordsucc y) q

Theorem. (Conj_PNo_rel_imv_ex__64__8)

PNoLt y p (ordsucc y) q → q y

In Proofgold the corresponding term root is b474bb... and proposition id is d28067...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_rel_imv_ex__64__8

Beginning of Section Conj_PNo_rel_imv_ex__65__3

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

Variable Q : (set → ((set → prop) → prop))

Variable x : set

Variable p : (set → prop)

Variable y : set

Hypothesis H0 : ordinal x

Hypothesis H1 : ordinal (ordsucc x)

Hypothesis H2 : PNo_rel_strict_imv P Q (ordsucc x) p

Hypothesis H4 : p y

Hypothesis H5 : (∀q : set → prop, PNo_rel_strict_imv P Q (ordsucc y) q → PNoEq_ (ordsucc y) (λz : set ⇒ ∀p2 : set → prop, PNo_rel_strict_imv P Q (ordsucc z) p2 → p2 z) q)

Theorem. (Conj_PNo_rel_imv_ex__65__3)

PNoEq_ (ordsucc y) (λz : set ⇒ ∀q : set → prop, PNo_rel_strict_imv P Q (ordsucc z) q → q z) p → (∀q : set → prop, PNo_rel_strict_imv P Q (ordsucc y) q → q y)

In Proofgold the corresponding term root is 8c96ea... and proposition id is 8b768a...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_rel_imv_ex__65__3

Beginning of Section Conj_PNo_rel_imv_ex__68__8

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

Variable Q : (set → ((set → prop) → prop))

Variable x : set

Variable p : (set → prop)

Variable y : set

Variable q : (set → prop)

Variable z : set

Hypothesis H0 : (∀w : set, w ∈ x → ordsucc w ∈ x)

Hypothesis H1 : (∀w : set, w ∈ x → PNo_rel_strict_uniq_imv P Q w (λu : set ⇒ ∀p2 : set → prop, PNo_rel_strict_imv P Q (ordsucc u) p2 → p2 u))

Hypothesis H2 : PNoEq_ y (λw : set ⇒ ∀p2 : set → prop, PNo_rel_strict_imv P Q (ordsucc w) p2 → p2 w) p

Hypothesis H3 : ordinal y

Hypothesis H4 : ordinal (ordsucc y)

Hypothesis H5 : PNo_rel_strict_imv P Q (ordsucc y) q

Hypothesis H6 : z ∈ y

Hypothesis H7 : ¬ p z

Hypothesis H9 : z ∈ x

Theorem. (Conj_PNo_rel_imv_ex__68__8)

ordsucc z ∈ x → q y

In Proofgold the corresponding term root is ec127a... and proposition id is d9314d...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_rel_imv_ex__68__8

Beginning of Section Conj_PNo_rel_imv_ex__71__8

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

Variable Q : (set → ((set → prop) → prop))

Variable x : set

Variable y : set

Variable p : (set → prop)

Variable z : set

Variable q : (set → prop)

Hypothesis H0 : TransSet x

Hypothesis H1 : (∀w : set, w ∈ x → ordsucc w ∈ x)

Hypothesis H2 : (∀w : set, w ∈ x → PNo_rel_strict_uniq_imv P Q w (λu : set ⇒ ∀p2 : set → prop, PNo_rel_strict_imv P Q (ordsucc u) p2 → p2 u))

Hypothesis H3 : PNo_downc P y p

Hypothesis H4 : ordinal y

Hypothesis H5 : z ∈ x

Hypothesis H6 : z ∈ y

Hypothesis H7 : PNoEq_ z (λw : set ⇒ ∀p2 : set → prop, PNo_rel_strict_imv P Q (ordsucc w) p2 → p2 w) p

Hypothesis H9 : ordinal z

Hypothesis H10 : ordinal (ordsucc z)

Hypothesis H11 : PNo_rel_strict_imv P Q (ordsucc z) q

Hypothesis H12 : PNo_rel_strict_upperbd P (ordsucc z) q

Theorem. (Conj_PNo_rel_imv_ex__71__8)

PNoLt z p (ordsucc z) q → q z

In Proofgold the corresponding term root is 1875f2... and proposition id is 1b79cd...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_rel_imv_ex__71__8

Beginning of Section Conj_PNo_rel_imv_ex__73__4

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

Variable Q : (set → ((set → prop) → prop))

Variable x : set

Variable y : set

Variable p : (set → prop)

Variable z : set

Hypothesis H0 : TransSet x

Hypothesis H1 : (∀w : set, w ∈ x → ordsucc w ∈ x)

Hypothesis H2 : (∀w : set, w ∈ x → PNo_rel_strict_uniq_imv P Q w (λu : set ⇒ ∀q : set → prop, PNo_rel_strict_imv P Q (ordsucc u) q → q u))

Hypothesis H3 : PNo_downc P y p

Hypothesis H5 : z ∈ x

Hypothesis H6 : z ∈ y

Hypothesis H7 : PNoEq_ z (λw : set ⇒ ∀q : set → prop, PNo_rel_strict_imv P Q (ordsucc w) q → q w) p

Hypothesis H8 : ¬ (∀q : set → prop, PNo_rel_strict_imv P Q (ordsucc z) q → q z)

Hypothesis H9 : p z

Theorem. (Conj_PNo_rel_imv_ex__73__4)

ordinal z → PNoLt y p x (λw : set ⇒ ∀q : set → prop, PNo_rel_strict_imv P Q (ordsucc w) q → q w)

In Proofgold the corresponding term root is 1de5d2... and proposition id is feb97a...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_rel_imv_ex__73__4

Beginning of Section Conj_PNo_rel_imv_ex__75__0

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

Variable Q : (set → ((set → prop) → prop))

Variable x : set

Variable y : set

Variable p : (set → prop)

Hypothesis H1 : TransSet x

Hypothesis H2 : (∀z : set, z ∈ x → ordsucc z ∈ x)

Hypothesis H3 : (∀z : set, z ∈ x → PNo_rel_strict_uniq_imv P Q z (λw : set ⇒ ∀q : set → prop, PNo_rel_strict_imv P Q (ordsucc w) q → q w))

Hypothesis H4 : y ∈ x

Hypothesis H5 : PNo_downc P y p

Theorem. (Conj_PNo_rel_imv_ex__75__0)

ordinal y → PNoLt y p x (λz : set ⇒ ∀q : set → prop, PNo_rel_strict_imv P Q (ordsucc z) q → q z)

In Proofgold the corresponding term root is 43c9c7... and proposition id is 5f8026...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_rel_imv_ex__75__0

Beginning of Section Conj_PNo_rel_imv_ex__77__2

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

Variable Q : (set → ((set → prop) → prop))

Variable x : set

Hypothesis H0 : ordinal x

Hypothesis H1 : TransSet x

Hypothesis H3 : (∀y : set, y ∈ x → (∃p : set → prop, PNo_rel_strict_uniq_imv P Q y p))

Hypothesis H4 : (∀y : set, y ∈ x → ordsucc y ∈ x)

Theorem. (Conj_PNo_rel_imv_ex__77__2)

¬ (∀y : set, ordinal y → y ∈ x → PNo_rel_strict_uniq_imv P Q y (λz : set ⇒ ∀p : set → prop, PNo_rel_strict_imv P Q (ordsucc z) p → p z))

In Proofgold the corresponding term root is d1dcc5... and proposition id is 773d2d...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_rel_imv_ex__77__2

Beginning of Section Conj_PNo_lenbdd_strict_imv_extend0__3__3

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

Variable x : set

Variable p : (set → prop)

Variable y : set

Variable q : (set → prop)

Hypothesis H0 : ordinal x

Hypothesis H1 : PNo_lenbdd x P

Hypothesis H2 : PNo_rel_strict_lowerbd P x p

Hypothesis H4 : PNoEq_ x p (λz : set ⇒ p z ∧ z ≠ x)

Hypothesis H5 : y ∈ ordsucc x

Hypothesis H6 : PNo_upc P y q

Theorem. (Conj_PNo_lenbdd_strict_imv_extend0__3__3)

ordinal y → PNoLt (ordsucc x) (λz : set ⇒ p z ∧ z ≠ x) y q

In Proofgold the corresponding term root is 47e1a3... and proposition id is c6c301...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_lenbdd_strict_imv_extend0__3__3

Beginning of Section Conj_PNo_lenbdd_strict_imv_extend0__4__2

Variable x : set

Variable p : (set → prop)

Variable y : set

Variable q : (set → prop)

Variable z : set

Hypothesis H0 : ordinal x

Hypothesis H1 : TransSet x

Hypothesis H3 : y ∈ x

Hypothesis H4 : z ∈ y

Theorem. (Conj_PNo_lenbdd_strict_imv_extend0__4__2)

z ∈ x → PNoEq_ z (λw : set ⇒ p w ∧ w ≠ x) q ∧ ¬ (p z ∧ z ≠ x) ∧ q z → PNoLt x p y q

In Proofgold the corresponding term root is 4b7934... and proposition id is 2db1e1...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_lenbdd_strict_imv_extend0__4__2

Beginning of Section Conj_PNo_lenbdd_strict_imv_extend0__5__0

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

Variable x : set

Variable p : (set → prop)

Variable y : set

Variable q : (set → prop)

Hypothesis H1 : TransSet x

Hypothesis H2 : PNo_rel_strict_upperbd P x p

Hypothesis H3 : ordinal (ordsucc x)

Hypothesis H4 : PNoEq_ x p (λz : set ⇒ p z ∧ z ≠ x)

Hypothesis H5 : ordinal y

Hypothesis H6 : y ∈ x

Hypothesis H7 : y ∈ ordsucc x

Hypothesis H8 : PNo_downc P y q

Theorem. (Conj_PNo_lenbdd_strict_imv_extend0__5__0)

PNoLt y q x p → PNoLt y q (ordsucc x) (λz : set ⇒ p z ∧ z ≠ x)

In Proofgold the corresponding term root is db129c... and proposition id is e737e1...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_lenbdd_strict_imv_extend0__5__0

Beginning of Section Conj_PNo_lenbdd_strict_imv_extend0__6__7

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

Variable x : set

Variable p : (set → prop)

Variable y : set

Variable q : (set → prop)

Hypothesis H0 : ordinal x

Hypothesis H1 : TransSet x

Hypothesis H2 : PNo_rel_strict_upperbd P x p

Hypothesis H3 : ordinal (ordsucc x)

Hypothesis H4 : PNoEq_ x p (λz : set ⇒ p z ∧ z ≠ x)

Hypothesis H5 : ordinal y

Hypothesis H6 : P y q

Hypothesis H8 : y ∈ ordsucc x

Theorem. (Conj_PNo_lenbdd_strict_imv_extend0__6__7)

PNo_downc P y q → PNoLt y q (ordsucc x) (λz : set ⇒ p z ∧ z ≠ x)

In Proofgold the corresponding term root is 6007a4... and proposition id is f7371a...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_lenbdd_strict_imv_extend0__6__7

Beginning of Section Conj_PNo_lenbdd_strict_imv_extend0__9__0

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

Variable x : set

Variable p : (set → prop)

Variable y : set

Variable q : (set → prop)

Hypothesis H1 : TransSet x

Hypothesis H2 : PNo_lenbdd x P

Hypothesis H3 : PNo_rel_strict_upperbd P x p

Hypothesis H4 : ordinal (ordsucc x)

Hypothesis H5 : PNoEq_ x p (λz : set ⇒ p z ∧ z ≠ x)

Hypothesis H6 : y ∈ ordsucc x

Hypothesis H7 : PNo_downc P y q

Theorem. (Conj_PNo_lenbdd_strict_imv_extend0__9__0)

ordinal y → PNoLt y q (ordsucc x) (λz : set ⇒ p z ∧ z ≠ x)

In Proofgold the corresponding term root is c6e08d... and proposition id is ab4fa2...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_lenbdd_strict_imv_extend0__9__0

Beginning of Section Conj_PNo_lenbdd_strict_imv_extend0__10__0

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

Variable Q : (set → ((set → prop) → prop))

Variable x : set

Variable p : (set → prop)

Hypothesis H1 : TransSet x

Hypothesis H2 : PNo_lenbdd x P

Hypothesis H3 : PNo_lenbdd x Q

Hypothesis H4 : PNo_rel_strict_upperbd P x p

Hypothesis H5 : PNo_rel_strict_lowerbd Q x p

Hypothesis H6 : ordinal (ordsucc x)

Theorem. (Conj_PNo_lenbdd_strict_imv_extend0__10__0)

PNoEq_ x p (λy : set ⇒ p y ∧ y ≠ x) → PNo_rel_strict_upperbd P (ordsucc x) (λy : set ⇒ p y ∧ y ≠ x) ∧ PNo_rel_strict_lowerbd Q (ordsucc x) (λy : set ⇒ p y ∧ y ≠ x)

In Proofgold the corresponding term root is ea39d4... and proposition id is fa1af6...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_lenbdd_strict_imv_extend0__10__0

Beginning of Section Conj_PNo_lenbdd_strict_imv_extend1__2__0

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

Variable x : set

Variable p : (set → prop)

Variable y : set

Variable q : (set → prop)

Hypothesis H1 : TransSet x

Hypothesis H2 : PNo_rel_strict_lowerbd P x p

Hypothesis H3 : ordinal (ordsucc x)

Hypothesis H4 : PNoEq_ x p (λz : set ⇒ p z ∨ z = x)

Hypothesis H5 : ordinal y

Hypothesis H6 : y ∈ x

Hypothesis H7 : y ∈ ordsucc x

Hypothesis H8 : PNo_upc P y q

Theorem. (Conj_PNo_lenbdd_strict_imv_extend1__2__0)

PNoLt x p y q → PNoLt (ordsucc x) (λz : set ⇒ p z ∨ z = x) y q

In Proofgold the corresponding term root is a48c87... and proposition id is acf5b6...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_lenbdd_strict_imv_extend1__2__0

Beginning of Section Conj_PNo_lenbdd_strict_imv_extend1__2__1

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

Variable x : set

Variable p : (set → prop)

Variable y : set

Variable q : (set → prop)

Hypothesis H0 : ordinal x

Hypothesis H2 : PNo_rel_strict_lowerbd P x p

Hypothesis H3 : ordinal (ordsucc x)

Hypothesis H4 : PNoEq_ x p (λz : set ⇒ p z ∨ z = x)

Hypothesis H5 : ordinal y

Hypothesis H6 : y ∈ x

Hypothesis H7 : y ∈ ordsucc x

Hypothesis H8 : PNo_upc P y q

Theorem. (Conj_PNo_lenbdd_strict_imv_extend1__2__1)

PNoLt x p y q → PNoLt (ordsucc x) (λz : set ⇒ p z ∨ z = x) y q

In Proofgold the corresponding term root is f5faa9... and proposition id is f4b34f...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_lenbdd_strict_imv_extend1__2__1

Beginning of Section Conj_PNo_lenbdd_strict_imv_extend1__2__5

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

Variable x : set

Variable p : (set → prop)

Variable y : set

Variable q : (set → prop)

Hypothesis H0 : ordinal x

Hypothesis H1 : TransSet x

Hypothesis H2 : PNo_rel_strict_lowerbd P x p

Hypothesis H3 : ordinal (ordsucc x)

Hypothesis H4 : PNoEq_ x p (λz : set ⇒ p z ∨ z = x)

Hypothesis H6 : y ∈ x

Hypothesis H7 : y ∈ ordsucc x

Hypothesis H8 : PNo_upc P y q

Theorem. (Conj_PNo_lenbdd_strict_imv_extend1__2__5)

PNoLt x p y q → PNoLt (ordsucc x) (λz : set ⇒ p z ∨ z = x) y q

In Proofgold the corresponding term root is 98bd96... and proposition id is 8008ed...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_lenbdd_strict_imv_extend1__2__5

Beginning of Section Conj_PNo_lenbdd_strict_imv_extend1__4__6

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

Variable x : set

Variable p : (set → prop)

Variable y : set

Variable q : (set → prop)

Hypothesis H0 : ordinal x

Hypothesis H1 : TransSet x

Hypothesis H2 : PNo_rel_strict_lowerbd P x p

Hypothesis H3 : ordinal (ordsucc x)

Hypothesis H4 : PNoEq_ x p (λz : set ⇒ p z ∨ z = x)

Hypothesis H5 : ordinal y

Hypothesis H7 : y ∈ x

Theorem. (Conj_PNo_lenbdd_strict_imv_extend1__4__6)

y ∈ ordsucc x → PNoLt (ordsucc x) (λz : set ⇒ p z ∨ z = x) y q

In Proofgold the corresponding term root is 464827... and proposition id is 5626a9...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_lenbdd_strict_imv_extend1__4__6

Beginning of Section Conj_PNo_lenbdd_strict_imv_extend1__7__6

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

Variable x : set

Variable p : (set → prop)

Variable y : set

Variable q : (set → prop)

Hypothesis H0 : ordinal x

Hypothesis H1 : TransSet x

Hypothesis H2 : PNo_lenbdd x P

Hypothesis H3 : PNo_rel_strict_lowerbd P x p

Hypothesis H4 : ordinal (ordsucc x)

Hypothesis H5 : PNoEq_ x p (λz : set ⇒ p z ∨ z = x)

Hypothesis H7 : PNo_upc P y q

Theorem. (Conj_PNo_lenbdd_strict_imv_extend1__7__6)

ordinal y → PNoLt (ordsucc x) (λz : set ⇒ p z ∨ z = x) y q

In Proofgold the corresponding term root is d948b1... and proposition id is 05de45...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_lenbdd_strict_imv_extend1__7__6

Beginning of Section Conj_PNo_strict_upperbd_imp_rel_strict_upperbd__1__5

Variable x : set

Variable y : set

Variable p : (set → prop)

Variable z : set

Variable q : (set → prop)

Hypothesis H0 : ordinal x

Hypothesis H1 : z ∈ y

Hypothesis H2 : TransSet x

Hypothesis H3 : ordinal y

Hypothesis H4 : ordinal z

Hypothesis H6 : PNoLt z q x p

Hypothesis H7 : z ∈ x

Theorem. (Conj_PNo_strict_upperbd_imp_rel_strict_upperbd__1__5)

Subq z x → PNoLt z q y p

In Proofgold the corresponding term root is 19af79... and proposition id is e8dc29...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_strict_upperbd_imp_rel_strict_upperbd__1__5

Beginning of Section Conj_PNo_strict_upperbd_imp_rel_strict_upperbd__3__9

Variable x : set

Variable y : set

Variable p : (set → prop)

Variable z : set

Variable q : (set → prop)

Variable w : set

Variable p2 : (set → prop)

Hypothesis H0 : ordinal x

Hypothesis H1 : y ∈ ordsucc x

Hypothesis H2 : z ∈ y

Hypothesis H3 : TransSet x

Hypothesis H4 : ordinal y

Hypothesis H5 : ordinal z

Hypothesis H6 : Subq z y

Hypothesis H7 : ordinal w

Hypothesis H8 : PNoLe z q w p2

Theorem. (Conj_PNo_strict_upperbd_imp_rel_strict_upperbd__3__9)

PNoLt z q x p → PNoLt z q y p

In Proofgold the corresponding term root is 57a9c8... and proposition id is 3a5b6c...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_strict_upperbd_imp_rel_strict_upperbd__3__9

Beginning of Section Conj_PNo_strict_upperbd_imp_rel_strict_upperbd__4__0

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

Variable x : set

Variable y : set

Variable p : (set → prop)

Variable z : set

Variable q : (set → prop)

Variable w : set

Variable p2 : (set → prop)

Hypothesis H1 : y ∈ ordsucc x

Hypothesis H2 : PNo_strict_upperbd P x p

Hypothesis H3 : z ∈ y

Hypothesis H4 : TransSet x

Hypothesis H5 : ordinal y

Hypothesis H6 : ordinal z

Hypothesis H7 : Subq z y

Hypothesis H8 : ordinal w

Hypothesis H9 : P w p2

Hypothesis H10 : PNoLe z q w p2

Theorem. (Conj_PNo_strict_upperbd_imp_rel_strict_upperbd__4__0)

PNoLt w p2 x p → PNoLt z q y p

In Proofgold the corresponding term root is 6be64c... and proposition id is 3d4191...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_strict_upperbd_imp_rel_strict_upperbd__4__0

Beginning of Section Conj_PNo_strict_upperbd_imp_rel_strict_upperbd__7__4

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

Variable x : set

Variable y : set

Variable p : (set → prop)

Variable z : set

Variable q : (set → prop)

Hypothesis H0 : ordinal x

Hypothesis H1 : y ∈ ordsucc x

Hypothesis H2 : PNo_strict_upperbd P x p

Hypothesis H3 : z ∈ y

Hypothesis H5 : TransSet x

Hypothesis H6 : ordinal y

Theorem. (Conj_PNo_strict_upperbd_imp_rel_strict_upperbd__7__4)

TransSet y → PNoLt z q y p

In Proofgold the corresponding term root is 0504d8... and proposition id is b18346...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_strict_upperbd_imp_rel_strict_upperbd__7__4

Beginning of Section Conj_PNo_strict_upperbd_imp_rel_strict_upperbd__9__2

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

Variable x : set

Variable y : set

Variable p : (set → prop)

Variable z : set

Variable q : (set → prop)

Hypothesis H0 : ordinal x

Hypothesis H1 : y ∈ ordsucc x

Hypothesis H3 : z ∈ y

Hypothesis H4 : PNo_downc P z q

Hypothesis H5 : TransSet x

Theorem. (Conj_PNo_strict_upperbd_imp_rel_strict_upperbd__9__2)

ordinal (ordsucc x) → PNoLt z q y p

In Proofgold the corresponding term root is d165a1... and proposition id is 973e14...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_strict_upperbd_imp_rel_strict_upperbd__9__2

Beginning of Section Conj_PNo_strict_lowerbd_imp_rel_strict_lowerbd__4__8

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

Variable x : set

Variable y : set

Variable p : (set → prop)

Variable z : set

Variable q : (set → prop)

Variable w : set

Variable p2 : (set → prop)

Hypothesis H0 : ordinal x

Hypothesis H1 : y ∈ ordsucc x

Hypothesis H2 : PNo_strict_lowerbd P x p

Hypothesis H3 : z ∈ y

Hypothesis H4 : TransSet x

Hypothesis H5 : ordinal y

Hypothesis H6 : ordinal z

Hypothesis H7 : Subq z y

Hypothesis H9 : P w p2

Hypothesis H10 : PNoLe w p2 z q

Theorem. (Conj_PNo_strict_lowerbd_imp_rel_strict_lowerbd__4__8)

PNoLt x p w p2 → PNoLt y p z q

In Proofgold the corresponding term root is 3eff33... and proposition id is 0009bf...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_strict_lowerbd_imp_rel_strict_lowerbd__4__8

Beginning of Section Conj_PNo_strict_lowerbd_imp_rel_strict_lowerbd__5__5

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

Variable x : set

Variable y : set

Variable p : (set → prop)

Variable z : set

Variable q : (set → prop)

Hypothesis H0 : ordinal x

Hypothesis H1 : y ∈ ordsucc x

Hypothesis H2 : PNo_strict_lowerbd P x p

Hypothesis H3 : z ∈ y

Hypothesis H4 : PNo_upc P z q

Hypothesis H6 : ordinal y

Hypothesis H7 : TransSet y

Hypothesis H8 : ordinal z

Theorem. (Conj_PNo_strict_lowerbd_imp_rel_strict_lowerbd__5__5)

Subq z y → PNoLt y p z q

In Proofgold the corresponding term root is 98f54d... and proposition id is ed1ac3...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_strict_lowerbd_imp_rel_strict_lowerbd__5__5

Beginning of Section Conj_PNo_strict_lowerbd_imp_rel_strict_lowerbd__7__2

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

Variable x : set

Variable y : set

Variable p : (set → prop)

Variable z : set

Variable q : (set → prop)

Hypothesis H0 : ordinal x

Hypothesis H1 : y ∈ ordsucc x

Hypothesis H3 : z ∈ y

Hypothesis H4 : PNo_upc P z q

Hypothesis H5 : TransSet x

Hypothesis H6 : ordinal y

Theorem. (Conj_PNo_strict_lowerbd_imp_rel_strict_lowerbd__7__2)

TransSet y → PNoLt y p z q

In Proofgold the corresponding term root is 3620ac... and proposition id is 76f790...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_strict_lowerbd_imp_rel_strict_lowerbd__7__2

Beginning of Section Conj_PNo_rel_split_imv_imp_strict_imv__3__0

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

Variable x : set

Variable p : (set → prop)

Variable y : set

Variable q : (set → prop)

Variable z : set

Hypothesis H1 : ordinal (ordsucc x)

Hypothesis H2 : PNo_rel_strict_lowerbd P (ordsucc x) (λw : set ⇒ p w ∨ w = x)

Hypothesis H3 : ordinal y

Hypothesis H4 : P y q

Hypothesis H5 : z ∈ ordsucc x

Hypothesis H6 : PNoEq_ z q p

Hypothesis H7 : p z ∨ z = x

Hypothesis H8 : ordinal z

Hypothesis H9 : PNoLt y q z q

Theorem. (Conj_PNo_rel_split_imv_imp_strict_imv__3__0)

¬ PNo_upc P z q

In Proofgold the corresponding term root is e36d58... and proposition id is 730d7b...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_rel_split_imv_imp_strict_imv__3__0

Beginning of Section Conj_PNo_rel_split_imv_imp_strict_imv__11__7

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

Variable x : set

Variable p : (set → prop)

Variable y : set

Variable q : (set → prop)

Variable z : set

Hypothesis H0 : ordinal x

Hypothesis H1 : ordinal (ordsucc x)

Hypothesis H2 : PNo_rel_strict_upperbd P (ordsucc x) (λw : set ⇒ p w ∧ w ≠ x)

Hypothesis H3 : ordinal y

Hypothesis H4 : P y q

Hypothesis H5 : z ∈ ordsucc x

Hypothesis H6 : PNoEq_ z p q

Hypothesis H8 : ordinal z

Hypothesis H9 : PNoLt z q y q

Theorem. (Conj_PNo_rel_split_imv_imp_strict_imv__11__7)

¬ PNo_downc P z q

In Proofgold the corresponding term root is 9002a6... and proposition id is f680b2...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_rel_split_imv_imp_strict_imv__11__7

Beginning of Section Conj_PNo_rel_split_imv_imp_strict_imv__14__6

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

Variable x : set

Variable p : (set → prop)

Variable y : set

Variable q : (set → prop)

Hypothesis H0 : ordinal x

Hypothesis H1 : ordinal (ordsucc x)

Hypothesis H2 : PNo_rel_strict_upperbd P (ordsucc x) (λz : set ⇒ p z ∧ z ≠ x)

Hypothesis H3 : ¬ (p x ∧ x ≠ x)

Hypothesis H4 : ordinal y

Hypothesis H5 : P y q

Theorem. (Conj_PNo_rel_split_imv_imp_strict_imv__14__6)

(∀z : set, z ∈ ordsucc x → z ∈ y → PNoEq_ z p q → q z → p z ∧ z ≠ x) → PNoLt y q x p

In Proofgold the corresponding term root is 43ba98... and proposition id is 42ce31...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_rel_split_imv_imp_strict_imv__14__6

Beginning of Section Conj_PNo_rel_split_imv_imp_strict_imv__15__2

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

Variable x : set

Variable p : (set → prop)

Variable y : set

Variable q : (set → prop)

Hypothesis H0 : ordinal x

Hypothesis H1 : ordinal (ordsucc x)

Hypothesis H3 : ¬ (p x ∧ x ≠ x)

Hypothesis H4 : PNoLt (ordsucc x) (λz : set ⇒ p z ∧ z ≠ x) x p

Hypothesis H5 : ordinal y

Hypothesis H6 : P y q

Hypothesis H7 : PNo_downc P y q

Theorem. (Conj_PNo_rel_split_imv_imp_strict_imv__15__2)

(y ∈ ordsucc x → PNoLt y q x p) → PNoLt y q x p

In Proofgold the corresponding term root is 0b205f... and proposition id is 8f0e92...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_rel_split_imv_imp_strict_imv__15__2

Beginning of Section Conj_PNo_rel_split_imv_imp_strict_imv__15__6

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

Variable x : set

Variable p : (set → prop)

Variable y : set

Variable q : (set → prop)

Hypothesis H0 : ordinal x

Hypothesis H1 : ordinal (ordsucc x)

Hypothesis H2 : PNo_rel_strict_upperbd P (ordsucc x) (λz : set ⇒ p z ∧ z ≠ x)

Hypothesis H3 : ¬ (p x ∧ x ≠ x)

Hypothesis H4 : PNoLt (ordsucc x) (λz : set ⇒ p z ∧ z ≠ x) x p

Hypothesis H5 : ordinal y

Hypothesis H7 : PNo_downc P y q

Theorem. (Conj_PNo_rel_split_imv_imp_strict_imv__15__6)

(y ∈ ordsucc x → PNoLt y q x p) → PNoLt y q x p

In Proofgold the corresponding term root is fbb0de... and proposition id is 03512a...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_rel_split_imv_imp_strict_imv__15__6

Beginning of Section Conj_PNo_rel_split_imv_imp_strict_imv__19__4

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

Variable Q : (set → ((set → prop) → prop))

Variable x : set

Variable p : (set → prop)

Hypothesis H0 : ordinal x

Hypothesis H1 : ordinal (ordsucc x)

Hypothesis H2 : PNo_rel_strict_upperbd P (ordsucc x) (λy : set ⇒ p y ∧ y ≠ x)

Hypothesis H3 : PNo_rel_strict_lowerbd Q (ordsucc x) (λy : set ⇒ p y ∨ y = x)

Theorem. (Conj_PNo_rel_split_imv_imp_strict_imv__19__4)

p x ∨ x = x → PNo_strict_upperbd P x p ∧ PNo_strict_lowerbd Q x p

In Proofgold the corresponding term root is 209657... and proposition id is efcf62...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_rel_split_imv_imp_strict_imv__19__4

Beginning of Section Conj_PNo_strict_imv_pred_eq__3__7

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

Variable Q : (set → ((set → prop) → prop))

Variable x : set

Variable p : (set → prop)

Variable q : (set → prop)

Variable y : set

Hypothesis H0 : ordinal x

Hypothesis H1 : (∀z : set, z ∈ x → (∀p2 : set → prop, ¬ PNo_strict_imv P Q z p2))

Hypothesis H2 : PNo_strict_lowerbd Q x p

Hypothesis H3 : PNo_strict_upperbd P x q

Hypothesis H4 : ordinal y

Hypothesis H5 : y ∈ x

Hypothesis H6 : ¬ q y

Theorem. (Conj_PNo_strict_imv_pred_eq__3__7)

¬ PNoLt x q y q

In Proofgold the corresponding term root is b6294d... and proposition id is f2e677...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_strict_imv_pred_eq__3__7

Beginning of Section Conj_PNo_strict_imv_pred_eq__6__3

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

Variable Q : (set → ((set → prop) → prop))

Variable x : set

Variable p : (set → prop)

Variable q : (set → prop)

Hypothesis H0 : ordinal x

Hypothesis H1 : TransSet x

Hypothesis H2 : (∀y : set, y ∈ x → (∀p2 : set → prop, ¬ PNo_strict_imv P Q y p2))

Hypothesis H4 : PNo_strict_lowerbd Q x p

Hypothesis H5 : PNo_strict_upperbd P x q

Hypothesis H6 : PNo_strict_lowerbd Q x q

Theorem. (Conj_PNo_strict_imv_pred_eq__6__3)

(∀y : set, ordinal y → y ∈ x → (p y ↔ q y)) → (∀y : set, y ∈ x → (p y ↔ q y))

In Proofgold the corresponding term root is 740615... and proposition id is d71fbf...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_strict_imv_pred_eq__6__3

Beginning of Section Conj_PNo_bd_In__1__3

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

Variable Q : (set → ((set → prop) → prop))

Variable x : set

Variable y : set

Variable p : (set → prop)

Hypothesis H0 : (∀z : set, z ∈ PNo_bd P Q → (∀q : set → prop, ¬ PNo_strict_imv P Q z q))

Hypothesis H1 : y ∈ ordsucc x

Hypothesis H2 : PNo_strict_imv P Q y p

Theorem. (Conj_PNo_bd_In__1__3)

¬ y ∈ PNo_bd P Q

In Proofgold the corresponding term root is 75a884... and proposition id is 33d612...

Proof:

The rest of the proof is missing.

End of Section Conj_PNo_bd_In__1__3

Beginning of Section Conj_SNoLtE__1__3

Variable x : set

Variable y : set

Variable P : prop

Variable z : set

Hypothesis H0 : (∀w : set, SNo w → SNoLev w ∈ binintersect (SNoLev x) (SNoLev y) → SNoEq_ (SNoLev w) w x → SNoEq_ (SNoLev w) w y → x < w → w < y → nIn (SNoLev w) x → SNoLev w ∈ y → P)

Hypothesis H1 : z ∈ binintersect (SNoLev x) (SNoLev y)

Hypothesis H2 : PNoEq_ z (λw : set ⇒ w ∈ x) (λw : set ⇒ w ∈ y)

Hypothesis H4 : z ∈ y

Hypothesis H5 : z ∈ SNoLev x

Hypothesis H6 : z ∈ SNoLev y

Hypothesis H7 : SNo (PSNo z (λw : set ⇒ w ∈ x))

Hypothesis H8 : SNoLev (PSNo z (λw : set ⇒ w ∈ x)) = z

Hypothesis H9 : SNoEq_ z (PSNo z (λw : set ⇒ w ∈ x)) x

Theorem. (Conj_SNoLtE__1__3)

SNoEq_ z (PSNo z (λw : set ⇒ w ∈ x)) y → P

In Proofgold the corresponding term root is 445d91... and proposition id is 267f4b...

Proof:

The rest of the proof is missing.

End of Section Conj_SNoLtE__1__3

Beginning of Section Conj_SNoLtE__1__4

Variable x : set

Variable y : set

Variable P : prop

Variable z : set

Hypothesis H0 : (∀w : set, SNo w → SNoLev w ∈ binintersect (SNoLev x) (SNoLev y) → SNoEq_ (SNoLev w) w x → SNoEq_ (SNoLev w) w y → x < w → w < y → nIn (SNoLev w) x → SNoLev w ∈ y → P)

Hypothesis H1 : z ∈ binintersect (SNoLev x) (SNoLev y)

Hypothesis H2 : PNoEq_ z (λw : set ⇒ w ∈ x) (λw : set ⇒ w ∈ y)

Hypothesis H3 : ¬ z ∈ x

Hypothesis H5 : z ∈ SNoLev x

Hypothesis H6 : z ∈ SNoLev y

Hypothesis H7 : SNo (PSNo z (λw : set ⇒ w ∈ x))

Hypothesis H8 : SNoLev (PSNo z (λw : set ⇒ w ∈ x)) = z

Hypothesis H9 : SNoEq_ z (PSNo z (λw : set ⇒ w ∈ x)) x

Theorem. (Conj_SNoLtE__1__4)

SNoEq_ z (PSNo z (λw : set ⇒ w ∈ x)) y → P

In Proofgold the corresponding term root is 2f0432... and proposition id is 2719d2...

Proof:

The rest of the proof is missing.

End of Section Conj_SNoLtE__1__4

Beginning of Section Conj_SNoLtE__1__5

Variable x : set

Variable y : set

Variable P : prop

Variable z : set

Hypothesis H0 : (∀w : set, SNo w → SNoLev w ∈ binintersect (SNoLev x) (SNoLev y) → SNoEq_ (SNoLev w) w x → SNoEq_ (SNoLev w) w y → x < w → w < y → nIn (SNoLev w) x → SNoLev w ∈ y → P)

Hypothesis H1 : z ∈ binintersect (SNoLev x) (SNoLev y)

Hypothesis H2 : PNoEq_ z (λw : set ⇒ w ∈ x) (λw : set ⇒ w ∈ y)

Hypothesis H3 : ¬ z ∈ x

Hypothesis H4 : z ∈ y

Hypothesis H6 : z ∈ SNoLev y

Hypothesis H7 : SNo (PSNo z (λw : set ⇒ w ∈ x))

Hypothesis H8 : SNoLev (PSNo z (λw : set ⇒ w ∈ x)) = z

Hypothesis H9 : SNoEq_ z (PSNo z (λw : set ⇒ w ∈ x)) x

Theorem. (Conj_SNoLtE__1__5)

SNoEq_ z (PSNo z (λw : set ⇒ w ∈ x)) y → P

In Proofgold the corresponding term root is f86dba... and proposition id is f28ab9...

Proof:

The rest of the proof is missing.

End of Section Conj_SNoLtE__1__5

Beginning of Section Conj_SNoLtE__1__8

Variable x : set

Variable y : set

Variable P : prop

Variable z : set

Hypothesis H0 : (∀w : set, SNo w → SNoLev w ∈ binintersect (SNoLev x) (SNoLev y) → SNoEq_ (SNoLev w) w x → SNoEq_ (SNoLev w) w y → x < w → w < y → nIn (SNoLev w) x → SNoLev w ∈ y → P)

Hypothesis H1 : z ∈ binintersect (SNoLev x) (SNoLev y)

Hypothesis H2 : PNoEq_ z (λw : set ⇒ w ∈ x) (λw : set ⇒ w ∈ y)

Hypothesis H3 : ¬ z ∈ x

Hypothesis H4 : z ∈ y

Hypothesis H5 : z ∈ SNoLev x

Hypothesis H6 : z ∈ SNoLev y

Hypothesis H7 : SNo (PSNo z (λw : set ⇒ w ∈ x))

Hypothesis H9 : SNoEq_ z (PSNo z (λw : set ⇒ w ∈ x)) x

Theorem. (Conj_SNoLtE__1__8)

SNoEq_ z (PSNo z (λw : set ⇒ w ∈ x)) y → P

In Proofgold the corresponding term root is c01103... and proposition id is c3520c...

Proof:

The rest of the proof is missing.

End of Section Conj_SNoLtE__1__8

Beginning of Section Conj_SNoLtE__1__9

Variable x : set

Variable y : set

Variable P : prop

Variable z : set

Hypothesis H0 : (∀w : set, SNo w → SNoLev w ∈ binintersect (SNoLev x) (SNoLev y) → SNoEq_ (SNoLev w) w x → SNoEq_ (SNoLev w) w y → x < w → w < y → nIn (SNoLev w) x → SNoLev w ∈ y → P)

Hypothesis H1 : z ∈ binintersect (SNoLev x) (SNoLev y)

Hypothesis H2 : PNoEq_ z (λw : set ⇒ w ∈ x) (λw : set ⇒ w ∈ y)

Hypothesis H3 : ¬ z ∈ x

Hypothesis H4 : z ∈ y

Hypothesis H5 : z ∈ SNoLev x

Hypothesis H6 : z ∈ SNoLev y

Hypothesis H7 : SNo (PSNo z (λw : set ⇒ w ∈ x))

Hypothesis H8 : SNoLev (PSNo z (λw : set ⇒ w ∈ x)) = z

Theorem. (Conj_SNoLtE__1__9)

SNoEq_ z (PSNo z (λw : set ⇒ w ∈ x)) y → P

In Proofgold the corresponding term root is ddbb2e... and proposition id is 8612ba...

Proof:

The rest of the proof is missing.

End of Section Conj_SNoLtE__1__9

Beginning of Section Conj_SNoLtE__6__5

Variable x : set

Variable y : set

Variable P : prop

Variable z : set

Hypothesis H0 : (∀w : set, SNo w → SNoLev w ∈ binintersect (SNoLev x) (SNoLev y) → SNoEq_ (SNoLev w) w x → SNoEq_ (SNoLev w) w y → x < w → w < y → nIn (SNoLev w) x → SNoLev w ∈ y → P)

Hypothesis H1 : ordinal (SNoLev x)

Hypothesis H2 : z ∈ binintersect (SNoLev x) (SNoLev y)

Hypothesis H3 : PNoEq_ z (λw : set ⇒ w ∈ x) (λw : set ⇒ w ∈ y)

Hypothesis H4 : ¬ z ∈ x

Hypothesis H6 : z ∈ SNoLev x

Hypothesis H7 : z ∈ SNoLev y

Theorem. (Conj_SNoLtE__6__5)

ordinal z → P

In Proofgold the corresponding term root is 4f4229... and proposition id is 98564e...

Proof:

The rest of the proof is missing.

End of Section Conj_SNoLtE__6__5

Beginning of Section Conj_SNoLtE__8__3

Variable x : set

Variable y : set

Variable P : prop

Hypothesis H0 : SNo x

Hypothesis H1 : SNo y

Hypothesis H2 : x < y

Hypothesis H4 : SNoLev x ∈ SNoLev y → SNoEq_ (SNoLev x) x y → SNoLev x ∈ y → P

Hypothesis H5 : SNoLev y ∈ SNoLev x → SNoEq_ (SNoLev y) x y → nIn (SNoLev y) x → P

Theorem. (Conj_SNoLtE__8__3)

ordinal (SNoLev x) → P

In Proofgold the corresponding term root is 9e8f80... and proposition id is 009cab...

Proof:

The rest of the proof is missing.

End of Section Conj_SNoLtE__8__3

Beginning of Section Conj_SNoCutP_SNoCut__1__4

Variable x : set

Variable y : set

Variable z : set

Hypothesis H0 : ordinal (PNo_bd (λw : set ⇒ λp : set → prop ⇒ ordinal w ∧ PSNo w p ∈ x) (λw : set ⇒ λp : set → prop ⇒ ordinal w ∧ PSNo w p ∈ y))

Hypothesis H1 : PNo_strict_upperbd (λw : set ⇒ λp : set → prop ⇒ ordinal w ∧ PSNo w p ∈ x) (PNo_bd (λw : set ⇒ λp : set → prop ⇒ ordinal w ∧ PSNo w p ∈ x) (λw : set ⇒ λp : set → prop ⇒ ordinal w ∧ PSNo w p ∈ y)) (PNo_pred (λw : set ⇒ λp : set → prop ⇒ ordinal w ∧ PSNo w p ∈ x) (λw : set ⇒ λp : set → prop ⇒ ordinal w ∧ PSNo w p ∈ y))

Hypothesis H2 : z ∈ x

Hypothesis H3 : ordinal (SNoLev z)

Theorem. (Conj_SNoCutP_SNoCut__1__4)

ordinal (SNoLev z) ∧ PSNo (SNoLev z) (λw : set ⇒ w ∈ z) ∈ x → z < PSNo (PNo_bd (λw : set ⇒ λp : set → prop ⇒ ordinal w ∧ PSNo w p ∈ x) (λw : set ⇒ λp : set → prop ⇒ ordinal w ∧ PSNo w p ∈ y)) (PNo_pred (λw : set ⇒ λp : set → prop ⇒ ordinal w ∧ PSNo w p ∈ x) (λw : set ⇒ λp : set → prop ⇒ ordinal w ∧ PSNo w p ∈ y))

In Proofgold the corresponding term root is 47ac26... and proposition id is d9ef37...

Proof:

The rest of the proof is missing.

End of Section Conj_SNoCutP_SNoCut__1__4

Beginning of Section Conj_SNoCutP_SNoCut__9__3

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Hypothesis H0 : ordinal (PNo_bd (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ x) (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ y))

Hypothesis H1 : PNo_strict_imv (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ x) (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ y) (PNo_bd (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ x) (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ y)) (PNo_pred (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ x) (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ y))

Hypothesis H2 : (∀u : set, u ∈ PNo_bd (λv : set ⇒ λp : set → prop ⇒ ordinal v ∧ PSNo v p ∈ x) (λv : set ⇒ λp : set → prop ⇒ ordinal v ∧ PSNo v p ∈ y) → (∀p : set → prop, ¬ PNo_strict_imv (λv : set ⇒ λq : set → prop ⇒ ordinal v ∧ PSNo v q ∈ x) (λv : set ⇒ λq : set → prop ⇒ ordinal v ∧ PSNo v q ∈ y) u p))

Hypothesis H4 : PNo_strict_imv (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ x) (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ y) (SNoLev z) (λu : set ⇒ u ∈ z)

Hypothesis H5 : Subq (PNo_bd (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ x) (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ y)) (SNoLev z)

Hypothesis H6 : w ∈ PNo_bd (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ x) (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ y)

Hypothesis H7 : PNoEq_ w (λu : set ⇒ u ∈ z) (PNo_pred (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ x) (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ y))

Hypothesis H8 : nIn w z

Hypothesis H9 : PNo_pred (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ x) (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ y) w

Hypothesis H10 : ordinal w

Hypothesis H11 : ordinal (ordsucc w)

Hypothesis H12 : ¬ (w ∈ z ∧ w ≠ w)

Theorem. (Conj_SNoCutP_SNoCut__9__3)

¬ (w ∈ z ∨ w = w)

In Proofgold the corresponding term root is 16dec8... and proposition id is 039f5e...

Proof:

The rest of the proof is missing.

End of Section Conj_SNoCutP_SNoCut__9__3

Beginning of Section Conj_SNoCutP_SNoCut__9__11

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Hypothesis H0 : ordinal (PNo_bd (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ x) (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ y))

Hypothesis H1 : PNo_strict_imv (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ x) (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ y) (PNo_bd (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ x) (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ y)) (PNo_pred (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ x) (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ y))

Hypothesis H2 : (∀u : set, u ∈ PNo_bd (λv : set ⇒ λp : set → prop ⇒ ordinal v ∧ PSNo v p ∈ x) (λv : set ⇒ λp : set → prop ⇒ ordinal v ∧ PSNo v p ∈ y) → (∀p : set → prop, ¬ PNo_strict_imv (λv : set ⇒ λq : set → prop ⇒ ordinal v ∧ PSNo v q ∈ x) (λv : set ⇒ λq : set → prop ⇒ ordinal v ∧ PSNo v q ∈ y) u p))

Hypothesis H3 : ordinal (SNoLev z)

Hypothesis H4 : PNo_strict_imv (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ x) (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ y) (SNoLev z) (λu : set ⇒ u ∈ z)

Hypothesis H5 : Subq (PNo_bd (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ x) (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ y)) (SNoLev z)

Hypothesis H6 : w ∈ PNo_bd (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ x) (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ y)

Hypothesis H7 : PNoEq_ w (λu : set ⇒ u ∈ z) (PNo_pred (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ x) (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ y))

Hypothesis H8 : nIn w z

Hypothesis H9 : PNo_pred (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ x) (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ y) w

Hypothesis H10 : ordinal w

Hypothesis H12 : ¬ (w ∈ z ∧ w ≠ w)

Theorem. (Conj_SNoCutP_SNoCut__9__11)

¬ (w ∈ z ∨ w = w)

In Proofgold the corresponding term root is dcdfad... and proposition id is 8140c3...

Proof:

The rest of the proof is missing.

End of Section Conj_SNoCutP_SNoCut__9__11

Beginning of Section Conj_SNoCutP_SNoCut__10__0

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Hypothesis H1 : PNo_strict_imv (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ x) (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ y) (PNo_bd (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ x) (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ y)) (PNo_pred (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ x) (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ y))

Hypothesis H2 : (∀u : set, u ∈ PNo_bd (λv : set ⇒ λp : set → prop ⇒ ordinal v ∧ PSNo v p ∈ x) (λv : set ⇒ λp : set → prop ⇒ ordinal v ∧ PSNo v p ∈ y) → (∀p : set → prop, ¬ PNo_strict_imv (λv : set ⇒ λq : set → prop ⇒ ordinal v ∧ PSNo v q ∈ x) (λv : set ⇒ λq : set → prop ⇒ ordinal v ∧ PSNo v q ∈ y) u p))

Hypothesis H3 : ordinal (SNoLev z)

Hypothesis H4 : PNo_strict_imv (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ x) (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ y) (SNoLev z) (λu : set ⇒ u ∈ z)

Hypothesis H5 : Subq (PNo_bd (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ x) (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ y)) (SNoLev z)

Hypothesis H6 : w ∈ PNo_bd (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ x) (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ y)

Hypothesis H7 : PNoEq_ w (λu : set ⇒ u ∈ z) (PNo_pred (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ x) (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ y))

Hypothesis H8 : nIn w z

Hypothesis H9 : PNo_pred (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ x) (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ y) w

Hypothesis H10 : ordinal w

Hypothesis H11 : ordinal (ordsucc w)

Theorem. (Conj_SNoCutP_SNoCut__10__0)

¬ ¬ (w ∈ z ∧ w ≠ w)

In Proofgold the corresponding term root is 6b8630... and proposition id is 219cfc...

Proof:

The rest of the proof is missing.

End of Section Conj_SNoCutP_SNoCut__10__0

Beginning of Section Conj_SNoCutP_SNoCut__12__7

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Hypothesis H0 : ordinal (PNo_bd (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ x) (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ y))

Hypothesis H1 : PNo_strict_imv (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ x) (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ y) (PNo_bd (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ x) (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ y)) (PNo_pred (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ x) (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ y))

Hypothesis H2 : (∀u : set, u ∈ PNo_bd (λv : set ⇒ λp : set → prop ⇒ ordinal v ∧ PSNo v p ∈ x) (λv : set ⇒ λp : set → prop ⇒ ordinal v ∧ PSNo v p ∈ y) → (∀p : set → prop, ¬ PNo_strict_imv (λv : set ⇒ λq : set → prop ⇒ ordinal v ∧ PSNo v q ∈ x) (λv : set ⇒ λq : set → prop ⇒ ordinal v ∧ PSNo v q ∈ y) u p))

Hypothesis H3 : ordinal (SNoLev z)

Hypothesis H4 : PNo_strict_imv (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ x) (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ y) (SNoLev z) (λu : set ⇒ u ∈ z)

Hypothesis H5 : Subq (PNo_bd (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ x) (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ y)) (SNoLev z)

Hypothesis H6 : w ∈ PNo_bd (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ x) (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ y)

Hypothesis H8 : nIn w z

Hypothesis H9 : PNo_pred (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ x) (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ y) w

Theorem. (Conj_SNoCutP_SNoCut__12__7)

¬ ordinal w

In Proofgold the corresponding term root is 61b482... and proposition id is f8c08b...

Proof:

The rest of the proof is missing.

End of Section Conj_SNoCutP_SNoCut__12__7

Beginning of Section Conj_SNoCutP_SNoCut__14__7

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Hypothesis H0 : ordinal (PNo_bd (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ x) (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ y))

Hypothesis H1 : PNo_strict_imv (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ x) (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ y) (PNo_bd (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ x) (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ y)) (PNo_pred (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ x) (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ y))

Hypothesis H2 : (∀u : set, u ∈ PNo_bd (λv : set ⇒ λp : set → prop ⇒ ordinal v ∧ PSNo v p ∈ x) (λv : set ⇒ λp : set → prop ⇒ ordinal v ∧ PSNo v p ∈ y) → (∀p : set → prop, ¬ PNo_strict_imv (λv : set ⇒ λq : set → prop ⇒ ordinal v ∧ PSNo v q ∈ x) (λv : set ⇒ λq : set → prop ⇒ ordinal v ∧ PSNo v q ∈ y) u p))

Hypothesis H3 : ordinal (SNoLev z)

Hypothesis H4 : PNo_strict_imv (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ x) (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ y) (SNoLev z) (λu : set ⇒ u ∈ z)

Hypothesis H5 : Subq (PNo_bd (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ x) (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ y)) (SNoLev z)

Hypothesis H6 : w ∈ PNo_bd (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ x) (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ y)

Hypothesis H8 : ¬ PNo_pred (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ x) (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ y) w

Hypothesis H9 : w ∈ z

Hypothesis H10 : ordinal w

Hypothesis H11 : ordinal (ordsucc w)

Theorem. (Conj_SNoCutP_SNoCut__14__7)

¬ ¬ (w ∈ z ∧ w ≠ w)

In Proofgold the corresponding term root is 344de8... and proposition id is 10e359...

Proof:

The rest of the proof is missing.

End of Section Conj_SNoCutP_SNoCut__14__7

Beginning of Section Conj_SNoCutP_SNoCut__15__3

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Hypothesis H0 : ordinal (PNo_bd (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ x) (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ y))

Hypothesis H1 : PNo_strict_imv (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ x) (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ y) (PNo_bd (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ x) (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ y)) (PNo_pred (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ x) (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ y))

Hypothesis H2 : (∀u : set, u ∈ PNo_bd (λv : set ⇒ λp : set → prop ⇒ ordinal v ∧ PSNo v p ∈ x) (λv : set ⇒ λp : set → prop ⇒ ordinal v ∧ PSNo v p ∈ y) → (∀p : set → prop, ¬ PNo_strict_imv (λv : set ⇒ λq : set → prop ⇒ ordinal v ∧ PSNo v q ∈ x) (λv : set ⇒ λq : set → prop ⇒ ordinal v ∧ PSNo v q ∈ y) u p))

Hypothesis H4 : PNo_strict_imv (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ x) (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ y) (SNoLev z) (λu : set ⇒ u ∈ z)

Hypothesis H5 : Subq (PNo_bd (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ x) (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ y)) (SNoLev z)

Hypothesis H6 : w ∈ PNo_bd (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ x) (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ y)

Hypothesis H7 : PNoEq_ w (PNo_pred (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ x) (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ y)) (λu : set ⇒ u ∈ z)

Hypothesis H8 : ¬ PNo_pred (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ x) (λu : set ⇒ λp : set → prop ⇒ ordinal u ∧ PSNo u p ∈ y) w

Hypothesis H9 : w ∈ z

Hypothesis H10 : ordinal w

Theorem. (Conj_SNoCutP_SNoCut__15__3)

¬ ordinal (ordsucc w)

In Proofgold the corresponding term root is 1334f6... and proposition id is 350c53...

Proof:

The rest of the proof is missing.

End of Section Conj_SNoCutP_SNoCut__15__3

Beginning of Section Conj_SNoCutP_SNoCut__20__2

Variable x : set

Variable y : set

Variable z : set

Hypothesis H0 : ordinal (PNo_bd (λw : set ⇒ λp : set → prop ⇒ ordinal w ∧ PSNo w p ∈ x) (λw : set ⇒ λp : set → prop ⇒ ordinal w ∧ PSNo w p ∈ y))

Hypothesis H1 : PNo_strict_imv (λw : set ⇒ λp : set → prop ⇒ ordinal w ∧ PSNo w p ∈ x) (λw : set ⇒ λp : set → prop ⇒ ordinal w ∧ PSNo w p ∈ y) (PNo_bd (λw : set ⇒ λp : set → prop ⇒ ordinal w ∧ PSNo w p ∈ x) (λw : set ⇒ λp : set → prop ⇒ ordinal w ∧ PSNo w p ∈ y)) (PNo_pred (λw : set ⇒ λp : set → prop ⇒ ordinal w ∧ PSNo w p ∈ x) (λw : set ⇒ λp : set → prop ⇒ ordinal w ∧ PSNo w p ∈ y))

Hypothesis H3 : SNoLev (SNoCut x y) = PNo_bd (λw : set ⇒ λp : set → prop ⇒ ordinal w ∧ PSNo w p ∈ x) (λw : set ⇒ λp : set → prop ⇒ ordinal w ∧ PSNo w p ∈ y)

Hypothesis H4 : PNoEq_ (PNo_bd (λw : set ⇒ λp : set → prop ⇒ ordinal w ∧ PSNo w p ∈ x) (λw : set ⇒ λp : set → prop ⇒ ordinal w ∧ PSNo w p ∈ y)) (λw : set ⇒ w ∈ SNoCut x y) (PNo_pred (λw : set ⇒ λp : set → prop ⇒ ordinal w ∧ PSNo w p ∈ x) (λw : set ⇒ λp : set → prop ⇒ ordinal w ∧ PSNo w p ∈ y))

Hypothesis H5 : SNo z

Hypothesis H6 : (∀w : set, w ∈ x → w < z)

Hypothesis H7 : (∀w : set, w ∈ y → z < w)

Theorem. (Conj_SNoCutP_SNoCut__20__2)

ordinal (SNoLev z) → Subq (SNoLev (SNoCut x y)) (SNoLev z) ∧ PNoEq_ (SNoLev (SNoCut x y)) (λw : set ⇒ w ∈ SNoCut x y) (λw : set ⇒ w ∈ z)

In Proofgold the corresponding term root is 46700e... and proposition id is b40f33...

Proof:

The rest of the proof is missing.

End of Section Conj_SNoCutP_SNoCut__20__2

Beginning of Section Conj_SNoCutP_SNoCut__21__7

Variable x : set

Variable y : set

Hypothesis H0 : (∀z : set, z ∈ y → SNo z)

Hypothesis H1 : ordinal (PNo_bd (λz : set ⇒ λp : set → prop ⇒ ordinal z ∧ PSNo z p ∈ x) (λz : set ⇒ λp : set → prop ⇒ ordinal z ∧ PSNo z p ∈ y))

Hypothesis H2 : PNo_strict_imv (λz : set ⇒ λp : set → prop ⇒ ordinal z ∧ PSNo z p ∈ x) (λz : set ⇒ λp : set → prop ⇒ ordinal z ∧ PSNo z p ∈ y) (PNo_bd (λz : set ⇒ λp : set → prop ⇒ ordinal z ∧ PSNo z p ∈ x) (λz : set ⇒ λp : set → prop ⇒ ordinal z ∧ PSNo z p ∈ y)) (PNo_pred (λz : set ⇒ λp : set → prop ⇒ ordinal z ∧ PSNo z p ∈ x) (λz : set ⇒ λp : set → prop ⇒ ordinal z ∧ PSNo z p ∈ y))

Hypothesis H3 : (∀z : set, z ∈ PNo_bd (λw : set ⇒ λp : set → prop ⇒ ordinal w ∧ PSNo w p ∈ x) (λw : set ⇒ λp : set → prop ⇒ ordinal w ∧ PSNo w p ∈ y) → (∀p : set → prop, ¬ PNo_strict_imv (λw : set ⇒ λq : set → prop ⇒ ordinal w ∧ PSNo w q ∈ x) (λw : set ⇒ λq : set → prop ⇒ ordinal w ∧ PSNo w q ∈ y) z p))

Hypothesis H4 : PNo_strict_lowerbd (λz : set ⇒ λp : set → prop ⇒ ordinal z ∧ PSNo z p ∈ y) (PNo_bd (λz : set ⇒ λp : set → prop ⇒ ordinal z ∧ PSNo z p ∈ x) (λz : set ⇒ λp : set → prop ⇒ ordinal z ∧ PSNo z p ∈ y)) (PNo_pred (λz : set ⇒ λp : set → prop ⇒ ordinal z ∧ PSNo z p ∈ x) (λz : set ⇒ λp : set → prop ⇒ ordinal z ∧ PSNo z p ∈ y))

Hypothesis H5 : SNo (SNoCut x y)

Hypothesis H6 : SNoLev (SNoCut x y) = PNo_bd (λz : set ⇒ λp : set → prop ⇒ ordinal z ∧ PSNo z p ∈ x) (λz : set ⇒ λp : set → prop ⇒ ordinal z ∧ PSNo z p ∈ y)

Hypothesis H8 : PNoEq_ (PNo_bd (λz : set ⇒ λp : set → prop ⇒ ordinal z ∧ PSNo z p ∈ x) (λz : set ⇒ λp : set → prop ⇒ ordinal z ∧ PSNo z p ∈ y)) (λz : set ⇒ z ∈ SNoCut x y) (PNo_pred (λz : set ⇒ λp : set → prop ⇒ ordinal z ∧ PSNo z p ∈ x) (λz : set ⇒ λp : set → prop ⇒ ordinal z ∧ PSNo z p ∈ y))

Hypothesis H9 : (∀z : set, z ∈ x → z < SNoCut x y)

Theorem. (Conj_SNoCutP_SNoCut__21__7)

(∀z : set, z ∈ y → SNoCut x y < z) → SNo (SNoCut x y) ∧ SNoLev (SNoCut x y) ∈ ordsucc (binunion (famunion x (λz : set ⇒ ordsucc (SNoLev z))) (famunion y (λz : set ⇒ ordsucc (SNoLev z)))) ∧ (∀z : set, z ∈ x → z < SNoCut x y) ∧ (∀z : set, z ∈ y → SNoCut x y < z) ∧ (∀z : set, SNo z → (∀w : set, w ∈ x → w < z) → (∀w : set, w ∈ y → z < w) → Subq (SNoLev (SNoCut x y)) (SNoLev z) ∧ PNoEq_ (SNoLev (SNoCut x y)) (λw : set ⇒ w ∈ SNoCut x y) (λw : set ⇒ w ∈ z))

In Proofgold the corresponding term root is c091db... and proposition id is 4be492...

Proof:

The rest of the proof is missing.

End of Section Conj_SNoCutP_SNoCut__21__7

Beginning of Section Conj_SNoCutP_SNoCut__29__1

Variable x : set

Variable y : set

Hypothesis H0 : (∀z : set, z ∈ x → SNo z)

Hypothesis H2 : PNoLt_pwise (λz : set ⇒ λp : set → prop ⇒ ordinal z ∧ PSNo z p ∈ x) (λz : set ⇒ λp : set → prop ⇒ ordinal z ∧ PSNo z p ∈ y)

Hypothesis H3 : ordinal (binunion (famunion x (λz : set ⇒ ordsucc (SNoLev z))) (famunion y (λz : set ⇒ ordsucc (SNoLev z))))

Hypothesis H4 : PNo_lenbdd (binunion (famunion x (λz : set ⇒ ordsucc (SNoLev z))) (famunion y (λz : set ⇒ ordsucc (SNoLev z)))) (λz : set ⇒ λp : set → prop ⇒ ordinal z ∧ PSNo z p ∈ x)

Theorem. (Conj_SNoCutP_SNoCut__29__1)

PNo_lenbdd (binunion (famunion x (λz : set ⇒ ordsucc (SNoLev z))) (famunion y (λz : set ⇒ ordsucc (SNoLev z)))) (λz : set ⇒ λp : set → prop ⇒ ordinal z ∧ PSNo z p ∈ y) → SNo (SNoCut x y) ∧ SNoLev (SNoCut x y) ∈ ordsucc (binunion (famunion x (λz : set ⇒ ordsucc (SNoLev z))) (famunion y (λz : set ⇒ ordsucc (SNoLev z)))) ∧ (∀z : set, z ∈ x → z < SNoCut x y) ∧ (∀z : set, z ∈ y → SNoCut x y < z) ∧ (∀z : set, SNo z → (∀w : set, w ∈ x → w < z) → (∀w : set, w ∈ y → z < w) → Subq (SNoLev (SNoCut x y)) (SNoLev z) ∧ PNoEq_ (SNoLev (SNoCut x y)) (λw : set ⇒ w ∈ SNoCut x y) (λw : set ⇒ w ∈ z))

In Proofgold the corresponding term root is fc51f0... and proposition id is 719171...

Proof:

The rest of the proof is missing.

End of Section Conj_SNoCutP_SNoCut__29__1

Beginning of Section Conj_SNoCutP_SNoCut__34__2

Variable x : set

Variable y : set

Hypothesis H0 : (∀z : set, z ∈ x → SNo z)

Hypothesis H1 : (∀z : set, z ∈ y → SNo z)

Theorem. (Conj_SNoCutP_SNoCut__34__2)

PNoLt_pwise (λz : set ⇒ λp : set → prop ⇒ ordinal z ∧ PSNo z p ∈ x) (λz : set ⇒ λp : set → prop ⇒ ordinal z ∧ PSNo z p ∈ y) → SNo (SNoCut x y) ∧ SNoLev (SNoCut x y) ∈ ordsucc (binunion (famunion x (λz : set ⇒ ordsucc (SNoLev z))) (famunion y (λz : set ⇒ ordsucc (SNoLev z)))) ∧ (∀z : set, z ∈ x → z < SNoCut x y) ∧ (∀z : set, z ∈ y → SNoCut x y < z) ∧ (∀z : set, SNo z → (∀w : set, w ∈ x → w < z) → (∀w : set, w ∈ y → z < w) → Subq (SNoLev (SNoCut x y)) (SNoLev z) ∧ PNoEq_ (SNoLev (SNoCut x y)) (λw : set ⇒ w ∈ SNoCut x y) (λw : set ⇒ w ∈ z))

In Proofgold the corresponding term root is 98a148... and proposition id is 5978fc...

Proof:

The rest of the proof is missing.

End of Section Conj_SNoCutP_SNoCut__34__2

Beginning of Section Conj_SNoCutP_SNoL_SNoR__5__1

Variable x : set

Hypothesis H0 : SNo x

Theorem. (Conj_SNoCutP_SNoL_SNoR__5__1)

(∀y : set, y ∈ SNoL x → SNo y) → (∀y : set, y ∈ SNoL x → SNo y) ∧ (∀y : set, y ∈ SNoR x → SNo y) ∧ (∀y : set, y ∈ SNoL x → (∀z : set, z ∈ SNoR x → y < z))

In Proofgold the corresponding term root is 41fe53... and proposition id is f0704e...

Proof:

The rest of the proof is missing.

End of Section Conj_SNoCutP_SNoL_SNoR__5__1

Beginning of Section Conj_SNo_eta__5__1

Variable x : set

Hypothesis H0 : SNo x

Theorem. (Conj_SNo_eta__5__1)

SNoCutP (SNoL x) (SNoR x) → x = SNoCut (SNoL x) (SNoR x)

In Proofgold the corresponding term root is 3e42c5... and proposition id is 6cf6d8...

Proof:

The rest of the proof is missing.

End of Section Conj_SNo_eta__5__1

Beginning of Section Conj_SNoCut_Le__3__5

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Hypothesis H0 : (∀v : set, v ∈ y → SNo v)

Hypothesis H1 : SNo (SNoCut x y)

Hypothesis H2 : (∀v : set, v ∈ y → SNoCut x y < v)

Hypothesis H3 : (∀v : set, SNo v → (∀x2 : set, x2 ∈ x → x2 < v) → (∀x2 : set, x2 ∈ y → v < x2) → Subq (SNoLev (SNoCut x y)) (SNoLev v) ∧ SNoEq_ (SNoLev (SNoCut x y)) (SNoCut x y) v)

Hypothesis H4 : SNo u

Hypothesis H6 : u < SNoCut x y

Hypothesis H7 : (∀v : set, v ∈ x → v < u)

Theorem. (Conj_SNoCut_Le__3__5)

¬ (∀v : set, v ∈ y → u < v)

In Proofgold the corresponding term root is a1e40f... and proposition id is 4b294f...

Proof:

The rest of the proof is missing.

End of Section Conj_SNoCut_Le__3__5

Beginning of Section Conj_SNoCut_ext__2__3

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Hypothesis H0 : SNoCutP x y

Hypothesis H1 : SNoCutP z w

Hypothesis H2 : (∀u : set, u ∈ x → u < SNoCut z w)

Hypothesis H4 : (∀u : set, u ∈ z → u < SNoCut x y)

Hypothesis H5 : (∀u : set, u ∈ w → SNoCut x y < u)

Theorem. (Conj_SNoCut_ext__2__3)

SNo (SNoCut x y) → SNoCut x y = SNoCut z w

In Proofgold the corresponding term root is cb3180... and proposition id is 205976...

Proof:

The rest of the proof is missing.

End of Section Conj_SNoCut_ext__2__3

Beginning of Section Conj_SNoCut_ext__2__5

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Hypothesis H0 : SNoCutP x y

Hypothesis H1 : SNoCutP z w

Hypothesis H2 : (∀u : set, u ∈ x → u < SNoCut z w)

Hypothesis H3 : (∀u : set, u ∈ y → SNoCut z w < u)

Hypothesis H4 : (∀u : set, u ∈ z → u < SNoCut x y)

Theorem. (Conj_SNoCut_ext__2__5)

SNo (SNoCut x y) → SNoCut x y = SNoCut z w

In Proofgold the corresponding term root is c5f161... and proposition id is c480b2...

Proof:

The rest of the proof is missing.

End of Section Conj_SNoCut_ext__2__5

Beginning of Section Conj_ordinal_SNoR__1__0

Variable x : set

Hypothesis H1 : SNo x

Theorem. (Conj_ordinal_SNoR__1__0)

SNoLev x = x → SNoR x = Empty

In Proofgold the corresponding term root is a6a7f0... and proposition id is dd834e...

Proof:

The rest of the proof is missing.

End of Section Conj_ordinal_SNoR__1__0

Beginning of Section Conj_ordinal_In_SNoLt__1__0

Variable x : set

Variable y : set

Hypothesis H1 : y ∈ x

Hypothesis H2 : ordinal y

Hypothesis H3 : SNo y

Theorem. (Conj_ordinal_In_SNoLt__1__0)

SNoLev y = y → y < x

In Proofgold the corresponding term root is 3b77e7... and proposition id is 7b81e0...

Proof:

The rest of the proof is missing.

End of Section Conj_ordinal_In_SNoLt__1__0

Beginning of Section Conj_ordinal_SNoLev_max_2__5__0

Variable x : set

Variable y : set

Hypothesis H1 : TransSet x

Hypothesis H2 : SNo y

Hypothesis H3 : SNo x

Hypothesis H4 : SNoLev x = x

Hypothesis H5 : SNoLev y = x

Hypothesis H6 : ¬ y ≤ x

Theorem. (Conj_ordinal_SNoLev_max_2__5__0)

¬ (∀z : set, ordinal z → z ∈ x → z ∈ y)

In Proofgold the corresponding term root is f375f8... and proposition id is 63f7aa...

Proof:

The rest of the proof is missing.

End of Section Conj_ordinal_SNoLev_max_2__5__0

Beginning of Section Conj_SNoL_1__1__0

Variable x : set

Hypothesis H1 : SNoLev x ∈ ordsucc Empty

Theorem. (Conj_SNoL_1__1__0)

Empty = x → x ∈ ordsucc Empty

In Proofgold the corresponding term root is a12e97... and proposition id is a558ae...

Proof:

The rest of the proof is missing.

End of Section Conj_SNoL_1__1__0

Beginning of Section Conj_SNo__eps___3__3

Variable x : set

Variable y : set

Variable z : set

Hypothesis H0 : nat_p x

Hypothesis H1 : y ∈ ordsucc x

Hypothesis H2 : nat_p z

Theorem. (Conj_SNo__eps___3__3)

nat_p y → exactly1of2 (SetAdjoin y (Sing (ordsucc Empty)) ∈ eps_ x) (y ∈ eps_ x)

In Proofgold the corresponding term root is 4bca0b... and proposition id is dcf98d...

Proof:

The rest of the proof is missing.

End of Section Conj_SNo__eps___3__3

Beginning of Section Conj_SNo_pos_eps_Lt__1__3

Variable x : set

Variable y : set

Hypothesis H0 : Empty < y

Hypothesis H1 : ordinal (SNoLev y)

Hypothesis H2 : SNo y

Theorem. (Conj_SNo_pos_eps_Lt__1__3)

y ≠ Empty

In Proofgold the corresponding term root is 2632dc... and proposition id is d43ffe...

Proof:

The rest of the proof is missing.

End of Section Conj_SNo_pos_eps_Lt__1__3

Beginning of Section Conj_SNo_pos_eps_Lt__2__3

Variable x : set

Variable y : set

Variable z : set

Hypothesis H0 : Empty < y

Hypothesis H1 : SNo y

Hypothesis H2 : SNo z

Hypothesis H4 : SNoLev z ∈ eps_ x

Theorem. (Conj_SNo_pos_eps_Lt__2__3)

z ≠ Empty

In Proofgold the corresponding term root is 1d6443... and proposition id is 296c65...

Proof:

The rest of the proof is missing.

End of Section Conj_SNo_pos_eps_Lt__2__3

Beginning of Section Conj_SNo_pos_eps_Le__1__3

Variable x : set

Variable y : set

Hypothesis H0 : Empty < y

Hypothesis H1 : ordinal (SNoLev y)

Hypothesis H2 : SNo y

Theorem. (Conj_SNo_pos_eps_Le__1__3)

y ≠ Empty

In Proofgold the corresponding term root is 2632dc... and proposition id is d43ffe...

Proof:

The rest of the proof is missing.

End of Section Conj_SNo_pos_eps_Le__1__3

Beginning of Section Conj_SNo_pos_eps_Le__2__3

Variable x : set

Variable y : set

Variable z : set

Hypothesis H0 : Empty < y

Hypothesis H1 : SNo y

Hypothesis H2 : SNo z

Hypothesis H4 : SNoLev z ∈ eps_ x

Theorem. (Conj_SNo_pos_eps_Le__2__3)

z ≠ Empty

In Proofgold the corresponding term root is 1d6443... and proposition id is 296c65...

Proof:

The rest of the proof is missing.

End of Section Conj_SNo_pos_eps_Le__2__3

Beginning of Section Conj_eps_SNoCut__5__2

Variable x : set

Variable y : set

Hypothesis H0 : (∀z : set, z ∈ Repl x eps_ → SNo z)

Hypothesis H1 : SNo (SNoCut (Sing Empty) (Repl x eps_))

Hypothesis H3 : (∀z : set, SNo z → (∀w : set, w ∈ Sing Empty → w < z) → (∀w : set, w ∈ Repl x eps_ → z < w) → Subq (SNoLev (SNoCut (Sing Empty) (Repl x eps_))) (SNoLev z) ∧ SNoEq_ (SNoLev (SNoCut (Sing Empty) (Repl x eps_))) (SNoCut (Sing Empty) (Repl x eps_)) z)

Hypothesis H4 : SNo y

Hypothesis H5 : SNoLev y ∈ binintersect (SNoLev (eps_ x)) (SNoLev (SNoCut (Sing Empty) (Repl x eps_)))

Hypothesis H6 : y < SNoCut (Sing Empty) (Repl x eps_)

Hypothesis H7 : (∀z : set, z ∈ Sing Empty → z < y)

Theorem. (Conj_eps_SNoCut__5__2)

¬ (∀z : set, z ∈ Repl x eps_ → y < z)

In Proofgold the corresponding term root is a34286... and proposition id is 0cfb50...

Proof:

The rest of the proof is missing.

End of Section Conj_eps_SNoCut__5__2

Beginning of Section Conj_eps_SNoCut__6__5

Variable x : set

Variable y : set

Hypothesis H0 : x ∈ ω

Hypothesis H1 : (∀z : set, z ∈ Repl x eps_ → SNo z)

Hypothesis H2 : SNo (SNoCut (Sing Empty) (Repl x eps_))

Hypothesis H3 : (∀z : set, z ∈ Repl x eps_ → SNoCut (Sing Empty) (Repl x eps_) < z)

Hypothesis H4 : (∀z : set, SNo z → (∀w : set, w ∈ Sing Empty → w < z) → (∀w : set, w ∈ Repl x eps_ → z < w) → Subq (SNoLev (SNoCut (Sing Empty) (Repl x eps_))) (SNoLev z) ∧ SNoEq_ (SNoLev (SNoCut (Sing Empty) (Repl x eps_))) (SNoCut (Sing Empty) (Repl x eps_)) z)

Hypothesis H6 : SNoLev y ∈ binintersect (SNoLev (eps_ x)) (SNoLev (SNoCut (Sing Empty) (Repl x eps_)))

Hypothesis H7 : eps_ x < y

Hypothesis H8 : y < SNoCut (Sing Empty) (Repl x eps_)

Theorem. (Conj_eps_SNoCut__6__5)

¬ (∀z : set, z ∈ Sing Empty → z < y)

In Proofgold the corresponding term root is 25bf6f... and proposition id is 1b5b9c...

Proof:

The rest of the proof is missing.

End of Section Conj_eps_SNoCut__6__5

Beginning of Section Conj_SNo_etaE__2__1

Variable x : set

Variable y : set

Variable z : set

Hypothesis H0 : y < x

Hypothesis H2 : SNo_ z y

Hypothesis H3 : ordinal z

Hypothesis H4 : SNo y

Theorem. (Conj_SNo_etaE__2__1)

SNoLev y = z → SNo y ∧ SNoLev y ∈ SNoLev x ∧ y < x

In Proofgold the corresponding term root is b6b811... and proposition id is 826135...

Proof:

The rest of the proof is missing.

End of Section Conj_SNo_etaE__2__1

Beginning of Section Conj_SNo_etaE__3__2

Variable x : set

Variable y : set

Variable z : set

Hypothesis H0 : y < x

Hypothesis H1 : z ∈ SNoLev x

Hypothesis H3 : ordinal z

Theorem. (Conj_SNo_etaE__3__2)

SNo y → SNo y ∧ SNoLev y ∈ SNoLev x ∧ y < x

In Proofgold the corresponding term root is 9070ac... and proposition id is 46b34d...

Proof:

The rest of the proof is missing.

End of Section Conj_SNo_etaE__3__2

Beginning of Section Conj_SNo_etaE__5__0

Variable x : set

Variable y : set

Variable z : set

Hypothesis H1 : z ∈ SNoLev x

Hypothesis H2 : SNo y

Hypothesis H3 : SNoLev y = z

Theorem. (Conj_SNo_etaE__5__0)

SNoLev y ∈ SNoLev x → SNo y ∧ SNoLev y ∈ SNoLev x ∧ x < y

In Proofgold the corresponding term root is ce96a0... and proposition id is 65298d...

Proof:

The rest of the proof is missing.

End of Section Conj_SNo_etaE__5__0

Beginning of Section Conj_SNo_etaE__5__1

Variable x : set

Variable y : set

Variable z : set

Hypothesis H0 : x < y

Hypothesis H2 : SNo y

Hypothesis H3 : SNoLev y = z

Theorem. (Conj_SNo_etaE__5__1)

SNoLev y ∈ SNoLev x → SNo y ∧ SNoLev y ∈ SNoLev x ∧ x < y

In Proofgold the corresponding term root is a9d1bd... and proposition id is 79465d...

Proof:

The rest of the proof is missing.

End of Section Conj_SNo_etaE__5__1

Beginning of Section Conj_SNo_etaE__7__0

Variable x : set

Variable y : set

Variable z : set

Hypothesis H1 : z ∈ SNoLev x

Hypothesis H2 : SNo_ z y

Hypothesis H3 : ordinal z

Theorem. (Conj_SNo_etaE__7__0)

SNo y → SNo y ∧ SNoLev y ∈ SNoLev x ∧ x < y

In Proofgold the corresponding term root is abe493... and proposition id is 8c3db9...

Proof:

The rest of the proof is missing.

End of Section Conj_SNo_etaE__7__0

Beginning of Section Conj_SNo_etaE__12__1

Variable x : set

Variable P : prop

Hypothesis H0 : SNo x

Theorem. (Conj_SNo_etaE__12__1)

ordinal (SNoLev x) → P

In Proofgold the corresponding term root is 743d86... and proposition id is ad676b...

Proof:

The rest of the proof is missing.

End of Section Conj_SNo_etaE__12__1

Beginning of Section Conj_SNo_rec2_eq_1__1__2

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

Variable x : set

Variable g : (set → (set → set))

Variable y : set

Variable f : (set → set)

Variable f2 : (set → set)

Hypothesis H0 : (∀z : set, SNo z → (∀w : set, SNo w → (∀h : set → set → set, ∀g2 : set → set → set, (∀u : set, u ∈ SNoS_ (SNoLev z) → (∀v : set, SNo v → h u v = g2 u v)) → (∀u : set, u ∈ SNoS_ (SNoLev w) → h z u = g2 z u) → P z w h = P z w g2)))

Hypothesis H1 : SNo x

Hypothesis H3 : (∀z : set, z ∈ SNoS_ (SNoLev y) → f z = f2 z)

Theorem. (Conj_SNo_rec2_eq_1__1__2)

(∀z : set, z ∈ SNoS_ (SNoLev x) → g z = g z) → P x y (λz : set ⇒ λw : set ⇒ If_i (z = x) (f w) (g z w)) = P x y (λz : set ⇒ λw : set ⇒ If_i (z = x) (f2 w) (g z w))

In Proofgold the corresponding term root is e9c444... and proposition id is 5fe1b1...

Proof:

The rest of the proof is missing.

End of Section Conj_SNo_rec2_eq_1__1__2

Beginning of Section Conj_SNo_rec2_eq__1__1

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

Variable x : set

Variable g : (set → (set → set))

Variable h : (set → (set → set))

Variable y : set

Hypothesis H0 : (∀z : set, SNo z → (∀w : set, SNo w → (∀g2 : set → set → set, ∀h2 : set → set → set, (∀u : set, u ∈ SNoS_ (SNoLev z) → (∀v : set, SNo v → g2 u v = h2 u v)) → (∀u : set, u ∈ SNoS_ (SNoLev w) → g2 z u = h2 z u) → P z w g2 = P z w h2)))

Hypothesis H2 : (∀z : set, z ∈ SNoS_ (SNoLev x) → g z = h z)

Hypothesis H3 : SNo y

Theorem. (Conj_SNo_rec2_eq__1__1)

(∀z : set, ordinal z → (∀w : set, w ∈ SNoS_ z → SNo_rec_i (λu : set ⇒ λf : set → set ⇒ P x u (λv : set ⇒ λx2 : set ⇒ If_i (v = x) (f x2) (g v x2))) w = SNo_rec_i (λu : set ⇒ λf : set → set ⇒ P x u (λv : set ⇒ λx2 : set ⇒ If_i (v = x) (f x2) (h v x2))) w)) → SNo_rec_i (λz : set ⇒ λf : set → set ⇒ P x z (λw : set ⇒ λu : set ⇒ If_i (w = x) (f u) (g w u))) y = SNo_rec_i (λz : set ⇒ λf : set → set ⇒ P x z (λw : set ⇒ λu : set ⇒ If_i (w = x) (f u) (h w u))) y

In Proofgold the corresponding term root is 1a8dec... and proposition id is 859184...

Proof:

The rest of the proof is missing.

End of Section Conj_SNo_rec2_eq__1__1

Beginning of Section Conj_SNo_rec2_eq__4__1

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

Variable x : set

Variable y : set

Hypothesis H0 : (∀z : set, SNo z → (∀w : set, SNo w → (∀g : set → set → set, ∀h : set → set → set, (∀u : set, u ∈ SNoS_ (SNoLev z) → (∀v : set, SNo v → g u v = h u v)) → (∀u : set, u ∈ SNoS_ (SNoLev w) → g z u = h z u) → P z w g = P z w h)))

Hypothesis H2 : SNo y

Hypothesis H3 : (∀z : set, SNo z → (∀g : set → set → set, ∀h : set → set → set, (∀w : set, w ∈ SNoS_ (SNoLev z) → g w = h w) → (λw : set ⇒ If_i (SNo w) (SNo_rec_i (λu : set ⇒ λf : set → set ⇒ P z u (λv : set ⇒ λx2 : set ⇒ If_i (v = z) (f x2) (g v x2))) w) Empty) = (λw : set ⇒ If_i (SNo w) (SNo_rec_i (λu : set ⇒ λf : set → set ⇒ P z u (λv : set ⇒ λx2 : set ⇒ If_i (v = z) (f x2) (h v x2))) w) Empty)))

Hypothesis H4 : (∀z : set, z ∈ SNoS_ (SNoLev x) → (∀w : set, SNo w → If_i (z = x) (SNo_rec_i (λu : set ⇒ λf : set → set ⇒ P x u (λv : set ⇒ λx2 : set ⇒ If_i (v = x) (f x2) (SNo_rec_ii (λy2 : set ⇒ λg : set → set → set ⇒ λz2 : set ⇒ If_i (SNo z2) (SNo_rec_i (λw2 : set ⇒ λf2 : set → set ⇒ P y2 w2 (λu2 : set ⇒ λv2 : set ⇒ If_i (u2 = y2) (f2 v2) (g u2 v2))) z2) Empty) v x2))) w) (SNo_rec_ii (λu : set ⇒ λg : set → set → set ⇒ λv : set ⇒ If_i (SNo v) (SNo_rec_i (λx2 : set ⇒ λf : set → set ⇒ P u x2 (λy2 : set ⇒ λz2 : set ⇒ If_i (y2 = u) (f z2) (g y2 z2))) v) Empty) z w) = SNo_rec_ii (λu : set ⇒ λg : set → set → set ⇒ λv : set ⇒ If_i (SNo v) (SNo_rec_i (λx2 : set ⇒ λf : set → set ⇒ P u x2 (λy2 : set ⇒ λz2 : set ⇒ If_i (y2 = u) (f z2) (g y2 z2))) v) Empty) z w))

Theorem. (Conj_SNo_rec2_eq__4__1)

(∀z : set, z ∈ SNoS_ (SNoLev y) → If_i (x = x) (SNo_rec_i (λw : set ⇒ λf : set → set ⇒ P x w (λu : set ⇒ λv : set ⇒ If_i (u = x) (f v) (SNo_rec_ii (λx2 : set ⇒ λg : set → set → set ⇒ λy2 : set ⇒ If_i (SNo y2) (SNo_rec_i (λz2 : set ⇒ λf2 : set → set ⇒ P x2 z2 (λw2 : set ⇒ λu2 : set ⇒ If_i (w2 = x2) (f2 u2) (g w2 u2))) y2) Empty) u v))) z) (SNo_rec_ii (λw : set ⇒ λg : set → set → set ⇒ λu : set ⇒ If_i (SNo u) (SNo_rec_i (λv : set ⇒ λf : set → set ⇒ P w v (λx2 : set ⇒ λy2 : set ⇒ If_i (x2 = w) (f y2) (g x2 y2))) u) Empty) x z) = SNo_rec_ii (λw : set ⇒ λg : set → set → set ⇒ λu : set ⇒ If_i (SNo u) (SNo_rec_i (λv : set ⇒ λf : set → set ⇒ P w v (λx2 : set ⇒ λy2 : set ⇒ If_i (x2 = w) (f y2) (g x2 y2))) u) Empty) x z) → P x y (λz : set ⇒ λw : set ⇒ If_i (z = x) (SNo_rec_i (λu : set ⇒ λf : set → set ⇒ P x u (λv : set ⇒ λx2 : set ⇒ If_i (v = x) (f x2) (SNo_rec_ii (λy2 : set ⇒ λg : set → set → set ⇒ λz2 : set ⇒ If_i (SNo z2) (SNo_rec_i (λw2 : set ⇒ λf2 : set → set ⇒ P y2 w2 (λu2 : set ⇒ λv2 : set ⇒ If_i (u2 = y2) (f2 v2) (g u2 v2))) z2) Empty) v x2))) w) (SNo_rec_ii (λu : set ⇒ λg : set → set → set ⇒ λv : set ⇒ If_i (SNo v) (SNo_rec_i (λx2 : set ⇒ λf : set → set ⇒ P u x2 (λy2 : set ⇒ λz2 : set ⇒ If_i (y2 = u) (f z2) (g y2 z2))) v) Empty) z w)) = P x y (SNo_rec_ii (λz : set ⇒ λg : set → set → set ⇒ λw : set ⇒ If_i (SNo w) (SNo_rec_i (λu : set ⇒ λf : set → set ⇒ P z u (λv : set ⇒ λx2 : set ⇒ If_i (v = z) (f x2) (g v x2))) w) Empty))

In Proofgold the corresponding term root is 380df4... and proposition id is 211ef4...

Proof:

The rest of the proof is missing.

End of Section Conj_SNo_rec2_eq__4__1

Beginning of Section Conj_SNo_ordinal_ind__2__1

Variable p : (set → prop)

Variable x : set

Hypothesis H0 : (∀y : set, ordinal y → (∀z : set, z ∈ SNoS_ y → p z))

Hypothesis H2 : ordinal (SNoLev x)

Theorem. (Conj_SNo_ordinal_ind__2__1)

ordinal (ordsucc (SNoLev x)) → p x

In Proofgold the corresponding term root is af5b2b... and proposition id is d73c1f...

Proof:

The rest of the proof is missing.

End of Section Conj_SNo_ordinal_ind__2__1

Beginning of Section Conj_SNo_ordinal_ind2__5__1

Variable r : (set → (set → prop))

Variable x : set

Variable y : set

Hypothesis H0 : (∀z : set, ordinal z → (∀w : set, ordinal w → (∀u : set, u ∈ SNoS_ z → (∀v : set, v ∈ SNoS_ w → r u v))))

Hypothesis H2 : SNo y

Hypothesis H3 : ordinal (SNoLev x)

Theorem. (Conj_SNo_ordinal_ind2__5__1)

ordinal (ordsucc (SNoLev x)) → r x y

In Proofgold the corresponding term root is 81b3ce... and proposition id is 918cf1...

Proof:

The rest of the proof is missing.

End of Section Conj_SNo_ordinal_ind2__5__1

Beginning of Section Conj_SNo_ordinal_ind3__6__1

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

Variable x : set

Variable y : set

Variable z : set

Hypothesis H0 : (∀w : set, ordinal w → (∀u : set, ordinal u → (∀v : set, ordinal v → (∀x2 : set, x2 ∈ SNoS_ w → (∀y2 : set, y2 ∈ SNoS_ u → (∀z2 : set, z2 ∈ SNoS_ v → P x2 y2 z2))))))

Hypothesis H2 : SNo z

Hypothesis H3 : ordinal (ordsucc (SNoLev x))

Hypothesis H4 : x ∈ SNoS_ (ordsucc (SNoLev x))

Theorem. (Conj_SNo_ordinal_ind3__6__1)

ordinal (SNoLev y) → P x y z

In Proofgold the corresponding term root is 86c6f8... and proposition id is cb0b1d...

Proof:

The rest of the proof is missing.

End of Section Conj_SNo_ordinal_ind3__6__1

Beginning of Section Conj_restr_SNo__1__2

Variable x : set

Variable y : set

Hypothesis H0 : SNo x

Hypothesis H1 : y ∈ SNoLev x

Theorem. (Conj_restr_SNo__1__2)

SNo_ y (binintersect x (SNoElts_ y)) → SNo (binintersect x (SNoElts_ y))

In Proofgold the corresponding term root is ad79ea... and proposition id is 614555...

Proof:

The rest of the proof is missing.

End of Section Conj_restr_SNo__1__2

Beginning of Section Conj_minus_SNo_prop1__1__2

Variable x : set

Variable y : set

Hypothesis H0 : SNo x

Hypothesis H1 : (∀z : set, z ∈ SNoS_ (SNoLev x) → SNo (- z) ∧ (∀w : set, w ∈ SNoL z → - z < - w) ∧ (∀w : set, w ∈ SNoR z → - w < - z) ∧ SNoCutP (Repl (SNoR z) minus_SNo) (Repl (SNoL z) minus_SNo))

Hypothesis H3 : SNoLev y ∈ SNoLev x

Theorem. (Conj_minus_SNo_prop1__1__2)

y ∈ SNoS_ (SNoLev x) → SNo (- y) ∧ (∀z : set, z ∈ SNoL y → - y < - z) ∧ (∀z : set, z ∈ SNoR y → - z < - y)

In Proofgold the corresponding term root is 02f59e... and proposition id is e0a4af...

Proof:

The rest of the proof is missing.

End of Section Conj_minus_SNo_prop1__1__2

Beginning of Section Conj_minus_SNo_prop1__2__2

Variable x : set

Variable y : set

Hypothesis H0 : SNo x

Hypothesis H1 : (∀z : set, z ∈ SNoS_ (SNoLev x) → SNo (- z) ∧ (∀w : set, w ∈ SNoL z → - z < - w) ∧ (∀w : set, w ∈ SNoR z → - w < - z) ∧ SNoCutP (Repl (SNoR z) minus_SNo) (Repl (SNoL z) minus_SNo))

Hypothesis H3 : SNoLev y ∈ SNoLev x

Theorem. (Conj_minus_SNo_prop1__2__2)

y ∈ SNoS_ (SNoLev x) → SNo (- y) ∧ (∀z : set, z ∈ SNoL y → - y < - z) ∧ (∀z : set, z ∈ SNoR y → - z < - y)

In Proofgold the corresponding term root is 02f59e... and proposition id is e0a4af...

Proof:

The rest of the proof is missing.

End of Section Conj_minus_SNo_prop1__2__2

Beginning of Section Conj_minus_SNo_prop1__4__5

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Hypothesis H0 : SNo x

Hypothesis H1 : (∀u : set, u ∈ SNoS_ (SNoLev x) → SNo (- u) ∧ (∀v : set, v ∈ SNoL u → - u < - v) ∧ (∀v : set, v ∈ SNoR u → - v < - u) ∧ SNoCutP (Repl (SNoR u) minus_SNo) (Repl (SNoL u) minus_SNo))

Hypothesis H2 : SNo y

Hypothesis H3 : SNoLev y ∈ SNoLev x

Hypothesis H4 : SNo z

Hypothesis H6 : (∀u : set, u ∈ SNoR z → - u < - z)

Hypothesis H7 : SNo (- y)

Hypothesis H8 : (∀u : set, u ∈ SNoL y → - y < - u)

Hypothesis H9 : SNo w

Hypothesis H10 : z < w

Hypothesis H11 : w < y

Hypothesis H12 : SNoLev w ∈ SNoLev z

Hypothesis H13 : SNoLev w ∈ SNoLev y

Theorem. (Conj_minus_SNo_prop1__4__5)

w ∈ SNoS_ (SNoLev x) → - y < - z

In Proofgold the corresponding term root is 0b4120... and proposition id is 4cc472...

Proof:

The rest of the proof is missing.

End of Section Conj_minus_SNo_prop1__4__5

Beginning of Section Conj_minus_SNo_prop1__5__7

Variable x : set

Variable y : set

Variable z : set

Hypothesis H0 : SNo x

Hypothesis H1 : (∀w : set, w ∈ SNoS_ (SNoLev x) → SNo (- w) ∧ (∀u : set, u ∈ SNoL w → - w < - u) ∧ (∀u : set, u ∈ SNoR w → - u < - w) ∧ SNoCutP (Repl (SNoR w) minus_SNo) (Repl (SNoL w) minus_SNo))

Hypothesis H2 : SNo y

Hypothesis H3 : SNoLev y ∈ SNoLev x

Hypothesis H4 : x < y

Hypothesis H5 : SNo z

Hypothesis H6 : z < x

Hypothesis H8 : (∀w : set, w ∈ SNoR z → - w < - z)

Hypothesis H9 : SNo (- y)

Hypothesis H10 : (∀w : set, w ∈ SNoL y → - y < - w)

Theorem. (Conj_minus_SNo_prop1__5__7)

z < y → - y < - z

In Proofgold the corresponding term root is 62be8a... and proposition id is ec8fd6...

Proof:

The rest of the proof is missing.

End of Section Conj_minus_SNo_prop1__5__7

Beginning of Section Conj_minus_SNo_prop1__5__9

Variable x : set

Variable y : set

Variable z : set

Hypothesis H0 : SNo x

Hypothesis H1 : (∀w : set, w ∈ SNoS_ (SNoLev x) → SNo (- w) ∧ (∀u : set, u ∈ SNoL w → - w < - u) ∧ (∀u : set, u ∈ SNoR w → - u < - w) ∧ SNoCutP (Repl (SNoR w) minus_SNo) (Repl (SNoL w) minus_SNo))

Hypothesis H2 : SNo y

Hypothesis H3 : SNoLev y ∈ SNoLev x

Hypothesis H4 : x < y

Hypothesis H5 : SNo z

Hypothesis H6 : z < x

Hypothesis H7 : SNo (- z)

Hypothesis H8 : (∀w : set, w ∈ SNoR z → - w < - z)

Hypothesis H10 : (∀w : set, w ∈ SNoL y → - y < - w)

Theorem. (Conj_minus_SNo_prop1__5__9)

z < y → - y < - z

In Proofgold the corresponding term root is c6de85... and proposition id is d0d3de...

Proof:

The rest of the proof is missing.

End of Section Conj_minus_SNo_prop1__5__9

Beginning of Section Conj_minus_SNo_prop1__9__3

Variable x : set

Hypothesis H0 : SNo x

Hypothesis H1 : (∀y : set, y ∈ SNoS_ (SNoLev x) → SNo (- y) ∧ (∀z : set, z ∈ SNoL y → - y < - z) ∧ (∀z : set, z ∈ SNoR y → - z < - y) ∧ SNoCutP (Repl (SNoR y) minus_SNo) (Repl (SNoL y) minus_SNo))

Hypothesis H2 : (∀y : set, y ∈ SNoL x → SNo (- y) ∧ (∀z : set, z ∈ SNoL y → - y < - z) ∧ (∀z : set, z ∈ SNoR y → - z < - y))

Theorem. (Conj_minus_SNo_prop1__9__3)

SNoCutP (Repl (SNoR x) minus_SNo) (Repl (SNoL x) minus_SNo) → SNo (- x) ∧ (∀y : set, y ∈ SNoL x → - x < - y) ∧ (∀y : set, y ∈ SNoR x → - y < - x) ∧ SNoCutP (Repl (SNoR x) minus_SNo) (Repl (SNoL x) minus_SNo)

In Proofgold the corresponding term root is 1db218... and proposition id is cf6dd2...

Proof:

The rest of the proof is missing.

End of Section Conj_minus_SNo_prop1__9__3

Beginning of Section Conj_minus_SNo_prop1__11__0

Variable x : set

Hypothesis H1 : (∀y : set, y ∈ SNoS_ (SNoLev x) → SNo (- y) ∧ (∀z : set, z ∈ SNoL y → - y < - z) ∧ (∀z : set, z ∈ SNoR y → - z < - y) ∧ SNoCutP (Repl (SNoR y) minus_SNo) (Repl (SNoL y) minus_SNo))

Theorem. (Conj_minus_SNo_prop1__11__0)

(∀y : set, y ∈ SNoL x → SNo (- y) ∧ (∀z : set, z ∈ SNoL y → - y < - z) ∧ (∀z : set, z ∈ SNoR y → - z < - y)) → SNo (- x) ∧ (∀y : set, y ∈ SNoL x → - x < - y) ∧ (∀y : set, y ∈ SNoR x → - y < - x) ∧ SNoCutP (Repl (SNoR x) minus_SNo) (Repl (SNoL x) minus_SNo)

In Proofgold the corresponding term root is cf94fc... and proposition id is aad4a2...

Proof:

The rest of the proof is missing.

End of Section Conj_minus_SNo_prop1__11__0

Beginning of Section Conj_minus_SNo_Lev_lem1__1__2

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Hypothesis H0 : y ∈ ordsucc (SNoLev z)

Hypothesis H1 : z = - w

Hypothesis H3 : Subq (SNoLev (- w)) (SNoLev w)

Hypothesis H4 : Subq (SNoLev x) y

Theorem. (Conj_minus_SNo_Lev_lem1__1__2)

¬ SNoLev w ∈ y

In Proofgold the corresponding term root is 9113ae... and proposition id is 658123...

Proof:

The rest of the proof is missing.

End of Section Conj_minus_SNo_Lev_lem1__1__2

Beginning of Section Conj_minus_SNo_Lev_lem1__3__1

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Hypothesis H0 : ordinal (SNoLev x)

Hypothesis H2 : z = - w

Hypothesis H3 : SNoLev w ∈ SNoLev x

Hypothesis H4 : Subq (SNoLev (- w)) (SNoLev w)

Hypothesis H5 : ordinal (SNoLev (- w))

Theorem. (Conj_minus_SNo_Lev_lem1__3__1)

ordinal (ordsucc (SNoLev z)) → y ∈ SNoLev x

In Proofgold the corresponding term root is d42ebf... and proposition id is 3489a1...

Proof:

The rest of the proof is missing.

End of Section Conj_minus_SNo_Lev_lem1__3__1

Beginning of Section Conj_minus_SNo_Lev_lem1__3__3

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Hypothesis H0 : ordinal (SNoLev x)

Hypothesis H1 : y ∈ ordsucc (SNoLev z)

Hypothesis H2 : z = - w

Hypothesis H4 : Subq (SNoLev (- w)) (SNoLev w)

Hypothesis H5 : ordinal (SNoLev (- w))

Theorem. (Conj_minus_SNo_Lev_lem1__3__3)

ordinal (ordsucc (SNoLev z)) → y ∈ SNoLev x

In Proofgold the corresponding term root is 07ccff... and proposition id is f77619...

Proof:

The rest of the proof is missing.

End of Section Conj_minus_SNo_Lev_lem1__3__3

Beginning of Section Conj_minus_SNo_Lev_lem1__3__5

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Hypothesis H0 : ordinal (SNoLev x)

Hypothesis H1 : y ∈ ordsucc (SNoLev z)

Hypothesis H2 : z = - w

Hypothesis H3 : SNoLev w ∈ SNoLev x

Hypothesis H4 : Subq (SNoLev (- w)) (SNoLev w)

Theorem. (Conj_minus_SNo_Lev_lem1__3__5)

ordinal (ordsucc (SNoLev z)) → y ∈ SNoLev x

In Proofgold the corresponding term root is 390b65... and proposition id is 39e564...

Proof:

The rest of the proof is missing.

End of Section Conj_minus_SNo_Lev_lem1__3__5

Beginning of Section Conj_minus_SNo_Lev_lem1__4__5

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Hypothesis H0 : ordinal (SNoLev x)

Hypothesis H1 : y ∈ ordsucc (SNoLev z)

Hypothesis H2 : z = - w

Hypothesis H3 : SNoLev w ∈ SNoLev x

Hypothesis H4 : Subq (SNoLev (- w)) (SNoLev w)

Theorem. (Conj_minus_SNo_Lev_lem1__4__5)

ordinal (SNoLev (- w)) → y ∈ SNoLev x

In Proofgold the corresponding term root is 6a63ca... and proposition id is 348a3b...

Proof:

The rest of the proof is missing.

End of Section Conj_minus_SNo_Lev_lem1__4__5

Beginning of Section Conj_minus_SNo_Lev_lem1__6__0

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Hypothesis H1 : y ∈ ordsucc (SNoLev z)

Hypothesis H2 : z = - w

Hypothesis H3 : SNo w

Hypothesis H4 : SNoLev w ∈ SNoLev x

Hypothesis H5 : Subq (SNoLev (- w)) (SNoLev w)

Theorem. (Conj_minus_SNo_Lev_lem1__6__0)

ordinal (SNoLev w) → y ∈ SNoLev x

In Proofgold the corresponding term root is b7ded1... and proposition id is 066f94...

Proof:

The rest of the proof is missing.

End of Section Conj_minus_SNo_Lev_lem1__6__0

Beginning of Section Conj_minus_SNo_Lev_lem1__6__4

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Hypothesis H0 : ordinal (SNoLev x)

Hypothesis H1 : y ∈ ordsucc (SNoLev z)

Hypothesis H2 : z = - w

Hypothesis H3 : SNo w

Hypothesis H5 : Subq (SNoLev (- w)) (SNoLev w)

Theorem. (Conj_minus_SNo_Lev_lem1__6__4)

ordinal (SNoLev w) → y ∈ SNoLev x

In Proofgold the corresponding term root is 90ad34... and proposition id is 85401b...

Proof:

The rest of the proof is missing.

End of Section Conj_minus_SNo_Lev_lem1__6__4

Beginning of Section Conj_minus_SNo_Lev_lem1__7__1

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Hypothesis H0 : (∀v : set, v ∈ x → (∀x2 : set, x2 ∈ SNoS_ v → Subq (SNoLev (- x2)) (SNoLev x2)))

Hypothesis H2 : z ∈ ordsucc (SNoLev w)

Hypothesis H3 : w = - u

Hypothesis H4 : SNo u

Hypothesis H5 : SNoLev u ∈ SNoLev y

Hypothesis H6 : u ∈ SNoS_ (ordsucc (SNoLev u))

Hypothesis H7 : ordsucc (SNoLev u) ∈ x

Theorem. (Conj_minus_SNo_Lev_lem1__7__1)

Subq (SNoLev (- u)) (SNoLev u) → z ∈ SNoLev y

In Proofgold the corresponding term root is b7a42e... and proposition id is 43b48c...

Proof:

The rest of the proof is missing.

End of Section Conj_minus_SNo_Lev_lem1__7__1

Beginning of Section Conj_minus_SNo_Lev_lem1__10__2

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Hypothesis H0 : y ∈ ordsucc (SNoLev z)

Hypothesis H1 : z = - w

Hypothesis H3 : Subq (SNoLev (- w)) (SNoLev w)

Hypothesis H4 : Subq (SNoLev x) y

Theorem. (Conj_minus_SNo_Lev_lem1__10__2)

¬ SNoLev w ∈ y

In Proofgold the corresponding term root is 9113ae... and proposition id is 658123...

Proof:

The rest of the proof is missing.

End of Section Conj_minus_SNo_Lev_lem1__10__2

Beginning of Section Conj_minus_SNo_Lev_lem1__12__1

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Hypothesis H0 : ordinal (SNoLev x)

Hypothesis H2 : z = - w

Hypothesis H3 : SNoLev w ∈ SNoLev x

Hypothesis H4 : Subq (SNoLev (- w)) (SNoLev w)

Hypothesis H5 : ordinal (SNoLev (- w))

Theorem. (Conj_minus_SNo_Lev_lem1__12__1)

ordinal (ordsucc (SNoLev z)) → y ∈ SNoLev x

In Proofgold the corresponding term root is d42ebf... and proposition id is 3489a1...

Proof:

The rest of the proof is missing.

End of Section Conj_minus_SNo_Lev_lem1__12__1

Beginning of Section Conj_minus_SNo_Lev_lem1__12__3

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Hypothesis H0 : ordinal (SNoLev x)

Hypothesis H1 : y ∈ ordsucc (SNoLev z)

Hypothesis H2 : z = - w

Hypothesis H4 : Subq (SNoLev (- w)) (SNoLev w)

Hypothesis H5 : ordinal (SNoLev (- w))

Theorem. (Conj_minus_SNo_Lev_lem1__12__3)

ordinal (ordsucc (SNoLev z)) → y ∈ SNoLev x

In Proofgold the corresponding term root is 07ccff... and proposition id is f77619...

Proof:

The rest of the proof is missing.

End of Section Conj_minus_SNo_Lev_lem1__12__3

Beginning of Section Conj_minus_SNo_Lev_lem1__12__5

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Hypothesis H0 : ordinal (SNoLev x)

Hypothesis H1 : y ∈ ordsucc (SNoLev z)

Hypothesis H2 : z = - w

Hypothesis H3 : SNoLev w ∈ SNoLev x

Hypothesis H4 : Subq (SNoLev (- w)) (SNoLev w)

Theorem. (Conj_minus_SNo_Lev_lem1__12__5)

ordinal (ordsucc (SNoLev z)) → y ∈ SNoLev x

In Proofgold the corresponding term root is 390b65... and proposition id is 39e564...

Proof:

The rest of the proof is missing.

End of Section Conj_minus_SNo_Lev_lem1__12__5

Beginning of Section Conj_minus_SNo_Lev_lem1__13__5

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Hypothesis H0 : ordinal (SNoLev x)

Hypothesis H1 : y ∈ ordsucc (SNoLev z)

Hypothesis H2 : z = - w

Hypothesis H3 : SNoLev w ∈ SNoLev x

Hypothesis H4 : Subq (SNoLev (- w)) (SNoLev w)

Theorem. (Conj_minus_SNo_Lev_lem1__13__5)

ordinal (SNoLev (- w)) → y ∈ SNoLev x

In Proofgold the corresponding term root is 6a63ca... and proposition id is 348a3b...

Proof:

The rest of the proof is missing.

End of Section Conj_minus_SNo_Lev_lem1__13__5

Beginning of Section Conj_minus_SNo_Lev_lem1__15__0

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Hypothesis H1 : y ∈ ordsucc (SNoLev z)

Hypothesis H2 : z = - w

Hypothesis H3 : SNo w

Hypothesis H4 : SNoLev w ∈ SNoLev x

Hypothesis H5 : Subq (SNoLev (- w)) (SNoLev w)

Theorem. (Conj_minus_SNo_Lev_lem1__15__0)

ordinal (SNoLev w) → y ∈ SNoLev x

In Proofgold the corresponding term root is b7ded1... and proposition id is 066f94...

Proof:

The rest of the proof is missing.

End of Section Conj_minus_SNo_Lev_lem1__15__0

Beginning of Section Conj_minus_SNo_Lev_lem1__15__4

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Hypothesis H0 : ordinal (SNoLev x)

Hypothesis H1 : y ∈ ordsucc (SNoLev z)

Hypothesis H2 : z = - w

Hypothesis H3 : SNo w

Hypothesis H5 : Subq (SNoLev (- w)) (SNoLev w)

Theorem. (Conj_minus_SNo_Lev_lem1__15__4)

ordinal (SNoLev w) → y ∈ SNoLev x

In Proofgold the corresponding term root is 90ad34... and proposition id is 85401b...

Proof:

The rest of the proof is missing.

End of Section Conj_minus_SNo_Lev_lem1__15__4

Beginning of Section Conj_minus_SNo_Lev_lem1__16__1

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Hypothesis H0 : (∀v : set, v ∈ x → (∀x2 : set, x2 ∈ SNoS_ v → Subq (SNoLev (- x2)) (SNoLev x2)))

Hypothesis H2 : z ∈ ordsucc (SNoLev w)

Hypothesis H3 : w = - u

Hypothesis H4 : SNo u

Hypothesis H5 : SNoLev u ∈ SNoLev y

Hypothesis H6 : u ∈ SNoS_ (ordsucc (SNoLev u))

Hypothesis H7 : ordsucc (SNoLev u) ∈ x

Theorem. (Conj_minus_SNo_Lev_lem1__16__1)

Subq (SNoLev (- u)) (SNoLev u) → z ∈ SNoLev y

In Proofgold the corresponding term root is b7a42e... and proposition id is 43b48c...

Proof:

The rest of the proof is missing.

End of Section Conj_minus_SNo_Lev_lem1__16__1

Beginning of Section Conj_minus_SNo_Lev_lem1__22__2

Variable x : set

Variable y : set

Hypothesis H0 : TransSet x

Hypothesis H1 : (∀z : set, z ∈ x → (∀w : set, w ∈ SNoS_ z → Subq (SNoLev (- w)) (SNoLev w)))

Hypothesis H3 : ordinal (SNoLev y)

Hypothesis H4 : SNo y

Theorem. (Conj_minus_SNo_Lev_lem1__22__2)

SNoCutP (Repl (SNoR y) minus_SNo) (Repl (SNoL y) minus_SNo) → Subq (SNoLev (- y)) (SNoLev y)

In Proofgold the corresponding term root is 7239d9... and proposition id is 49f1d3...

Proof:

The rest of the proof is missing.

End of Section Conj_minus_SNo_Lev_lem1__22__2

Beginning of Section Conj_minus_SNo_invol__5__6

Variable x : set

Variable y : set

Hypothesis H0 : SNoCutP x y

Hypothesis H1 : (∀z : set, z ∈ x → - (- z) = z)

Hypothesis H2 : (∀z : set, z ∈ y → - (- z) = z)

Hypothesis H3 : (∀z : set, z ∈ x → SNo z)

Hypothesis H4 : (∀z : set, z ∈ y → SNo z)

Hypothesis H5 : SNo (SNoCut x y)

Hypothesis H7 : SNo (- (- (SNoCut x y)))

Theorem. (Conj_minus_SNo_invol__5__6)

Subq (SNoLev (SNoCut x y)) (SNoLev (- (- (SNoCut x y)))) ∧ SNoEq_ (SNoLev (SNoCut x y)) (SNoCut x y) (- (- (SNoCut x y))) → - (- (SNoCut x y)) = SNoCut x y

In Proofgold the corresponding term root is 6ebb6d... and proposition id is 59be3a...

Proof:

The rest of the proof is missing.

End of Section Conj_minus_SNo_invol__5__6

Beginning of Section Conj_minus_SNo_invol__8__0

Variable x : set

Variable y : set

Hypothesis H1 : (∀z : set, z ∈ x → - (- z) = z)

Hypothesis H2 : (∀z : set, z ∈ y → - (- z) = z)

Hypothesis H3 : (∀z : set, z ∈ x → SNo z)

Hypothesis H4 : (∀z : set, z ∈ y → SNo z)

Theorem. (Conj_minus_SNo_invol__8__0)

SNo (SNoCut x y) → - (- (SNoCut x y)) = SNoCut x y

In Proofgold the corresponding term root is 138f41... and proposition id is 687fa7...

Proof:

The rest of the proof is missing.

End of Section Conj_minus_SNo_invol__8__0

Beginning of Section Conj_minus_SNo_invol__8__2

Variable x : set

Variable y : set

Hypothesis H0 : SNoCutP x y

Hypothesis H1 : (∀z : set, z ∈ x → - (- z) = z)

Hypothesis H3 : (∀z : set, z ∈ x → SNo z)

Hypothesis H4 : (∀z : set, z ∈ y → SNo z)

Theorem. (Conj_minus_SNo_invol__8__2)

SNo (SNoCut x y) → - (- (SNoCut x y)) = SNoCut x y

In Proofgold the corresponding term root is 1195c2... and proposition id is a064b7...

Proof:

The rest of the proof is missing.

End of Section Conj_minus_SNo_invol__8__2

Beginning of Section Conj_minus_SNoCut_eq_lem__5__2

Variable x : set

Variable y : set

Variable z : set

Hypothesis H0 : SNo x

Hypothesis H1 : (∀w : set, w ∈ SNoS_ (SNoLev x) → (∀u : set, ∀v : set, SNoCutP u v → w = SNoCut u v → - w = SNoCut (Repl v minus_SNo) (Repl u minus_SNo)))

Hypothesis H3 : (∀w : set, w ∈ z → SNo w)

Hypothesis H4 : x = SNoCut y z

Hypothesis H5 : SNoCutP (Repl z minus_SNo) (Repl y minus_SNo)

Hypothesis H6 : SNo (SNoCut (Repl z minus_SNo) (Repl y minus_SNo))

Hypothesis H7 : SNoLev (SNoCut (Repl z (λw : set ⇒ - w)) (Repl y (λw : set ⇒ - w))) ∈ SNoLev (- x)

Theorem. (Conj_minus_SNoCut_eq_lem__5__2)

¬ SNoCut (Repl z minus_SNo) (Repl y minus_SNo) ∈ SNoS_ (SNoLev x)

In Proofgold the corresponding term root is 068a0e... and proposition id is b7b604...

Proof:

The rest of the proof is missing.

End of Section Conj_minus_SNoCut_eq_lem__5__2

Beginning of Section Conj_minus_SNoCut_eq_lem__6__2

Variable x : set

Variable y : set

Variable z : set

Hypothesis H0 : SNo x

Hypothesis H1 : (∀w : set, w ∈ SNoS_ (SNoLev x) → (∀u : set, ∀v : set, SNoCutP u v → w = SNoCut u v → - w = SNoCut (Repl v minus_SNo) (Repl u minus_SNo)))

Hypothesis H3 : (∀w : set, w ∈ z → SNo w)

Hypothesis H4 : x = SNoCut y z

Hypothesis H5 : SNoCutP (Repl z minus_SNo) (Repl y minus_SNo)

Hypothesis H6 : SNo (SNoCut (Repl z minus_SNo) (Repl y minus_SNo))

Hypothesis H7 : Subq (SNoLev (SNoCut (Repl z (λw : set ⇒ - w)) (Repl y (λw : set ⇒ - w)))) (SNoLev (- x))

Hypothesis H8 : SNoEq_ (SNoLev (SNoCut (Repl z (λw : set ⇒ - w)) (Repl y (λw : set ⇒ - w)))) (SNoCut (Repl z (λw : set ⇒ - w)) (Repl y (λw : set ⇒ - w))) (- x)

Hypothesis H9 : ordinal (SNoLev (SNoCut (Repl z minus_SNo) (Repl y minus_SNo)))

Theorem. (Conj_minus_SNoCut_eq_lem__6__2)

ordinal (SNoLev (- x)) → - x = SNoCut (Repl z minus_SNo) (Repl y minus_SNo)

In Proofgold the corresponding term root is baab8a... and proposition id is 9b6ecd...

Proof:

The rest of the proof is missing.

End of Section Conj_minus_SNoCut_eq_lem__6__2

Beginning of Section Conj_minus_SNoCut_eq_lem__6__9

Variable x : set

Variable y : set

Variable z : set

Hypothesis H0 : SNo x

Hypothesis H1 : (∀w : set, w ∈ SNoS_ (SNoLev x) → (∀u : set, ∀v : set, SNoCutP u v → w = SNoCut u v → - w = SNoCut (Repl v minus_SNo) (Repl u minus_SNo)))

Hypothesis H2 : (∀w : set, w ∈ y → SNo w)

Hypothesis H3 : (∀w : set, w ∈ z → SNo w)

Hypothesis H4 : x = SNoCut y z

Hypothesis H5 : SNoCutP (Repl z minus_SNo) (Repl y minus_SNo)

Hypothesis H6 : SNo (SNoCut (Repl z minus_SNo) (Repl y minus_SNo))

Hypothesis H7 : Subq (SNoLev (SNoCut (Repl z (λw : set ⇒ - w)) (Repl y (λw : set ⇒ - w)))) (SNoLev (- x))

Hypothesis H8 : SNoEq_ (SNoLev (SNoCut (Repl z (λw : set ⇒ - w)) (Repl y (λw : set ⇒ - w)))) (SNoCut (Repl z (λw : set ⇒ - w)) (Repl y (λw : set ⇒ - w))) (- x)

Theorem. (Conj_minus_SNoCut_eq_lem__6__9)

ordinal (SNoLev (- x)) → - x = SNoCut (Repl z minus_SNo) (Repl y minus_SNo)

In Proofgold the corresponding term root is 9c762b... and proposition id is c30e63...

Proof:

The rest of the proof is missing.

End of Section Conj_minus_SNoCut_eq_lem__6__9

Beginning of Section Conj_minus_SNoCut_eq_lem__7__5

Variable x : set

Variable y : set

Variable z : set

Hypothesis H0 : SNo x

Hypothesis H1 : (∀w : set, w ∈ SNoS_ (SNoLev x) → (∀u : set, ∀v : set, SNoCutP u v → w = SNoCut u v → - w = SNoCut (Repl v minus_SNo) (Repl u minus_SNo)))

Hypothesis H2 : (∀w : set, w ∈ y → SNo w)

Hypothesis H3 : (∀w : set, w ∈ z → SNo w)

Hypothesis H4 : x = SNoCut y z

Hypothesis H6 : SNo (SNoCut (Repl z minus_SNo) (Repl y minus_SNo))

Hypothesis H7 : Subq (SNoLev (SNoCut (Repl z (λw : set ⇒ - w)) (Repl y (λw : set ⇒ - w)))) (SNoLev (- x))

Hypothesis H8 : SNoEq_ (SNoLev (SNoCut (Repl z (λw : set ⇒ - w)) (Repl y (λw : set ⇒ - w)))) (SNoCut (Repl z (λw : set ⇒ - w)) (Repl y (λw : set ⇒ - w))) (- x)

Theorem. (Conj_minus_SNoCut_eq_lem__7__5)

ordinal (SNoLev (SNoCut (Repl z minus_SNo) (Repl y minus_SNo))) → - x = SNoCut (Repl z minus_SNo) (Repl y minus_SNo)

In Proofgold the corresponding term root is 5304c2... and proposition id is 1bc03b...

Proof:

The rest of the proof is missing.

End of Section Conj_minus_SNoCut_eq_lem__7__5

Beginning of Section Conj_minus_SNoCut_eq_lem__8__3

Variable x : set

Variable y : set

Variable z : set

Hypothesis H0 : SNo x

Hypothesis H1 : (∀w : set, w ∈ SNoS_ (SNoLev x) → (∀u : set, ∀v : set, SNoCutP u v → w = SNoCut u v → - w = SNoCut (Repl v minus_SNo) (Repl u minus_SNo)))

Hypothesis H2 : SNoCutP y z

Hypothesis H4 : (∀w : set, w ∈ z → SNo w)

Hypothesis H5 : x = SNoCut y z

Hypothesis H6 : SNoCutP (Repl z minus_SNo) (Repl y minus_SNo)

Hypothesis H7 : SNo (SNoCut (Repl z minus_SNo) (Repl y minus_SNo))

Hypothesis H8 : (∀w : set, SNo w → (∀u : set, u ∈ Repl z minus_SNo → u < w) → (∀u : set, u ∈ Repl y minus_SNo → w < u) → Subq (SNoLev (SNoCut (Repl z minus_SNo) (Repl y minus_SNo))) (SNoLev w) ∧ SNoEq_ (SNoLev (SNoCut (Repl z minus_SNo) (Repl y minus_SNo))) (SNoCut (Repl z minus_SNo) (Repl y minus_SNo)) w)

Hypothesis H9 : (∀w : set, w ∈ Repl z minus_SNo → w < - x)

Theorem. (Conj_minus_SNoCut_eq_lem__8__3)

(∀w : set, w ∈ Repl y minus_SNo → - x < w) → - x = SNoCut (Repl z minus_SNo) (Repl y minus_SNo)

In Proofgold the corresponding term root is 34872f... and proposition id is da648d...

Proof:

The rest of the proof is missing.

End of Section Conj_minus_SNoCut_eq_lem__8__3

Beginning of Section Conj_minus_SNoCut_eq_lem__11__3

Variable x : set

Variable y : set

Variable z : set

Hypothesis H0 : SNo x

Hypothesis H1 : (∀w : set, w ∈ SNoS_ (SNoLev x) → (∀u : set, ∀v : set, SNoCutP u v → w = SNoCut u v → - w = SNoCut (Repl v minus_SNo) (Repl u minus_SNo)))

Hypothesis H2 : SNoCutP y z

Hypothesis H4 : (∀w : set, w ∈ z → SNo w)

Hypothesis H5 : x = SNoCut y z

Theorem. (Conj_minus_SNoCut_eq_lem__11__3)

SNo (SNoCut y z) → - x = SNoCut (Repl z minus_SNo) (Repl y minus_SNo)

In Proofgold the corresponding term root is 30015a... and proposition id is 9d1d72...

Proof:

The rest of the proof is missing.

End of Section Conj_minus_SNoCut_eq_lem__11__3

Beginning of Section Conj_minus_SNoCut_eq_lem__11__5

Variable x : set

Variable y : set

Variable z : set

Hypothesis H0 : SNo x

Hypothesis H1 : (∀w : set, w ∈ SNoS_ (SNoLev x) → (∀u : set, ∀v : set, SNoCutP u v → w = SNoCut u v → - w = SNoCut (Repl v minus_SNo) (Repl u minus_SNo)))

Hypothesis H2 : SNoCutP y z

Hypothesis H3 : (∀w : set, w ∈ y → SNo w)

Hypothesis H4 : (∀w : set, w ∈ z → SNo w)

Theorem. (Conj_minus_SNoCut_eq_lem__11__5)

SNo (SNoCut y z) → - x = SNoCut (Repl z minus_SNo) (Repl y minus_SNo)

In Proofgold the corresponding term root is cab5bc... and proposition id is 2e22cf...

Proof:

The rest of the proof is missing.

End of Section Conj_minus_SNoCut_eq_lem__11__5

Beginning of Section Conj_add_SNo_prop1__1__1

Variable x : set

Variable y : set

Variable z : set

Hypothesis H0 : SNo x

Hypothesis H2 : SNo z

Hypothesis H3 : SNoLev z ∈ SNoLev x

Theorem. (Conj_add_SNo_prop1__1__1)

z ∈ SNoS_ (SNoLev x) → SNo (z + y) ∧ (∀w : set, w ∈ SNoL z → (w + y) < z + y) ∧ (∀w : set, w ∈ SNoR z → (z + y) < w + y) ∧ (∀w : set, w ∈ SNoL y → (z + w) < z + y) ∧ (∀w : set, w ∈ SNoR y → (z + y) < z + w) ∧ SNoCutP (binunion (Repl (SNoL z) (λw : set ⇒ w + y)) (Repl (SNoL y) (add_SNo z))) (binunion (Repl (SNoR z) (λw : set ⇒ w + y)) (Repl (SNoR y) (add_SNo z)))

In Proofgold the corresponding term root is 6e0d02... and proposition id is 7b0caf...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_prop1__1__1

Beginning of Section Conj_add_SNo_prop1__2__1

Variable x : set

Variable y : set

Variable z : set

Hypothesis H0 : SNo x

Hypothesis H2 : SNo z

Hypothesis H3 : SNoLev z ∈ SNoLev x

Theorem. (Conj_add_SNo_prop1__2__1)

z ∈ SNoS_ (SNoLev x) → SNo (z + y) ∧ (∀w : set, w ∈ SNoL z → (w + y) < z + y) ∧ (∀w : set, w ∈ SNoR z → (z + y) < w + y) ∧ (∀w : set, w ∈ SNoL y → (z + w) < z + y) ∧ (∀w : set, w ∈ SNoR y → (z + y) < z + w) ∧ SNoCutP (binunion (Repl (SNoL z) (λw : set ⇒ w + y)) (Repl (SNoL y) (add_SNo z))) (binunion (Repl (SNoR z) (λw : set ⇒ w + y)) (Repl (SNoR y) (add_SNo z)))

In Proofgold the corresponding term root is 6e0d02... and proposition id is 7b0caf...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_prop1__2__1

Beginning of Section Conj_add_SNo_prop1__3__2

Variable x : set

Variable y : set

Variable z : set

Hypothesis H0 : SNo y

Hypothesis H1 : (∀w : set, w ∈ SNoS_ (SNoLev y) → SNo (x + w) ∧ (∀u : set, u ∈ SNoL x → (u + w) < x + w) ∧ (∀u : set, u ∈ SNoR x → (x + w) < u + w) ∧ (∀u : set, u ∈ SNoL w → (x + u) < x + w) ∧ (∀u : set, u ∈ SNoR w → (x + w) < x + u) ∧ SNoCutP (binunion (Repl (SNoL x) (λu : set ⇒ u + w)) (Repl (SNoL w) (add_SNo x))) (binunion (Repl (SNoR x) (λu : set ⇒ u + w)) (Repl (SNoR w) (add_SNo x))))

Hypothesis H3 : SNoLev z ∈ SNoLev y

Theorem. (Conj_add_SNo_prop1__3__2)

z ∈ SNoS_ (SNoLev y) → SNo (x + z) ∧ (∀w : set, w ∈ SNoL x → (w + z) < x + z) ∧ (∀w : set, w ∈ SNoR x → (x + z) < w + z) ∧ (∀w : set, w ∈ SNoL z → (x + w) < x + z) ∧ (∀w : set, w ∈ SNoR z → (x + z) < x + w) ∧ SNoCutP (binunion (Repl (SNoL x) (λw : set ⇒ w + z)) (Repl (SNoL z) (add_SNo x))) (binunion (Repl (SNoR x) (λw : set ⇒ w + z)) (Repl (SNoR z) (add_SNo x)))

In Proofgold the corresponding term root is 9bef0a... and proposition id is 5ece17...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_prop1__3__2

Beginning of Section Conj_add_SNo_prop1__4__2

Variable x : set

Variable y : set

Variable z : set

Hypothesis H0 : SNo y

Hypothesis H1 : (∀w : set, w ∈ SNoS_ (SNoLev y) → SNo (x + w) ∧ (∀u : set, u ∈ SNoL x → (u + w) < x + w) ∧ (∀u : set, u ∈ SNoR x → (x + w) < u + w) ∧ (∀u : set, u ∈ SNoL w → (x + u) < x + w) ∧ (∀u : set, u ∈ SNoR w → (x + w) < x + u) ∧ SNoCutP (binunion (Repl (SNoL x) (λu : set ⇒ u + w)) (Repl (SNoL w) (add_SNo x))) (binunion (Repl (SNoR x) (λu : set ⇒ u + w)) (Repl (SNoR w) (add_SNo x))))

Hypothesis H3 : SNoLev z ∈ SNoLev y

Theorem. (Conj_add_SNo_prop1__4__2)

z ∈ SNoS_ (SNoLev y) → SNo (x + z) ∧ (∀w : set, w ∈ SNoL x → (w + z) < x + z) ∧ (∀w : set, w ∈ SNoR x → (x + z) < w + z) ∧ (∀w : set, w ∈ SNoL z → (x + w) < x + z) ∧ (∀w : set, w ∈ SNoR z → (x + z) < x + w) ∧ SNoCutP (binunion (Repl (SNoL x) (λw : set ⇒ w + z)) (Repl (SNoL z) (add_SNo x))) (binunion (Repl (SNoR x) (λw : set ⇒ w + z)) (Repl (SNoR z) (add_SNo x)))

In Proofgold the corresponding term root is 9bef0a... and proposition id is 5ece17...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_prop1__4__2

Beginning of Section Conj_add_SNo_prop1__5__5

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Hypothesis H0 : (∀v : set, ∀x2 : set, SNo (v + x2) ∧ (∀y2 : set, y2 ∈ SNoL v → (y2 + x2) < v + x2) ∧ (∀y2 : set, y2 ∈ SNoR v → (v + x2) < y2 + x2) ∧ (∀y2 : set, y2 ∈ SNoL x2 → (v + y2) < v + x2) ∧ (∀y2 : set, y2 ∈ SNoR x2 → (v + x2) < v + y2) ∧ SNoCutP (binunion (Repl (SNoL v) (λy2 : set ⇒ y2 + x2)) (Repl (SNoL x2) (add_SNo v))) (binunion (Repl (SNoR v) (λy2 : set ⇒ y2 + x2)) (Repl (SNoR x2) (add_SNo v))) → (∀P : prop, (SNo (v + x2) → (∀y2 : set, y2 ∈ SNoL v → (y2 + x2) < v + x2) → (∀y2 : set, y2 ∈ SNoR v → (v + x2) < y2 + x2) → (∀y2 : set, y2 ∈ SNoL x2 → (v + y2) < v + x2) → (∀y2 : set, y2 ∈ SNoR x2 → (v + x2) < v + y2) → P) → P))

Hypothesis H1 : (∀v : set, v ∈ SNoS_ (SNoLev y) → SNo (x + v) ∧ (∀x2 : set, x2 ∈ SNoL x → (x2 + v) < x + v) ∧ (∀x2 : set, x2 ∈ SNoR x → (x + v) < x2 + v) ∧ (∀x2 : set, x2 ∈ SNoL v → (x + x2) < x + v) ∧ (∀x2 : set, x2 ∈ SNoR v → (x + v) < x + x2) ∧ SNoCutP (binunion (Repl (SNoL x) (λx2 : set ⇒ x2 + v)) (Repl (SNoL v) (add_SNo x))) (binunion (Repl (SNoR x) (λx2 : set ⇒ x2 + v)) (Repl (SNoR v) (add_SNo x))))

Hypothesis H2 : SNo z

Hypothesis H3 : SNo (x + z)

Hypothesis H4 : (∀v : set, v ∈ SNoR z → (x + z) < x + v)

Hypothesis H6 : SNo (x + w)

Hypothesis H7 : (∀v : set, v ∈ SNoL w → (x + v) < x + w)

Hypothesis H8 : SNo u

Hypothesis H9 : z < u

Hypothesis H10 : u < w

Hypothesis H11 : SNoLev u ∈ SNoLev z

Hypothesis H12 : SNoLev u ∈ SNoLev w

Hypothesis H13 : u ∈ SNoS_ (SNoLev y)

Theorem. (Conj_add_SNo_prop1__5__5)

SNo (x + u) → (x + z) < x + w

In Proofgold the corresponding term root is 4866ff... and proposition id is def21a...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_prop1__5__5

Beginning of Section Conj_add_SNo_prop1__5__13

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Hypothesis H0 : (∀v : set, ∀x2 : set, SNo (v + x2) ∧ (∀y2 : set, y2 ∈ SNoL v → (y2 + x2) < v + x2) ∧ (∀y2 : set, y2 ∈ SNoR v → (v + x2) < y2 + x2) ∧ (∀y2 : set, y2 ∈ SNoL x2 → (v + y2) < v + x2) ∧ (∀y2 : set, y2 ∈ SNoR x2 → (v + x2) < v + y2) ∧ SNoCutP (binunion (Repl (SNoL v) (λy2 : set ⇒ y2 + x2)) (Repl (SNoL x2) (add_SNo v))) (binunion (Repl (SNoR v) (λy2 : set ⇒ y2 + x2)) (Repl (SNoR x2) (add_SNo v))) → (∀P : prop, (SNo (v + x2) → (∀y2 : set, y2 ∈ SNoL v → (y2 + x2) < v + x2) → (∀y2 : set, y2 ∈ SNoR v → (v + x2) < y2 + x2) → (∀y2 : set, y2 ∈ SNoL x2 → (v + y2) < v + x2) → (∀y2 : set, y2 ∈ SNoR x2 → (v + x2) < v + y2) → P) → P))

Hypothesis H1 : (∀v : set, v ∈ SNoS_ (SNoLev y) → SNo (x + v) ∧ (∀x2 : set, x2 ∈ SNoL x → (x2 + v) < x + v) ∧ (∀x2 : set, x2 ∈ SNoR x → (x + v) < x2 + v) ∧ (∀x2 : set, x2 ∈ SNoL v → (x + x2) < x + v) ∧ (∀x2 : set, x2 ∈ SNoR v → (x + v) < x + x2) ∧ SNoCutP (binunion (Repl (SNoL x) (λx2 : set ⇒ x2 + v)) (Repl (SNoL v) (add_SNo x))) (binunion (Repl (SNoR x) (λx2 : set ⇒ x2 + v)) (Repl (SNoR v) (add_SNo x))))

Hypothesis H2 : SNo z

Hypothesis H3 : SNo (x + z)

Hypothesis H4 : (∀v : set, v ∈ SNoR z → (x + z) < x + v)

Hypothesis H5 : SNo w

Hypothesis H6 : SNo (x + w)

Hypothesis H7 : (∀v : set, v ∈ SNoL w → (x + v) < x + w)

Hypothesis H8 : SNo u

Hypothesis H9 : z < u

Hypothesis H10 : u < w

Hypothesis H11 : SNoLev u ∈ SNoLev z

Hypothesis H12 : SNoLev u ∈ SNoLev w

Theorem. (Conj_add_SNo_prop1__5__13)

SNo (x + u) → (x + z) < x + w

In Proofgold the corresponding term root is ebf76b... and proposition id is d2c42e...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_prop1__5__13

Beginning of Section Conj_add_SNo_prop1__6__4

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Hypothesis H0 : (∀v : set, ∀x2 : set, SNo (v + x2) ∧ (∀y2 : set, y2 ∈ SNoL v → (y2 + x2) < v + x2) ∧ (∀y2 : set, y2 ∈ SNoR v → (v + x2) < y2 + x2) ∧ (∀y2 : set, y2 ∈ SNoL x2 → (v + y2) < v + x2) ∧ (∀y2 : set, y2 ∈ SNoR x2 → (v + x2) < v + y2) ∧ SNoCutP (binunion (Repl (SNoL v) (λy2 : set ⇒ y2 + x2)) (Repl (SNoL x2) (add_SNo v))) (binunion (Repl (SNoR v) (λy2 : set ⇒ y2 + x2)) (Repl (SNoR x2) (add_SNo v))) → (∀P : prop, (SNo (v + x2) → (∀y2 : set, y2 ∈ SNoL v → (y2 + x2) < v + x2) → (∀y2 : set, y2 ∈ SNoR v → (v + x2) < y2 + x2) → (∀y2 : set, y2 ∈ SNoL x2 → (v + y2) < v + x2) → (∀y2 : set, y2 ∈ SNoR x2 → (v + x2) < v + y2) → P) → P))

Hypothesis H1 : SNo y

Hypothesis H2 : (∀v : set, v ∈ SNoS_ (SNoLev y) → SNo (x + v) ∧ (∀x2 : set, x2 ∈ SNoL x → (x2 + v) < x + v) ∧ (∀x2 : set, x2 ∈ SNoR x → (x + v) < x2 + v) ∧ (∀x2 : set, x2 ∈ SNoL v → (x + x2) < x + v) ∧ (∀x2 : set, x2 ∈ SNoR v → (x + v) < x + x2) ∧ SNoCutP (binunion (Repl (SNoL x) (λx2 : set ⇒ x2 + v)) (Repl (SNoL v) (add_SNo x))) (binunion (Repl (SNoR x) (λx2 : set ⇒ x2 + v)) (Repl (SNoR v) (add_SNo x))))

Hypothesis H3 : SNo z

Hypothesis H5 : (∀v : set, v ∈ SNoR z → (x + z) < x + v)

Hypothesis H6 : SNo w

Hypothesis H7 : SNo (x + w)

Hypothesis H8 : (∀v : set, v ∈ SNoL w → (x + v) < x + w)

Hypothesis H9 : SNo u

Hypothesis H10 : z < u

Hypothesis H11 : u < w

Hypothesis H12 : SNoLev u ∈ SNoLev z

Hypothesis H13 : SNoLev u ∈ SNoLev w

Hypothesis H14 : SNoLev u ∈ SNoLev y

Theorem. (Conj_add_SNo_prop1__6__4)

u ∈ SNoS_ (SNoLev y) → (x + z) < x + w

In Proofgold the corresponding term root is cec830... and proposition id is ebe2dd...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_prop1__6__4

Beginning of Section Conj_add_SNo_prop1__8__1

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Hypothesis H0 : (∀u : set, ∀v : set, SNo (u + v) ∧ (∀x2 : set, x2 ∈ SNoL u → (x2 + v) < u + v) ∧ (∀x2 : set, x2 ∈ SNoR u → (u + v) < x2 + v) ∧ (∀x2 : set, x2 ∈ SNoL v → (u + x2) < u + v) ∧ (∀x2 : set, x2 ∈ SNoR v → (u + v) < u + x2) ∧ SNoCutP (binunion (Repl (SNoL u) (λx2 : set ⇒ x2 + v)) (Repl (SNoL v) (add_SNo u))) (binunion (Repl (SNoR u) (λx2 : set ⇒ x2 + v)) (Repl (SNoR v) (add_SNo u))) → (∀P : prop, (SNo (u + v) → (∀x2 : set, x2 ∈ SNoL u → (x2 + v) < u + v) → (∀x2 : set, x2 ∈ SNoR u → (u + v) < x2 + v) → (∀x2 : set, x2 ∈ SNoL v → (u + x2) < u + v) → (∀x2 : set, x2 ∈ SNoR v → (u + v) < u + x2) → P) → P))

Hypothesis H2 : (∀u : set, u ∈ SNoS_ (SNoLev y) → SNo (x + u) ∧ (∀v : set, v ∈ SNoL x → (v + u) < x + u) ∧ (∀v : set, v ∈ SNoR x → (x + u) < v + u) ∧ (∀v : set, v ∈ SNoL u → (x + v) < x + u) ∧ (∀v : set, v ∈ SNoR u → (x + u) < x + v) ∧ SNoCutP (binunion (Repl (SNoL x) (λv : set ⇒ v + u)) (Repl (SNoL u) (add_SNo x))) (binunion (Repl (SNoR x) (λv : set ⇒ v + u)) (Repl (SNoR u) (add_SNo x))))

Hypothesis H3 : TransSet (SNoLev y)

Hypothesis H4 : SNo z

Hypothesis H5 : z < y

Hypothesis H6 : SNo (x + z)

Hypothesis H7 : (∀u : set, u ∈ SNoR z → (x + z) < x + u)

Hypothesis H8 : SNo w

Hypothesis H9 : SNoLev w ∈ SNoLev y

Hypothesis H10 : y < w

Hypothesis H11 : SNo (x + w)

Hypothesis H12 : (∀u : set, u ∈ SNoL w → (x + u) < x + w)

Theorem. (Conj_add_SNo_prop1__8__1)

z < w → (x + z) < x + w

In Proofgold the corresponding term root is 9c23c1... and proposition id is 89392f...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_prop1__8__1

Beginning of Section Conj_add_SNo_prop1__8__10

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Hypothesis H0 : (∀u : set, ∀v : set, SNo (u + v) ∧ (∀x2 : set, x2 ∈ SNoL u → (x2 + v) < u + v) ∧ (∀x2 : set, x2 ∈ SNoR u → (u + v) < x2 + v) ∧ (∀x2 : set, x2 ∈ SNoL v → (u + x2) < u + v) ∧ (∀x2 : set, x2 ∈ SNoR v → (u + v) < u + x2) ∧ SNoCutP (binunion (Repl (SNoL u) (λx2 : set ⇒ x2 + v)) (Repl (SNoL v) (add_SNo u))) (binunion (Repl (SNoR u) (λx2 : set ⇒ x2 + v)) (Repl (SNoR v) (add_SNo u))) → (∀P : prop, (SNo (u + v) → (∀x2 : set, x2 ∈ SNoL u → (x2 + v) < u + v) → (∀x2 : set, x2 ∈ SNoR u → (u + v) < x2 + v) → (∀x2 : set, x2 ∈ SNoL v → (u + x2) < u + v) → (∀x2 : set, x2 ∈ SNoR v → (u + v) < u + x2) → P) → P))

Hypothesis H1 : SNo y

Hypothesis H2 : (∀u : set, u ∈ SNoS_ (SNoLev y) → SNo (x + u) ∧ (∀v : set, v ∈ SNoL x → (v + u) < x + u) ∧ (∀v : set, v ∈ SNoR x → (x + u) < v + u) ∧ (∀v : set, v ∈ SNoL u → (x + v) < x + u) ∧ (∀v : set, v ∈ SNoR u → (x + u) < x + v) ∧ SNoCutP (binunion (Repl (SNoL x) (λv : set ⇒ v + u)) (Repl (SNoL u) (add_SNo x))) (binunion (Repl (SNoR x) (λv : set ⇒ v + u)) (Repl (SNoR u) (add_SNo x))))

Hypothesis H3 : TransSet (SNoLev y)

Hypothesis H4 : SNo z

Hypothesis H5 : z < y

Hypothesis H6 : SNo (x + z)

Hypothesis H7 : (∀u : set, u ∈ SNoR z → (x + z) < x + u)

Hypothesis H8 : SNo w

Hypothesis H9 : SNoLev w ∈ SNoLev y

Hypothesis H11 : SNo (x + w)

Hypothesis H12 : (∀u : set, u ∈ SNoL w → (x + u) < x + w)

Theorem. (Conj_add_SNo_prop1__8__10)

z < w → (x + z) < x + w

In Proofgold the corresponding term root is 0308e2... and proposition id is 959578...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_prop1__8__10

Beginning of Section Conj_add_SNo_prop1__10__9

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Hypothesis H0 : (∀v : set, ∀x2 : set, SNo (v + x2) ∧ (∀y2 : set, y2 ∈ SNoL v → (y2 + x2) < v + x2) ∧ (∀y2 : set, y2 ∈ SNoR v → (v + x2) < y2 + x2) ∧ (∀y2 : set, y2 ∈ SNoL x2 → (v + y2) < v + x2) ∧ (∀y2 : set, y2 ∈ SNoR x2 → (v + x2) < v + y2) ∧ SNoCutP (binunion (Repl (SNoL v) (λy2 : set ⇒ y2 + x2)) (Repl (SNoL x2) (add_SNo v))) (binunion (Repl (SNoR v) (λy2 : set ⇒ y2 + x2)) (Repl (SNoR x2) (add_SNo v))) → (∀P : prop, (SNo (v + x2) → (∀y2 : set, y2 ∈ SNoL v → (y2 + x2) < v + x2) → (∀y2 : set, y2 ∈ SNoR v → (v + x2) < y2 + x2) → (∀y2 : set, y2 ∈ SNoL x2 → (v + y2) < v + x2) → (∀y2 : set, y2 ∈ SNoR x2 → (v + x2) < v + y2) → P) → P))

Hypothesis H1 : SNo x

Hypothesis H2 : SNo y

Hypothesis H3 : (∀v : set, v ∈ SNoS_ (SNoLev y) → SNo (x + v) ∧ (∀x2 : set, x2 ∈ SNoL x → (x2 + v) < x + v) ∧ (∀x2 : set, x2 ∈ SNoR x → (x + v) < x2 + v) ∧ (∀x2 : set, x2 ∈ SNoL v → (x + x2) < x + v) ∧ (∀x2 : set, x2 ∈ SNoR v → (x + v) < x + x2) ∧ SNoCutP (binunion (Repl (SNoL x) (λx2 : set ⇒ x2 + v)) (Repl (SNoL v) (add_SNo x))) (binunion (Repl (SNoR x) (λx2 : set ⇒ x2 + v)) (Repl (SNoR v) (add_SNo x))))

Hypothesis H4 : (∀v : set, v ∈ SNoS_ (SNoLev x) → (∀x2 : set, x2 ∈ SNoS_ (SNoLev y) → SNo (v + x2) ∧ (∀y2 : set, y2 ∈ SNoL v → (y2 + x2) < v + x2) ∧ (∀y2 : set, y2 ∈ SNoR v → (v + x2) < y2 + x2) ∧ (∀y2 : set, y2 ∈ SNoL x2 → (v + y2) < v + x2) ∧ (∀y2 : set, y2 ∈ SNoR x2 → (v + x2) < v + y2) ∧ SNoCutP (binunion (Repl (SNoL v) (λy2 : set ⇒ y2 + x2)) (Repl (SNoL x2) (add_SNo v))) (binunion (Repl (SNoR v) (λy2 : set ⇒ y2 + x2)) (Repl (SNoR x2) (add_SNo v)))))

Hypothesis H5 : TransSet (SNoLev y)

Hypothesis H6 : (∀v : set, v ∈ SNoR x → SNo (v + y) ∧ (∀x2 : set, x2 ∈ SNoL v → (x2 + y) < v + y) ∧ (∀x2 : set, x2 ∈ SNoR v → (v + y) < x2 + y) ∧ (∀x2 : set, x2 ∈ SNoL y → (v + x2) < v + y) ∧ (∀x2 : set, x2 ∈ SNoR y → (v + y) < v + x2) ∧ SNoCutP (binunion (Repl (SNoL v) (λx2 : set ⇒ x2 + y)) (Repl (SNoL y) (add_SNo v))) (binunion (Repl (SNoR v) (λx2 : set ⇒ x2 + y)) (Repl (SNoR y) (add_SNo v))))

Hypothesis H7 : (∀v : set, v ∈ SNoL y → SNo (x + v) ∧ (∀x2 : set, x2 ∈ SNoL x → (x2 + v) < x + v) ∧ (∀x2 : set, x2 ∈ SNoR x → (x + v) < x2 + v) ∧ (∀x2 : set, x2 ∈ SNoL v → (x + x2) < x + v) ∧ (∀x2 : set, x2 ∈ SNoR v → (x + v) < x + x2) ∧ SNoCutP (binunion (Repl (SNoL x) (λx2 : set ⇒ x2 + v)) (Repl (SNoL v) (add_SNo x))) (binunion (Repl (SNoR x) (λx2 : set ⇒ x2 + v)) (Repl (SNoR v) (add_SNo x))))

Hypothesis H8 : (∀v : set, v ∈ SNoR y → SNo (x + v) ∧ (∀x2 : set, x2 ∈ SNoL x → (x2 + v) < x + v) ∧ (∀x2 : set, x2 ∈ SNoR x → (x + v) < x2 + v) ∧ (∀x2 : set, x2 ∈ SNoL v → (x + x2) < x + v) ∧ (∀x2 : set, x2 ∈ SNoR v → (x + v) < x + x2) ∧ SNoCutP (binunion (Repl (SNoL x) (λx2 : set ⇒ x2 + v)) (Repl (SNoL v) (add_SNo x))) (binunion (Repl (SNoR x) (λx2 : set ⇒ x2 + v)) (Repl (SNoR v) (add_SNo x))))

Hypothesis H10 : u ∈ SNoL y

Hypothesis H11 : z = x + u

Hypothesis H12 : SNo u

Hypothesis H13 : SNoLev u ∈ SNoLev y

Hypothesis H14 : u < y

Theorem. (Conj_add_SNo_prop1__10__9)

u ∈ SNoS_ (SNoLev y) → z < w

In Proofgold the corresponding term root is 3e613f... and proposition id is 821f21...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_prop1__10__9

Beginning of Section Conj_add_SNo_prop1__11__8

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Hypothesis H0 : (∀v : set, ∀x2 : set, SNo (v + x2) ∧ (∀y2 : set, y2 ∈ SNoL v → (y2 + x2) < v + x2) ∧ (∀y2 : set, y2 ∈ SNoR v → (v + x2) < y2 + x2) ∧ (∀y2 : set, y2 ∈ SNoL x2 → (v + y2) < v + x2) ∧ (∀y2 : set, y2 ∈ SNoR x2 → (v + x2) < v + y2) ∧ SNoCutP (binunion (Repl (SNoL v) (λy2 : set ⇒ y2 + x2)) (Repl (SNoL x2) (add_SNo v))) (binunion (Repl (SNoR v) (λy2 : set ⇒ y2 + x2)) (Repl (SNoR x2) (add_SNo v))) → (∀P : prop, (SNo (v + x2) → (∀y2 : set, y2 ∈ SNoL v → (y2 + x2) < v + x2) → (∀y2 : set, y2 ∈ SNoR v → (v + x2) < y2 + x2) → (∀y2 : set, y2 ∈ SNoL x2 → (v + y2) < v + x2) → (∀y2 : set, y2 ∈ SNoR x2 → (v + x2) < v + y2) → P) → P))

Hypothesis H1 : SNo x

Hypothesis H2 : SNo y

Hypothesis H3 : (∀v : set, v ∈ SNoS_ (SNoLev x) → (∀x2 : set, x2 ∈ SNoS_ (SNoLev y) → SNo (v + x2) ∧ (∀y2 : set, y2 ∈ SNoL v → (y2 + x2) < v + x2) ∧ (∀y2 : set, y2 ∈ SNoR v → (v + x2) < y2 + x2) ∧ (∀y2 : set, y2 ∈ SNoL x2 → (v + y2) < v + x2) ∧ (∀y2 : set, y2 ∈ SNoR x2 → (v + x2) < v + y2) ∧ SNoCutP (binunion (Repl (SNoL v) (λy2 : set ⇒ y2 + x2)) (Repl (SNoL x2) (add_SNo v))) (binunion (Repl (SNoR v) (λy2 : set ⇒ y2 + x2)) (Repl (SNoR x2) (add_SNo v)))))

Hypothesis H4 : (∀v : set, v ∈ SNoR y → SNo (x + v) ∧ (∀x2 : set, x2 ∈ SNoL x → (x2 + v) < x + v) ∧ (∀x2 : set, x2 ∈ SNoR x → (x + v) < x2 + v) ∧ (∀x2 : set, x2 ∈ SNoL v → (x + x2) < x + v) ∧ (∀x2 : set, x2 ∈ SNoR v → (x + v) < x + x2) ∧ SNoCutP (binunion (Repl (SNoL x) (λx2 : set ⇒ x2 + v)) (Repl (SNoL v) (add_SNo x))) (binunion (Repl (SNoR x) (λx2 : set ⇒ x2 + v)) (Repl (SNoR v) (add_SNo x))))

Hypothesis H5 : SNo w

Hypothesis H6 : SNoLev w ∈ SNoLev x

Hypothesis H7 : w < x

Hypothesis H9 : SNo (w + y)

Hypothesis H10 : (∀v : set, v ∈ SNoR y → (w + y) < w + v)

Hypothesis H11 : u ∈ SNoR y

Hypothesis H12 : z = x + u

Hypothesis H13 : SNo u

Hypothesis H14 : SNoLev u ∈ SNoLev y

Hypothesis H15 : y < u

Theorem. (Conj_add_SNo_prop1__11__8)

u ∈ SNoS_ (SNoLev y) → (w + y) < z

In Proofgold the corresponding term root is 42e809... and proposition id is a6fba0...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_prop1__11__8

Beginning of Section Conj_add_SNo_prop1__13__13

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Hypothesis H0 : (∀v : set, ∀x2 : set, SNo (v + x2) ∧ (∀y2 : set, y2 ∈ SNoL v → (y2 + x2) < v + x2) ∧ (∀y2 : set, y2 ∈ SNoR v → (v + x2) < y2 + x2) ∧ (∀y2 : set, y2 ∈ SNoL x2 → (v + y2) < v + x2) ∧ (∀y2 : set, y2 ∈ SNoR x2 → (v + x2) < v + y2) ∧ SNoCutP (binunion (Repl (SNoL v) (λy2 : set ⇒ y2 + x2)) (Repl (SNoL x2) (add_SNo v))) (binunion (Repl (SNoR v) (λy2 : set ⇒ y2 + x2)) (Repl (SNoR x2) (add_SNo v))) → (∀P : prop, (SNo (v + x2) → (∀y2 : set, y2 ∈ SNoL v → (y2 + x2) < v + x2) → (∀y2 : set, y2 ∈ SNoR v → (v + x2) < y2 + x2) → (∀y2 : set, y2 ∈ SNoL x2 → (v + y2) < v + x2) → (∀y2 : set, y2 ∈ SNoR x2 → (v + x2) < v + y2) → P) → P))

Hypothesis H1 : SNo x

Hypothesis H2 : (∀v : set, v ∈ SNoS_ (SNoLev x) → SNo (v + y) ∧ (∀x2 : set, x2 ∈ SNoL v → (x2 + y) < v + y) ∧ (∀x2 : set, x2 ∈ SNoR v → (v + y) < x2 + y) ∧ (∀x2 : set, x2 ∈ SNoL y → (v + x2) < v + y) ∧ (∀x2 : set, x2 ∈ SNoR y → (v + y) < v + x2) ∧ SNoCutP (binunion (Repl (SNoL v) (λx2 : set ⇒ x2 + y)) (Repl (SNoL y) (add_SNo v))) (binunion (Repl (SNoR v) (λx2 : set ⇒ x2 + y)) (Repl (SNoR y) (add_SNo v))))

Hypothesis H3 : SNo z

Hypothesis H4 : SNo (z + y)

Hypothesis H5 : (∀v : set, v ∈ SNoR z → (z + y) < v + y)

Hypothesis H6 : SNo w

Hypothesis H7 : SNo (w + y)

Hypothesis H8 : (∀v : set, v ∈ SNoL w → (v + y) < w + y)

Hypothesis H9 : SNo u

Hypothesis H10 : z < u

Hypothesis H11 : u < w

Hypothesis H12 : SNoLev u ∈ SNoLev z

Hypothesis H14 : SNoLev u ∈ SNoLev x

Theorem. (Conj_add_SNo_prop1__13__13)

u ∈ SNoS_ (SNoLev x) → (z + y) < w + y

In Proofgold the corresponding term root is 5c0b9b... and proposition id is 354f83...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_prop1__13__13

Beginning of Section Conj_add_SNo_prop1__14__3

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Hypothesis H0 : (∀v : set, ∀x2 : set, SNo (v + x2) ∧ (∀y2 : set, y2 ∈ SNoL v → (y2 + x2) < v + x2) ∧ (∀y2 : set, y2 ∈ SNoR v → (v + x2) < y2 + x2) ∧ (∀y2 : set, y2 ∈ SNoL x2 → (v + y2) < v + x2) ∧ (∀y2 : set, y2 ∈ SNoR x2 → (v + x2) < v + y2) ∧ SNoCutP (binunion (Repl (SNoL v) (λy2 : set ⇒ y2 + x2)) (Repl (SNoL x2) (add_SNo v))) (binunion (Repl (SNoR v) (λy2 : set ⇒ y2 + x2)) (Repl (SNoR x2) (add_SNo v))) → (∀P : prop, (SNo (v + x2) → (∀y2 : set, y2 ∈ SNoL v → (y2 + x2) < v + x2) → (∀y2 : set, y2 ∈ SNoR v → (v + x2) < y2 + x2) → (∀y2 : set, y2 ∈ SNoL x2 → (v + y2) < v + x2) → (∀y2 : set, y2 ∈ SNoR x2 → (v + x2) < v + y2) → P) → P))

Hypothesis H1 : SNo x

Hypothesis H2 : (∀v : set, v ∈ SNoS_ (SNoLev x) → SNo (v + y) ∧ (∀x2 : set, x2 ∈ SNoL v → (x2 + y) < v + y) ∧ (∀x2 : set, x2 ∈ SNoR v → (v + y) < x2 + y) ∧ (∀x2 : set, x2 ∈ SNoL y → (v + x2) < v + y) ∧ (∀x2 : set, x2 ∈ SNoR y → (v + y) < v + x2) ∧ SNoCutP (binunion (Repl (SNoL v) (λx2 : set ⇒ x2 + y)) (Repl (SNoL y) (add_SNo v))) (binunion (Repl (SNoR v) (λx2 : set ⇒ x2 + y)) (Repl (SNoR y) (add_SNo v))))

Hypothesis H4 : SNo z

Hypothesis H5 : SNoLev z ∈ SNoLev x

Hypothesis H6 : SNo (z + y)

Hypothesis H7 : (∀v : set, v ∈ SNoR z → (z + y) < v + y)

Hypothesis H8 : SNo w

Hypothesis H9 : SNo (w + y)

Hypothesis H10 : (∀v : set, v ∈ SNoL w → (v + y) < w + y)

Hypothesis H11 : SNo u

Hypothesis H12 : z < u

Hypothesis H13 : u < w

Hypothesis H14 : SNoLev u ∈ SNoLev z

Hypothesis H15 : SNoLev u ∈ SNoLev w

Theorem. (Conj_add_SNo_prop1__14__3)

SNoLev u ∈ SNoLev x → (z + y) < w + y

In Proofgold the corresponding term root is 4e3d09... and proposition id is 1239a1...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_prop1__14__3

Beginning of Section Conj_add_SNo_prop1__16__5

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Hypothesis H0 : (∀v : set, ∀x2 : set, SNo (v + x2) ∧ (∀y2 : set, y2 ∈ SNoL v → (y2 + x2) < v + x2) ∧ (∀y2 : set, y2 ∈ SNoR v → (v + x2) < y2 + x2) ∧ (∀y2 : set, y2 ∈ SNoL x2 → (v + y2) < v + x2) ∧ (∀y2 : set, y2 ∈ SNoR x2 → (v + x2) < v + y2) ∧ SNoCutP (binunion (Repl (SNoL v) (λy2 : set ⇒ y2 + x2)) (Repl (SNoL x2) (add_SNo v))) (binunion (Repl (SNoR v) (λy2 : set ⇒ y2 + x2)) (Repl (SNoR x2) (add_SNo v))) → (∀P : prop, (SNo (v + x2) → (∀y2 : set, y2 ∈ SNoL v → (y2 + x2) < v + x2) → (∀y2 : set, y2 ∈ SNoR v → (v + x2) < y2 + x2) → (∀y2 : set, y2 ∈ SNoL x2 → (v + y2) < v + x2) → (∀y2 : set, y2 ∈ SNoR x2 → (v + x2) < v + y2) → P) → P))

Hypothesis H1 : SNo x

Hypothesis H2 : SNo y

Hypothesis H3 : (∀v : set, v ∈ SNoS_ (SNoLev x) → SNo (v + y) ∧ (∀x2 : set, x2 ∈ SNoL v → (x2 + y) < v + y) ∧ (∀x2 : set, x2 ∈ SNoR v → (v + y) < x2 + y) ∧ (∀x2 : set, x2 ∈ SNoL y → (v + x2) < v + y) ∧ (∀x2 : set, x2 ∈ SNoR y → (v + y) < v + x2) ∧ SNoCutP (binunion (Repl (SNoL v) (λx2 : set ⇒ x2 + y)) (Repl (SNoL y) (add_SNo v))) (binunion (Repl (SNoR v) (λx2 : set ⇒ x2 + y)) (Repl (SNoR y) (add_SNo v))))

Hypothesis H4 : (∀v : set, v ∈ SNoS_ (SNoLev x) → (∀x2 : set, x2 ∈ SNoS_ (SNoLev y) → SNo (v + x2) ∧ (∀y2 : set, y2 ∈ SNoL v → (y2 + x2) < v + x2) ∧ (∀y2 : set, y2 ∈ SNoR v → (v + x2) < y2 + x2) ∧ (∀y2 : set, y2 ∈ SNoL x2 → (v + y2) < v + x2) ∧ (∀y2 : set, y2 ∈ SNoR x2 → (v + x2) < v + y2) ∧ SNoCutP (binunion (Repl (SNoL v) (λy2 : set ⇒ y2 + x2)) (Repl (SNoL x2) (add_SNo v))) (binunion (Repl (SNoR v) (λy2 : set ⇒ y2 + x2)) (Repl (SNoR x2) (add_SNo v)))))

Hypothesis H6 : (∀v : set, v ∈ SNoL x → SNo (v + y) ∧ (∀x2 : set, x2 ∈ SNoL v → (x2 + y) < v + y) ∧ (∀x2 : set, x2 ∈ SNoR v → (v + y) < x2 + y) ∧ (∀x2 : set, x2 ∈ SNoL y → (v + x2) < v + y) ∧ (∀x2 : set, x2 ∈ SNoR y → (v + y) < v + x2) ∧ SNoCutP (binunion (Repl (SNoL v) (λx2 : set ⇒ x2 + y)) (Repl (SNoL y) (add_SNo v))) (binunion (Repl (SNoR v) (λx2 : set ⇒ x2 + y)) (Repl (SNoR y) (add_SNo v))))

Hypothesis H7 : (∀v : set, v ∈ SNoR x → SNo (v + y) ∧ (∀x2 : set, x2 ∈ SNoL v → (x2 + y) < v + y) ∧ (∀x2 : set, x2 ∈ SNoR v → (v + y) < x2 + y) ∧ (∀x2 : set, x2 ∈ SNoL y → (v + x2) < v + y) ∧ (∀x2 : set, x2 ∈ SNoR y → (v + y) < v + x2) ∧ SNoCutP (binunion (Repl (SNoL v) (λx2 : set ⇒ x2 + y)) (Repl (SNoL y) (add_SNo v))) (binunion (Repl (SNoR v) (λx2 : set ⇒ x2 + y)) (Repl (SNoR y) (add_SNo v))))

Hypothesis H8 : (∀v : set, v ∈ SNoR y → SNo (x + v) ∧ (∀x2 : set, x2 ∈ SNoL x → (x2 + v) < x + v) ∧ (∀x2 : set, x2 ∈ SNoR x → (x + v) < x2 + v) ∧ (∀x2 : set, x2 ∈ SNoL v → (x + x2) < x + v) ∧ (∀x2 : set, x2 ∈ SNoR v → (x + v) < x + x2) ∧ SNoCutP (binunion (Repl (SNoL x) (λx2 : set ⇒ x2 + v)) (Repl (SNoL v) (add_SNo x))) (binunion (Repl (SNoR x) (λx2 : set ⇒ x2 + v)) (Repl (SNoR v) (add_SNo x))))

Hypothesis H9 : w ∈ binunion (Repl (SNoR x) (λv : set ⇒ v + y)) (Repl (SNoR y) (add_SNo x))

Hypothesis H10 : u ∈ SNoL x

Hypothesis H11 : z = u + y

Hypothesis H12 : SNo u

Hypothesis H13 : SNoLev u ∈ SNoLev x

Hypothesis H14 : u < x

Theorem. (Conj_add_SNo_prop1__16__5)

u ∈ SNoS_ (SNoLev x) → z < w

In Proofgold the corresponding term root is 4a144b... and proposition id is 9f3e3d...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_prop1__16__5

Beginning of Section Conj_add_SNo_prop1__21__2

Variable x : set

Variable y : set

Hypothesis H0 : SNo x

Hypothesis H1 : SNo y

Theorem. (Conj_add_SNo_prop1__21__2)

SNo (SNoCut (binunion (Repl (SNoL x) (λz : set ⇒ z + y)) (Repl (SNoL y) (add_SNo x))) (binunion (Repl (SNoR x) (λz : set ⇒ z + y)) (Repl (SNoR y) (add_SNo x)))) → SNo (x + y) ∧ (∀z : set, z ∈ SNoL x → (z + y) < x + y) ∧ (∀z : set, z ∈ SNoR x → (x + y) < z + y) ∧ (∀z : set, z ∈ SNoL y → (x + z) < x + y) ∧ (∀z : set, z ∈ SNoR y → (x + y) < x + z) ∧ SNoCutP (binunion (Repl (SNoL x) (λz : set ⇒ z + y)) (Repl (SNoL y) (add_SNo x))) (binunion (Repl (SNoR x) (λz : set ⇒ z + y)) (Repl (SNoR y) (add_SNo x)))

In Proofgold the corresponding term root is 4858bc... and proposition id is 5467b7...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_prop1__21__2

Beginning of Section Conj_add_SNo_prop1__28__1

Variable x : set

Variable y : set

Hypothesis H0 : (∀z : set, ∀w : set, SNo (z + w) ∧ (∀u : set, u ∈ SNoL z → (u + w) < z + w) ∧ (∀u : set, u ∈ SNoR z → (z + w) < u + w) ∧ (∀u : set, u ∈ SNoL w → (z + u) < z + w) ∧ (∀u : set, u ∈ SNoR w → (z + w) < z + u) ∧ SNoCutP (binunion (Repl (SNoL z) (λu : set ⇒ u + w)) (Repl (SNoL w) (add_SNo z))) (binunion (Repl (SNoR z) (λu : set ⇒ u + w)) (Repl (SNoR w) (add_SNo z))) → (∀P : prop, (SNo (z + w) → (∀u : set, u ∈ SNoL z → (u + w) < z + w) → (∀u : set, u ∈ SNoR z → (z + w) < u + w) → (∀u : set, u ∈ SNoL w → (z + u) < z + w) → (∀u : set, u ∈ SNoR w → (z + w) < z + u) → P) → P))

Hypothesis H2 : SNo y

Hypothesis H3 : (∀z : set, z ∈ SNoS_ (SNoLev x) → SNo (z + y) ∧ (∀w : set, w ∈ SNoL z → (w + y) < z + y) ∧ (∀w : set, w ∈ SNoR z → (z + y) < w + y) ∧ (∀w : set, w ∈ SNoL y → (z + w) < z + y) ∧ (∀w : set, w ∈ SNoR y → (z + y) < z + w) ∧ SNoCutP (binunion (Repl (SNoL z) (λw : set ⇒ w + y)) (Repl (SNoL y) (add_SNo z))) (binunion (Repl (SNoR z) (λw : set ⇒ w + y)) (Repl (SNoR y) (add_SNo z))))

Hypothesis H4 : (∀z : set, z ∈ SNoS_ (SNoLev y) → SNo (x + z) ∧ (∀w : set, w ∈ SNoL x → (w + z) < x + z) ∧ (∀w : set, w ∈ SNoR x → (x + z) < w + z) ∧ (∀w : set, w ∈ SNoL z → (x + w) < x + z) ∧ (∀w : set, w ∈ SNoR z → (x + z) < x + w) ∧ SNoCutP (binunion (Repl (SNoL x) (λw : set ⇒ w + z)) (Repl (SNoL z) (add_SNo x))) (binunion (Repl (SNoR x) (λw : set ⇒ w + z)) (Repl (SNoR z) (add_SNo x))))

Hypothesis H5 : (∀z : set, z ∈ SNoS_ (SNoLev x) → (∀w : set, w ∈ SNoS_ (SNoLev y) → SNo (z + w) ∧ (∀u : set, u ∈ SNoL z → (u + w) < z + w) ∧ (∀u : set, u ∈ SNoR z → (z + w) < u + w) ∧ (∀u : set, u ∈ SNoL w → (z + u) < z + w) ∧ (∀u : set, u ∈ SNoR w → (z + w) < z + u) ∧ SNoCutP (binunion (Repl (SNoL z) (λu : set ⇒ u + w)) (Repl (SNoL w) (add_SNo z))) (binunion (Repl (SNoR z) (λu : set ⇒ u + w)) (Repl (SNoR w) (add_SNo z)))))

Hypothesis H6 : TransSet (SNoLev x)

Theorem. (Conj_add_SNo_prop1__28__1)

ordinal (SNoLev y) → SNo (x + y) ∧ (∀z : set, z ∈ SNoL x → (z + y) < x + y) ∧ (∀z : set, z ∈ SNoR x → (x + y) < z + y) ∧ (∀z : set, z ∈ SNoL y → (x + z) < x + y) ∧ (∀z : set, z ∈ SNoR y → (x + y) < x + z) ∧ SNoCutP (binunion (Repl (SNoL x) (λz : set ⇒ z + y)) (Repl (SNoL y) (add_SNo x))) (binunion (Repl (SNoR x) (λz : set ⇒ z + y)) (Repl (SNoR y) (add_SNo x)))

In Proofgold the corresponding term root is e7d4a6... and proposition id is 6386e5...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_prop1__28__1

Beginning of Section Conj_add_SNo_com__1__1

Variable x : set

Variable y : set

Variable z : set

Hypothesis H0 : SNo x

Hypothesis H2 : SNo z

Hypothesis H3 : SNoLev z ∈ SNoLev x

Theorem. (Conj_add_SNo_com__1__1)

z ∈ SNoS_ (SNoLev x) → z + y = y + z

In Proofgold the corresponding term root is 93fc44... and proposition id is a0faea...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_com__1__1

Beginning of Section Conj_add_SNo_com__1__3

Variable x : set

Variable y : set

Variable z : set

Hypothesis H0 : SNo x

Hypothesis H1 : (∀w : set, w ∈ SNoS_ (SNoLev x) → w + y = y + w)

Hypothesis H2 : SNo z

Theorem. (Conj_add_SNo_com__1__3)

z ∈ SNoS_ (SNoLev x) → z + y = y + z

In Proofgold the corresponding term root is 26f467... and proposition id is 70a693...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_com__1__3

Beginning of Section Conj_add_SNo_com__2__1

Variable x : set

Variable y : set

Variable z : set

Hypothesis H0 : SNo x

Hypothesis H2 : SNo z

Hypothesis H3 : SNoLev z ∈ SNoLev x

Theorem. (Conj_add_SNo_com__2__1)

z ∈ SNoS_ (SNoLev x) → z + y = y + z

In Proofgold the corresponding term root is 93fc44... and proposition id is a0faea...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_com__2__1

Beginning of Section Conj_add_SNo_com__2__3

Variable x : set

Variable y : set

Variable z : set

Hypothesis H0 : SNo x

Hypothesis H1 : (∀w : set, w ∈ SNoS_ (SNoLev x) → w + y = y + w)

Hypothesis H2 : SNo z

Theorem. (Conj_add_SNo_com__2__3)

z ∈ SNoS_ (SNoLev x) → z + y = y + z

In Proofgold the corresponding term root is 26f467... and proposition id is 70a693...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_com__2__3

Beginning of Section Conj_add_SNo_com__6__2

Variable x : set

Variable y : set

Hypothesis H0 : (∀z : set, z ∈ SNoR x → z + y = y + z)

Hypothesis H1 : (∀z : set, z ∈ SNoR y → x + z = z + x)

Hypothesis H3 : Repl (SNoL y) (add_SNo x) = Repl (SNoL y) (λz : set ⇒ z + x)

Theorem. (Conj_add_SNo_com__6__2)

Repl (SNoR x) (λz : set ⇒ z + y) = Repl (SNoR x) (add_SNo y) → SNoCut (binunion (Repl (SNoL x) (λz : set ⇒ z + y)) (Repl (SNoL y) (add_SNo x))) (binunion (Repl (SNoR x) (λz : set ⇒ z + y)) (Repl (SNoR y) (add_SNo x))) = SNoCut (binunion (Repl (SNoL y) (λz : set ⇒ z + x)) (Repl (SNoL x) (add_SNo y))) (binunion (Repl (SNoR y) (λz : set ⇒ z + x)) (Repl (SNoR x) (add_SNo y)))

In Proofgold the corresponding term root is 8a9177... and proposition id is 7d56eb...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_com__6__2

Beginning of Section Conj_add_SNo_com__9__0

Variable x : set

Variable y : set

Hypothesis H1 : SNo y

Hypothesis H2 : (∀z : set, z ∈ SNoS_ (SNoLev y) → x + z = z + x)

Hypothesis H3 : (∀z : set, z ∈ SNoL x → z + y = y + z)

Hypothesis H4 : (∀z : set, z ∈ SNoR x → z + y = y + z)

Hypothesis H5 : (∀z : set, z ∈ SNoL y → x + z = z + x)

Theorem. (Conj_add_SNo_com__9__0)

(∀z : set, z ∈ SNoR y → x + z = z + x) → x + y = y + x

In Proofgold the corresponding term root is 865e2d... and proposition id is 4c69e2...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_com__9__0

Beginning of Section Conj_add_SNo_com__10__1

Variable x : set

Variable y : set

Hypothesis H0 : SNo x

Hypothesis H2 : (∀z : set, z ∈ SNoS_ (SNoLev y) → x + z = z + x)

Hypothesis H3 : (∀z : set, z ∈ SNoL x → z + y = y + z)

Hypothesis H4 : (∀z : set, z ∈ SNoR x → z + y = y + z)

Theorem. (Conj_add_SNo_com__10__1)

(∀z : set, z ∈ SNoL y → x + z = z + x) → x + y = y + x

In Proofgold the corresponding term root is 13b2b7... and proposition id is 77f7f7...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_com__10__1

Beginning of Section Conj_add_SNo_minus_SNo_linv__4__0

Variable x : set

Variable y : set

Variable z : set

Hypothesis H1 : SNo (- x)

Hypothesis H2 : y = z + x

Hypothesis H3 : SNo z

Hypothesis H4 : - x < z

Hypothesis H5 : SNo (- z)

Hypothesis H6 : - z + z = Empty

Theorem. (Conj_add_SNo_minus_SNo_linv__4__0)

- z < x → Empty < y

In Proofgold the corresponding term root is 645386... and proposition id is f04f61...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_minus_SNo_linv__4__0

Beginning of Section Conj_add_SNo_minus_SNo_linv__8__6

Variable x : set

Variable y : set

Variable z : set

Hypothesis H0 : SNo x

Hypothesis H1 : (∀w : set, w ∈ SNoS_ (SNoLev x) → - w + w = Empty)

Hypothesis H2 : SNo (- x)

Hypothesis H3 : y = - x + z

Hypothesis H4 : SNo z

Hypothesis H5 : SNoLev z ∈ SNoLev x

Hypothesis H7 : SNo (- z)

Theorem. (Conj_add_SNo_minus_SNo_linv__8__6)

- z + z = Empty → y < Empty

In Proofgold the corresponding term root is e3ef4f... and proposition id is cb65a8...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_minus_SNo_linv__8__6

Beginning of Section Conj_add_SNo_minus_SNo_linv__9__5

Variable x : set

Variable y : set

Variable z : set

Hypothesis H0 : SNo x

Hypothesis H1 : (∀w : set, w ∈ SNoS_ (SNoLev x) → - w + w = Empty)

Hypothesis H2 : SNo (- x)

Hypothesis H3 : y = - x + z

Hypothesis H4 : SNo z

Hypothesis H6 : z < x

Theorem. (Conj_add_SNo_minus_SNo_linv__9__5)

SNo (- z) → y < Empty

In Proofgold the corresponding term root is 9f61aa... and proposition id is 6cfb53...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_minus_SNo_linv__9__5

Beginning of Section Conj_add_SNo_ordinal_ordinal__3__3

Variable x : set

Variable y : set

Hypothesis H0 : ordinal x

Hypothesis H1 : ordinal y

Hypothesis H2 : SNo x

Theorem. (Conj_add_SNo_ordinal_ordinal__3__3)

SNo (x + y) → ordinal (x + y)

In Proofgold the corresponding term root is b4fe2a... and proposition id is df8dd9...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_ordinal_ordinal__3__3

Beginning of Section Conj_add_SNo_ordinal_ordinal__4__1

Variable x : set

Variable y : set

Hypothesis H0 : ordinal x

Hypothesis H2 : SNo x

Theorem. (Conj_add_SNo_ordinal_ordinal__4__1)

SNo y → ordinal (x + y)

In Proofgold the corresponding term root is b2ae97... and proposition id is d0ad0e...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_ordinal_ordinal__4__1

Beginning of Section Conj_add_SNo_ordinal_ordinal__4__2

Variable x : set

Variable y : set

Hypothesis H0 : ordinal x

Hypothesis H1 : ordinal y

Theorem. (Conj_add_SNo_ordinal_ordinal__4__2)

SNo y → ordinal (x + y)

In Proofgold the corresponding term root is ad88d2... and proposition id is d2f6bb...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_ordinal_ordinal__4__2

Beginning of Section Conj_add_SNo_ordinal_SL__1__0

Variable x : set

Variable y : set

Variable z : set

Hypothesis H1 : SNo x

Hypothesis H2 : SNo y

Hypothesis H3 : ordinal (x + y)

Hypothesis H4 : SNo (ordsucc x)

Hypothesis H5 : ordinal (ordsucc (x + y))

Hypothesis H6 : SNo (ordsucc (x + y))

Hypothesis H7 : SNoLev z ∈ y

Hypothesis H8 : ordinal (SNoLev z)

Hypothesis H9 : SNo z

Hypothesis H10 : ordsucc x + SNoLev z = ordsucc (x + SNoLev z)

Hypothesis H11 : SNo (ordsucc x + z)

Hypothesis H12 : ordinal (x + SNoLev z)

Hypothesis H13 : ordinal (ordsucc x + SNoLev z)

Theorem. (Conj_add_SNo_ordinal_SL__1__0)

SNo (ordsucc x + SNoLev z) → (ordsucc x + z) < ordsucc (x + y)

In Proofgold the corresponding term root is eebf2b... and proposition id is 959830...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_ordinal_SL__1__0

Beginning of Section Conj_add_SNo_ordinal_SL__1__4

Variable x : set

Variable y : set

Variable z : set

Hypothesis H0 : ordinal y

Hypothesis H1 : SNo x

Hypothesis H2 : SNo y

Hypothesis H3 : ordinal (x + y)

Hypothesis H5 : ordinal (ordsucc (x + y))

Hypothesis H6 : SNo (ordsucc (x + y))

Hypothesis H7 : SNoLev z ∈ y

Hypothesis H8 : ordinal (SNoLev z)

Hypothesis H9 : SNo z

Hypothesis H10 : ordsucc x + SNoLev z = ordsucc (x + SNoLev z)

Hypothesis H11 : SNo (ordsucc x + z)

Hypothesis H12 : ordinal (x + SNoLev z)

Hypothesis H13 : ordinal (ordsucc x + SNoLev z)

Theorem. (Conj_add_SNo_ordinal_SL__1__4)

SNo (ordsucc x + SNoLev z) → (ordsucc x + z) < ordsucc (x + y)

In Proofgold the corresponding term root is eb3930... and proposition id is 8914fd...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_ordinal_SL__1__4

Beginning of Section Conj_add_SNo_ordinal_SL__6__8

Variable x : set

Variable y : set

Variable z : set

Hypothesis H0 : ordinal x

Hypothesis H1 : SNo x

Hypothesis H2 : SNo y

Hypothesis H3 : ordinal (x + y)

Hypothesis H4 : ordinal (ordsucc (x + y))

Hypothesis H5 : SNo (ordsucc (x + y))

Hypothesis H6 : SNoLev z ∈ ordsucc x

Hypothesis H7 : ordinal (SNoLev z)

Hypothesis H9 : ordinal (SNoLev z + y)

Theorem. (Conj_add_SNo_ordinal_SL__6__8)

SNo (SNoLev z + y) → (z + y) < ordsucc (x + y)

In Proofgold the corresponding term root is b45f72... and proposition id is 3db4ce...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_ordinal_SL__6__8

Beginning of Section Conj_add_SNo_ordinal_SL__7__1

Variable x : set

Variable y : set

Variable z : set

Hypothesis H0 : ordinal x

Hypothesis H2 : SNo x

Hypothesis H3 : SNo y

Hypothesis H4 : ordinal (x + y)

Hypothesis H5 : ordinal (ordsucc (x + y))

Hypothesis H6 : SNo (ordsucc (x + y))

Hypothesis H7 : SNoLev z ∈ ordsucc x

Hypothesis H8 : ordinal (SNoLev z)

Hypothesis H9 : SNo z

Theorem. (Conj_add_SNo_ordinal_SL__7__1)

ordinal (SNoLev z + y) → (z + y) < ordsucc (x + y)

In Proofgold the corresponding term root is 3cb115... and proposition id is 2c4c4a...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_ordinal_SL__7__1

Beginning of Section Conj_add_SNo_ordinal_SL__7__3

Variable x : set

Variable y : set

Variable z : set

Hypothesis H0 : ordinal x

Hypothesis H1 : ordinal y

Hypothesis H2 : SNo x

Hypothesis H4 : ordinal (x + y)

Hypothesis H5 : ordinal (ordsucc (x + y))

Hypothesis H6 : SNo (ordsucc (x + y))

Hypothesis H7 : SNoLev z ∈ ordsucc x

Hypothesis H8 : ordinal (SNoLev z)

Hypothesis H9 : SNo z

Theorem. (Conj_add_SNo_ordinal_SL__7__3)

ordinal (SNoLev z + y) → (z + y) < ordsucc (x + y)

In Proofgold the corresponding term root is 40084b... and proposition id is d6040b...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_ordinal_SL__7__3

Beginning of Section Conj_add_SNo_ordinal_SL__11__9

Variable x : set

Variable y : set

Hypothesis H0 : ordinal x

Hypothesis H1 : ordinal y

Hypothesis H2 : (∀z : set, z ∈ y → ordsucc x + z = ordsucc (x + z))

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : ordinal (x + y)

Hypothesis H6 : ordinal (ordsucc x)

Hypothesis H7 : SNo (ordsucc x)

Hypothesis H8 : ordinal (ordsucc x + y)

Hypothesis H10 : ordsucc (x + y) ∈ ordsucc x + y

Theorem. (Conj_add_SNo_ordinal_SL__11__9)

¬ ordinal (ordsucc (x + y))

In Proofgold the corresponding term root is 4e932a... and proposition id is 8c7322...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_ordinal_SL__11__9

Beginning of Section Conj_add_SNo_ordinal_SL__14__0

Variable x : set

Variable y : set

Hypothesis H1 : ordinal y

Hypothesis H2 : (∀z : set, z ∈ y → ordsucc x + z = ordsucc (x + z))

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : ordinal (x + y)

Hypothesis H6 : ordinal (ordsucc x)

Theorem. (Conj_add_SNo_ordinal_SL__14__0)

SNo (ordsucc x) → ordsucc x + y = ordsucc (x + y)

In Proofgold the corresponding term root is 99b3d4... and proposition id is 4d514b...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_ordinal_SL__14__0

Beginning of Section Conj_add_SNo_ordinal_SR__4__0

Variable x : set

Variable y : set

Hypothesis H1 : ordinal y

Theorem. (Conj_add_SNo_ordinal_SR__4__0)

SNo y → x + ordsucc y = ordsucc (x + y)

In Proofgold the corresponding term root is d784d4... and proposition id is b9ae95...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_ordinal_SR__4__0

Beginning of Section Conj_add_SNo_ordinal_SR__5__1

Variable x : set

Variable y : set

Hypothesis H0 : ordinal x

Theorem. (Conj_add_SNo_ordinal_SR__5__1)

SNo x → x + ordsucc y = ordsucc (x + y)

In Proofgold the corresponding term root is a0db9a... and proposition id is 6ffc39...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_ordinal_SR__5__1

Beginning of Section Conj_add_SNo_ordinal_InR__1__1

Variable x : set

Variable y : set

Variable z : set

Hypothesis H0 : ordinal x

Hypothesis H2 : z ∈ y

Hypothesis H3 : SNo x

Hypothesis H4 : SNo y

Hypothesis H5 : ordinal z

Theorem. (Conj_add_SNo_ordinal_InR__1__1)

SNo z → x + z ∈ x + y

In Proofgold the corresponding term root is aa9906... and proposition id is e51a9a...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_ordinal_InR__1__1

Beginning of Section Conj_add_nat_add_SNo__1__1

Variable x : set

Hypothesis H0 : ordinal x

Theorem. (Conj_add_nat_add_SNo__1__1)

(∀y : set, nat_p y → add_nat x y = x + y) → (∀y : set, y ∈ ω → add_nat x y = x + y)

In Proofgold the corresponding term root is d6ce08... and proposition id is b53aa2...

Proof:

The rest of the proof is missing.

End of Section Conj_add_nat_add_SNo__1__1

Beginning of Section Conj_add_SNo_SNoL_interpolate__2__11

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Hypothesis H0 : SNo x

Hypothesis H1 : SNo y

Hypothesis H2 : SNo (x + y)

Hypothesis H3 : SNo z

Hypothesis H4 : (∀u : set, u ∈ SNoS_ (SNoLev z) → SNoLev u ∈ SNoLev (x + y) → u < x + y → (∃v : set, v ∈ SNoL x ∧ u ≤ v + y) ∨ (∃v : set, v ∈ SNoL y ∧ u ≤ x + v))

Hypothesis H5 : SNoLev z ∈ SNoLev (x + y)

Hypothesis H6 : ¬ ((∃u : set, u ∈ SNoL x ∧ z ≤ u + y) ∨ (∃u : set, u ∈ SNoL y ∧ z ≤ x + u))

Hypothesis H7 : w ∈ SNoR z

Hypothesis H8 : SNo w

Hypothesis H9 : SNoLev w ∈ SNoLev z

Hypothesis H10 : z < w

Theorem. (Conj_add_SNo_SNoL_interpolate__2__11)

¬ w ∈ SNoS_ (SNoLev z)

In Proofgold the corresponding term root is 46345c... and proposition id is b1fc76...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_SNoL_interpolate__2__11

Beginning of Section Conj_add_SNo_SNoR_interpolate__1__1

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Hypothesis H0 : SNo x

Hypothesis H2 : ¬ ((∃u : set, u ∈ SNoR x ∧ (u + y) ≤ z) ∨ (∃u : set, u ∈ SNoR y ∧ (x + u) ≤ z))

Hypothesis H3 : w ∈ SNoR y

Hypothesis H4 : SNo w

Theorem. (Conj_add_SNo_SNoR_interpolate__1__1)

SNo (x + w) → z < x + w

In Proofgold the corresponding term root is 5e3928... and proposition id is 19eea3...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_SNoR_interpolate__1__1

Beginning of Section Conj_add_SNo_assoc__3__0

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Hypothesis H1 : SNo y

Hypothesis H2 : SNo z

Hypothesis H3 : (∀v : set, v ∈ SNoS_ (SNoLev x) → v + y + z = (v + y) + z)

Hypothesis H4 : SNo (y + z)

Hypothesis H5 : SNo w

Hypothesis H6 : u ∈ SNoR x

Hypothesis H7 : (u + y) ≤ w

Hypothesis H8 : SNo u

Hypothesis H9 : x < u

Theorem. (Conj_add_SNo_assoc__3__0)

u + y + z = (u + y) + z → (x + y + z) < w + z

In Proofgold the corresponding term root is d647d4... and proposition id is 52df83...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_assoc__3__0

Beginning of Section Conj_add_SNo_assoc__6__7

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Hypothesis H0 : SNo x

Hypothesis H1 : SNo y

Hypothesis H2 : SNo z

Hypothesis H3 : (∀v : set, v ∈ SNoS_ (SNoLev x) → v + y + z = (v + y) + z)

Hypothesis H4 : SNo (y + z)

Hypothesis H5 : SNo w

Hypothesis H6 : u ∈ SNoL x

Hypothesis H8 : SNo u

Hypothesis H9 : u < x

Theorem. (Conj_add_SNo_assoc__6__7)

u + y + z = (u + y) + z → (w + z) < x + y + z

In Proofgold the corresponding term root is e820fd... and proposition id is 214a95...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_assoc__6__7

Beginning of Section Conj_add_SNo_assoc__7__3

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Hypothesis H0 : SNo x

Hypothesis H1 : SNo y

Hypothesis H2 : SNo z

Hypothesis H4 : SNo (x + y)

Hypothesis H5 : SNo w

Hypothesis H6 : u ∈ SNoR z

Hypothesis H7 : (y + u) ≤ w

Hypothesis H8 : SNo u

Hypothesis H9 : z < u

Theorem. (Conj_add_SNo_assoc__7__3)

x + y + u = (x + y) + u → ((x + y) + z) < x + w

In Proofgold the corresponding term root is 86edac... and proposition id is e5d8e6...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_assoc__7__3

Beginning of Section Conj_add_SNo_assoc__10__0

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Hypothesis H1 : SNo y

Hypothesis H2 : SNo z

Hypothesis H3 : (∀v : set, v ∈ SNoS_ (SNoLev z) → x + y + v = (x + y) + v)

Hypothesis H4 : SNo (x + y)

Hypothesis H5 : SNo w

Hypothesis H6 : u ∈ SNoL z

Hypothesis H7 : w ≤ y + u

Hypothesis H8 : SNo u

Hypothesis H9 : u < z

Theorem. (Conj_add_SNo_assoc__10__0)

x + y + u = (x + y) + u → (x + w) < (x + y) + z

In Proofgold the corresponding term root is 2b0565... and proposition id is 019879...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_assoc__10__0

Beginning of Section Conj_add_SNo_assoc__14__4

Variable x : set

Variable y : set

Variable z : set

Hypothesis H0 : SNo x

Hypothesis H1 : SNo y

Hypothesis H2 : SNo z

Hypothesis H3 : (∀w : set, w ∈ SNoS_ (SNoLev x) → w + y + z = (w + y) + z)

Hypothesis H5 : (∀w : set, w ∈ SNoS_ (SNoLev z) → x + y + w = (x + y) + w)

Hypothesis H6 : SNo (x + y)

Hypothesis H7 : SNo (y + z)

Theorem. (Conj_add_SNo_assoc__14__4)

SNoCutP (binunion (Repl (SNoL x) (λw : set ⇒ w + y + z)) (Repl (SNoL (y + z)) (add_SNo x))) (binunion (Repl (SNoR x) (λw : set ⇒ w + y + z)) (Repl (SNoR (y + z)) (add_SNo x))) → SNoCut (binunion (Repl (SNoL x) (λw : set ⇒ w + y + z)) (Repl (SNoL (y + z)) (add_SNo x))) (binunion (Repl (SNoR x) (λw : set ⇒ w + y + z)) (Repl (SNoR (y + z)) (add_SNo x))) = SNoCut (binunion (Repl (SNoL (x + y)) (λw : set ⇒ w + z)) (Repl (SNoL z) (add_SNo (x + y)))) (binunion (Repl (SNoR (x + y)) (λw : set ⇒ w + z)) (Repl (SNoR z) (add_SNo (x + y))))

In Proofgold the corresponding term root is 11b8db... and proposition id is 5aa7b6...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_assoc__14__4

Beginning of Section Conj_add_SNo_cancel_L__2__3

Variable x : set

Variable y : set

Variable z : set

Hypothesis H0 : SNo x

Hypothesis H1 : SNo y

Hypothesis H2 : SNo z

Hypothesis H4 : SNo (- x)

Theorem. (Conj_add_SNo_cancel_L__2__3)

- x + x + y = y → y = z

In Proofgold the corresponding term root is c17b67... and proposition id is c2b6b1...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_cancel_L__2__3

Beginning of Section Conj_minus_add_SNo_distr__1__0

Variable x : set

Variable y : set

Hypothesis H1 : SNo y

Hypothesis H2 : SNo (- x)

Hypothesis H3 : SNo (- y)

Hypothesis H4 : SNo (x + y)

Theorem. (Conj_minus_add_SNo_distr__1__0)

(x + y) + - (x + y) = (x + y) + - x + - y → - (x + y) = - x + - y

In Proofgold the corresponding term root is 77189e... and proposition id is 66ed72...

Proof:

The rest of the proof is missing.

End of Section Conj_minus_add_SNo_distr__1__0

Beginning of Section Conj_minus_add_SNo_distr__3__2

Variable x : set

Variable y : set

Hypothesis H0 : SNo x

Hypothesis H1 : SNo y

Theorem. (Conj_minus_add_SNo_distr__3__2)

SNo (- y) → - (x + y) = - x + - y

In Proofgold the corresponding term root is e06335... and proposition id is 75d78f...

Proof:

The rest of the proof is missing.

End of Section Conj_minus_add_SNo_distr__3__2

Beginning of Section Conj_add_SNo_Lev_bd__3__0

Variable x : set

Variable y : set

Variable z : set

Variable p : (set → prop)

Variable w : set

Hypothesis H1 : w ∈ SNoR x

Hypothesis H2 : z = w + y

Theorem. (Conj_add_SNo_Lev_bd__3__0)

w ∈ SNoS_ (SNoLev x) → SNo w → SNoLev w ∈ SNoLev x → x < w → p (w + y)

In Proofgold the corresponding term root is 41ac1a... and proposition id is 10aafd...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_Lev_bd__3__0

Beginning of Section Conj_add_SNo_Lev_bd__6__2

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Hypothesis H0 : SNo x

Hypothesis H1 : ordinal (SNoLev x + SNoLev y)

Hypothesis H3 : z ∈ ordsucc (SNoLev (x + w))

Hypothesis H4 : ordinal z

Hypothesis H5 : Subq (SNoLev x + SNoLev y) z

Hypothesis H6 : Subq (SNoLev (x + w)) (SNoLev x + SNoLev w)

Hypothesis H7 : SNoLev x + SNoLev w ∈ SNoLev x + SNoLev y

Theorem. (Conj_add_SNo_Lev_bd__6__2)

¬ Subq (SNoLev x + SNoLev w) (SNoLev x + SNoLev y)

In Proofgold the corresponding term root is aafc31... and proposition id is 04cec9...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_Lev_bd__6__2

Beginning of Section Conj_add_SNo_Lev_bd__7__7

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Hypothesis H0 : SNo x

Hypothesis H1 : SNo y

Hypothesis H2 : ordinal (SNoLev x + SNoLev y)

Hypothesis H3 : SNo w

Hypothesis H4 : SNoLev w ∈ SNoLev y

Hypothesis H5 : z ∈ ordsucc (SNoLev (x + w))

Hypothesis H6 : ordinal z

Hypothesis H8 : Subq (SNoLev (x + w)) (SNoLev x + SNoLev w)

Theorem. (Conj_add_SNo_Lev_bd__7__7)

¬ SNoLev x + SNoLev w ∈ SNoLev x + SNoLev y

In Proofgold the corresponding term root is 4ef372... and proposition id is ed6e9f...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_Lev_bd__7__7

Beginning of Section Conj_add_SNo_Lev_bd__10__5

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Hypothesis H0 : SNo y

Hypothesis H1 : SNo w

Hypothesis H2 : z ∈ ordsucc (SNoLev (w + y))

Hypothesis H3 : ordinal z

Hypothesis H4 : Subq (SNoLev x + SNoLev y) z

Hypothesis H6 : SNoLev w + SNoLev y ∈ SNoLev x + SNoLev y

Theorem. (Conj_add_SNo_Lev_bd__10__5)

¬ Subq z (SNoLev (w + y))

In Proofgold the corresponding term root is a552af... and proposition id is bae0de...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_Lev_bd__10__5

Beginning of Section Conj_add_SNo_Lev_bd__11__2

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Hypothesis H0 : SNo y

Hypothesis H1 : ordinal (SNoLev x + SNoLev y)

Hypothesis H3 : z ∈ ordsucc (SNoLev (w + y))

Hypothesis H4 : ordinal z

Hypothesis H5 : Subq (SNoLev x + SNoLev y) z

Hypothesis H6 : Subq (SNoLev (w + y)) (SNoLev w + SNoLev y)

Hypothesis H7 : SNoLev w + SNoLev y ∈ SNoLev x + SNoLev y

Theorem. (Conj_add_SNo_Lev_bd__11__2)

¬ Subq (SNoLev w + SNoLev y) (SNoLev x + SNoLev y)

In Proofgold the corresponding term root is 2c6c95... and proposition id is 82480a...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_Lev_bd__11__2

Beginning of Section Conj_add_SNo_Lev_bd__12__6

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Hypothesis H0 : SNo x

Hypothesis H1 : SNo y

Hypothesis H2 : ordinal (SNoLev x + SNoLev y)

Hypothesis H3 : SNo w

Hypothesis H4 : SNoLev w ∈ SNoLev x

Hypothesis H5 : z ∈ ordsucc (SNoLev (w + y))

Hypothesis H7 : Subq (SNoLev x + SNoLev y) z

Hypothesis H8 : Subq (SNoLev (w + y)) (SNoLev w + SNoLev y)

Theorem. (Conj_add_SNo_Lev_bd__12__6)

¬ SNoLev w + SNoLev y ∈ SNoLev x + SNoLev y

In Proofgold the corresponding term root is 619007... and proposition id is 345e59...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_Lev_bd__12__6

Beginning of Section Conj_add_SNo_Lev_bd__13__3

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Hypothesis H0 : SNo x

Hypothesis H1 : SNo y

Hypothesis H2 : ordinal (SNoLev x + SNoLev y)

Hypothesis H4 : w ∈ SNoS_ (SNoLev x)

Hypothesis H5 : SNo w

Hypothesis H6 : SNoLev w ∈ SNoLev x

Hypothesis H7 : z ∈ ordsucc (SNoLev (w + y))

Hypothesis H8 : ordinal z

Hypothesis H9 : Subq (SNoLev x + SNoLev y) z

Theorem. (Conj_add_SNo_Lev_bd__13__3)

¬ Subq (SNoLev (w + y)) (SNoLev w + SNoLev y)

In Proofgold the corresponding term root is 667ef2... and proposition id is b84773...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_Lev_bd__13__3

Beginning of Section Conj_add_SNo_Lev_bd__13__5

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Hypothesis H0 : SNo x

Hypothesis H1 : SNo y

Hypothesis H2 : ordinal (SNoLev x + SNoLev y)

Hypothesis H3 : (∀u : set, u ∈ SNoS_ (SNoLev x) → Subq (SNoLev (u + y)) (SNoLev u + SNoLev y))

Hypothesis H4 : w ∈ SNoS_ (SNoLev x)

Hypothesis H6 : SNoLev w ∈ SNoLev x

Hypothesis H7 : z ∈ ordsucc (SNoLev (w + y))

Hypothesis H8 : ordinal z

Hypothesis H9 : Subq (SNoLev x + SNoLev y) z

Theorem. (Conj_add_SNo_Lev_bd__13__5)

¬ Subq (SNoLev (w + y)) (SNoLev w + SNoLev y)

In Proofgold the corresponding term root is 942f3a... and proposition id is 86a991...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_Lev_bd__13__5

Beginning of Section Conj_add_SNo_Lev_bd__13__6

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Hypothesis H0 : SNo x

Hypothesis H1 : SNo y

Hypothesis H2 : ordinal (SNoLev x + SNoLev y)

Hypothesis H3 : (∀u : set, u ∈ SNoS_ (SNoLev x) → Subq (SNoLev (u + y)) (SNoLev u + SNoLev y))

Hypothesis H4 : w ∈ SNoS_ (SNoLev x)

Hypothesis H5 : SNo w

Hypothesis H7 : z ∈ ordsucc (SNoLev (w + y))

Hypothesis H8 : ordinal z

Hypothesis H9 : Subq (SNoLev x + SNoLev y) z

Theorem. (Conj_add_SNo_Lev_bd__13__6)

¬ Subq (SNoLev (w + y)) (SNoLev w + SNoLev y)

In Proofgold the corresponding term root is 0ecea1... and proposition id is 57bf76...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_Lev_bd__13__6

Beginning of Section Conj_add_SNo_Lev_bd__13__7

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Hypothesis H0 : SNo x

Hypothesis H1 : SNo y

Hypothesis H2 : ordinal (SNoLev x + SNoLev y)

Hypothesis H3 : (∀u : set, u ∈ SNoS_ (SNoLev x) → Subq (SNoLev (u + y)) (SNoLev u + SNoLev y))

Hypothesis H4 : w ∈ SNoS_ (SNoLev x)

Hypothesis H5 : SNo w

Hypothesis H6 : SNoLev w ∈ SNoLev x

Hypothesis H8 : ordinal z

Hypothesis H9 : Subq (SNoLev x + SNoLev y) z

Theorem. (Conj_add_SNo_Lev_bd__13__7)

¬ Subq (SNoLev (w + y)) (SNoLev w + SNoLev y)

In Proofgold the corresponding term root is 965c98... and proposition id is 8a6ac5...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_Lev_bd__13__7

Beginning of Section Conj_add_SNo_Lev_bd__14__5

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Hypothesis H0 : SNo x

Hypothesis H1 : SNo y

Hypothesis H2 : ordinal (SNoLev x + SNoLev y)

Hypothesis H3 : (∀u : set, u ∈ SNoS_ (SNoLev x) → Subq (SNoLev (u + y)) (SNoLev u + SNoLev y))

Hypothesis H4 : w ∈ SNoS_ (SNoLev x)

Hypothesis H6 : SNoLev w ∈ SNoLev x

Hypothesis H7 : z ∈ ordsucc (SNoLev (w + y))

Theorem. (Conj_add_SNo_Lev_bd__14__5)

ordinal z → z ∈ SNoLev x + SNoLev y

In Proofgold the corresponding term root is 3a22f8... and proposition id is 931664...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_Lev_bd__14__5

Beginning of Section Conj_add_SNo_Lev_bd__16__2

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Hypothesis H0 : SNo x

Hypothesis H1 : ordinal (SNoLev x + SNoLev y)

Hypothesis H3 : z ∈ ordsucc (SNoLev (x + w))

Hypothesis H4 : ordinal z

Hypothesis H5 : Subq (SNoLev x + SNoLev y) z

Hypothesis H6 : Subq (SNoLev (x + w)) (SNoLev x + SNoLev w)

Hypothesis H7 : SNoLev x + SNoLev w ∈ SNoLev x + SNoLev y

Theorem. (Conj_add_SNo_Lev_bd__16__2)

¬ Subq (SNoLev x + SNoLev w) (SNoLev x + SNoLev y)

In Proofgold the corresponding term root is aafc31... and proposition id is 04cec9...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_Lev_bd__16__2

Beginning of Section Conj_add_SNo_Lev_bd__17__7

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Hypothesis H0 : SNo x

Hypothesis H1 : SNo y

Hypothesis H2 : ordinal (SNoLev x + SNoLev y)

Hypothesis H3 : SNo w

Hypothesis H4 : SNoLev w ∈ SNoLev y

Hypothesis H5 : z ∈ ordsucc (SNoLev (x + w))

Hypothesis H6 : ordinal z

Hypothesis H8 : Subq (SNoLev (x + w)) (SNoLev x + SNoLev w)

Theorem. (Conj_add_SNo_Lev_bd__17__7)

¬ SNoLev x + SNoLev w ∈ SNoLev x + SNoLev y

In Proofgold the corresponding term root is 4ef372... and proposition id is ed6e9f...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_Lev_bd__17__7

Beginning of Section Conj_add_SNo_Lev_bd__20__5

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Hypothesis H0 : SNo y

Hypothesis H1 : SNo w

Hypothesis H2 : z ∈ ordsucc (SNoLev (w + y))

Hypothesis H3 : ordinal z

Hypothesis H4 : Subq (SNoLev x + SNoLev y) z

Hypothesis H6 : SNoLev w + SNoLev y ∈ SNoLev x + SNoLev y

Theorem. (Conj_add_SNo_Lev_bd__20__5)

¬ Subq z (SNoLev (w + y))

In Proofgold the corresponding term root is a552af... and proposition id is bae0de...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_Lev_bd__20__5

Beginning of Section Conj_add_SNo_Lev_bd__21__2

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Hypothesis H0 : SNo y

Hypothesis H1 : ordinal (SNoLev x + SNoLev y)

Hypothesis H3 : z ∈ ordsucc (SNoLev (w + y))

Hypothesis H4 : ordinal z

Hypothesis H5 : Subq (SNoLev x + SNoLev y) z

Hypothesis H6 : Subq (SNoLev (w + y)) (SNoLev w + SNoLev y)

Hypothesis H7 : SNoLev w + SNoLev y ∈ SNoLev x + SNoLev y

Theorem. (Conj_add_SNo_Lev_bd__21__2)

¬ Subq (SNoLev w + SNoLev y) (SNoLev x + SNoLev y)

In Proofgold the corresponding term root is 2c6c95... and proposition id is 82480a...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_Lev_bd__21__2

Beginning of Section Conj_add_SNo_Lev_bd__22__6

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Hypothesis H0 : SNo x

Hypothesis H1 : SNo y

Hypothesis H2 : ordinal (SNoLev x + SNoLev y)

Hypothesis H3 : SNo w

Hypothesis H4 : SNoLev w ∈ SNoLev x

Hypothesis H5 : z ∈ ordsucc (SNoLev (w + y))

Hypothesis H7 : Subq (SNoLev x + SNoLev y) z

Hypothesis H8 : Subq (SNoLev (w + y)) (SNoLev w + SNoLev y)

Theorem. (Conj_add_SNo_Lev_bd__22__6)

¬ SNoLev w + SNoLev y ∈ SNoLev x + SNoLev y

In Proofgold the corresponding term root is 619007... and proposition id is 345e59...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_Lev_bd__22__6

Beginning of Section Conj_add_SNo_Lev_bd__23__3

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Hypothesis H0 : SNo x

Hypothesis H1 : SNo y

Hypothesis H2 : ordinal (SNoLev x + SNoLev y)

Hypothesis H4 : w ∈ SNoS_ (SNoLev x)

Hypothesis H5 : SNo w

Hypothesis H6 : SNoLev w ∈ SNoLev x

Hypothesis H7 : z ∈ ordsucc (SNoLev (w + y))

Hypothesis H8 : ordinal z

Hypothesis H9 : Subq (SNoLev x + SNoLev y) z

Theorem. (Conj_add_SNo_Lev_bd__23__3)

¬ Subq (SNoLev (w + y)) (SNoLev w + SNoLev y)

In Proofgold the corresponding term root is 667ef2... and proposition id is b84773...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_Lev_bd__23__3

Beginning of Section Conj_add_SNo_Lev_bd__23__5

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Hypothesis H0 : SNo x

Hypothesis H1 : SNo y

Hypothesis H2 : ordinal (SNoLev x + SNoLev y)

Hypothesis H3 : (∀u : set, u ∈ SNoS_ (SNoLev x) → Subq (SNoLev (u + y)) (SNoLev u + SNoLev y))

Hypothesis H4 : w ∈ SNoS_ (SNoLev x)

Hypothesis H6 : SNoLev w ∈ SNoLev x

Hypothesis H7 : z ∈ ordsucc (SNoLev (w + y))

Hypothesis H8 : ordinal z

Hypothesis H9 : Subq (SNoLev x + SNoLev y) z

Theorem. (Conj_add_SNo_Lev_bd__23__5)

¬ Subq (SNoLev (w + y)) (SNoLev w + SNoLev y)

In Proofgold the corresponding term root is 942f3a... and proposition id is 86a991...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_Lev_bd__23__5

Beginning of Section Conj_add_SNo_Lev_bd__23__6

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Hypothesis H0 : SNo x

Hypothesis H1 : SNo y

Hypothesis H2 : ordinal (SNoLev x + SNoLev y)

Hypothesis H3 : (∀u : set, u ∈ SNoS_ (SNoLev x) → Subq (SNoLev (u + y)) (SNoLev u + SNoLev y))

Hypothesis H4 : w ∈ SNoS_ (SNoLev x)

Hypothesis H5 : SNo w

Hypothesis H7 : z ∈ ordsucc (SNoLev (w + y))

Hypothesis H8 : ordinal z

Hypothesis H9 : Subq (SNoLev x + SNoLev y) z

Theorem. (Conj_add_SNo_Lev_bd__23__6)

¬ Subq (SNoLev (w + y)) (SNoLev w + SNoLev y)

In Proofgold the corresponding term root is 0ecea1... and proposition id is 57bf76...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_Lev_bd__23__6

Beginning of Section Conj_add_SNo_Lev_bd__23__7

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Hypothesis H0 : SNo x

Hypothesis H1 : SNo y

Hypothesis H2 : ordinal (SNoLev x + SNoLev y)

Hypothesis H3 : (∀u : set, u ∈ SNoS_ (SNoLev x) → Subq (SNoLev (u + y)) (SNoLev u + SNoLev y))

Hypothesis H4 : w ∈ SNoS_ (SNoLev x)

Hypothesis H5 : SNo w

Hypothesis H6 : SNoLev w ∈ SNoLev x

Hypothesis H8 : ordinal z

Hypothesis H9 : Subq (SNoLev x + SNoLev y) z

Theorem. (Conj_add_SNo_Lev_bd__23__7)

¬ Subq (SNoLev (w + y)) (SNoLev w + SNoLev y)

In Proofgold the corresponding term root is 965c98... and proposition id is 8a6ac5...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_Lev_bd__23__7

Beginning of Section Conj_add_SNo_Lev_bd__24__5

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Hypothesis H0 : SNo x

Hypothesis H1 : SNo y

Hypothesis H2 : ordinal (SNoLev x + SNoLev y)

Hypothesis H3 : (∀u : set, u ∈ SNoS_ (SNoLev x) → Subq (SNoLev (u + y)) (SNoLev u + SNoLev y))

Hypothesis H4 : w ∈ SNoS_ (SNoLev x)

Hypothesis H6 : SNoLev w ∈ SNoLev x

Hypothesis H7 : z ∈ ordsucc (SNoLev (w + y))

Theorem. (Conj_add_SNo_Lev_bd__24__5)

ordinal z → z ∈ SNoLev x + SNoLev y

In Proofgold the corresponding term root is 3a22f8... and proposition id is 931664...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_Lev_bd__24__5

Beginning of Section Conj_add_SNo_Lev_bd__29__1

Variable x : set

Variable y : set

Hypothesis H0 : SNo x

Hypothesis H2 : ordinal (SNoLev x + SNoLev y)

Hypothesis H3 : (∀z : set, z ∈ SNoS_ (SNoLev x) → Subq (SNoLev (z + y)) (SNoLev z + SNoLev y))

Hypothesis H4 : (∀z : set, z ∈ SNoS_ (SNoLev y) → Subq (SNoLev (x + z)) (SNoLev x + SNoLev z))

Hypothesis H5 : SNoLev (SNoCut (binunion (Repl (SNoL x) (λz : set ⇒ z + y)) (Repl (SNoL y) (add_SNo x))) (binunion (Repl (SNoR x) (λz : set ⇒ z + y)) (Repl (SNoR y) (add_SNo x)))) ∈ ordsucc (binunion (famunion (binunion (Repl (SNoL x) (λz : set ⇒ z + y)) (Repl (SNoL y) (add_SNo x))) (λz : set ⇒ ordsucc (SNoLev z))) (famunion (binunion (Repl (SNoR x) (λz : set ⇒ z + y)) (Repl (SNoR y) (add_SNo x))) (λz : set ⇒ ordsucc (SNoLev z))))

Hypothesis H6 : (∀z : set, z ∈ Repl (SNoL x) (λw : set ⇒ w + y) → (∀p : set → prop, (∀w : set, w ∈ SNoS_ (SNoLev x) → z = w + y → SNo w → SNoLev w ∈ SNoLev x → w < x → p (w + y)) → p z))

Hypothesis H7 : (∀z : set, z ∈ Repl (SNoL y) (add_SNo x) → (∀p : set → prop, (∀w : set, w ∈ SNoS_ (SNoLev y) → z = x + w → SNo w → SNoLev w ∈ SNoLev y → w < y → p (x + w)) → p z))

Hypothesis H8 : (∀z : set, z ∈ Repl (SNoR x) (λw : set ⇒ w + y) → (∀p : set → prop, (∀w : set, w ∈ SNoS_ (SNoLev x) → z = w + y → SNo w → SNoLev w ∈ SNoLev x → x < w → p (w + y)) → p z))

Hypothesis H9 : (∀z : set, z ∈ Repl (SNoR y) (add_SNo x) → (∀p : set → prop, (∀w : set, w ∈ SNoS_ (SNoLev y) → z = x + w → SNo w → SNoLev w ∈ SNoLev y → y < w → p (x + w)) → p z))

Hypothesis H10 : (∀z : set, z ∈ Repl (SNoL x) (λw : set ⇒ w + y) → SNo z)

Hypothesis H11 : (∀z : set, z ∈ Repl (SNoL y) (add_SNo x) → SNo z)

Theorem. (Conj_add_SNo_Lev_bd__29__1)

(∀z : set, z ∈ Repl (SNoR x) (λw : set ⇒ w + y) → SNo z) → Subq (SNoLev (SNoCut (binunion (Repl (SNoL x) (λz : set ⇒ z + y)) (Repl (SNoL y) (add_SNo x))) (binunion (Repl (SNoR x) (λz : set ⇒ z + y)) (Repl (SNoR y) (add_SNo x))))) (SNoLev x + SNoLev y)

In Proofgold the corresponding term root is fbb395... and proposition id is 021de9...

Proof:

The rest of the proof is missing.

End of Section Conj_add_SNo_Lev_bd__29__1

Beginning of Section Conj_add_SNo_Lev_bd__29__4