Proofgold Address

Known 1dd21..^{SetAdjoin_def} : SetAdjoin = λ x1 x2 . binunion x1 (Sing x2)
Known 0ce8c..^binunionI1 : ∀ x0 x1 x2 . In x2 x0 ⟶ In x2 (binunion x0 x1)
Theorem 84417..^SetAdjoinI1 : ∀ x0 x1 x2 . In x2 x0 ⟶ In x2 (SetAdjoin x0 x1) (proof)
Known eb8b4..^binunionI2 : ∀ x0 x1 x2 . In x2 x1 ⟶ In x2 (binunion x0 x1)
Known 1f15b..^SingI : ∀ x0 . In x0 (Sing x0)
Theorem 163d4..^SetAdjoinI2 : ∀ x0 x1 . In x1 (SetAdjoin x0 x1) (proof)
Known f9974..^{binunionE_cases} : ∀ x0 x1 x2 . In x2 (binunion x0 x1) ⟶ ∀ x3 : ο . (In x2 x0 ⟶ x3) ⟶ (In x2 x1 ⟶ x3) ⟶ x3
Known 9ae18..^SingE : ∀ x0 x1 . In x1 (Sing x0) ⟶ x1 = x0
Theorem 07300..^SetAdjoinE : ∀ x0 x1 x2 . In x2 (SetAdjoin x0 x1) ⟶ ∀ x3 : ο . (In x2 x0 ⟶ x3) ⟶ (x2 = x1 ⟶ x3) ⟶ x3 (proof)
Known 56b90..^PNoEq__def : PNoEq_ = λ x1 . λ x2 x3 : ι → ο . ∀ x4 . In x4 x1 ⟶ iff (x2 x4) (x3 x4)
Theorem e5ee4..^PNoEq__I : ∀ x0 . ∀ x1 x2 : ι → ο . (∀ x3 . In x3 x0 ⟶ iff (x1 x3) (x2 x3)) ⟶ PNoEq_ x0 x1 x2 (proof)
Theorem f5b7e..^PNoEq__E : ∀ x0 . ∀ x1 x2 : ι → ο . ∀ x3 : ο . ((∀ x4 . In x4 x0 ⟶ iff (x1 x4) (x2 x4)) ⟶ x3) ⟶ PNoEq_ x0 x1 x2 ⟶ x3 (proof)
Known aebc2..^PNoLt__def : PNoLt_ = λ x1 . λ x2 x3 : ι → ο . ∀ x4 : ο . (∀ x5 . and (In x5 x1) (and (and (PNoEq_ x5 x2 x3) (not (x2 x5))) (x3 x5)) ⟶ x4) ⟶ x4
Known 7c02f..^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known f6404..^and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Theorem e7258..^PNoLt__I : ∀ x0 x1 . In x0 x1 ⟶ ∀ x2 x3 : ι → ο . PNoEq_ x0 x2 x3 ⟶ not (x2 x0) ⟶ x3 x0 ⟶ PNoLt_ x1 x2 x3 (proof)
Known andE^andE : ∀ x0 x1 : ο . and x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Known cd094..^and3E : ∀ x0 x1 x2 : ο . and (and x0 x1) x2 ⟶ ∀ x3 : ο . (x0 ⟶ x1 ⟶ x2 ⟶ x3) ⟶ x3
Theorem 3e48a..^PNoLt__E : ∀ x0 . ∀ x1 x2 : ι → ο . ∀ x3 : ο . (∀ x4 . In x4 x0 ⟶ PNoEq_ x4 x1 x2 ⟶ not (x1 x4) ⟶ x2 x4 ⟶ x3) ⟶ PNoLt_ x0 x1 x2 ⟶ x3 (proof)
Known 8cb38..^or3E : ∀ x0 x1 x2 : ο . or (or x0 x1) x2 ⟶ ∀ x3 : ο . (x0 ⟶ x3) ⟶ (x1 ⟶ x3) ⟶ (x2 ⟶ x3) ⟶ x3
Known 7adfb..^{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)
Theorem ebdc6..^{PNoLt_trichotomy_or_impred} : ∀ x0 x1 . ∀ x2 x3 : ι → ο . ordinal x0 ⟶ ordinal x1 ⟶ ∀ x4 : ο . (PNoLt x0 x2 x1 x3 ⟶ x4) ⟶ (x0 = x1 ⟶ PNoEq_ x0 x2 x3 ⟶ x4) ⟶ (PNoLt x1 x3 x0 x2 ⟶ x4) ⟶ x4 (proof)
Known 22e4a..^{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 54baf..^{PNoLe_antisym_impred} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ ∀ x2 x3 : ι → ο . PNoLe x0 x2 x1 x3 ⟶ PNoLe x1 x3 x0 x2 ⟶ ∀ x4 : ο . (x0 = x1 ⟶ PNoEq_ x0 x2 x3 ⟶ x4) ⟶ x4 (proof)
Known 92a82..^{PNo_downc_def} : PNo_downc = λ x1 : ι → (ι → ο) → ο . λ x2 . λ x3 : ι → ο . ∀ x4 : ο . (∀ x5 . and (ordinal x5) (∀ x6 : ο . (∀ x7 : ι → ο . and (x1 x5 x7) (PNoLe x2 x3 x5 x7) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4
Theorem abb07..^PNo_downc_I : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 : ι → (ι → ο) → ο . ∀ x3 . ∀ x4 : ι → ο . ordinal x0 ⟶ x2 x0 x1 ⟶ PNoLe x3 x4 x0 x1 ⟶ PNo_downc x2 x3 x4 (proof)
Theorem 856d5..^PNo_downc_E : ∀ x0 : ι → (ι → ο) → ο . ∀ x1 . ∀ x2 : ι → ο . ∀ x3 : ο . (∀ x4 . ordinal x4 ⟶ ∀ x5 : ι → ο . x0 x4 x5 ⟶ PNoLe x1 x2 x4 x5 ⟶ x3) ⟶ PNo_downc x0 x1 x2 ⟶ x3 (proof)
Known e06f2..^PNo_upc_def : PNo_upc = λ x1 : ι → (ι → ο) → ο . λ x2 . λ x3 : ι → ο . ∀ x4 : ο . (∀ x5 . and (ordinal x5) (∀ x6 : ο . (∀ x7 : ι → ο . and (x1 x5 x7) (PNoLe x5 x7 x2 x3) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4
Theorem 09507..^PNo_upc_I : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 : ι → (ι → ο) → ο . ∀ x3 . ∀ x4 : ι → ο . ordinal x0 ⟶ x2 x0 x1 ⟶ PNoLe x0 x1 x3 x4 ⟶ PNo_upc x2 x3 x4 (proof)
Theorem 9ad5c..^PNo_upc_E : ∀ x0 : ι → (ι → ο) → ο . ∀ x1 . ∀ x2 : ι → ο . ∀ x3 : ο . (∀ x4 . ordinal x4 ⟶ ∀ x5 : ι → ο . x0 x4 x5 ⟶ PNoLe x4 x5 x1 x2 ⟶ x3) ⟶ PNo_upc x0 x1 x2 ⟶ x3 (proof)
Known ae672..^PNoLe_ref : ∀ x0 . ∀ x1 : ι → ο . PNoLe x0 x1 x0 x1
Theorem 2c3b7..^{PNo_downc_ref} : ∀ x0 : ι → (ι → ο) → ο . ∀ x1 . ordinal x1 ⟶ ∀ x2 : ι → ο . x0 x1 x2 ⟶ PNo_downc x0 x1 x2 (proof)
Theorem 2d1be..^PNo_upc_ref : ∀ x0 : ι → (ι → ο) → ο . ∀ x1 . ordinal x1 ⟶ ∀ x2 : ι → ο . x0 x1 x2 ⟶ PNo_upc x0 x1 x2 (proof)
Known e23c1..^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 371b3..^PNoLe_downc : ∀ x0 : ι → (ι → ο) → ο . ∀ x1 x2 . ∀ x3 x4 : ι → ο . ordinal x1 ⟶ ordinal x2 ⟶ PNo_downc x0 x1 x3 ⟶ PNoLe x2 x4 x1 x3 ⟶ PNo_downc x0 x2 x4 (proof)
Theorem 62abf..^PNoLe_upc : ∀ x0 : ι → (ι → ο) → ο . ∀ x1 x2 . ∀ x3 x4 : ι → ο . ordinal x1 ⟶ ordinal x2 ⟶ PNo_upc x0 x1 x3 ⟶ PNoLe x1 x3 x2 x4 ⟶ PNo_upc x0 x2 x4 (proof)
Definition 3f2f5..^PNoLt_pwise := λ x0 x1 : ι → (ι → ο) → ο . ∀ x2 . ordinal x2 ⟶ ∀ x3 : ι → ο . x0 x2 x3 ⟶ ∀ x4 . ordinal x4 ⟶ ∀ x5 : ι → ο . x1 x4 x5 ⟶ PNoLt x2 x3 x4 x5
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Known 289e1..^{PNoLt_irref_b} : ∀ x0 . ∀ x1 : ι → ο . PNoLt x0 x1 x0 x1 ⟶ False
Known a6669..^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
Known 3c4f3..^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
Known 13ed3..^PNoLeI2 : ∀ x0 . ∀ x1 x2 : ι → ο . PNoEq_ x0 x1 x2 ⟶ PNoLe x0 x1 x0 x2
Known d0c10..^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 aaa5d..^{PNoLt_pwise_downc_upc} : ∀ x0 x1 : ι → (ι → ο) → ο . 3f2f5.. x0 x1 ⟶ 3f2f5.. (PNo_downc x0) (PNo_upc x1) (proof)
Known notE^notE : ∀ x0 : ο . not x0 ⟶ x0 ⟶ False
Known e3ec9..^neq_0_1 : not (0 = 1)
Known 6e976..^TransSetEb : ∀ x0 . TransSet x0 ⟶ ∀ x1 . In x1 x0 ⟶ ∀ x2 . In x2 x1 ⟶ In x2 x0
Known 0978b..^In_0_1 : In 0 1
Theorem a1968..^{not_TransSet_Sing1} : TransSet (Sing 1) ⟶ False (proof)
Known 339db..^{ordinal_TransSet} : ∀ x0 . ordinal x0 ⟶ TransSet x0
Theorem 01d96..^{not_ordinal_Sing1} : ordinal (Sing 1) ⟶ False (proof)
Known 14977..^{ordinal_Hered} : ∀ x0 . ordinal x0 ⟶ ∀ x1 . In x1 x0 ⟶ ordinal x1
Theorem 29576..^{tagged_not_ordinal} : ∀ x0 . ordinal (SetAdjoin x0 (Sing 1)) ⟶ False (proof)
Theorem 9f8b9..^{tagged_notin_ordinal} : ∀ x0 x1 . ordinal x0 ⟶ In (SetAdjoin x1 (Sing 1)) x0 ⟶ False (proof)
Known b0dce..^SubqI : ∀ x0 x1 . (∀ x2 . In x2 x0 ⟶ In x2 x1) ⟶ Subq x0 x1
Theorem 4c588..^{tagged_eqE_Subq} : ∀ x0 x1 . ordinal x0 ⟶ SetAdjoin x0 (Sing 1) = SetAdjoin x1 (Sing 1) ⟶ Subq x0 x1 (proof)
Known b3824..^set_ext : ∀ x0 x1 . Subq x0 x1 ⟶ Subq x1 x0 ⟶ x0 = x1
Theorem c908d..^{tagged_eqE_eq} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ SetAdjoin x0 (Sing 1) = SetAdjoin x1 (Sing 1) ⟶ x0 = x1 (proof)
Known 0f096..^ReplE2 : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 (Repl x0 x1) ⟶ ∀ x3 : ο . (∀ x4 . In x4 x0 ⟶ x2 = x1 x4 ⟶ x3) ⟶ x3
Theorem a9755..^tagged_ReplE : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ In (SetAdjoin x1 (Sing 1)) (Repl x0 (λ x2 . SetAdjoin x2 (Sing 1))) ⟶ In x1 x0 (proof)
Theorem e995a..^{ordinal_notin_tagged_Repl} : ∀ x0 x1 . ordinal x0 ⟶ In x0 (Repl x1 (λ x2 . SetAdjoin x2 (Sing 1))) ⟶ False (proof)
Known e46d9..^SNoElts__def : SNoElts_ = λ x1 . binunion x1 (Repl x1 (λ x2 . SetAdjoin x2 (Sing 1)))
Theorem 92d43..^SNoElts__I1 : ∀ x0 x1 . In x1 x0 ⟶ In x1 (SNoElts_ x0) (proof)
Known f1bf4..^ReplI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 x0 ⟶ In (x1 x2) (Repl x0 x1)
Theorem dbfee..^SNoElts__I2 : ∀ x0 x1 . In x1 x0 ⟶ In (SetAdjoin x1 (Sing 1)) (SNoElts_ x0) (proof)
Theorem eb8f8..^SNoElts__E : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . In x2 x0 ⟶ x1 x2) ⟶ (∀ x2 . In x2 x0 ⟶ x1 (SetAdjoin x2 (Sing 1))) ⟶ ∀ x2 . In x2 (SNoElts_ x0) ⟶ x1 x2 (proof)
Known 367e6..^SubqE : ∀ x0 x1 . Subq x0 x1 ⟶ ∀ x2 . In x2 x0 ⟶ In x2 x1
Theorem aabcd..^SNoElts_mon : ∀ x0 x1 . Subq x0 x1 ⟶ Subq (SNoElts_ x0) (SNoElts_ x1) (proof)
Known 55472..^SNo__def : SNo_ = λ x1 x2 . and (Subq x2 (SNoElts_ x1)) (∀ x3 . In x3 x1 ⟶ exactly1of2 (In (SetAdjoin x3 (Sing 1)) x2) (In x3 x2))
Theorem 4abfb..^SNo__I : ∀ x0 x1 . Subq x1 (SNoElts_ x0) ⟶ (∀ x2 . In x2 x0 ⟶ exactly1of2 (In (SetAdjoin x2 (Sing 1)) x1) (In x2 x1)) ⟶ SNo_ x0 x1 (proof)
Theorem 7b10a..^SNo__E : ∀ x0 x1 . ∀ x2 : ο . (Subq x1 (SNoElts_ x0) ⟶ (∀ x3 . In x3 x0 ⟶ exactly1of2 (In (SetAdjoin x3 (Sing 1)) x1) (In x3 x1)) ⟶ x2) ⟶ SNo_ x0 x1 ⟶ x2 (proof)
Known 8856d..^PSNo_def : PSNo = λ x1 . λ x2 : ι → ο . binunion (Sep x1 x2) (ReplSep x1 (λ x3 . not (x2 x3)) (λ x3 . SetAdjoin x3 (Sing 1)))
Known dab1f..^SepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . In x2 x0 ⟶ x1 x2 ⟶ In x2 (Sep x0 x1)
Theorem 919d0..^PSNo_I1 : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . In x2 x0 ⟶ x1 x2 ⟶ In x2 (PSNo x0 x1) (proof)
Known 9fdc4..^ReplSepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 : ι → ι . ∀ x3 . In x3 x0 ⟶ x1 x3 ⟶ In (x2 x3) (ReplSep x0 x1 x2)
Theorem e6dfe..^PSNo_I2 : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . In x2 x0 ⟶ not (x1 x2) ⟶ In (SetAdjoin x2 (Sing 1)) (PSNo x0 x1) (proof)
Known aa3f4..^SepE_impred : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . In x2 (Sep x0 x1) ⟶ ∀ x3 : ο . (In x2 x0 ⟶ x1 x2 ⟶ x3) ⟶ x3
Known 65d0d..^{ReplSepE_impred} : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 : ι → ι . ∀ x3 . In x3 (ReplSep x0 x1 x2) ⟶ ∀ x4 : ο . (∀ x5 . In x5 x0 ⟶ x1 x5 ⟶ x3 = x2 x5 ⟶ x4) ⟶ x4
Theorem 9e1f7..^PSNo_E : ∀ x0 . ∀ x1 x2 : ι → ο . (∀ x3 . In x3 x0 ⟶ x1 x3 ⟶ x2 x3) ⟶ (∀ x3 . In x3 x0 ⟶ not (x1 x3) ⟶ x2 (SetAdjoin x3 (Sing 1))) ⟶ ∀ x3 . In x3 (PSNo x0 x1) ⟶ x2 x3 (proof)
Known 32c82..^iffI : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ iff x0 x1
Theorem 2fcd7..^PNoEq_PSNo : ∀ x0 . ordinal x0 ⟶ ∀ x1 : ι → ο . PNoEq_ x0 (λ x2 . In x2 (PSNo x0 x1)) x1 (proof)
Known 47706..^xmcases : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (not x0 ⟶ x1) ⟶ x1
Known e4955..^{exactly1of2_I2} : ∀ x0 x1 : ο . not x0 ⟶ x1 ⟶ exactly1of2 x0 x1
Known 8106d..^notI : ∀ x0 : ο . (x0 ⟶ False) ⟶ not x0
Known c603f..^{exactly1of2_I1} : ∀ x0 x1 : ο . x0 ⟶ not x1 ⟶ exactly1of2 x0 x1
Theorem ccc82..^SNo_PSNo : ∀ x0 . ordinal x0 ⟶ ∀ x1 : ι → ο . SNo_ x0 (PSNo x0 x1) (proof)
Known 535f2..^set_ext_2 : ∀ x0 x1 . (∀ x2 . In x2 x0 ⟶ In x2 x1) ⟶ (∀ x2 . In x2 x1 ⟶ In x2 x0) ⟶ x0 = x1
Known 9001d..^{exactly1of2_E} : ∀ x0 x1 : ο . exactly1of2 x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ not x1 ⟶ x2) ⟶ (not x0 ⟶ x1 ⟶ x2) ⟶ x2
Theorem bffec..^{SNo_PSNo_eta_} : ∀ x0 x1 . ordinal x0 ⟶ SNo_ x0 x1 ⟶ x1 = PSNo x0 (λ x3 . In x3 x1) (proof)
Known 450e1..^SNo_def : SNo = λ x1 . ∀ x2 : ο . (∀ x3 . and (ordinal x3) (SNo_ x3 x1) ⟶ x2) ⟶ x2
Theorem f8a9f..^SNo_I : ∀ x0 . ordinal x0 ⟶ ∀ x1 . SNo_ x0 x1 ⟶ SNo x1 (proof)
Theorem ba9d6..^SNo_E : ∀ x0 . SNo x0 ⟶ ∀ x1 : ο . (∀ x2 . ordinal x2 ⟶ SNo_ x2 x0 ⟶ x1) ⟶ x1 (proof)
Theorem 21c1b..^{SNoLev_uniq_Subq} : ∀ x0 x1 x2 . ordinal x1 ⟶ ordinal x2 ⟶ SNo_ x1 x0 ⟶ SNo_ x2 x0 ⟶ Subq x1 x2 (proof)
Theorem da796..^SNoLev_uniq : ∀ x0 x1 x2 . ordinal x1 ⟶ ordinal x2 ⟶ SNo_ x1 x0 ⟶ SNo_ x2 x0 ⟶ x1 = x2 (proof)
Known 06156..^SNoLev_def : SNoLev = λ x1 . Eps_i (λ x2 . and (ordinal x2) (SNo_ x2 x1))
Known 4cb75..^Eps_i_R : ∀ x0 : ι → ο . ∀ x1 . x0 x1 ⟶ x0 (Eps_i x0)
Theorem defb9..^SNoLev_prop : ∀ x0 . SNo x0 ⟶ and (ordinal (SNoLev x0)) (SNo_ (SNoLev x0) x0) (proof)
Theorem d259b..^{SNoLev_prop_impred} : ∀ x0 . SNo x0 ⟶ ∀ x1 : ο . (ordinal (SNoLev x0) ⟶ SNo_ (SNoLev x0) x0 ⟶ x1) ⟶ x1 (proof)
Theorem e3541..^{SNoLev_ordinal} : ∀ x0 . SNo x0 ⟶ ordinal (SNoLev x0) (proof)
Theorem 93516..^SNoLev_ : ∀ x0 . SNo x0 ⟶ SNo_ (SNoLev x0) x0 (proof)
Theorem a923b..^SNo_PSNo_eta : ∀ x0 . SNo x0 ⟶ x0 = PSNo (SNoLev x0) (λ x2 . In x2 x0) (proof)
Theorem 7e47a..^SNoLev_PSNo : ∀ x0 . ordinal x0 ⟶ ∀ x1 : ι → ο . SNoLev (PSNo x0 x1) = x0 (proof)
Known 50594..^iffEL : ∀ x0 x1 : ο . iff x0 x1 ⟶ x0 ⟶ x1
Known 93720..^iffER : ∀ x0 x1 : ο . iff x0 x1 ⟶ x1 ⟶ x0
Theorem 4e72d..^SNo_Subq : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ Subq (SNoLev x0) (SNoLev x1) ⟶ (∀ x2 . In x2 (SNoLev x0) ⟶ iff (In x2 x0) (In x2 x1)) ⟶ Subq x0 x1 (proof)
Known ebfb4..^SNoEq__def : SNoEq_ = λ x1 x2 x3 . PNoEq_ x1 (λ x4 . In x4 x2) (λ x4 . In x4 x3)
Theorem fcab6..^SNoEq_I : ∀ x0 x1 x2 . PNoEq_ x0 (λ x3 . In x3 x1) (λ x3 . In x3 x2) ⟶ SNoEq_ x0 x1 x2 (proof)
Theorem f2976..^SNoEq_E : ∀ x0 x1 x2 . SNoEq_ x0 x1 x2 ⟶ PNoEq_ x0 (λ x3 . In x3 x1) (λ x3 . In x3 x2) (proof)
Theorem 42e4e..^SNoEq_E : ∀ x0 x1 x2 . ∀ x3 : ο . (PNoEq_ x0 (λ x4 . In x4 x1) (λ x4 . In x4 x2) ⟶ x3) ⟶ SNoEq_ x0 x1 x2 ⟶ x3 (proof)
Theorem 98d3d..^SNoEq_E1 : ∀ x0 x1 x2 . SNoEq_ x0 x1 x2 ⟶ ∀ x3 . In x3 x0 ⟶ In x3 x1 ⟶ In x3 x2 (proof)
Theorem d996f..^SNoEq_E2 : ∀ x0 x1 x2 . SNoEq_ x0 x1 x2 ⟶ ∀ x3 . In x3 x0 ⟶ In x3 x2 ⟶ In x3 x1 (proof)
Known d26f4..^{PNoEq_antimon_} : ∀ x0 x1 : ι → ο . ∀ x2 . ordinal x2 ⟶ ∀ x3 . In x3 x2 ⟶ PNoEq_ x2 x0 x1 ⟶ PNoEq_ x3 x0 x1
Theorem d1804..^{SNoEq_antimon_} : ∀ x0 . ordinal x0 ⟶ ∀ x1 . In x1 x0 ⟶ ∀ x2 x3 . SNoEq_ x0 x2 x3 ⟶ SNoEq_ x1 x2 x3 (proof)
Known 6696a..^Subq_ref : ∀ x0 . Subq x0 x0
Known 3d208..^iff_sym : ∀ x0 x1 : ο . iff x0 x1 ⟶ iff x1 x0
Theorem 443ed..^SNo_eq : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ SNoLev x0 = SNoLev x1 ⟶ SNoEq_ (SNoLev x0) x0 x1 ⟶ x0 = x1 (proof)
Known 3e1b8..^SNoLt_def : SNoLt = λ x1 x2 . PNoLt (SNoLev x1) (λ x3 . In x3 x1) (SNoLev x2) (λ x3 . In x3 x2)
Theorem 3014e..^SNoLtI : ∀ x0 x1 . PNoLt (SNoLev x0) (λ x2 . In x2 x0) (SNoLev x1) (λ x2 . In x2 x1) ⟶ SNoLt x0 x1 (proof)
Theorem d2f9b..^SNoLtE : ∀ x0 x1 . SNoLt x0 x1 ⟶ PNoLt (SNoLev x0) (λ x2 . In x2 x0) (SNoLev x1) (λ x2 . In x2 x1) (proof)
Theorem 4b3ee..^SNoLtE : ∀ x0 x1 . ∀ x2 : ο . (PNoLt (SNoLev x0) (λ x3 . In x3 x0) (SNoLev x1) (λ x3 . In x3 x1) ⟶ x2) ⟶ SNoLt x0 x1 ⟶ x2 (proof)
Known 375e0..^SNoLe_def : SNoLe = λ x1 x2 . PNoLe (SNoLev x1) (λ x3 . In x3 x1) (SNoLev x2) (λ x3 . In x3 x2)
Theorem 3983e..^SNoLeI : ∀ x0 x1 . PNoLe (SNoLev x0) (λ x2 . In x2 x0) (SNoLev x1) (λ x2 . In x2 x1) ⟶ SNoLe x0 x1 (proof)
Theorem 359b8..^SNoLeE : ∀ x0 x1 . SNoLe x0 x1 ⟶ PNoLe (SNoLev x0) (λ x2 . In x2 x0) (SNoLev x1) (λ x2 . In x2 x1) (proof)
Theorem 14de9..^SNoLeE : ∀ x0 x1 . ∀ x2 : ο . (PNoLe (SNoLev x0) (λ x3 . In x3 x0) (SNoLev x1) (λ x3 . In x3 x1) ⟶ x2) ⟶ SNoLe x0 x1 ⟶ x2 (proof)
Known 478b3..^PNoLeI1 : ∀ x0 x1 . ∀ x2 x3 : ι → ο . PNoLt x0 x2 x1 x3 ⟶ PNoLe x0 x2 x1 x3
Theorem 904b5..^SNoLtLe : ∀ x0 x1 . SNoLt x0 x1 ⟶ SNoLe x0 x1 (proof)
Known 806be..^PNoLeE : ∀ x0 x1 . ∀ x2 x3 : ι → ο . PNoLe x0 x2 x1 x3 ⟶ ∀ x4 : ο . (PNoLt x0 x2 x1 x3 ⟶ x4) ⟶ (x0 = x1 ⟶ PNoEq_ x0 x2 x3 ⟶ x4) ⟶ x4
Known dcbd9..^orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Known eca40..^orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Theorem 28d43..^SNoLeE_or : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ SNoLe x0 x1 ⟶ or (SNoLt x0 x1) (x0 = x1) (proof)
Known 5d346..^PNoEq_ref_ : ∀ x0 . ∀ x1 : ι → ο . PNoEq_ x0 x1 x1
Theorem 5193e..^SNoEq_ref_ : ∀ x0 x1 . SNoEq_ x0 x1 x1 (proof)
Known b96d4..^PNoEq_sym_ : ∀ x0 . ∀ x1 x2 : ι → ο . PNoEq_ x0 x1 x2 ⟶ PNoEq_ x0 x2 x1
Theorem 125cd..^SNoEq_sym_ : ∀ x0 x1 x2 . SNoEq_ x0 x1 x2 ⟶ SNoEq_ x0 x2 x1 (proof)
Known f3029..^PNoEq_tra_ : ∀ x0 . ∀ x1 x2 x3 : ι → ο . PNoEq_ x0 x1 x2 ⟶ PNoEq_ x0 x2 x3 ⟶ PNoEq_ x0 x1 x3
Theorem fa016..^SNoEq_tra_ : ∀ x0 x1 x2 x3 . SNoEq_ x0 x1 x2 ⟶ SNoEq_ x0 x2 x3 ⟶ SNoEq_ x0 x1 x3 (proof)
Known e0ec6..^PNoLtE : ∀ x0 x1 . ∀ x2 x3 : ι → ο . PNoLt x0 x2 x1 x3 ⟶ ∀ x4 : ο . (PNoLt_ (binintersect x0 x1) x2 x3 ⟶ x4) ⟶ (In x0 x1 ⟶ PNoEq_ x0 x2 x3 ⟶ x3 x0 ⟶ x4) ⟶ (In x1 x0 ⟶ PNoEq_ x1 x2 x3 ⟶ not (x2 x1) ⟶ x4) ⟶ x4
Known 44198..^PNoLt_E_ : ∀ x0 . ∀ x1 x2 : ι → ο . PNoLt_ x0 x1 x2 ⟶ ∀ x3 : ο . (∀ x4 . In x4 x0 ⟶ PNoEq_ x4 x1 x2 ⟶ not (x1 x4) ⟶ x2 x4 ⟶ x3) ⟶ x3
Known 9c451..^{binintersectE_impred} : ∀ x0 x1 x2 . In x2 (binintersect x0 x1) ⟶ ∀ x3 : ο . (In x2 x0 ⟶ In x2 x1 ⟶ x3) ⟶ x3
Known ae95b..^PNoLtI3 : ∀ x0 x1 . ∀ x2 x3 : ι → ο . In x1 x0 ⟶ PNoEq_ x1 x2 x3 ⟶ not (x2 x1) ⟶ PNoLt x0 x2 x1 x3
Known 67fa1..^PNoLtI2 : ∀ x0 x1 . ∀ x2 x3 : ι → ο . In x0 x1 ⟶ PNoEq_ x0 x2 x3 ⟶ x3 x0 ⟶ PNoLt x0 x2 x1 x3
Known 6abef..^nIn_I : ∀ x0 x1 . not (In x0 x1) ⟶ nIn x0 x1
Theorem e884b..^SNoLtE3 : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ SNoLt x0 x1 ⟶ ∀ x2 : ο . (∀ x3 . SNo x3 ⟶ In (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 ⟶ In (SNoLev x3) x1 ⟶ x2) ⟶ (In (SNoLev x0) (SNoLev x1) ⟶ SNoEq_ (SNoLev x0) x0 x1 ⟶ In (SNoLev x0) x1 ⟶ x2) ⟶ (In (SNoLev x1) (SNoLev x0) ⟶ SNoEq_ (SNoLev x1) x0 x1 ⟶ nIn (SNoLev x1) x0 ⟶ x2) ⟶ x2 (proof)
Theorem ac8dd..^SNoLtI2 : ∀ x0 x1 . In (SNoLev x0) (SNoLev x1) ⟶ SNoEq_ (SNoLev x0) x0 x1 ⟶ In (SNoLev x0) x1 ⟶ SNoLt x0 x1 (proof)
Known f0129..^nIn_E : ∀ x0 x1 . nIn x0 x1 ⟶ not (In x0 x1)
Theorem 94072..^SNoLtI3 : ∀ x0 x1 . In (SNoLev x1) (SNoLev x0) ⟶ SNoEq_ (SNoLev x1) x0 x1 ⟶ nIn (SNoLev x1) x0 ⟶ SNoLt x0 x1 (proof)
Known 96df0..^PNoLt_irref : ∀ x0 . ∀ x1 : ι → ο . not (PNoLt x0 x1 x0 x1)
Theorem 3de72..^SNoLt_irref : ∀ x0 . not (SNoLt x0 x0) (proof)
Known cb243..^or3I1 : ∀ x0 x1 x2 : ο . x0 ⟶ or (or x0 x1) x2
Known 8aff3..^or3I2 : ∀ x0 x1 x2 : ο . x1 ⟶ or (or x0 x1) x2
Known a4277..^or3I3 : ∀ x0 x1 x2 : ο . x2 ⟶ or (or x0 x1) x2
Theorem 38ea3..^{SNoLt_trichotomy_or} : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ or (or (SNoLt x0 x1) (x0 = x1)) (SNoLt x1 x0) (proof)
Theorem 12d25..^{SNoLt_trichotomy_or_impred} : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ ∀ x2 : ο . (SNoLt x0 x1 ⟶ x2) ⟶ (x0 = x1 ⟶ x2) ⟶ (SNoLt x1 x0 ⟶ x2) ⟶ x2 (proof)
Theorem b2f09..^SNoLt_tra : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNoLt x0 x1 ⟶ SNoLt x1 x2 ⟶ SNoLt x0 x2 (proof)
Theorem c44b9..^SNoLe_ref : ∀ x0 . SNoLe x0 x0 (proof)
Theorem 11181..^{SNoLe_antisym} : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ SNoLe x0 x1 ⟶ SNoLe x1 x0 ⟶ x0 = x1 (proof)
Theorem 49ec6..^SNoLtLe_tra : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNoLt x0 x1 ⟶ SNoLe x1 x2 ⟶ SNoLt x0 x2 (proof)
Theorem 33812..^SNoLeLt_tra : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNoLe x0 x1 ⟶ SNoLt x1 x2 ⟶ SNoLt x0 x2 (proof)
Theorem 64763..^SNoLe_tra : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNoLe x0 x1 ⟶ SNoLe x1 x2 ⟶ SNoLe x0 x2 (proof)
Theorem 541dd..^SNoLtLe_or : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ or (SNoLt x0 x1) (SNoLe x1 x0) (proof)
Known 37124..^orE : ∀ x0 x1 : ο . or x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Theorem c54bb..^{SNoLtLe_or_impred} : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ ∀ x2 : ο . (SNoLt x0 x1 ⟶ x2) ⟶ (SNoLe x1 x0 ⟶ x2) ⟶ x2 (proof)
Known 492f5..^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 76102..^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 e0163..^{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 a46f6..^{PNoLt_SNoLt_PSNo} : ∀ x0 x1 . ∀ x2 x3 : ι → ο . ordinal x0 ⟶ ordinal x1 ⟶ PNoLt x0 x2 x1 x3 ⟶ SNoLt (PSNo x0 x2) (PSNo x1 x3) (proof)