Proofgold Address

Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Theorem exandE_i^exandE_i : ∀ x0 x1 : ι → ο . (∀ x2 : ο . (∀ x3 . and (x0 x3) (x1 x3) ⟶ x2) ⟶ x2) ⟶ ∀ x2 : ο . (∀ x3 . x0 x3 ⟶ x1 x3 ⟶ x2) ⟶ x2 (proof)
Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Definition If_Vo4^If_Vo4 := λ x0 : ο . λ x1 x2 : (((ι → ο) → ο) → ο) → ο . λ x3 : ((ι → ο) → ο) → ο . and (x0 ⟶ x1 x3) (not x0 ⟶ x2 x3)
Known prop_ext_2^prop_ext_2 : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ x0 = x1
Known andEL^andEL : ∀ x0 x1 : ο . and x0 x1 ⟶ x0
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Known notE^notE : ∀ x0 : ο . not x0 ⟶ x0 ⟶ False
Theorem If_Vo4_1^If_Vo4_1 : ∀ x0 : ο . ∀ x1 x2 : (((ι → ο) → ο) → ο) → ο . x0 ⟶ If_Vo4 x0 x1 x2 = x1 (proof)
Known andER^andER : ∀ x0 x1 : ο . and x0 x1 ⟶ x1
Theorem If_Vo4_0^If_Vo4_0 : ∀ x0 : ο . ∀ x1 x2 : (((ι → ο) → ο) → ο) → ο . not x0 ⟶ If_Vo4 x0 x1 x2 = x2 (proof)
Definition Descr_Vo4^Descr_Vo4 := λ x0 : ((((ι → ο) → ο) → ο) → ο) → ο . λ x1 : ((ι → ο) → ο) → ο . ∀ x2 : (((ι → ο) → ο) → ο) → ο . x0 x2 ⟶ x2 x1
Theorem Descr_Vo4_prop^{Descr_Vo4_prop} : ∀ x0 : ((((ι → ο) → ο) → ο) → ο) → ο . (∀ x1 : ο . (∀ x2 : (((ι → ο) → ο) → ο) → ο . x0 x2 ⟶ x1) ⟶ x1) ⟶ (∀ x1 x2 : (((ι → ο) → ο) → ο) → ο . x0 x1 ⟶ x0 x2 ⟶ x1 = x2) ⟶ x0 (Descr_Vo4 x0) (proof)
Definition 461b4.. := λ x0 : ι → (ι → (((ι → ο) → ο) → ο) → ο) → (((ι → ο) → ο) → ο) → ο . λ x1 . λ x2 : (((ι → ο) → ο) → ο) → ο . ∀ x3 : ι → ((((ι → ο) → ο) → ο) → ο) → ο . (∀ x4 . ∀ x5 : ι → (((ι → ο) → ο) → ο) → ο . (∀ x6 . x6 ∈ x4 ⟶ x3 x6 (x5 x6)) ⟶ x3 x4 (x0 x4 x5)) ⟶ x3 x1 x2
Definition In_rec_Vo4^In_rec_Vo4 := λ x0 : ι → (ι → (((ι → ο) → ο) → ο) → ο) → (((ι → ο) → ο) → ο) → ο . λ x1 . Descr_Vo4 (461b4.. x0 x1)
Theorem 23e18.. : ∀ x0 : ι → (ι → (((ι → ο) → ο) → ο) → ο) → (((ι → ο) → ο) → ο) → ο . ∀ x1 . ∀ x2 : ι → (((ι → ο) → ο) → ο) → ο . (∀ x3 . x3 ∈ x1 ⟶ 461b4.. x0 x3 (x2 x3)) ⟶ 461b4.. x0 x1 (x0 x1 x2) (proof)
Theorem 45e15.. : ∀ x0 : ι → (ι → (((ι → ο) → ο) → ο) → ο) → (((ι → ο) → ο) → ο) → ο . ∀ x1 . ∀ x2 : (((ι → ο) → ο) → ο) → ο . 461b4.. x0 x1 x2 ⟶ ∀ x3 : ο . (∀ x4 : ι → (((ι → ο) → ο) → ο) → ο . and (∀ x5 . x5 ∈ x1 ⟶ 461b4.. x0 x5 (x4 x5)) (x2 = x0 x1 x4) ⟶ x3) ⟶ x3 (proof)
Known In_ind^In_ind : ∀ x0 : ι → ο . (∀ x1 . (∀ x2 . x2 ∈ x1 ⟶ x0 x2) ⟶ x0 x1) ⟶ ∀ x1 . x0 x1
Theorem 87941.. : ∀ x0 : ι → (ι → (((ι → ο) → ο) → ο) → ο) → (((ι → ο) → ο) → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → (((ι → ο) → ο) → ο) → ο . (∀ x4 . x4 ∈ x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . ∀ x2 x3 : (((ι → ο) → ο) → ο) → ο . 461b4.. x0 x1 x2 ⟶ 461b4.. x0 x1 x3 ⟶ x2 = x3 (proof)
Theorem 6dcc7.. : ∀ x0 : ι → (ι → (((ι → ο) → ο) → ο) → ο) → (((ι → ο) → ο) → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → (((ι → ο) → ο) → ο) → ο . (∀ x4 . x4 ∈ x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 461b4.. x0 x1 (In_rec_Vo4 x0 x1) (proof)
Theorem 05f75.. : ∀ x0 : ι → (ι → (((ι → ο) → ο) → ο) → ο) → (((ι → ο) → ο) → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → (((ι → ο) → ο) → ο) → ο . (∀ x4 . x4 ∈ x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 461b4.. x0 x1 (x0 x1 (In_rec_Vo4 x0)) (proof)
Theorem In_rec_Vo4_eq^{In_rec_Vo4_eq} : ∀ x0 : ι → (ι → (((ι → ο) → ο) → ο) → ο) → (((ι → ο) → ο) → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → (((ι → ο) → ο) → ο) → ο . (∀ x4 . x4 ∈ x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . In_rec_Vo4 x0 x1 = x0 x1 (In_rec_Vo4 x0) (proof)
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known xm^xm : ∀ x0 : ο . or x0 (not x0)
Known orIR^orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Known orIL^orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Known not_and_or_demorgan^{not_and_or_demorgan} : ∀ x0 x1 : ο . not (and x0 x1) ⟶ or (not x0) (not x1)
Theorem eq_imp_or^eq_imp_or : (λ x1 x2 : ο . x1 ⟶ x2) = λ x1 : ο . or (not x1) (proof)
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Definition nIn^nIn := λ x0 x1 . not (x0 ∈ x1)
Known Subq_contra^Subq_contra : ∀ x0 x1 x2 . x0 ⊆ x1 ⟶ nIn x2 x1 ⟶ nIn x2 x0
Known set_ext^set_ext : ∀ x0 x1 . x0 ⊆ x1 ⟶ x1 ⊆ x0 ⟶ x0 = x1
Known Subq_Empty^Subq_Empty : ∀ x0 . 0 ⊆ x0
Known Empty_Subq_eq^{Empty_Subq_eq} : ∀ x0 . x0 ⊆ 0 ⟶ x0 = 0
Known Empty_eq^Empty_eq : ∀ x0 . (∀ x1 . nIn x1 x0) ⟶ x0 = 0
Known UnionE^UnionE : ∀ x0 x1 . x1 ∈ prim3 x0 ⟶ ∀ x2 : ο . (∀ x3 . and (x1 ∈ x3) (x3 ∈ x0) ⟶ x2) ⟶ x2
Known EmptyE^EmptyE : ∀ x0 . nIn x0 0
Known Union_Empty^Union_Empty : prim3 0 = 0
Known PowerE^PowerE : ∀ x0 x1 . x1 ∈ prim4 x0 ⟶ x1 ⊆ x0
Known Union_Power_Subq^{Union_Power_Subq} : ∀ x0 . prim3 (prim4 x0) ⊆ x0
Known ReplE_impred^ReplE_impred : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ prim5 x0 x1 ⟶ ∀ x3 : ο . (∀ x4 . x4 ∈ x0 ⟶ x2 = x1 x4 ⟶ x3) ⟶ x3
Known Repl_Empty^Repl_Empty : ∀ x0 : ι → ι . prim5 0 x0 = 0
Known ReplI^ReplI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ x1 x2 ∈ prim5 x0 x1
Known ReplEq_ext_sub^{ReplEq_ext_sub} : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x1 x3 = x2 x3) ⟶ prim5 x0 x1 ⊆ prim5 x0 x2
Known ReplEq_ext^ReplEq_ext : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x1 x3 = x2 x3) ⟶ prim5 x0 x1 = prim5 x0 x2
Param UPair^UPair : ι → ι → ι
Known UPairE^UPairE : ∀ x0 x1 x2 . x0 ∈ UPair x1 x2 ⟶ or (x0 = x1) (x0 = x2)
Known UPairI2^UPairI2 : ∀ x0 x1 . x1 ∈ UPair x0 x1
Known UPairI1^UPairI1 : ∀ x0 x1 . x0 ∈ UPair x0 x1
Known 93b47.. : ∀ x0 x1 . UPair x0 x1 ⊆ UPair x1 x0
Known UPair_com^UPair_com : ∀ x0 x1 . UPair x0 x1 = UPair x1 x0
Param binunion^binunion : ι → ι → ι
Param Sing^Sing : ι → ι
Definition SetAdjoin^SetAdjoin := λ x0 x1 . binunion x0 (Sing x1)
Known SingI^SingI : ∀ x0 . x0 ∈ Sing x0
Known SingE^SingE : ∀ x0 x1 . x1 ∈ Sing x0 ⟶ x1 = x0
Known Empty_In_Power^{Empty_In_Power} : ∀ x0 . 0 ∈ prim4 x0
Known Power_0_Sing_0^{Power_0_Sing_0} : prim4 0 = Sing 0
Known Repl_UPair^Repl_UPair : ∀ x0 : ι → ι . ∀ x1 x2 . prim5 (UPair x1 x2) x0 = UPair (x0 x1) (x0 x2)
Known Repl_Sing^Repl_Sing : ∀ x0 : ι → ι . ∀ x1 . prim5 (Sing x1) x0 = Sing (x0 x1)
Known ReplE^ReplE : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ prim5 x0 x1 ⟶ ∀ x3 : ο . (∀ x4 . and (x4 ∈ x0) (x2 = x1 x4) ⟶ x3) ⟶ x3
Known ReplEq_ext_sub^{ReplEq_ext_sub} : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x1 x3 = x2 x3) ⟶ prim5 x0 x1 ⊆ prim5 x0 x2
Known ReplEq_ext^ReplEq_ext : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x1 x3 = x2 x3) ⟶ prim5 x0 x1 = prim5 x0 x2
Definition famunion^famunion := λ x0 . λ x1 : ι → ι . prim3 (prim5 x0 x1)
Known UnionI^UnionI : ∀ x0 x1 x2 . x1 ∈ x2 ⟶ x2 ∈ x0 ⟶ x1 ∈ prim3 x0
Known famunionI^famunionI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . x2 ∈ x0 ⟶ x3 ∈ x1 x2 ⟶ x3 ∈ famunion x0 x1
Known UnionE_impred^{UnionE_impred} : ∀ x0 x1 . x1 ∈ prim3 x0 ⟶ ∀ x2 : ο . (∀ x3 . x1 ∈ x3 ⟶ x3 ∈ x0 ⟶ x2) ⟶ x2
Known famunionE^famunionE : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ famunion x0 x1 ⟶ ∀ x3 : ο . (∀ x4 . and (x4 ∈ x0) (x2 ∈ x1 x4) ⟶ x3) ⟶ x3
Known famunionE_impred^{famunionE_impred} : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ famunion x0 x1 ⟶ ∀ x3 : ο . (∀ x4 . x4 ∈ x0 ⟶ x2 ∈ x1 x4 ⟶ x3) ⟶ x3
Known UnionEq_famunionId^{UnionEq_famunionId} : ∀ x0 . prim3 x0 = famunion x0 (λ x2 . x2)
Known ReplEq_famunion_Sing^{ReplEq_famunion_Sing} : ∀ x0 . ∀ x1 : ι → ι . prim5 x0 x1 = famunion x0 (λ x3 . Sing (x1 x3))
Theorem Empty_or_ex^Empty_or_ex : ∀ x0 . or (x0 = 0) (∀ x1 : ο . (∀ x2 . x2 ∈ x0 ⟶ x1) ⟶ x1) (proof)