Proofgold Address

Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Definition TransSet^TransSet := λ x0 . ∀ x1 . x1 ∈ x0 ⟶ x1 ⊆ x0
Param Sing^Sing : ι → ι
Param ordsucc^ordsucc : ι → ι
Known neq_0_1^neq_0_1 : 0 = 1 ⟶ ∀ x0 : ο . x0
Known SingE^SingE : ∀ x0 x1 . x1 ∈ Sing x0 ⟶ x1 = x0
Known SingI^SingI : ∀ x0 . x0 ∈ Sing x0
Known In_0_1^In_0_1 : 0 ∈ 1
Theorem not_TransSet_Sing1^{not_TransSet_Sing1} : not (TransSet (Sing 1)) (proof)
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition ordinal^ordinal := λ x0 . and (TransSet x0) (∀ x1 . x1 ∈ x0 ⟶ TransSet x1)
Theorem not_ordinal_Sing1^{not_ordinal_Sing1} : not (ordinal (Sing 1)) (proof)
Param binunion^binunion : ι → ι → ι
Definition SetAdjoin^SetAdjoin := λ x0 x1 . binunion x0 (Sing x1)
Known ordinal_Hered^{ordinal_Hered} : ∀ x0 . ordinal x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ ordinal x1
Known binunionI2^binunionI2 : ∀ x0 x1 x2 . x2 ∈ x1 ⟶ x2 ∈ binunion x0 x1
Theorem tagged_not_ordinal^{tagged_not_ordinal} : ∀ x0 . not (ordinal (SetAdjoin x0 (Sing 1))) (proof)
Definition nIn^nIn := λ x0 x1 . not (x0 ∈ x1)
Theorem tagged_notin_ordinal^{tagged_notin_ordinal} : ∀ x0 x1 . ordinal x0 ⟶ nIn (SetAdjoin x1 (Sing 1)) x0 (proof)
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known binunionE^binunionE : ∀ x0 x1 x2 . x2 ∈ binunion x0 x1 ⟶ or (x2 ∈ x0) (x2 ∈ x1)
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Known binunionI1^binunionI1 : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ x2 ∈ binunion x0 x1
Theorem tagged_eqE_Subq^{tagged_eqE_Subq} : ∀ x0 x1 . ordinal x0 ⟶ SetAdjoin x0 (Sing 1) = SetAdjoin x1 (Sing 1) ⟶ x0 ⊆ x1 (proof)
Known set_ext^set_ext : ∀ x0 x1 . x0 ⊆ x1 ⟶ x1 ⊆ x0 ⟶ x0 = x1
Theorem tagged_eqE_eq^{tagged_eqE_eq} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ SetAdjoin x0 (Sing 1) = SetAdjoin x1 (Sing 1) ⟶ x0 = x1 (proof)
Known ReplE_impred^ReplE_impred : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ prim5 x0 x1 ⟶ ∀ x3 : ο . (∀ x4 . x4 ∈ x0 ⟶ x2 = x1 x4 ⟶ x3) ⟶ x3
Theorem tagged_ReplE^tagged_ReplE : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ SetAdjoin x1 (Sing 1) ∈ {SetAdjoin x2 (Sing 1)|x2 ∈ x0} ⟶ x1 ∈ x0 (proof)
Theorem ordinal_notin_tagged_Repl^{ordinal_notin_tagged_Repl} : ∀ x0 x1 . ordinal x0 ⟶ nIn x0 {SetAdjoin x2 (Sing 1)|x2 ∈ x1} (proof)
Definition SNoElts_^SNoElts_ := λ x0 . binunion x0 {SetAdjoin x1 (Sing 1)|x1 ∈ x0}
Known ReplI^ReplI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ x1 x2 ∈ prim5 x0 x1
Theorem SNoElts_mon^SNoElts_mon : ∀ x0 x1 . x0 ⊆ x1 ⟶ SNoElts_ x0 ⊆ SNoElts_ x1 (proof)
Param exactly1of2^exactly1of2 : ο → ο → ο
Definition SNo_^SNo_ := λ x0 x1 . and (x1 ⊆ SNoElts_ x0) (∀ x2 . x2 ∈ x0 ⟶ exactly1of2 (SetAdjoin x2 (Sing 1) ∈ x1) (x2 ∈ x1))
Param Sep^Sep : ι → (ι → ο) → ι
Param ReplSep^ReplSep : ι → (ι → ο) → (ι → ι) → ι
Definition PSNo^PSNo := λ x0 . λ x1 : ι → ο . binunion (Sep x0 x1) {SetAdjoin x2 (Sing 1)|x2 ∈ x0,not (x1 x2)}
Definition iff^iff := λ x0 x1 : ο . and (x0 ⟶ x1) (x1 ⟶ x0)
Definition PNoEq_^PNoEq_ := λ x0 . λ x1 x2 : ι → ο . ∀ x3 . x3 ∈ x0 ⟶ iff (x1 x3) (x2 x3)
Known iffI^iffI : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ iff x0 x1
Known SepE2^SepE2 : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ Sep x0 x1 ⟶ x1 x2
Known ReplSepE_impred^{ReplSepE_impred} : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 : ι → ι . ∀ x3 . x3 ∈ ReplSep x0 x1 x2 ⟶ ∀ x4 : ο . (∀ x5 . x5 ∈ x0 ⟶ x1 x5 ⟶ x3 = x2 x5 ⟶ x4) ⟶ x4
Known SepI^SepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ x0 ⟶ x1 x2 ⟶ x2 ∈ Sep x0 x1
Theorem PNoEq_PSNo^PNoEq_PSNo : ∀ x0 . ordinal x0 ⟶ ∀ x1 : ι → ο . PNoEq_ x0 (λ x2 . x2 ∈ PSNo x0 x1) x1 (proof)
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known SepE^SepE : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ Sep x0 x1 ⟶ and (x2 ∈ x0) (x1 x2)
Known xm^xm : ∀ x0 : ο . or x0 (not x0)
Known exactly1of2_I2^{exactly1of2_I2} : ∀ x0 x1 : ο . not x0 ⟶ x1 ⟶ exactly1of2 x0 x1
Known exactly1of2_I1^{exactly1of2_I1} : ∀ x0 x1 : ο . x0 ⟶ not x1 ⟶ exactly1of2 x0 x1
Known ReplSepI^ReplSepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 : ι → ι . ∀ x3 . x3 ∈ x0 ⟶ x1 x3 ⟶ x2 x3 ∈ ReplSep x0 x1 x2
Theorem SNo_PSNo^SNo_PSNo : ∀ x0 . ordinal x0 ⟶ ∀ x1 : ι → ο . SNo_ x0 (PSNo x0 x1) (proof)
Known exactly1of2_E^{exactly1of2_E} : ∀ x0 x1 : ο . exactly1of2 x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ not x1 ⟶ x2) ⟶ (not x0 ⟶ x1 ⟶ x2) ⟶ x2
Theorem SNo_PSNo_eta_^{SNo_PSNo_eta_} : ∀ x0 x1 . ordinal x0 ⟶ SNo_ x0 x1 ⟶ x1 = PSNo x0 (λ x3 . x3 ∈ x1) (proof)
Definition SNo^SNo := λ x0 . ∀ x1 : ο . (∀ x2 . and (ordinal x2) (SNo_ x2 x0) ⟶ x1) ⟶ x1
Theorem SNo_SNo^SNo_SNo : ∀ x0 . ordinal x0 ⟶ ∀ x1 . SNo_ x0 x1 ⟶ SNo x1 (proof)
Definition SNoLev^SNoLev := λ x0 . prim0 (λ x1 . and (ordinal x1) (SNo_ x1 x0))
Known exactly1of2_or^{exactly1of2_or} : ∀ x0 x1 : ο . exactly1of2 x0 x1 ⟶ or x0 x1
Theorem SNoLev_uniq_Subq^{SNoLev_uniq_Subq} : ∀ x0 x1 x2 . ordinal x1 ⟶ ordinal x2 ⟶ SNo_ x1 x0 ⟶ SNo_ x2 x0 ⟶ x1 ⊆ x2 (proof)
Theorem SNoLev_uniq^SNoLev_uniq : ∀ x0 x1 x2 . ordinal x1 ⟶ ordinal x2 ⟶ SNo_ x1 x0 ⟶ SNo_ x2 x0 ⟶ x1 = x2 (proof)
Known Eps_i_ex^Eps_i_ex : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . x0 x2 ⟶ x1) ⟶ x1) ⟶ x0 (prim0 x0)
Theorem SNoLev_prop^SNoLev_prop : ∀ x0 . SNo x0 ⟶ and (ordinal (SNoLev x0)) (SNo_ (SNoLev x0) x0) (proof)
Theorem SNoLev_ordinal^{SNoLev_ordinal} : ∀ x0 . SNo x0 ⟶ ordinal (SNoLev x0) (proof)
Theorem SNoLev_^SNoLev_ : ∀ x0 . SNo x0 ⟶ SNo_ (SNoLev x0) x0 (proof)
Theorem SNo_PSNo_eta^SNo_PSNo_eta : ∀ x0 . SNo x0 ⟶ x0 = PSNo (SNoLev x0) (λ x2 . x2 ∈ x0) (proof)
Theorem SNoLev_PSNo^SNoLev_PSNo : ∀ x0 . ordinal x0 ⟶ ∀ x1 : ι → ο . SNoLev (PSNo x0 x1) = x0 (proof)
Theorem SNo_Subq^SNo_Subq : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ SNoLev x0 ⊆ SNoLev x1 ⟶ (∀ x2 . x2 ∈ SNoLev x0 ⟶ iff (x2 ∈ x0) (x2 ∈ x1)) ⟶ x0 ⊆ x1 (proof)
Definition SNoEq_^SNoEq_ := λ x0 x1 x2 . PNoEq_ x0 (λ x3 . x3 ∈ x1) (λ x3 . x3 ∈ x2)
Theorem SNoEq_I^SNoEq_I : ∀ x0 x1 x2 . (∀ x3 . x3 ∈ x0 ⟶ iff (x3 ∈ x1) (x3 ∈ x2)) ⟶ SNoEq_ x0 x1 x2 (proof)
Theorem SNoEq_E^SNoEq_E : ∀ x0 x1 x2 . SNoEq_ x0 x1 x2 ⟶ ∀ x3 . x3 ∈ x0 ⟶ iff (x3 ∈ x1) (x3 ∈ x2) (proof)
Theorem SNoEq_E1^SNoEq_E1 : ∀ x0 x1 x2 . SNoEq_ x0 x1 x2 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x3 ∈ x1 ⟶ x3 ∈ x2 (proof)
Theorem SNoEq_E2^SNoEq_E2 : ∀ x0 x1 x2 . SNoEq_ x0 x1 x2 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x3 ∈ x2 ⟶ x3 ∈ x1 (proof)
Known PNoEq_antimon_^{PNoEq_antimon_} : ∀ x0 x1 : ι → ο . ∀ x2 . ordinal x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ PNoEq_ x2 x0 x1 ⟶ PNoEq_ x3 x0 x1
Theorem SNoEq_antimon_^{SNoEq_antimon_} : ∀ x0 . ordinal x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ ∀ x2 x3 . SNoEq_ x0 x2 x3 ⟶ SNoEq_ x1 x2 x3 (proof)
Known Subq_ref^Subq_ref : ∀ x0 . x0 ⊆ x0
Known iff_sym^iff_sym : ∀ x0 x1 : ο . iff x0 x1 ⟶ iff x1 x0
Theorem SNo_eq^SNo_eq : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ SNoLev x0 = SNoLev x1 ⟶ SNoEq_ (SNoLev x0) x0 x1 ⟶ x0 = x1 (proof)
Param PNoLt^PNoLt : ι → (ι → ο) → ι → (ι → ο) → ο
Definition SNoLt^SNoLt := λ x0 x1 . PNoLt (SNoLev x0) (λ x2 . x2 ∈ x0) (SNoLev x1) (λ x2 . x2 ∈ x1)
Definition PNoLe^PNoLe := λ x0 . λ x1 : ι → ο . λ x2 . λ x3 : ι → ο . or (PNoLt x0 x1 x2 x3) (and (x0 = x2) (PNoEq_ x0 x1 x3))
Definition SNoLe^SNoLe := λ x0 x1 . PNoLe (SNoLev x0) (λ x2 . x2 ∈ x0) (SNoLev x1) (λ x2 . x2 ∈ x1)
Known PNoLeI1^PNoLeI1 : ∀ x0 x1 . ∀ x2 x3 : ι → ο . PNoLt x0 x2 x1 x3 ⟶ PNoLe x0 x2 x1 x3
Theorem SNoLtLe^SNoLtLe : ∀ x0 x1 . SNoLt x0 x1 ⟶ SNoLe x0 x1 (proof)
Known orIL^orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Known orIR^orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Theorem SNoLeE^SNoLeE : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ SNoLe x0 x1 ⟶ or (SNoLt x0 x1) (x0 = x1) (proof)
Known PNoEq_ref_^PNoEq_ref_ : ∀ x0 . ∀ x1 : ι → ο . PNoEq_ x0 x1 x1
Theorem SNoEq_ref_^SNoEq_ref_ : ∀ x0 x1 . SNoEq_ x0 x1 x1 (proof)
Known PNoEq_sym_^PNoEq_sym_ : ∀ x0 . ∀ x1 x2 : ι → ο . PNoEq_ x0 x1 x2 ⟶ PNoEq_ x0 x2 x1
Theorem SNoEq_sym_^SNoEq_sym_ : ∀ x0 x1 x2 . SNoEq_ x0 x1 x2 ⟶ SNoEq_ x0 x2 x1 (proof)
Known PNoEq_tra_^PNoEq_tra_ : ∀ x0 . ∀ x1 x2 x3 : ι → ο . PNoEq_ x0 x1 x2 ⟶ PNoEq_ x0 x2 x3 ⟶ PNoEq_ x0 x1 x3
Theorem SNoEq_tra_^SNoEq_tra_ : ∀ x0 x1 x2 x3 . SNoEq_ x0 x1 x2 ⟶ SNoEq_ x0 x2 x3 ⟶ SNoEq_ x0 x1 x3 (proof)
Param binintersect^binintersect : ι → ι → ι
Definition PNoLt_^PNoLt_ := λ x0 . λ x1 x2 : ι → ο . ∀ x3 : ο . (∀ x4 . and (x4 ∈ x0) (and (and (PNoEq_ x4 x1 x2) (not (x1 x4))) (x2 x4)) ⟶ x3) ⟶ x3
Known PNoLtE^PNoLtE : ∀ x0 x1 . ∀ x2 x3 : ι → ο . PNoLt x0 x2 x1 x3 ⟶ ∀ x4 : ο . (PNoLt_ (binintersect x0 x1) x2 x3 ⟶ x4) ⟶ (x0 ∈ x1 ⟶ PNoEq_ x0 x2 x3 ⟶ x3 x0 ⟶ x4) ⟶ (x1 ∈ x0 ⟶ PNoEq_ x1 x2 x3 ⟶ not (x2 x1) ⟶ x4) ⟶ x4
Known PNoLt_E_^PNoLt_E_ : ∀ x0 . ∀ x1 x2 : ι → ο . PNoLt_ x0 x1 x2 ⟶ ∀ x3 : ο . (∀ x4 . x4 ∈ x0 ⟶ PNoEq_ x4 x1 x2 ⟶ not (x1 x4) ⟶ x2 x4 ⟶ x3) ⟶ x3
Known binintersectE^{binintersectE} : ∀ x0 x1 x2 . x2 ∈ binintersect x0 x1 ⟶ and (x2 ∈ x0) (x2 ∈ x1)
Known PNoLtI3^PNoLtI3 : ∀ x0 x1 . ∀ x2 x3 : ι → ο . x1 ∈ x0 ⟶ PNoEq_ x1 x2 x3 ⟶ not (x2 x1) ⟶ PNoLt x0 x2 x1 x3
Known PNoLtI2^PNoLtI2 : ∀ x0 x1 . ∀ x2 x3 : ι → ο . x0 ∈ x1 ⟶ PNoEq_ x0 x2 x3 ⟶ x3 x0 ⟶ PNoLt x0 x2 x1 x3
Theorem SNoLtE^SNoLtE : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ SNoLt x0 x1 ⟶ ∀ x2 : ο . (∀ x3 . SNo x3 ⟶ SNoLev x3 ∈ binintersect (SNoLev x0) (SNoLev x1) ⟶ SNoEq_ (SNoLev x3) x3 x0 ⟶ SNoEq_ (SNoLev x3) x3 x1 ⟶ SNoLt x0 x3 ⟶ SNoLt x3 x1 ⟶ nIn (SNoLev x3) x0 ⟶ SNoLev x3 ∈ x1 ⟶ x2) ⟶ (SNoLev x0 ∈ SNoLev x1 ⟶ SNoEq_ (SNoLev x0) x0 x1 ⟶ SNoLev x0 ∈ x1 ⟶ x2) ⟶ (SNoLev x1 ∈ SNoLev x0 ⟶ SNoEq_ (SNoLev x1) x0 x1 ⟶ nIn (SNoLev x1) x0 ⟶ x2) ⟶ x2 (proof)
Theorem SNoLtI2^SNoLtI2 : ∀ x0 x1 . SNoLev x0 ∈ SNoLev x1 ⟶ SNoEq_ (SNoLev x0) x0 x1 ⟶ SNoLev x0 ∈ x1 ⟶ SNoLt x0 x1 (proof)
Theorem SNoLtI3^SNoLtI3 : ∀ x0 x1 . SNoLev x1 ∈ SNoLev x0 ⟶ SNoEq_ (SNoLev x1) x0 x1 ⟶ nIn (SNoLev x1) x0 ⟶ SNoLt x0 x1 (proof)
Known PNoLt_irref^PNoLt_irref : ∀ x0 . ∀ x1 : ι → ο . not (PNoLt x0 x1 x0 x1)
Theorem SNoLt_irref^SNoLt_irref : ∀ x0 . not (SNoLt x0 x0) (proof)
Known PNoLt_trichotomy_or^{PNoLt_trichotomy_or} : ∀ x0 x1 . ∀ x2 x3 : ι → ο . ordinal x0 ⟶ ordinal x1 ⟶ or (or (PNoLt x0 x2 x1 x3) (and (x0 = x1) (PNoEq_ x0 x2 x3))) (PNoLt x1 x3 x0 x2)
Known or3I1^or3I1 : ∀ x0 x1 x2 : ο . x0 ⟶ or (or x0 x1) x2
Known or3I2^or3I2 : ∀ x0 x1 x2 : ο . x1 ⟶ or (or x0 x1) x2
Known or3I3^or3I3 : ∀ x0 x1 x2 : ο . x2 ⟶ or (or x0 x1) x2
Theorem SNoLt_trichotomy_or^{SNoLt_trichotomy_or} : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ or (or (SNoLt x0 x1) (x0 = x1)) (SNoLt x1 x0) (proof)
Known PNoLt_tra^PNoLt_tra : ∀ x0 x1 x2 . ordinal x0 ⟶ ordinal x1 ⟶ ordinal x2 ⟶ ∀ x3 x4 x5 : ι → ο . PNoLt x0 x3 x1 x4 ⟶ PNoLt x1 x4 x2 x5 ⟶ PNoLt x0 x3 x2 x5
Theorem SNoLt_tra^SNoLt_tra : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNoLt x0 x1 ⟶ SNoLt x1 x2 ⟶ SNoLt x0 x2 (proof)
Known PNoLe_ref^PNoLe_ref : ∀ x0 . ∀ x1 : ι → ο . PNoLe x0 x1 x0 x1
Theorem SNoLe_ref^SNoLe_ref : ∀ x0 . SNoLe x0 x0 (proof)
Known PNoLe_antisym^{PNoLe_antisym} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ ∀ x2 x3 : ι → ο . PNoLe x0 x2 x1 x3 ⟶ PNoLe x1 x3 x0 x2 ⟶ and (x0 = x1) (PNoEq_ x0 x2 x3)
Theorem SNoLe_antisym^{SNoLe_antisym} : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ SNoLe x0 x1 ⟶ SNoLe x1 x0 ⟶ x0 = x1 (proof)
Known PNoLtLe_tra^PNoLtLe_tra : ∀ x0 x1 x2 . ordinal x0 ⟶ ordinal x1 ⟶ ordinal x2 ⟶ ∀ x3 x4 x5 : ι → ο . PNoLt x0 x3 x1 x4 ⟶ PNoLe x1 x4 x2 x5 ⟶ PNoLt x0 x3 x2 x5
Theorem SNoLtLe_tra^SNoLtLe_tra : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNoLt x0 x1 ⟶ SNoLe x1 x2 ⟶ SNoLt x0 x2 (proof)
Known PNoLeLt_tra^PNoLeLt_tra : ∀ x0 x1 x2 . ordinal x0 ⟶ ordinal x1 ⟶ ordinal x2 ⟶ ∀ x3 x4 x5 : ι → ο . PNoLe x0 x3 x1 x4 ⟶ PNoLt x1 x4 x2 x5 ⟶ PNoLt x0 x3 x2 x5
Theorem SNoLeLt_tra^SNoLeLt_tra : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNoLe x0 x1 ⟶ SNoLt x1 x2 ⟶ SNoLt x0 x2 (proof)
Known PNoLe_tra^PNoLe_tra : ∀ x0 x1 x2 . ordinal x0 ⟶ ordinal x1 ⟶ ordinal x2 ⟶ ∀ x3 x4 x5 : ι → ο . PNoLe x0 x3 x1 x4 ⟶ PNoLe x1 x4 x2 x5 ⟶ PNoLe x0 x3 x2 x5
Theorem SNoLe_tra^SNoLe_tra : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNoLe x0 x1 ⟶ SNoLe x1 x2 ⟶ SNoLe x0 x2 (proof)
Theorem SNoLtLe_or^SNoLtLe_or : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ or (SNoLt x0 x1) (SNoLe x1 x0) (proof)
Known PNoEqLt_tra^PNoEqLt_tra : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ ∀ x2 x3 x4 : ι → ο . PNoEq_ x0 x2 x3 ⟶ PNoLt x0 x3 x1 x4 ⟶ PNoLt x0 x2 x1 x4
Known PNoLtEq_tra^PNoLtEq_tra : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ ∀ x2 x3 x4 : ι → ο . PNoLt x0 x2 x1 x3 ⟶ PNoEq_ x1 x3 x4 ⟶ PNoLt x0 x2 x1 x4
Theorem SNoLt_PSNo_PNoLt^{SNoLt_PSNo_PNoLt} : ∀ x0 x1 . ∀ x2 x3 : ι → ο . ordinal x0 ⟶ ordinal x1 ⟶ SNoLt (PSNo x0 x2) (PSNo x1 x3) ⟶ PNoLt x0 x2 x1 x3 (proof)
Theorem PNoLt_SNoLt_PSNo^{PNoLt_SNoLt_PSNo} : ∀ x0 x1 . ∀ x2 x3 : ι → ο . ordinal x0 ⟶ ordinal x1 ⟶ PNoLt x0 x2 x1 x3 ⟶ SNoLt (PSNo x0 x2) (PSNo x1 x3) (proof)
Param PNo_bd^PNo_bd : (ι → (ι → ο) → ο) → (ι → (ι → ο) → ο) → ι
Param PNo_pred^PNo_pred : (ι → (ι → ο) → ο) → (ι → (ι → ο) → ο) → ι → ο
Definition SNoCut^SNoCut := λ x0 x1 . PSNo (PNo_bd (λ x2 . λ x3 : ι → ο . and (ordinal x2) (PSNo x2 x3 ∈ x0)) (λ x2 . λ x3 : ι → ο . and (ordinal x2) (PSNo x2 x3 ∈ x1))) (PNo_pred (λ x2 . λ x3 : ι → ο . and (ordinal x2) (PSNo x2 x3 ∈ x0)) (λ x2 . λ x3 : ι → ο . and (ordinal x2) (PSNo x2 x3 ∈ x1)))
Definition SNoCutP^SNoCutP := λ x0 x1 . and (and (∀ x2 . x2 ∈ x0 ⟶ SNo x2) (∀ x2 . x2 ∈ x1 ⟶ SNo x2)) (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x1 ⟶ SNoLt x2 x3)
Param famunion^famunion : ι → (ι → ι) → ι
Definition PNoLt_pwise^PNoLt_pwise := λ x0 x1 : ι → (ι → ο) → ο . ∀ x2 . ordinal x2 ⟶ ∀ x3 : ι → ο . x0 x2 x3 ⟶ ∀ x4 . ordinal x4 ⟶ ∀ x5 : ι → ο . x1 x4 x5 ⟶ PNoLt x2 x3 x4 x5
Definition PNo_lenbdd^PNo_lenbdd := λ x0 . λ x1 : ι → (ι → ο) → ο . ∀ x2 . ∀ x3 : ι → ο . x1 x2 x3 ⟶ x2 ∈ x0
Definition PNo_strict_upperbd^{PNo_strict_upperbd} := λ x0 : ι → (ι → ο) → ο . λ x1 . λ x2 : ι → ο . ∀ x3 . ordinal x3 ⟶ ∀ x4 : ι → ο . x0 x3 x4 ⟶ PNoLt x3 x4 x1 x2
Definition PNo_strict_lowerbd^{PNo_strict_lowerbd} := λ x0 : ι → (ι → ο) → ο . λ x1 . λ x2 : ι → ο . ∀ x3 . ordinal x3 ⟶ ∀ x4 : ι → ο . x0 x3 x4 ⟶ PNoLt x1 x2 x3 x4
Definition PNo_strict_imv^{PNo_strict_imv} := λ x0 x1 : ι → (ι → ο) → ο . λ x2 . λ x3 : ι → ο . and (PNo_strict_upperbd x0 x2 x3) (PNo_strict_lowerbd x1 x2 x3)
Definition PNo_least_rep^{PNo_least_rep} := λ x0 x1 : ι → (ι → ο) → ο . λ x2 . λ x3 : ι → ο . and (and (ordinal x2) (PNo_strict_imv x0 x1 x2 x3)) (∀ x4 . x4 ∈ x2 ⟶ ∀ x5 : ι → ο . not (PNo_strict_imv x0 x1 x4 x5))
Known PNo_bd_pred^PNo_bd_pred : ∀ x0 x1 : ι → (ι → ο) → ο . PNoLt_pwise x0 x1 ⟶ ∀ x2 . ordinal x2 ⟶ PNo_lenbdd x2 x0 ⟶ PNo_lenbdd x2 x1 ⟶ PNo_least_rep x0 x1 (PNo_bd x0 x1) (PNo_pred x0 x1)
Known and5I^and5I : ∀ x0 x1 x2 x3 x4 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ and (and (and (and x0 x1) x2) x3) x4
Known PNoLt_trichotomy_or_^{PNoLt_trichotomy_or_} : ∀ x0 x1 : ι → ο . ∀ x2 . ordinal x2 ⟶ or (or (PNoLt_ x2 x0 x1) (PNoEq_ x2 x0 x1)) (PNoLt_ x2 x1 x0)
Param PNo_rel_strict_imv^{PNo_rel_strict_imv} : (ι → (ι → ο) → ο) → (ι → (ι → ο) → ο) → ι → (ι → ο) → ο
Definition PNo_rel_strict_split_imv^{PNo_rel_strict_split_imv} := λ x0 x1 : ι → (ι → ο) → ο . λ x2 . λ x3 : ι → ο . and (PNo_rel_strict_imv x0 x1 (ordsucc x2) (λ x4 . and (x3 x4) (x4 = x2 ⟶ ∀ x5 : ο . x5))) (PNo_rel_strict_imv x0 x1 (ordsucc x2) (λ x4 . or (x3 x4) (x4 = x2)))
Known PNo_rel_split_imv_imp_strict_imv^{PNo_rel_split_imv_imp_strict_imv} : ∀ x0 x1 : ι → (ι → ο) → ο . ∀ x2 . ordinal x2 ⟶ ∀ x3 : ι → ο . PNo_rel_strict_split_imv x0 x1 x2 x3 ⟶ PNo_strict_imv x0 x1 x2 x3
Known PNoEq_rel_strict_imv^{PNoEq_rel_strict_imv} : ∀ x0 x1 : ι → (ι → ο) → ο . ∀ x2 . ordinal x2 ⟶ ∀ x3 x4 : ι → ο . PNoEq_ x2 x3 x4 ⟶ PNo_rel_strict_imv x0 x1 x2 x3 ⟶ PNo_rel_strict_imv x0 x1 x2 x4
Known ordsuccE^ordsuccE : ∀ x0 x1 . x1 ∈ ordsucc x0 ⟶ or (x1 ∈ x0) (x1 = x0)
Known iff_trans^iff_trans : ∀ x0 x1 x2 : ο . iff x0 x1 ⟶ iff x1 x2 ⟶ iff x0 x2
Known PNo_extend0_eq^{PNo_extend0_eq} : ∀ x0 . ∀ x1 : ι → ο . PNoEq_ x0 x1 (λ x2 . and (x1 x2) (x2 = x0 ⟶ ∀ x3 : ο . x3))
Known PNo_strict_imv_imp_rel_strict_imv^{PNo_strict_imv_imp_rel_strict_imv} : ∀ x0 x1 : ι → (ι → ο) → ο . ∀ x2 . ordinal x2 ⟶ ∀ x3 . x3 ∈ ordsucc x2 ⟶ ∀ x4 : ι → ο . PNo_strict_imv x0 x1 x2 x4 ⟶ PNo_rel_strict_imv x0 x1 x3 x4
Known ordinal_ordsucc_In^{ordinal_ordsucc_In} : ∀ x0 . ordinal x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ ordsucc x1 ∈ ordsucc x0
Known PNo_extend1_eq^{PNo_extend1_eq} : ∀ x0 . ∀ x1 : ι → ο . PNoEq_ x0 x1 (λ x2 . or (x1 x2) (x2 = x0))
Known ordinal_ordsucc^{ordinal_ordsucc} : ∀ x0 . ordinal x0 ⟶ ordinal (ordsucc x0)
Known ordinal_In_Or_Subq^{ordinal_In_Or_Subq} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ or (x0 ∈ x1) (x1 ⊆ x0)
Known PNo_bd_In^PNo_bd_In : ∀ x0 x1 : ι → (ι → ο) → ο . PNoLt_pwise x0 x1 ⟶ ∀ x2 . ordinal x2 ⟶ PNo_lenbdd x2 x0 ⟶ PNo_lenbdd x2 x1 ⟶ PNo_bd x0 x1 ∈ ordsucc x2
Known famunionI^famunionI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . x2 ∈ x0 ⟶ x3 ∈ x1 x2 ⟶ x3 ∈ famunion x0 x1
Known ordsuccI2^ordsuccI2 : ∀ x0 . x0 ∈ ordsucc x0
Known ordinal_linear^{ordinal_linear} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ or (x0 ⊆ x1) (x1 ⊆ x0)
Known Subq_binunion_eq^{Subq_binunion_eq} : ∀ x0 x1 . x0 ⊆ x1 = (binunion x0 x1 = x1)
Known binunion_com^binunion_com : ∀ x0 x1 . binunion x0 x1 = binunion x1 x0
Known ordinal_famunion^{ordinal_famunion} : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . x2 ∈ x0 ⟶ ordinal (x1 x2)) ⟶ ordinal (famunion x0 x1)
Theorem SNoCutP_SNoCut^{SNoCutP_SNoCut} : ∀ x0 x1 . SNoCutP x0 x1 ⟶ and (and (and (and (SNo (SNoCut x0 x1)) (SNoLev (SNoCut x0 x1) ∈ ordsucc (binunion (famunion x0 (λ x2 . ordsucc (SNoLev x2))) (famunion x1 (λ x2 . ordsucc (SNoLev x2)))))) (∀ x2 . x2 ∈ x0 ⟶ SNoLt x2 (SNoCut x0 x1))) (∀ x2 . x2 ∈ x1 ⟶ SNoLt (SNoCut x0 x1) x2)) (∀ x2 . SNo x2 ⟶ (∀ x3 . x3 ∈ x0 ⟶ SNoLt x3 x2) ⟶ (∀ x3 . x3 ∈ x1 ⟶ SNoLt x2 x3) ⟶ and (SNoLev (SNoCut x0 x1) ⊆ SNoLev x2) (SNoEq_ (SNoLev (SNoCut x0 x1)) (SNoCut x0 x1) x2)) (proof)
Definition SNoS_^SNoS_ := λ x0 . {x1 ∈ prim4 (SNoElts_ x0)|∀ x2 : ο . (∀ x3 . and (x3 ∈ x0) (SNo_ x3 x1) ⟶ x2) ⟶ x2}
Theorem SNoS_E^SNoS_E : ∀ x0 . ordinal x0 ⟶ ∀ x1 . x1 ∈ SNoS_ x0 ⟶ ∀ x2 : ο . (∀ x3 . and (x3 ∈ x0) (SNo_ x3 x1) ⟶ x2) ⟶ x2 (proof)
Known PowerI^PowerI : ∀ x0 x1 . x1 ⊆ x0 ⟶ x1 ∈ prim4 x0
Known Subq_tra^Subq_tra : ∀ x0 x1 x2 . x0 ⊆ x1 ⟶ x1 ⊆ x2 ⟶ x0 ⊆ x2
Theorem SNoS_I^SNoS_I : ∀ x0 . ordinal x0 ⟶ ∀ x1 x2 . x2 ∈ x0 ⟶ SNo_ x2 x1 ⟶ x1 ∈ SNoS_ x0 (proof)
Theorem SNoS_I2^SNoS_I2 : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ SNoLev x0 ∈ SNoLev x1 ⟶ x0 ∈ SNoS_ (SNoLev x1) (proof)
Theorem SNoS_Subq^SNoS_Subq : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ x0 ⊆ x1 ⟶ SNoS_ x0 ⊆ SNoS_ x1 (proof)
Theorem SNoLev_uniq2^SNoLev_uniq2 : ∀ x0 . ordinal x0 ⟶ ∀ x1 . SNo_ x0 x1 ⟶ SNoLev x1 = x0 (proof)
Theorem SNoS_E2^SNoS_E2 : ∀ x0 . ordinal x0 ⟶ ∀ x1 . x1 ∈ SNoS_ x0 ⟶ ∀ x2 : ο . (SNoLev x1 ∈ x0 ⟶ ordinal (SNoLev x1) ⟶ SNo x1 ⟶ SNo_ (SNoLev x1) x1 ⟶ x2) ⟶ x2 (proof)
Known In_irref^In_irref : ∀ x0 . nIn x0 x0
Theorem SNoS_In_neq^SNoS_In_neq : ∀ x0 . SNo x0 ⟶ ∀ x1 . x1 ∈ SNoS_ (SNoLev x0) ⟶ x1 = x0 ⟶ ∀ x2 : ο . x2 (proof)
Theorem SNoS_SNoLev^SNoS_SNoLev : ∀ x0 . SNo x0 ⟶ x0 ∈ SNoS_ (ordsucc (SNoLev x0)) (proof)
Definition SNoL^SNoL := λ x0 . {x1 ∈ SNoS_ (SNoLev x0)|SNoLt x1 x0}
Definition SNoR^SNoR := λ x0 . Sep (SNoS_ (SNoLev x0)) (SNoLt x0)
Known and3I^and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Known SepE1^SepE1 : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ Sep x0 x1 ⟶ x2 ∈ x0
Theorem SNoCutP_SNoL_SNoR^{SNoCutP_SNoL_SNoR} : ∀ x0 . SNo x0 ⟶ SNoCutP (SNoL x0) (SNoR x0) (proof)
Theorem SNoL_E^SNoL_E : ∀ x0 . SNo x0 ⟶ ∀ x1 . x1 ∈ SNoL x0 ⟶ ∀ x2 : ο . (SNo x1 ⟶ SNoLev x1 ∈ SNoLev x0 ⟶ SNoLt x1 x0 ⟶ x2) ⟶ x2 (proof)
Theorem SNoR_E^SNoR_E : ∀ x0 . SNo x0 ⟶ ∀ x1 . x1 ∈ SNoR x0 ⟶ ∀ x2 : ο . (SNo x1 ⟶ SNoLev x1 ∈ SNoLev x0 ⟶ SNoLt x0 x1 ⟶ x2) ⟶ x2 (proof)
Theorem SNoL_SNoS^SNoL_SNoS : ∀ x0 . SNo x0 ⟶ ∀ x1 . x1 ∈ SNoL x0 ⟶ x1 ∈ SNoS_ (SNoLev x0) (proof)
Theorem SNoR_SNoS^SNoR_SNoS : ∀ x0 . SNo x0 ⟶ ∀ x1 . x1 ∈ SNoR x0 ⟶ x1 ∈ SNoS_ (SNoLev x0) (proof)
Theorem SNoL_I^SNoL_I : ∀ x0 . SNo x0 ⟶ ∀ x1 . SNo x1 ⟶ SNoLev x1 ∈ SNoLev x0 ⟶ SNoLt x1 x0 ⟶ x1 ∈ SNoL x0 (proof)
Theorem SNoR_I^SNoR_I : ∀ x0 . SNo x0 ⟶ ∀ x1 . SNo x1 ⟶ SNoLev x1 ∈ SNoLev x0 ⟶ SNoLt x0 x1 ⟶ x1 ∈ SNoR x0 (proof)
Known ordinal_trichotomy_or^{ordinal_trichotomy_or} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ or (or (x0 ∈ x1) (x0 = x1)) (x1 ∈ x0)
Theorem SNo_eta^SNo_eta : ∀ x0 . SNo x0 ⟶ x0 = SNoCut (SNoL x0) (SNoR x0) (proof)
Theorem SNoCutP_SNo_SNoCut^{SNoCutP_SNo_SNoCut} : ∀ x0 x1 . SNoCutP x0 x1 ⟶ SNo (SNoCut x0 x1) (proof)
Theorem SNoCutP_SNoCut_L^{SNoCutP_SNoCut_L} : ∀ x0 x1 . SNoCutP x0 x1 ⟶ ∀ x2 . x2 ∈ x0 ⟶ SNoLt x2 (SNoCut x0 x1) (proof)
Theorem SNoCutP_SNoCut_R^{SNoCutP_SNoCut_R} : ∀ x0 x1 . SNoCutP x0 x1 ⟶ ∀ x2 . x2 ∈ x1 ⟶ SNoLt (SNoCut x0 x1) x2 (proof)
Theorem SNoCutP_SNoCut_fst^{SNoCutP_SNoCut_fst} : ∀ x0 x1 . SNoCutP x0 x1 ⟶ ∀ x2 . SNo x2 ⟶ (∀ x3 . x3 ∈ x0 ⟶ SNoLt x3 x2) ⟶ (∀ x3 . x3 ∈ x1 ⟶ SNoLt x2 x3) ⟶ and (SNoLev (SNoCut x0 x1) ⊆ SNoLev x2) (SNoEq_ (SNoLev (SNoCut x0 x1)) (SNoCut x0 x1) x2) (proof)
Known binintersectE2^{binintersectE2} : ∀ x0 x1 x2 . x2 ∈ binintersect x0 x1 ⟶ x2 ∈ x1
Theorem SNoCut_Le^SNoCut_Le : ∀ x0 x1 x2 x3 . SNoCutP x0 x1 ⟶ SNoCutP x2 x3 ⟶ (∀ x4 . x4 ∈ x0 ⟶ SNoLt x4 (SNoCut x2 x3)) ⟶ (∀ x4 . x4 ∈ x3 ⟶ SNoLt (SNoCut x0 x1) x4) ⟶ SNoLe (SNoCut x0 x1) (SNoCut x2 x3) (proof)
Theorem SNoCut_ext^SNoCut_ext : ∀ x0 x1 x2 x3 . SNoCutP x0 x1 ⟶ SNoCutP x2 x3 ⟶ (∀ x4 . x4 ∈ x0 ⟶ SNoLt x4 (SNoCut x2 x3)) ⟶ (∀ x4 . x4 ∈ x1 ⟶ SNoLt (SNoCut x2 x3) x4) ⟶ (∀ x4 . x4 ∈ x2 ⟶ SNoLt x4 (SNoCut x0 x1)) ⟶ (∀ x4 . x4 ∈ x3 ⟶ SNoLt (SNoCut x0 x1) x4) ⟶ SNoCut x0 x1 = SNoCut x2 x3 (proof)
Theorem ordinal_SNo_^ordinal_SNo_ : ∀ x0 . ordinal x0 ⟶ SNo_ x0 x0 (proof)
Definition SNo_extend0^SNo_extend0 := λ x0 . PSNo (ordsucc (SNoLev x0)) (λ x1 . and (x1 ∈ x0) (x1 = SNoLev x0 ⟶ ∀ x2 : ο . x2))
Definition SNo_extend1^SNo_extend1 := λ x0 . PSNo (ordsucc (SNoLev x0)) (λ x1 . or (x1 ∈ x0) (x1 = SNoLev x0))
Theorem SNo_extend0_SNo_^{SNo_extend0_SNo_} : ∀ x0 . SNo x0 ⟶ SNo_ (ordsucc (SNoLev x0)) (SNo_extend0 x0) (proof)
Theorem SNo_extend1_SNo_^{SNo_extend1_SNo_} : ∀ x0 . SNo x0 ⟶ SNo_ (ordsucc (SNoLev x0)) (SNo_extend1 x0) (proof)
Theorem SNo_extend0_SNo^{SNo_extend0_SNo} : ∀ x0 . SNo x0 ⟶ SNo (SNo_extend0 x0) (proof)
Theorem SNo_extend1_SNo^{SNo_extend1_SNo} : ∀ x0 . SNo x0 ⟶ SNo (SNo_extend1 x0) (proof)
Theorem SNo_extend0_SNoLev^{SNo_extend0_SNoLev} : ∀ x0 . SNo x0 ⟶ SNoLev (SNo_extend0 x0) = ordsucc (SNoLev x0) (proof)
Theorem SNo_extend1_SNoLev^{SNo_extend1_SNoLev} : ∀ x0 . SNo x0 ⟶ SNoLev (SNo_extend1 x0) = ordsucc (SNoLev x0) (proof)
Theorem SNo_extend0_nIn^{SNo_extend0_nIn} : ∀ x0 . SNo x0 ⟶ nIn (SNoLev x0) (SNo_extend0 x0) (proof)
Theorem SNo_extend1_In^{SNo_extend1_In} : ∀ x0 . SNo x0 ⟶ SNoLev x0 ∈ SNo_extend1 x0 (proof)
Theorem SNo_extend0_SNoEq^{SNo_extend0_SNoEq} : ∀ x0 . SNo x0 ⟶ SNoEq_ (SNoLev x0) (SNo_extend0 x0) x0 (proof)
Theorem SNo_extend1_SNoEq^{SNo_extend1_SNoEq} : ∀ x0 . SNo x0 ⟶ SNoEq_ (SNoLev x0) (SNo_extend1 x0) x0 (proof)
Theorem ordinal_SNo^ordinal_SNo : ∀ x0 . ordinal x0 ⟶ SNo x0 (proof)
Theorem ordinal_SNoLev^{ordinal_SNoLev} : ∀ x0 . ordinal x0 ⟶ SNoLev x0 = x0 (proof)
Known binintersectE1^{binintersectE1} : ∀ x0 x1 x2 . x2 ∈ binintersect x0 x1 ⟶ x2 ∈ x0
Known In_no2cycle^In_no2cycle : ∀ x0 x1 . x0 ∈ x1 ⟶ x1 ∈ x0 ⟶ False
Theorem ordinal_SNoLev_max^{ordinal_SNoLev_max} : ∀ x0 . ordinal x0 ⟶ ∀ x1 . SNo x1 ⟶ SNoLev x1 ∈ x0 ⟶ SNoLt x1 x0 (proof)
Theorem ordinal_In_SNoLt^{ordinal_In_SNoLt} : ∀ x0 . ordinal x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ SNoLt x1 x0 (proof)
Known dneg^dneg : ∀ x0 : ο . not (not x0) ⟶ x0
Known ordinal_ind^ordinal_ind : ∀ x0 : ι → ο . (∀ x1 . ordinal x1 ⟶ (∀ x2 . x2 ∈ x1 ⟶ x0 x2) ⟶ x0 x1) ⟶ ∀ x1 . ordinal x1 ⟶ x0 x1
Theorem ordinal_SNoLev_max_2^{ordinal_SNoLev_max_2} : ∀ x0 . ordinal x0 ⟶ ∀ x1 . SNo x1 ⟶ SNoLev x1 ∈ ordsucc x0 ⟶ SNoLe x1 x0 (proof)
Known ordsuccI1^ordsuccI1 : ∀ x0 . x0 ⊆ ordsucc x0
Theorem ordinal_Subq_SNoLe^{ordinal_Subq_SNoLe} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ x0 ⊆ x1 ⟶ SNoLe x0 x1 (proof)
Theorem SNo_etaE^SNo_etaE : ∀ x0 . SNo x0 ⟶ ∀ x1 : ο . (∀ x2 x3 . SNoCutP x2 x3 ⟶ (∀ x4 . x4 ∈ x2 ⟶ SNoLev x4 ∈ SNoLev x0) ⟶ (∀ x4 . x4 ∈ x3 ⟶ SNoLev x4 ∈ SNoLev x0) ⟶ x0 = SNoCut x2 x3 ⟶ x1) ⟶ x1 (proof)
Theorem SNo_ind^SNo_ind : ∀ x0 : ι → ο . (∀ x1 x2 . SNoCutP x1 x2 ⟶ (∀ x3 . x3 ∈ x1 ⟶ x0 x3) ⟶ (∀ x3 . x3 ∈ x2 ⟶ x0 x3) ⟶ x0 (SNoCut x1 x2)) ⟶ ∀ x1 . SNo x1 ⟶ x0 x1 (proof)