Search for blocks/addresses/...

Proofgold Address

address
PUQ2YRkcBuqCZtcGAK5rxfxVmX5Dg8Z1wms
total
0
mg
-
conjpub
-
current assets
6e441../2da37.. bday: 4903 doc published by Pr6Pc..
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Definition iffiff := λ x0 x1 : ο . and (x0x1) (x1x0)
Known andIandI : ∀ x0 x1 : ο . x0x1and x0 x1
Known iff_refliff_refl : ∀ x0 : ο . iff x0 x0
Known iffIiffI : ∀ x0 x1 : ο . (x0x1)(x1x0)iff x0 x1
Theorem iff_symiff_sym : ∀ x0 x1 : ο . iff x0 x1iff x1 x0 (proof)
Theorem iff_transiff_trans : ∀ x0 x1 x2 : ο . iff x0 x1iff x1 x2iff x0 x2 (proof)
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Definition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)x2
Known orILorIL : ∀ x0 x1 : ο . x0or x0 x1
Known orIRorIR : ∀ x0 x1 : ο . x1or x0 x1
Theorem not_or_and_demorgannot_or_and_demorgan : ∀ x0 x1 : ο . not (or x0 x1)and (not x0) (not x1) (proof)
Theorem and_not_or_demorganand_not_or_demorgan : ∀ x0 x1 : ο . and (not x0) (not x1)not (or x0 x1) (proof)
Theorem not_ex_all_demorgan_inot_ex_all_demorgan_i : ∀ x0 : ι → ο . not (∀ x1 : ο . (∀ x2 . x0 x2x1)x1)∀ x1 . not (x0 x1) (proof)
Known dnegdneg : ∀ x0 : ο . not (not x0)x0
Theorem not_all_ex_demorgan_inot_all_ex_demorgan_i : ∀ x0 : ι → ο . not (∀ x1 . x0 x1)∀ x1 : ο . (∀ x2 . not (x0 x2)x1)x1 (proof)
Known prop_ext_2prop_ext_2 : ∀ x0 x1 : ο . (x0x1)(x1x0)x0 = x1
Known xmxm : ∀ x0 : ο . or x0 (not x0)
Theorem eq_or_nandeq_or_nand : or = λ x1 x2 : ο . not (and (not x1) (not x2)) (proof)
Definition EpsR_i_i_1EpsR_i_i_1 := λ x0 : ι → ι → ο . prim0 (λ x1 . ∀ x2 : ο . (∀ x3 . x0 x1 x3x2)x2)
Definition EpsR_i_i_2EpsR_i_i_2 := λ x0 : ι → ι → ο . prim0 (x0 (EpsR_i_i_1 x0))
Known Eps_i_exEps_i_ex : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . x0 x2x1)x1)x0 (prim0 x0)
Theorem EpsR_i_i_12EpsR_i_i_12 : ∀ x0 : ι → ι → ο . (∀ x1 : ο . (∀ x2 . (∀ x3 : ο . (∀ x4 . x0 x2 x4x3)x3)x1)x1)x0 (EpsR_i_i_1 x0) (EpsR_i_i_2 x0) (proof)
Definition DescrR_i_io_1DescrR_i_io_1 := λ x0 : ι → (ι → ο) → ο . prim0 (λ x1 . and (∀ x2 : ο . (∀ x3 : ι → ο . x0 x1 x3x2)x2) (∀ x2 x3 : ι → ο . x0 x1 x2x0 x1 x3x2 = x3))
Param Descr_Vo1Descr_Vo1 : ((ιο) → ο) → ιο
Definition DescrR_i_io_2DescrR_i_io_2 := λ x0 : ι → (ι → ο) → ο . Descr_Vo1 (x0 (DescrR_i_io_1 x0))
Known Descr_Vo1_propDescr_Vo1_prop : ∀ x0 : (ι → ο) → ο . (∀ x1 : ο . (∀ x2 : ι → ο . x0 x2x1)x1)(∀ x1 x2 : ι → ο . x0 x1x0 x2x1 = x2)x0 (Descr_Vo1 x0)
Theorem DescrR_i_io_12DescrR_i_io_12 : ∀ x0 : ι → (ι → ο) → ο . (∀ x1 : ο . (∀ x2 . and (∀ x3 : ο . (∀ x4 : ι → ο . x0 x2 x4x3)x3) (∀ x3 x4 : ι → ο . x0 x2 x3x0 x2 x4x3 = x4)x1)x1)x0 (DescrR_i_io_1 x0) (DescrR_i_io_2 x0) (proof)
Definition PNoEq_PNoEq_ := λ x0 . λ x1 x2 : ι → ο . ∀ x3 . x3x0iff (x1 x3) (x2 x3)
Theorem PNoEq_ref_PNoEq_ref_ : ∀ x0 . ∀ x1 : ι → ο . PNoEq_ x0 x1 x1 (proof)
Theorem PNoEq_sym_PNoEq_sym_ : ∀ x0 . ∀ x1 x2 : ι → ο . PNoEq_ x0 x1 x2PNoEq_ x0 x2 x1 (proof)
Theorem PNoEq_tra_PNoEq_tra_ : ∀ x0 . ∀ x1 x2 x3 : ι → ο . PNoEq_ x0 x1 x2PNoEq_ x0 x2 x3PNoEq_ x0 x1 x3 (proof)
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Definition TransSetTransSet := λ x0 . ∀ x1 . x1x0x1x0
Definition ordinalordinal := λ x0 . and (TransSet x0) (∀ x1 . x1x0TransSet x1)
Theorem PNoEq_antimon_PNoEq_antimon_ : ∀ x0 x1 : ι → ο . ∀ x2 . ordinal x2∀ x3 . x3x2PNoEq_ x2 x0 x1PNoEq_ x3 x0 x1 (proof)
Definition PNoLt_PNoLt_ := λ x0 . λ x1 x2 : ι → ο . ∀ x3 : ο . (∀ x4 . and (x4x0) (and (and (PNoEq_ x4 x1 x2) (not (x1 x4))) (x2 x4))x3)x3
Theorem PNoLt_E_PNoLt_E_ : ∀ x0 . ∀ x1 x2 : ι → ο . PNoLt_ x0 x1 x2∀ x3 : ο . (∀ x4 . x4x0PNoEq_ x4 x1 x2not (x1 x4)x2 x4x3)x3 (proof)
Theorem PNoLt_irref_PNoLt_irref_ : ∀ x0 . ∀ x1 : ι → ο . not (PNoLt_ x0 x1 x1) (proof)
Theorem PNoLt_mon_PNoLt_mon_ : ∀ x0 x1 : ι → ο . ∀ x2 . ordinal x2∀ x3 . x3x2PNoLt_ x3 x0 x1PNoLt_ x2 x0 x1 (proof)
Known ordinal_indordinal_ind : ∀ x0 : ι → ο . (∀ x1 . ordinal x1(∀ x2 . x2x1x0 x2)x0 x1)∀ x1 . ordinal x1x0 x1
Known FalseEFalseE : False∀ x0 : ο . x0
Known and3Iand3I : ∀ x0 x1 x2 : ο . x0x1x2and (and x0 x1) x2
Definition nInnIn := λ x0 x1 . not (x0x1)
Theorem PNoLt_trichotomy_or_PNoLt_trichotomy_or_ : ∀ x0 x1 : ι → ο . ∀ x2 . ordinal x2or (or (PNoLt_ x2 x0 x1) (PNoEq_ x2 x0 x1)) (PNoLt_ x2 x1 x0) (proof)
Known ordinal_trichotomy_orordinal_trichotomy_or : ∀ x0 x1 . ordinal x0ordinal x1or (or (x0x1) (x0 = x1)) (x1x0)
Known ordinal_Heredordinal_Hered : ∀ x0 . ordinal x0∀ x1 . x1x0ordinal x1
Theorem PNoLt_tra_PNoLt_tra_ : ∀ x0 . ordinal x0∀ x1 x2 x3 : ι → ο . PNoLt_ x0 x1 x2PNoLt_ x0 x2 x3PNoLt_ x0 x1 x3 (proof)
Param binintersectbinintersect : ιιι
Definition PNoLtPNoLt := λ x0 . λ x1 : ι → ο . λ x2 . λ x3 : ι → ο . or (or (PNoLt_ (binintersect x0 x2) x1 x3) (and (and (x0x2) (PNoEq_ x0 x1 x3)) (x3 x0))) (and (and (x2x0) (PNoEq_ x2 x1 x3)) (not (x1 x2)))
Known or3I1or3I1 : ∀ x0 x1 x2 : ο . x0or (or x0 x1) x2
Theorem PNoLtI1PNoLtI1 : ∀ x0 x1 . ∀ x2 x3 : ι → ο . PNoLt_ (binintersect x0 x1) x2 x3PNoLt x0 x2 x1 x3 (proof)
Known or3I2or3I2 : ∀ x0 x1 x2 : ο . x1or (or x0 x1) x2
Theorem PNoLtI2PNoLtI2 : ∀ x0 x1 . ∀ x2 x3 : ι → ο . x0x1PNoEq_ x0 x2 x3x3 x0PNoLt x0 x2 x1 x3 (proof)
Known or3I3or3I3 : ∀ x0 x1 x2 : ο . x2or (or x0 x1) x2
Theorem PNoLtI3PNoLtI3 : ∀ x0 x1 . ∀ x2 x3 : ι → ο . x1x0PNoEq_ x1 x2 x3not (x2 x1)PNoLt x0 x2 x1 x3 (proof)
Theorem PNoLtEPNoLtE : ∀ x0 x1 . ∀ x2 x3 : ι → ο . PNoLt x0 x2 x1 x3∀ x4 : ο . (PNoLt_ (binintersect x0 x1) x2 x3x4)(x0x1PNoEq_ x0 x2 x3x3 x0x4)(x1x0PNoEq_ x1 x2 x3not (x2 x1)x4)x4 (proof)
Known binintersect_idembinintersect_idem : ∀ x0 . binintersect x0 x0 = x0
Known In_irrefIn_irref : ∀ x0 . nIn x0 x0
Theorem PNoLtE2PNoLtE2 : ∀ x0 . ∀ x1 x2 : ι → ο . PNoLt x0 x1 x0 x2PNoLt_ x0 x1 x2 (proof)
Theorem PNoLt_irrefPNoLt_irref : ∀ x0 . ∀ x1 : ι → ο . not (PNoLt x0 x1 x0 x1) (proof)
Known binintersect_Subq_eq_1binintersect_Subq_eq_1 : ∀ x0 x1 . x0x1binintersect x0 x1 = x0
Known Subq_refSubq_ref : ∀ x0 . x0x0
Known binintersect_combinintersect_com : ∀ x0 x1 . binintersect x0 x1 = binintersect x1 x0
Known ordinal_binintersectordinal_binintersect : ∀ x0 x1 . ordinal x0ordinal x1ordinal (binintersect x0 x1)
Theorem PNoLt_trichotomy_orPNoLt_trichotomy_or : ∀ x0 x1 . ∀ x2 x3 : ι → ο . ordinal x0ordinal x1or (or (PNoLt x0 x2 x1 x3) (and (x0 = x1) (PNoEq_ x0 x2 x3))) (PNoLt x1 x3 x0 x2) (proof)
Known binintersectEbinintersectE : ∀ x0 x1 x2 . x2binintersect x0 x1and (x2x0) (x2x1)
Known iffELiffEL : ∀ x0 x1 : ο . iff x0 x1x0x1
Theorem PNoLtEq_traPNoLtEq_tra : ∀ x0 x1 . ordinal x0ordinal x1∀ x2 x3 x4 : ι → ο . PNoLt x0 x2 x1 x3PNoEq_ x1 x3 x4PNoLt x0 x2 x1 x4 (proof)
Theorem PNoEqLt_traPNoEqLt_tra : ∀ x0 x1 . ordinal x0ordinal x1∀ x2 x3 x4 : ι → ο . PNoEq_ x0 x2 x3PNoLt x0 x3 x1 x4PNoLt x0 x2 x1 x4 (proof)
Known binintersectIbinintersectI : ∀ x0 x1 x2 . x2x0x2x1x2binintersect x0 x1
Theorem PNoLt_traPNoLt_tra : ∀ x0 x1 x2 . ordinal x0ordinal x1ordinal x2∀ x3 x4 x5 : ι → ο . PNoLt x0 x3 x1 x4PNoLt x1 x4 x2 x5PNoLt x0 x3 x2 x5 (proof)
Definition PNoLePNoLe := λ x0 . λ x1 : ι → ο . λ x2 . λ x3 : ι → ο . or (PNoLt x0 x1 x2 x3) (and (x0 = x2) (PNoEq_ x0 x1 x3))
Theorem PNoLeI1PNoLeI1 : ∀ x0 x1 . ∀ x2 x3 : ι → ο . PNoLt x0 x2 x1 x3PNoLe x0 x2 x1 x3 (proof)
Theorem PNoLeI2PNoLeI2 : ∀ x0 . ∀ x1 x2 : ι → ο . PNoEq_ x0 x1 x2PNoLe x0 x1 x0 x2 (proof)
Theorem PNoLe_refPNoLe_ref : ∀ x0 . ∀ x1 : ι → ο . PNoLe x0 x1 x0 x1 (proof)
Theorem PNoLe_antisymPNoLe_antisym : ∀ x0 x1 . ordinal x0ordinal x1∀ x2 x3 : ι → ο . PNoLe x0 x2 x1 x3PNoLe x1 x3 x0 x2and (x0 = x1) (PNoEq_ x0 x2 x3) (proof)
Theorem PNoLtLe_traPNoLtLe_tra : ∀ x0 x1 x2 . ordinal x0ordinal x1ordinal x2∀ x3 x4 x5 : ι → ο . PNoLt x0 x3 x1 x4PNoLe x1 x4 x2 x5PNoLt x0 x3 x2 x5 (proof)
Theorem PNoLeLt_traPNoLeLt_tra : ∀ x0 x1 x2 . ordinal x0ordinal x1ordinal x2∀ x3 x4 x5 : ι → ο . PNoLe x0 x3 x1 x4PNoLt x1 x4 x2 x5PNoLt x0 x3 x2 x5 (proof)
Theorem PNoEqLe_traPNoEqLe_tra : ∀ x0 x1 . ordinal x0ordinal x1∀ x2 x3 x4 : ι → ο . PNoEq_ x0 x2 x3PNoLe x0 x3 x1 x4PNoLe x0 x2 x1 x4 (proof)
Theorem PNoLeEq_traPNoLeEq_tra : ∀ x0 x1 . ordinal x0ordinal x1∀ x2 x3 x4 : ι → ο . PNoLe x0 x2 x1 x3PNoEq_ x1 x3 x4PNoLe x0 x2 x1 x4 (proof)
Theorem PNoLe_traPNoLe_tra : ∀ x0 x1 x2 . ordinal x0ordinal x1ordinal x2∀ x3 x4 x5 : ι → ο . PNoLe x0 x3 x1 x4PNoLe x1 x4 x2 x5PNoLe x0 x3 x2 x5 (proof)
Definition PNo_downcPNo_downc := λ x0 : ι → (ι → ο) → ο . λ x1 . λ x2 : ι → ο . ∀ x3 : ο . (∀ x4 . and (ordinal x4) (∀ x5 : ο . (∀ x6 : ι → ο . and (x0 x4 x6) (PNoLe x1 x2 x4 x6)x5)x5)x3)x3
Definition PNo_upcPNo_upc := λ x0 : ι → (ι → ο) → ο . λ x1 . λ x2 : ι → ο . ∀ x3 : ο . (∀ x4 . and (ordinal x4) (∀ x5 : ο . (∀ x6 : ι → ο . and (x0 x4 x6) (PNoLe x4 x6 x1 x2)x5)x5)x3)x3
Theorem PNoLe_downcPNoLe_downc : ∀ x0 : ι → (ι → ο) → ο . ∀ x1 x2 . ∀ x3 x4 : ι → ο . ordinal x1ordinal x2PNo_downc x0 x1 x3PNoLe x2 x4 x1 x3PNo_downc x0 x2 x4 (proof)
Theorem PNo_downc_refPNo_downc_ref : ∀ x0 : ι → (ι → ο) → ο . ∀ x1 . ordinal x1∀ x2 : ι → ο . x0 x1 x2PNo_downc x0 x1 x2 (proof)
Theorem PNo_upc_refPNo_upc_ref : ∀ x0 : ι → (ι → ο) → ο . ∀ x1 . ordinal x1∀ x2 : ι → ο . x0 x1 x2PNo_upc x0 x1 x2 (proof)
Theorem PNoLe_upcPNoLe_upc : ∀ x0 : ι → (ι → ο) → ο . ∀ x1 x2 . ∀ x3 x4 : ι → ο . ordinal x1ordinal x2PNo_upc x0 x1 x3PNoLe x1 x3 x2 x4PNo_upc x0 x2 x4 (proof)
Definition PNoLt_pwisePNoLt_pwise := λ x0 x1 : ι → (ι → ο) → ο . ∀ x2 . ordinal x2∀ x3 : ι → ο . x0 x2 x3∀ x4 . ordinal x4∀ x5 : ι → ο . x1 x4 x5PNoLt x2 x3 x4 x5
Theorem PNoLt_pwise_downc_upcPNoLt_pwise_downc_upc : ∀ x0 x1 : ι → (ι → ο) → ο . PNoLt_pwise x0 x1PNoLt_pwise (PNo_downc x0) (PNo_upc x1) (proof)
Definition PNo_rel_strict_upperbdPNo_rel_strict_upperbd := λ x0 : ι → (ι → ο) → ο . λ x1 . λ x2 : ι → ο . ∀ x3 . x3x1∀ x4 : ι → ο . PNo_downc x0 x3 x4PNoLt x3 x4 x1 x2
Definition PNo_rel_strict_lowerbdPNo_rel_strict_lowerbd := λ x0 : ι → (ι → ο) → ο . λ x1 . λ x2 : ι → ο . ∀ x3 . x3x1∀ x4 : ι → ο . PNo_upc x0 x3 x4PNoLt x1 x2 x3 x4
Definition PNo_rel_strict_imvPNo_rel_strict_imv := λ x0 x1 : ι → (ι → ο) → ο . λ x2 . λ x3 : ι → ο . and (PNo_rel_strict_upperbd x0 x2 x3) (PNo_rel_strict_lowerbd x1 x2 x3)
Theorem PNoEq_rel_strict_upperbdPNoEq_rel_strict_upperbd : ∀ x0 : ι → (ι → ο) → ο . ∀ x1 . ordinal x1∀ x2 x3 : ι → ο . PNoEq_ x1 x2 x3PNo_rel_strict_upperbd x0 x1 x2PNo_rel_strict_upperbd x0 x1 x3 (proof)
Known In_no2cycleIn_no2cycle : ∀ x0 x1 . x0x1x1x0False
Theorem PNo_rel_strict_upperbd_antimonPNo_rel_strict_upperbd_antimon : ∀ x0 : ι → (ι → ο) → ο . ∀ x1 . ordinal x1∀ x2 : ι → ο . ∀ x3 . x3x1PNo_rel_strict_upperbd x0 x1 x2PNo_rel_strict_upperbd x0 x3 x2 (proof)
Theorem PNoEq_rel_strict_lowerbdPNoEq_rel_strict_lowerbd : ∀ x0 : ι → (ι → ο) → ο . ∀ x1 . ordinal x1∀ x2 x3 : ι → ο . PNoEq_ x1 x2 x3PNo_rel_strict_lowerbd x0 x1 x2PNo_rel_strict_lowerbd x0 x1 x3 (proof)
Theorem PNo_rel_strict_lowerbd_antimonPNo_rel_strict_lowerbd_antimon : ∀ x0 : ι → (ι → ο) → ο . ∀ x1 . ordinal x1∀ x2 : ι → ο . ∀ x3 . x3x1PNo_rel_strict_lowerbd x0 x1 x2PNo_rel_strict_lowerbd x0 x3 x2 (proof)
Theorem PNoEq_rel_strict_imvPNoEq_rel_strict_imv : ∀ x0 x1 : ι → (ι → ο) → ο . ∀ x2 . ordinal x2∀ x3 x4 : ι → ο . PNoEq_ x2 x3 x4PNo_rel_strict_imv x0 x1 x2 x3PNo_rel_strict_imv x0 x1 x2 x4 (proof)
Theorem PNo_rel_strict_imv_antimonPNo_rel_strict_imv_antimon : ∀ x0 x1 : ι → (ι → ο) → ο . ∀ x2 . ordinal x2∀ x3 : ι → ο . ∀ x4 . x4x2PNo_rel_strict_imv x0 x1 x2 x3PNo_rel_strict_imv x0 x1 x4 x3 (proof)
Definition PNo_rel_strict_uniq_imvPNo_rel_strict_uniq_imv := λ x0 x1 : ι → (ι → ο) → ο . λ x2 . λ x3 : ι → ο . and (PNo_rel_strict_imv x0 x1 x2 x3) (∀ x4 : ι → ο . PNo_rel_strict_imv x0 x1 x2 x4PNoEq_ x2 x3 x4)
Param ordsuccordsucc : ιι
Definition PNo_rel_strict_split_imvPNo_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)))
Theorem PNo_extend0_eqPNo_extend0_eq : ∀ x0 . ∀ x1 : ι → ο . PNoEq_ x0 x1 (λ x2 . and (x1 x2) (x2 = x0∀ x3 : ο . x3)) (proof)
Theorem PNo_extend1_eqPNo_extend1_eq : ∀ x0 . ∀ x1 : ι → ο . PNoEq_ x0 x1 (λ x2 . or (x1 x2) (x2 = x0)) (proof)
Known ordinal_lim_or_succordinal_lim_or_succ : ∀ x0 . ordinal x0or (∀ x1 . x1x0ordsucc x1x0) (∀ x1 : ο . (∀ x2 . and (x2x0) (x0 = ordsucc x2)x1)x1)
Known iffERiffER : ∀ x0 x1 : ο . iff x0 x1x1x0
Known ordsuccI2ordsuccI2 : ∀ x0 . x0ordsucc x0
Known ordinal_ordsucc_Inordinal_ordsucc_In : ∀ x0 . ordinal x0∀ x1 . x1x0ordsucc x1ordsucc x0
Known ordinal_ordsuccordinal_ordsucc : ∀ x0 . ordinal x0ordinal (ordsucc x0)
Known ordinal_ordsucc_In_eqordinal_ordsucc_In_eq : ∀ x0 x1 . ordinal x0x1x0or (ordsucc x1x0) (x0 = ordsucc x1)
Known ordsuccEordsuccE : ∀ x0 x1 . x1ordsucc x0or (x1x0) (x1 = x0)
Known ordsuccI1ordsuccI1 : ∀ x0 . x0ordsucc x0
Theorem PNo_rel_imv_exPNo_rel_imv_ex : ∀ x0 x1 : ι → (ι → ο) → ο . PNoLt_pwise x0 x1∀ x2 . ordinal x2or (∀ x3 : ο . (∀ x4 : ι → ο . PNo_rel_strict_uniq_imv x0 x1 x2 x4x3)x3) (∀ x3 : ο . (∀ x4 . and (x4x2) (∀ x5 : ο . (∀ x6 : ι → ο . PNo_rel_strict_split_imv x0 x1 x4 x6x5)x5)x3)x3) (proof)
Definition PNo_lenbddPNo_lenbdd := λ x0 . λ x1 : ι → (ι → ο) → ο . ∀ x2 . ∀ x3 : ι → ο . x1 x2 x3x2x0
Theorem PNo_lenbdd_strict_imv_extend0PNo_lenbdd_strict_imv_extend0 : ∀ x0 x1 : ι → (ι → ο) → ο . ∀ x2 . ordinal x2PNo_lenbdd x2 x0PNo_lenbdd x2 x1∀ x3 : ι → ο . PNo_rel_strict_imv x0 x1 x2 x3PNo_rel_strict_imv x0 x1 (ordsucc x2) (λ x4 . and (x3 x4) (x4 = x2∀ x5 : ο . x5)) (proof)
Theorem PNo_lenbdd_strict_imv_extend1PNo_lenbdd_strict_imv_extend1 : ∀ x0 x1 : ι → (ι → ο) → ο . ∀ x2 . ordinal x2PNo_lenbdd x2 x0PNo_lenbdd x2 x1∀ x3 : ι → ο . PNo_rel_strict_imv x0 x1 x2 x3PNo_rel_strict_imv x0 x1 (ordsucc x2) (λ x4 . or (x3 x4) (x4 = x2)) (proof)
Theorem PNo_lenbdd_strict_imv_splitPNo_lenbdd_strict_imv_split : ∀ x0 x1 : ι → (ι → ο) → ο . ∀ x2 . ordinal x2PNo_lenbdd x2 x0PNo_lenbdd x2 x1∀ x3 : ι → ο . PNo_rel_strict_imv x0 x1 x2 x3PNo_rel_strict_split_imv x0 x1 x2 x3 (proof)
Theorem PNo_rel_imv_bdd_exPNo_rel_imv_bdd_ex : ∀ x0 x1 : ι → (ι → ο) → ο . PNoLt_pwise x0 x1∀ x2 . ordinal x2PNo_lenbdd x2 x0PNo_lenbdd x2 x1∀ x3 : ο . (∀ x4 . and (x4ordsucc x2) (∀ x5 : ο . (∀ x6 : ι → ο . PNo_rel_strict_split_imv x0 x1 x4 x6x5)x5)x3)x3 (proof)
Definition PNo_strict_upperbdPNo_strict_upperbd := λ x0 : ι → (ι → ο) → ο . λ x1 . λ x2 : ι → ο . ∀ x3 . ordinal x3∀ x4 : ι → ο . x0 x3 x4PNoLt x3 x4 x1 x2
Definition PNo_strict_lowerbdPNo_strict_lowerbd := λ x0 : ι → (ι → ο) → ο . λ x1 . λ x2 : ι → ο . ∀ x3 . ordinal x3∀ x4 : ι → ο . x0 x3 x4PNoLt x1 x2 x3 x4
Definition PNo_strict_imvPNo_strict_imv := λ x0 x1 : ι → (ι → ο) → ο . λ x2 . λ x3 : ι → ο . and (PNo_strict_upperbd x0 x2 x3) (PNo_strict_lowerbd x1 x2 x3)
Theorem PNoEq_strict_upperbdPNoEq_strict_upperbd : ∀ x0 : ι → (ι → ο) → ο . ∀ x1 . ordinal x1∀ x2 x3 : ι → ο . PNoEq_ x1 x2 x3PNo_strict_upperbd x0 x1 x2PNo_strict_upperbd x0 x1 x3 (proof)
Theorem PNoEq_strict_lowerbdPNoEq_strict_lowerbd : ∀ x0 : ι → (ι → ο) → ο . ∀ x1 . ordinal x1∀ x2 x3 : ι → ο . PNoEq_ x1 x2 x3PNo_strict_lowerbd x0 x1 x2PNo_strict_lowerbd x0 x1 x3 (proof)
Theorem PNoEq_strict_imvPNoEq_strict_imv : ∀ x0 x1 : ι → (ι → ο) → ο . ∀ x2 . ordinal x2∀ x3 x4 : ι → ο . PNoEq_ x2 x3 x4PNo_strict_imv x0 x1 x2 x3PNo_strict_imv x0 x1 x2 x4 (proof)
Theorem PNo_strict_upperbd_imp_rel_strict_upperbdPNo_strict_upperbd_imp_rel_strict_upperbd : ∀ x0 : ι → (ι → ο) → ο . ∀ x1 . ordinal x1∀ x2 . x2ordsucc x1∀ x3 : ι → ο . PNo_strict_upperbd x0 x1 x3PNo_rel_strict_upperbd x0 x2 x3 (proof)
Theorem PNo_strict_lowerbd_imp_rel_strict_lowerbdPNo_strict_lowerbd_imp_rel_strict_lowerbd : ∀ x0 : ι → (ι → ο) → ο . ∀ x1 . ordinal x1∀ x2 . x2ordsucc x1∀ x3 : ι → ο . PNo_strict_lowerbd x0 x1 x3PNo_rel_strict_lowerbd x0 x2 x3 (proof)
Theorem PNo_strict_imv_imp_rel_strict_imvPNo_strict_imv_imp_rel_strict_imv : ∀ x0 x1 : ι → (ι → ο) → ο . ∀ x2 . ordinal x2∀ x3 . x3ordsucc x2∀ x4 : ι → ο . PNo_strict_imv x0 x1 x2 x4PNo_rel_strict_imv x0 x1 x3 x4 (proof)
Theorem PNo_rel_split_imv_imp_strict_imvPNo_rel_split_imv_imp_strict_imv : ∀ x0 x1 : ι → (ι → ο) → ο . ∀ x2 . ordinal x2∀ x3 : ι → ο . PNo_rel_strict_split_imv x0 x1 x2 x3PNo_strict_imv x0 x1 x2 x3 (proof)
Theorem ordinal_PNo_strict_imvordinal_PNo_strict_imv : ∀ x0 x1 : ι → (ι → ο) → ο . ∀ x2 . ordinal x2∀ x3 : ι → ο . (∀ x4 . x4x2x3 x4)(∀ x4 . ordinal x4∀ x5 : ι → ο . x0 x4 x5x4x2)(∀ x4 . x4x2x0 x4 x3)(∀ x4 . ordinal x4∀ x5 : ι → ο . not (x1 x4 x5))PNo_strict_imv x0 x1 x2 x3 (proof)
Theorem PNo_lenbdd_strict_imv_exPNo_lenbdd_strict_imv_ex : ∀ x0 x1 : ι → (ι → ο) → ο . PNoLt_pwise x0 x1∀ x2 . ordinal x2PNo_lenbdd x2 x0PNo_lenbdd x2 x1∀ x3 : ο . (∀ x4 . and (x4ordsucc x2) (∀ x5 : ο . (∀ x6 : ι → ο . PNo_strict_imv x0 x1 x4 x6x5)x5)x3)x3 (proof)
Definition PNo_least_repPNo_least_rep := λ x0 x1 : ι → (ι → ο) → ο . λ x2 . λ x3 : ι → ο . and (and (ordinal x2) (PNo_strict_imv x0 x1 x2 x3)) (∀ x4 . x4x2∀ x5 : ι → ο . not (PNo_strict_imv x0 x1 x4 x5))
Known least_ordinal_exleast_ordinal_ex : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . and (ordinal x2) (x0 x2)x1)x1)∀ x1 : ο . (∀ x2 . and (and (ordinal x2) (x0 x2)) (∀ x3 . x3x2not (x0 x3))x1)x1
Theorem PNo_lenbdd_least_rep_exPNo_lenbdd_least_rep_ex : ∀ x0 x1 : ι → (ι → ο) → ο . PNoLt_pwise x0 x1∀ x2 . ordinal x2PNo_lenbdd x2 x0PNo_lenbdd x2 x1∀ x3 : ο . (∀ x4 . (∀ x5 : ο . (∀ x6 : ι → ο . PNo_least_rep x0 x1 x4 x6x5)x5)x3)x3 (proof)
Definition PNo_least_rep2PNo_least_rep2 := λ x0 x1 : ι → (ι → ο) → ο . λ x2 . λ x3 : ι → ο . and (PNo_least_rep x0 x1 x2 x3) (∀ x4 . nIn x4 x2not (x3 x4))
Theorem PNo_strict_imv_pred_eqPNo_strict_imv_pred_eq : ∀ x0 x1 : ι → (ι → ο) → ο . PNoLt_pwise x0 x1∀ x2 . ordinal x2∀ x3 x4 : ι → ο . PNo_least_rep x0 x1 x2 x3PNo_strict_imv x0 x1 x2 x4∀ x5 . x5x2iff (x3 x5) (x4 x5) (proof)
Known pred_extpred_ext : ∀ x0 x1 : ι → ο . (∀ x2 . iff (x0 x2) (x1 x2))x0 = x1
Theorem PNo_lenbdd_least_rep2_exuniq2PNo_lenbdd_least_rep2_exuniq2 : ∀ x0 x1 : ι → (ι → ο) → ο . PNoLt_pwise x0 x1∀ x2 . ordinal x2PNo_lenbdd x2 x0PNo_lenbdd x2 x1∀ x3 : ο . (∀ x4 . and (∀ x5 : ο . (∀ x6 : ι → ο . PNo_least_rep2 x0 x1 x4 x6x5)x5) (∀ x5 x6 : ι → ο . PNo_least_rep2 x0 x1 x4 x5PNo_least_rep2 x0 x1 x4 x6x5 = x6)x3)x3 (proof)
Definition PNo_bdPNo_bd := λ x0 x1 : ι → (ι → ο) → ο . DescrR_i_io_1 (PNo_least_rep2 x0 x1)
Definition PNo_predPNo_pred := λ x0 x1 : ι → (ι → ο) → ο . DescrR_i_io_2 (PNo_least_rep2 x0 x1)
Theorem PNo_bd_pred_lemPNo_bd_pred_lem : ∀ x0 x1 : ι → (ι → ο) → ο . PNoLt_pwise x0 x1∀ x2 . ordinal x2PNo_lenbdd x2 x0PNo_lenbdd x2 x1PNo_least_rep2 x0 x1 (PNo_bd x0 x1) (PNo_pred x0 x1) (proof)
Theorem PNo_bd_predPNo_bd_pred : ∀ x0 x1 : ι → (ι → ο) → ο . PNoLt_pwise x0 x1∀ x2 . ordinal x2PNo_lenbdd x2 x0PNo_lenbdd x2 x1PNo_least_rep x0 x1 (PNo_bd x0 x1) (PNo_pred x0 x1) (proof)
Theorem PNo_bd_ordPNo_bd_ord : ∀ x0 x1 : ι → (ι → ο) → ο . PNoLt_pwise x0 x1∀ x2 . ordinal x2PNo_lenbdd x2 x0PNo_lenbdd x2 x1ordinal (PNo_bd x0 x1) (proof)
Theorem PNo_bd_pred_strict_imvPNo_bd_pred_strict_imv : ∀ x0 x1 : ι → (ι → ο) → ο . PNoLt_pwise x0 x1∀ x2 . ordinal x2PNo_lenbdd x2 x0PNo_lenbdd x2 x1PNo_strict_imv x0 x1 (PNo_bd x0 x1) (PNo_pred x0 x1) (proof)
Theorem PNo_bd_least_imvPNo_bd_least_imv : ∀ x0 x1 : ι → (ι → ο) → ο . PNoLt_pwise x0 x1∀ x2 . ordinal x2PNo_lenbdd x2 x0PNo_lenbdd x2 x1∀ x3 . x3PNo_bd x0 x1∀ x4 : ι → ο . not (PNo_strict_imv x0 x1 x3 x4) (proof)
Known ordinal_In_Or_Subqordinal_In_Or_Subq : ∀ x0 x1 . ordinal x0ordinal x1or (x0x1) (x1x0)
Theorem PNo_bd_InPNo_bd_In : ∀ x0 x1 : ι → (ι → ο) → ο . PNoLt_pwise x0 x1∀ x2 . ordinal x2PNo_lenbdd x2 x0PNo_lenbdd x2 x1PNo_bd x0 x1ordsucc x2 (proof)
Definition PNoCutLPNoCutL := λ x0 . λ x1 : ι → ο . λ x2 . λ x3 : ι → ο . and (x2x0) (PNoLt x2 x3 x0 x1)
Definition PNoCutRPNoCutR := λ x0 . λ x1 : ι → ο . λ x2 . λ x3 : ι → ο . and (x2x0) (PNoLt x0 x1 x2 x3)
Theorem PNoCutL_lenbddPNoCutL_lenbdd : ∀ x0 . ∀ x1 : ι → ο . PNo_lenbdd x0 (PNoCutL x0 x1) (proof)
Theorem PNoCutR_lenbddPNoCutR_lenbdd : ∀ x0 . ∀ x1 : ι → ο . PNo_lenbdd x0 (PNoCutR x0 x1) (proof)
Theorem PNoCut_pwisePNoCut_pwise : ∀ x0 . ordinal x0∀ x1 : ι → ο . PNoLt_pwise (PNoCutL x0 x1) (PNoCutR x0 x1) (proof)
Theorem PNoCut_strict_imvPNoCut_strict_imv : ∀ x0 . ordinal x0∀ x1 : ι → ο . PNo_strict_imv (PNoCutL x0 x1) (PNoCutR x0 x1) x0 x1 (proof)
Theorem PNoCut_bd_eqPNoCut_bd_eq : ∀ x0 . ordinal x0∀ x1 : ι → ο . PNo_bd (PNoCutL x0 x1) (PNoCutR x0 x1) = x0 (proof)
Theorem PNoCut_pred_eqPNoCut_pred_eq : ∀ x0 . ordinal x0∀ x1 : ι → ο . PNoEq_ x0 x1 (PNo_pred (PNoCutL x0 x1) (PNoCutR x0 x1)) (proof)

previous assets