Proofgold Address

Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition iff^iff := λ x0 x1 : ο . and (x0 ⟶ x1) (x1 ⟶ x0)
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known iff_refl^iff_refl : ∀ x0 : ο . iff x0 x0
Known iffI^iffI : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ iff x0 x1
Theorem iff_sym^iff_sym : ∀ x0 x1 : ο . iff x0 x1 ⟶ iff x1 x0 (proof)
Theorem iff_trans^iff_trans : ∀ x0 x1 x2 : ο . iff x0 x1 ⟶ iff x1 x2 ⟶ iff x0 x2 (proof)
Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known orIL^orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Known orIR^orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Theorem not_or_and_demorgan^{not_or_and_demorgan} : ∀ x0 x1 : ο . not (or x0 x1) ⟶ and (not x0) (not x1) (proof)
Theorem and_not_or_demorgan^{and_not_or_demorgan} : ∀ x0 x1 : ο . and (not x0) (not x1) ⟶ not (or x0 x1) (proof)
Theorem not_ex_all_demorgan_i^{not_ex_all_demorgan_i} : ∀ x0 : ι → ο . not (∀ x1 : ο . (∀ x2 . x0 x2 ⟶ x1) ⟶ x1) ⟶ ∀ x1 . not (x0 x1) (proof)
Known dneg^dneg : ∀ x0 : ο . not (not x0) ⟶ x0
Theorem not_all_ex_demorgan_i^{not_all_ex_demorgan_i} : ∀ x0 : ι → ο . not (∀ x1 . x0 x1) ⟶ ∀ x1 : ο . (∀ x2 . not (x0 x2) ⟶ x1) ⟶ x1 (proof)
Known prop_ext_2^prop_ext_2 : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ x0 = x1
Known xm^xm : ∀ x0 : ο . or x0 (not x0)
Theorem eq_or_nand^eq_or_nand : or = λ x1 x2 : ο . not (and (not x1) (not x2)) (proof)
Definition EpsR_i_i_1^EpsR_i_i_1 := λ x0 : ι → ι → ο . prim0 (λ x1 . ∀ x2 : ο . (∀ x3 . x0 x1 x3 ⟶ x2) ⟶ x2)
Definition EpsR_i_i_2^EpsR_i_i_2 := λ x0 : ι → ι → ο . prim0 (x0 (EpsR_i_i_1 x0))
Known Eps_i_ex^Eps_i_ex : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . x0 x2 ⟶ x1) ⟶ x1) ⟶ x0 (prim0 x0)
Theorem EpsR_i_i_12^EpsR_i_i_12 : ∀ x0 : ι → ι → ο . (∀ x1 : ο . (∀ x2 . (∀ x3 : ο . (∀ x4 . x0 x2 x4 ⟶ x3) ⟶ x3) ⟶ x1) ⟶ x1) ⟶ x0 (EpsR_i_i_1 x0) (EpsR_i_i_2 x0) (proof)
Definition DescrR_i_io_1^{DescrR_i_io_1} := λ x0 : ι → (ι → ο) → ο . prim0 (λ x1 . and (∀ x2 : ο . (∀ x3 : ι → ο . x0 x1 x3 ⟶ x2) ⟶ x2) (∀ x2 x3 : ι → ο . x0 x1 x2 ⟶ x0 x1 x3 ⟶ x2 = x3))
Param Descr_Vo1^Descr_Vo1 : ((ι → ο) → ο) → ι → ο
Definition DescrR_i_io_2^{DescrR_i_io_2} := λ x0 : ι → (ι → ο) → ο . Descr_Vo1 (x0 (DescrR_i_io_1 x0))
Known Descr_Vo1_prop^{Descr_Vo1_prop} : ∀ x0 : (ι → ο) → ο . (∀ x1 : ο . (∀ x2 : ι → ο . x0 x2 ⟶ x1) ⟶ x1) ⟶ (∀ x1 x2 : ι → ο . x0 x1 ⟶ x0 x2 ⟶ x1 = x2) ⟶ x0 (Descr_Vo1 x0)
Theorem DescrR_i_io_12^{DescrR_i_io_12} : ∀ x0 : ι → (ι → ο) → ο . (∀ x1 : ο . (∀ x2 . and (∀ x3 : ο . (∀ x4 : ι → ο . x0 x2 x4 ⟶ x3) ⟶ x3) (∀ x3 x4 : ι → ο . x0 x2 x3 ⟶ x0 x2 x4 ⟶ x3 = x4) ⟶ x1) ⟶ x1) ⟶ x0 (DescrR_i_io_1 x0) (DescrR_i_io_2 x0) (proof)
Definition PNoEq_^PNoEq_ := λ x0 . λ x1 x2 : ι → ο . ∀ x3 . x3 ∈ x0 ⟶ iff (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 x2 ⟶ PNoEq_ x0 x2 x1 (proof)
Theorem PNoEq_tra_^PNoEq_tra_ : ∀ x0 . ∀ x1 x2 x3 : ι → ο . PNoEq_ x0 x1 x2 ⟶ PNoEq_ x0 x2 x3 ⟶ PNoEq_ x0 x1 x3 (proof)
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Definition TransSet^TransSet := λ x0 . ∀ x1 . x1 ∈ x0 ⟶ x1 ⊆ x0
Definition ordinal^ordinal := λ x0 . and (TransSet x0) (∀ x1 . x1 ∈ x0 ⟶ TransSet x1)
Theorem PNoEq_antimon_^{PNoEq_antimon_} : ∀ x0 x1 : ι → ο . ∀ x2 . ordinal x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ PNoEq_ x2 x0 x1 ⟶ PNoEq_ x3 x0 x1 (proof)
Definition PNoLt_^PNoLt_ := λ x0 . λ x1 x2 : ι → ο . ∀ x3 : ο . (∀ x4 . and (x4 ∈ x0) (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 . x4 ∈ x0 ⟶ PNoEq_ x4 x1 x2 ⟶ not (x1 x4) ⟶ x2 x4 ⟶ x3) ⟶ 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 . x3 ∈ x2 ⟶ PNoLt_ x3 x0 x1 ⟶ PNoLt_ x2 x0 x1 (proof)
Known ordinal_ind^ordinal_ind : ∀ x0 : ι → ο . (∀ x1 . ordinal x1 ⟶ (∀ x2 . x2 ∈ x1 ⟶ x0 x2) ⟶ x0 x1) ⟶ ∀ x1 . ordinal x1 ⟶ x0 x1
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Known and3I^and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Definition nIn^nIn := λ x0 x1 . not (x0 ∈ x1)
Theorem 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) (proof)
Known ordinal_trichotomy_or^{ordinal_trichotomy_or} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ or (or (x0 ∈ x1) (x0 = x1)) (x1 ∈ x0)
Known ordinal_Hered^{ordinal_Hered} : ∀ x0 . ordinal x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ ordinal x1
Theorem PNoLt_tra_^PNoLt_tra_ : ∀ x0 . ordinal x0 ⟶ ∀ x1 x2 x3 : ι → ο . PNoLt_ x0 x1 x2 ⟶ PNoLt_ x0 x2 x3 ⟶ PNoLt_ x0 x1 x3 (proof)
Param binintersect^binintersect : ι → ι → ι
Definition PNoLt^PNoLt := λ x0 . λ x1 : ι → ο . λ x2 . λ x3 : ι → ο . or (or (PNoLt_ (binintersect x0 x2) x1 x3) (and (and (x0 ∈ x2) (PNoEq_ x0 x1 x3)) (x3 x0))) (and (and (x2 ∈ x0) (PNoEq_ x2 x1 x3)) (not (x1 x2)))
Known or3I1^or3I1 : ∀ x0 x1 x2 : ο . x0 ⟶ or (or x0 x1) x2
Theorem PNoLtI1^PNoLtI1 : ∀ x0 x1 . ∀ x2 x3 : ι → ο . PNoLt_ (binintersect x0 x1) x2 x3 ⟶ PNoLt x0 x2 x1 x3 (proof)
Known or3I2^or3I2 : ∀ x0 x1 x2 : ο . x1 ⟶ or (or x0 x1) x2
Theorem PNoLtI2^PNoLtI2 : ∀ x0 x1 . ∀ x2 x3 : ι → ο . x0 ∈ x1 ⟶ PNoEq_ x0 x2 x3 ⟶ x3 x0 ⟶ PNoLt x0 x2 x1 x3 (proof)
Known or3I3^or3I3 : ∀ x0 x1 x2 : ο . x2 ⟶ or (or x0 x1) x2
Theorem PNoLtI3^PNoLtI3 : ∀ x0 x1 . ∀ x2 x3 : ι → ο . x1 ∈ x0 ⟶ PNoEq_ x1 x2 x3 ⟶ not (x2 x1) ⟶ PNoLt x0 x2 x1 x3 (proof)
Theorem 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 (proof)
Known binintersect_idem^{binintersect_idem} : ∀ x0 . binintersect x0 x0 = x0
Known In_irref^In_irref : ∀ x0 . nIn x0 x0
Theorem PNoLtE2^PNoLtE2 : ∀ x0 . ∀ x1 x2 : ι → ο . PNoLt x0 x1 x0 x2 ⟶ PNoLt_ x0 x1 x2 (proof)
Theorem PNoLt_irref^PNoLt_irref : ∀ x0 . ∀ x1 : ι → ο . not (PNoLt x0 x1 x0 x1) (proof)
Known binintersect_Subq_eq_1^{binintersect_Subq_eq_1} : ∀ x0 x1 . x0 ⊆ x1 ⟶ binintersect x0 x1 = x0
Known Subq_ref^Subq_ref : ∀ x0 . x0 ⊆ x0
Known binintersect_com^{binintersect_com} : ∀ x0 x1 . binintersect x0 x1 = binintersect x1 x0
Known ordinal_binintersect^{ordinal_binintersect} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ ordinal (binintersect x0 x1)
Theorem 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) (proof)
Known binintersectE^{binintersectE} : ∀ x0 x1 x2 . x2 ∈ binintersect x0 x1 ⟶ and (x2 ∈ x0) (x2 ∈ x1)
Known iffEL^iffEL : ∀ x0 x1 : ο . iff x0 x1 ⟶ x0 ⟶ x1
Theorem 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 (proof)
Theorem 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 (proof)
Known binintersectI^{binintersectI} : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ x2 ∈ x1 ⟶ x2 ∈ binintersect x0 x1
Theorem 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 (proof)
Definition PNoLe^PNoLe := λ x0 . λ x1 : ι → ο . λ x2 . λ x3 : ι → ο . or (PNoLt x0 x1 x2 x3) (and (x0 = x2) (PNoEq_ x0 x1 x3))
Theorem PNoLeI1^PNoLeI1 : ∀ x0 x1 . ∀ x2 x3 : ι → ο . PNoLt x0 x2 x1 x3 ⟶ PNoLe x0 x2 x1 x3 (proof)
Theorem PNoLeI2^PNoLeI2 : ∀ x0 . ∀ x1 x2 : ι → ο . PNoEq_ x0 x1 x2 ⟶ PNoLe x0 x1 x0 x2 (proof)
Theorem PNoLe_ref^PNoLe_ref : ∀ x0 . ∀ x1 : ι → ο . PNoLe x0 x1 x0 x1 (proof)
Theorem 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) (proof)
Theorem 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 (proof)
Theorem 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 (proof)
Theorem PNoEqLe_tra^PNoEqLe_tra : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ ∀ x2 x3 x4 : ι → ο . PNoEq_ x0 x2 x3 ⟶ PNoLe x0 x3 x1 x4 ⟶ PNoLe x0 x2 x1 x4 (proof)
Theorem PNoLeEq_tra^PNoLeEq_tra : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ ∀ x2 x3 x4 : ι → ο . PNoLe x0 x2 x1 x3 ⟶ PNoEq_ x1 x3 x4 ⟶ PNoLe x0 x2 x1 x4 (proof)
Theorem 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 (proof)
Definition PNo_downc^PNo_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_upc^PNo_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_downc^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 PNo_downc_ref^{PNo_downc_ref} : ∀ x0 : ι → (ι → ο) → ο . ∀ x1 . ordinal x1 ⟶ ∀ x2 : ι → ο . x0 x1 x2 ⟶ PNo_downc x0 x1 x2 (proof)
Theorem PNo_upc_ref^PNo_upc_ref : ∀ x0 : ι → (ι → ο) → ο . ∀ x1 . ordinal x1 ⟶ ∀ x2 : ι → ο . x0 x1 x2 ⟶ PNo_upc x0 x1 x2 (proof)
Theorem PNoLe_upc^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 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
Theorem PNoLt_pwise_downc_upc^{PNoLt_pwise_downc_upc} : ∀ x0 x1 : ι → (ι → ο) → ο . PNoLt_pwise x0 x1 ⟶ PNoLt_pwise (PNo_downc x0) (PNo_upc x1) (proof)
Definition PNo_rel_strict_upperbd^{PNo_rel_strict_upperbd} := λ x0 : ι → (ι → ο) → ο . λ x1 . λ x2 : ι → ο . ∀ x3 . x3 ∈ x1 ⟶ ∀ x4 : ι → ο . PNo_downc x0 x3 x4 ⟶ PNoLt x3 x4 x1 x2
Definition PNo_rel_strict_lowerbd^{PNo_rel_strict_lowerbd} := λ x0 : ι → (ι → ο) → ο . λ x1 . λ x2 : ι → ο . ∀ x3 . x3 ∈ x1 ⟶ ∀ x4 : ι → ο . PNo_upc x0 x3 x4 ⟶ PNoLt x1 x2 x3 x4
Definition PNo_rel_strict_imv^{PNo_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_upperbd^{PNoEq_rel_strict_upperbd} : ∀ x0 : ι → (ι → ο) → ο . ∀ x1 . ordinal x1 ⟶ ∀ x2 x3 : ι → ο . PNoEq_ x1 x2 x3 ⟶ PNo_rel_strict_upperbd x0 x1 x2 ⟶ PNo_rel_strict_upperbd x0 x1 x3 (proof)
Known In_no2cycle^In_no2cycle : ∀ x0 x1 . x0 ∈ x1 ⟶ x1 ∈ x0 ⟶ False
Theorem PNo_rel_strict_upperbd_antimon^{PNo_rel_strict_upperbd_antimon} : ∀ x0 : ι → (ι → ο) → ο . ∀ x1 . ordinal x1 ⟶ ∀ x2 : ι → ο . ∀ x3 . x3 ∈ x1 ⟶ PNo_rel_strict_upperbd x0 x1 x2 ⟶ PNo_rel_strict_upperbd x0 x3 x2 (proof)
Theorem PNoEq_rel_strict_lowerbd^{PNoEq_rel_strict_lowerbd} : ∀ x0 : ι → (ι → ο) → ο . ∀ x1 . ordinal x1 ⟶ ∀ x2 x3 : ι → ο . PNoEq_ x1 x2 x3 ⟶ PNo_rel_strict_lowerbd x0 x1 x2 ⟶ PNo_rel_strict_lowerbd x0 x1 x3 (proof)
Theorem PNo_rel_strict_lowerbd_antimon^{PNo_rel_strict_lowerbd_antimon} : ∀ x0 : ι → (ι → ο) → ο . ∀ x1 . ordinal x1 ⟶ ∀ x2 : ι → ο . ∀ x3 . x3 ∈ x1 ⟶ PNo_rel_strict_lowerbd x0 x1 x2 ⟶ PNo_rel_strict_lowerbd x0 x3 x2 (proof)
Theorem 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 (proof)
Theorem PNo_rel_strict_imv_antimon^{PNo_rel_strict_imv_antimon} : ∀ x0 x1 : ι → (ι → ο) → ο . ∀ x2 . ordinal x2 ⟶ ∀ x3 : ι → ο . ∀ x4 . x4 ∈ x2 ⟶ PNo_rel_strict_imv x0 x1 x2 x3 ⟶ PNo_rel_strict_imv x0 x1 x4 x3 (proof)
Definition PNo_rel_strict_uniq_imv^{PNo_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 x4 ⟶ PNoEq_ x2 x3 x4)
Param ordsucc^ordsucc : ι → ι
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)))
Theorem PNo_extend0_eq^{PNo_extend0_eq} : ∀ x0 . ∀ x1 : ι → ο . PNoEq_ x0 x1 (λ x2 . and (x1 x2) (x2 = x0 ⟶ ∀ x3 : ο . x3)) (proof)
Theorem PNo_extend1_eq^{PNo_extend1_eq} : ∀ x0 . ∀ x1 : ι → ο . PNoEq_ x0 x1 (λ x2 . or (x1 x2) (x2 = x0)) (proof)
Known ordinal_lim_or_succ^{ordinal_lim_or_succ} : ∀ x0 . ordinal x0 ⟶ or (∀ x1 . x1 ∈ x0 ⟶ ordsucc x1 ∈ x0) (∀ x1 : ο . (∀ x2 . and (x2 ∈ x0) (x0 = ordsucc x2) ⟶ x1) ⟶ x1)
Known iffER^iffER : ∀ x0 x1 : ο . iff x0 x1 ⟶ x1 ⟶ x0
Known ordsuccI2^ordsuccI2 : ∀ x0 . x0 ∈ ordsucc x0
Known ordinal_ordsucc_In^{ordinal_ordsucc_In} : ∀ x0 . ordinal x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ ordsucc x1 ∈ ordsucc x0
Known ordinal_ordsucc^{ordinal_ordsucc} : ∀ x0 . ordinal x0 ⟶ ordinal (ordsucc x0)
Known ordinal_ordsucc_In_eq^{ordinal_ordsucc_In_eq} : ∀ x0 x1 . ordinal x0 ⟶ x1 ∈ x0 ⟶ or (ordsucc x1 ∈ x0) (x0 = ordsucc x1)
Known ordsuccE^ordsuccE : ∀ x0 x1 . x1 ∈ ordsucc x0 ⟶ or (x1 ∈ x0) (x1 = x0)
Known ordsuccI1^ordsuccI1 : ∀ x0 . x0 ⊆ ordsucc x0
Theorem PNo_rel_imv_ex^{PNo_rel_imv_ex} : ∀ x0 x1 : ι → (ι → ο) → ο . PNoLt_pwise x0 x1 ⟶ ∀ x2 . ordinal x2 ⟶ or (∀ x3 : ο . (∀ x4 : ι → ο . PNo_rel_strict_uniq_imv x0 x1 x2 x4 ⟶ x3) ⟶ x3) (∀ x3 : ο . (∀ x4 . and (x4 ∈ x2) (∀ x5 : ο . (∀ x6 : ι → ο . PNo_rel_strict_split_imv x0 x1 x4 x6 ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3) (proof)
Definition PNo_lenbdd^PNo_lenbdd := λ x0 . λ x1 : ι → (ι → ο) → ο . ∀ x2 . ∀ x3 : ι → ο . x1 x2 x3 ⟶ x2 ∈ x0
Theorem PNo_lenbdd_strict_imv_extend0^{PNo_lenbdd_strict_imv_extend0} : ∀ x0 x1 : ι → (ι → ο) → ο . ∀ x2 . ordinal x2 ⟶ PNo_lenbdd x2 x0 ⟶ PNo_lenbdd x2 x1 ⟶ ∀ x3 : ι → ο . PNo_rel_strict_imv x0 x1 x2 x3 ⟶ PNo_rel_strict_imv x0 x1 (ordsucc x2) (λ x4 . and (x3 x4) (x4 = x2 ⟶ ∀ x5 : ο . x5)) (proof)
Theorem PNo_lenbdd_strict_imv_extend1^{PNo_lenbdd_strict_imv_extend1} : ∀ x0 x1 : ι → (ι → ο) → ο . ∀ x2 . ordinal x2 ⟶ PNo_lenbdd x2 x0 ⟶ PNo_lenbdd x2 x1 ⟶ ∀ x3 : ι → ο . PNo_rel_strict_imv x0 x1 x2 x3 ⟶ PNo_rel_strict_imv x0 x1 (ordsucc x2) (λ x4 . or (x3 x4) (x4 = x2)) (proof)
Theorem PNo_lenbdd_strict_imv_split^{PNo_lenbdd_strict_imv_split} : ∀ x0 x1 : ι → (ι → ο) → ο . ∀ x2 . ordinal x2 ⟶ PNo_lenbdd x2 x0 ⟶ PNo_lenbdd x2 x1 ⟶ ∀ x3 : ι → ο . PNo_rel_strict_imv x0 x1 x2 x3 ⟶ PNo_rel_strict_split_imv x0 x1 x2 x3 (proof)
Theorem PNo_rel_imv_bdd_ex^{PNo_rel_imv_bdd_ex} : ∀ x0 x1 : ι → (ι → ο) → ο . PNoLt_pwise x0 x1 ⟶ ∀ x2 . ordinal x2 ⟶ PNo_lenbdd x2 x0 ⟶ PNo_lenbdd x2 x1 ⟶ ∀ x3 : ο . (∀ x4 . and (x4 ∈ ordsucc x2) (∀ x5 : ο . (∀ x6 : ι → ο . PNo_rel_strict_split_imv x0 x1 x4 x6 ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3 (proof)
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)
Theorem PNoEq_strict_upperbd^{PNoEq_strict_upperbd} : ∀ x0 : ι → (ι → ο) → ο . ∀ x1 . ordinal x1 ⟶ ∀ x2 x3 : ι → ο . PNoEq_ x1 x2 x3 ⟶ PNo_strict_upperbd x0 x1 x2 ⟶ PNo_strict_upperbd x0 x1 x3 (proof)
Theorem PNoEq_strict_lowerbd^{PNoEq_strict_lowerbd} : ∀ x0 : ι → (ι → ο) → ο . ∀ x1 . ordinal x1 ⟶ ∀ x2 x3 : ι → ο . PNoEq_ x1 x2 x3 ⟶ PNo_strict_lowerbd x0 x1 x2 ⟶ PNo_strict_lowerbd x0 x1 x3 (proof)
Theorem PNoEq_strict_imv^{PNoEq_strict_imv} : ∀ x0 x1 : ι → (ι → ο) → ο . ∀ x2 . ordinal x2 ⟶ ∀ x3 x4 : ι → ο . PNoEq_ x2 x3 x4 ⟶ PNo_strict_imv x0 x1 x2 x3 ⟶ PNo_strict_imv x0 x1 x2 x4 (proof)
Theorem PNo_strict_upperbd_imp_rel_strict_upperbd^{PNo_strict_upperbd_imp_rel_strict_upperbd} : ∀ x0 : ι → (ι → ο) → ο . ∀ x1 . ordinal x1 ⟶ ∀ x2 . x2 ∈ ordsucc x1 ⟶ ∀ x3 : ι → ο . PNo_strict_upperbd x0 x1 x3 ⟶ PNo_rel_strict_upperbd x0 x2 x3 (proof)
Theorem PNo_strict_lowerbd_imp_rel_strict_lowerbd^{PNo_strict_lowerbd_imp_rel_strict_lowerbd} : ∀ x0 : ι → (ι → ο) → ο . ∀ x1 . ordinal x1 ⟶ ∀ x2 . x2 ∈ ordsucc x1 ⟶ ∀ x3 : ι → ο . PNo_strict_lowerbd x0 x1 x3 ⟶ PNo_rel_strict_lowerbd x0 x2 x3 (proof)
Theorem 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 (proof)
Theorem 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 (proof)
Theorem ordinal_PNo_strict_imv^{ordinal_PNo_strict_imv} : ∀ x0 x1 : ι → (ι → ο) → ο . ∀ x2 . ordinal x2 ⟶ ∀ x3 : ι → ο . (∀ x4 . x4 ∈ x2 ⟶ x3 x4) ⟶ (∀ x4 . ordinal x4 ⟶ ∀ x5 : ι → ο . x0 x4 x5 ⟶ x4 ∈ x2) ⟶ (∀ x4 . x4 ∈ x2 ⟶ x0 x4 x3) ⟶ (∀ x4 . ordinal x4 ⟶ ∀ x5 : ι → ο . not (x1 x4 x5)) ⟶ PNo_strict_imv x0 x1 x2 x3 (proof)
Theorem PNo_lenbdd_strict_imv_ex^{PNo_lenbdd_strict_imv_ex} : ∀ x0 x1 : ι → (ι → ο) → ο . PNoLt_pwise x0 x1 ⟶ ∀ x2 . ordinal x2 ⟶ PNo_lenbdd x2 x0 ⟶ PNo_lenbdd x2 x1 ⟶ ∀ x3 : ο . (∀ x4 . and (x4 ∈ ordsucc x2) (∀ x5 : ο . (∀ x6 : ι → ο . PNo_strict_imv x0 x1 x4 x6 ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3 (proof)
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 least_ordinal_ex^{least_ordinal_ex} : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . and (ordinal x2) (x0 x2) ⟶ x1) ⟶ x1) ⟶ ∀ x1 : ο . (∀ x2 . and (and (ordinal x2) (x0 x2)) (∀ x3 . x3 ∈ x2 ⟶ not (x0 x3)) ⟶ x1) ⟶ x1
Theorem PNo_lenbdd_least_rep_ex^{PNo_lenbdd_least_rep_ex} : ∀ x0 x1 : ι → (ι → ο) → ο . PNoLt_pwise x0 x1 ⟶ ∀ x2 . ordinal x2 ⟶ PNo_lenbdd x2 x0 ⟶ PNo_lenbdd x2 x1 ⟶ ∀ x3 : ο . (∀ x4 . (∀ x5 : ο . (∀ x6 : ι → ο . PNo_least_rep x0 x1 x4 x6 ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3 (proof)
Definition PNo_least_rep2^{PNo_least_rep2} := λ x0 x1 : ι → (ι → ο) → ο . λ x2 . λ x3 : ι → ο . and (PNo_least_rep x0 x1 x2 x3) (∀ x4 . nIn x4 x2 ⟶ not (x3 x4))
Theorem PNo_strict_imv_pred_eq^{PNo_strict_imv_pred_eq} : ∀ x0 x1 : ι → (ι → ο) → ο . PNoLt_pwise x0 x1 ⟶ ∀ x2 . ordinal x2 ⟶ ∀ x3 x4 : ι → ο . PNo_least_rep x0 x1 x2 x3 ⟶ PNo_strict_imv x0 x1 x2 x4 ⟶ ∀ x5 . x5 ∈ x2 ⟶ iff (x3 x5) (x4 x5) (proof)
Known pred_ext^pred_ext : ∀ x0 x1 : ι → ο . (∀ x2 . iff (x0 x2) (x1 x2)) ⟶ x0 = x1
Theorem PNo_lenbdd_least_rep2_exuniq2^{PNo_lenbdd_least_rep2_exuniq2} : ∀ x0 x1 : ι → (ι → ο) → ο . PNoLt_pwise x0 x1 ⟶ ∀ x2 . ordinal x2 ⟶ PNo_lenbdd x2 x0 ⟶ PNo_lenbdd x2 x1 ⟶ ∀ x3 : ο . (∀ x4 . and (∀ x5 : ο . (∀ x6 : ι → ο . PNo_least_rep2 x0 x1 x4 x6 ⟶ x5) ⟶ x5) (∀ x5 x6 : ι → ο . PNo_least_rep2 x0 x1 x4 x5 ⟶ PNo_least_rep2 x0 x1 x4 x6 ⟶ x5 = x6) ⟶ x3) ⟶ x3 (proof)
Definition PNo_bd^PNo_bd := λ x0 x1 : ι → (ι → ο) → ο . DescrR_i_io_1 (PNo_least_rep2 x0 x1)
Definition PNo_pred^PNo_pred := λ x0 x1 : ι → (ι → ο) → ο . DescrR_i_io_2 (PNo_least_rep2 x0 x1)
Theorem PNo_bd_pred_lem^{PNo_bd_pred_lem} : ∀ x0 x1 : ι → (ι → ο) → ο . PNoLt_pwise x0 x1 ⟶ ∀ x2 . ordinal x2 ⟶ PNo_lenbdd x2 x0 ⟶ PNo_lenbdd x2 x1 ⟶ PNo_least_rep2 x0 x1 (PNo_bd x0 x1) (PNo_pred x0 x1) (proof)
Theorem 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) (proof)
Theorem PNo_bd_ord^PNo_bd_ord : ∀ x0 x1 : ι → (ι → ο) → ο . PNoLt_pwise x0 x1 ⟶ ∀ x2 . ordinal x2 ⟶ PNo_lenbdd x2 x0 ⟶ PNo_lenbdd x2 x1 ⟶ ordinal (PNo_bd x0 x1) (proof)
Theorem PNo_bd_pred_strict_imv^{PNo_bd_pred_strict_imv} : ∀ x0 x1 : ι → (ι → ο) → ο . PNoLt_pwise x0 x1 ⟶ ∀ x2 . ordinal x2 ⟶ PNo_lenbdd x2 x0 ⟶ PNo_lenbdd x2 x1 ⟶ PNo_strict_imv x0 x1 (PNo_bd x0 x1) (PNo_pred x0 x1) (proof)
Theorem PNo_bd_least_imv^{PNo_bd_least_imv} : ∀ x0 x1 : ι → (ι → ο) → ο . PNoLt_pwise x0 x1 ⟶ ∀ x2 . ordinal x2 ⟶ PNo_lenbdd x2 x0 ⟶ PNo_lenbdd x2 x1 ⟶ ∀ x3 . x3 ∈ PNo_bd x0 x1 ⟶ ∀ x4 : ι → ο . not (PNo_strict_imv x0 x1 x3 x4) (proof)
Known ordinal_In_Or_Subq^{ordinal_In_Or_Subq} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ or (x0 ∈ x1) (x1 ⊆ x0)
Theorem 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 (proof)
Definition PNoCutL^PNoCutL := λ x0 . λ x1 : ι → ο . λ x2 . λ x3 : ι → ο . and (x2 ∈ x0) (PNoLt x2 x3 x0 x1)
Definition PNoCutR^PNoCutR := λ x0 . λ x1 : ι → ο . λ x2 . λ x3 : ι → ο . and (x2 ∈ x0) (PNoLt x0 x1 x2 x3)
Theorem PNoCutL_lenbdd^{PNoCutL_lenbdd} : ∀ x0 . ∀ x1 : ι → ο . PNo_lenbdd x0 (PNoCutL x0 x1) (proof)
Theorem PNoCutR_lenbdd^{PNoCutR_lenbdd} : ∀ x0 . ∀ x1 : ι → ο . PNo_lenbdd x0 (PNoCutR x0 x1) (proof)
Theorem PNoCut_pwise^PNoCut_pwise : ∀ x0 . ordinal x0 ⟶ ∀ x1 : ι → ο . PNoLt_pwise (PNoCutL x0 x1) (PNoCutR x0 x1) (proof)
Theorem PNoCut_strict_imv^{PNoCut_strict_imv} : ∀ x0 . ordinal x0 ⟶ ∀ x1 : ι → ο . PNo_strict_imv (PNoCutL x0 x1) (PNoCutR x0 x1) x0 x1 (proof)
Theorem PNoCut_bd_eq^PNoCut_bd_eq : ∀ x0 . ordinal x0 ⟶ ∀ x1 : ι → ο . PNo_bd (PNoCutL x0 x1) (PNoCutR x0 x1) = x0 (proof)
Theorem PNoCut_pred_eq^{PNoCut_pred_eq} : ∀ x0 . ordinal x0 ⟶ ∀ x1 : ι → ο . PNoEq_ x0 x1 (PNo_pred (PNoCutL x0 x1) (PNoCutR x0 x1)) (proof)