Proofgold Address

Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Param setsum^setsum : ι → ι → ι
Definition tuple_p^tuple_p := λ x0 x1 . ∀ x2 . x2 ∈ x1 ⟶ ∀ x3 : ο . (∀ x4 . and (x4 ∈ x0) (∀ x5 : ο . (∀ x6 . x2 = setsum x4 x6 ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3
Param lam^Sigma : ι → (ι → ι) → ι
Param ap^ap : ι → ι → ι
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Known set_ext^set_ext : ∀ x0 x1 . x0 ⊆ x1 ⟶ x1 ⊆ x0 ⟶ x0 = x1
Known lamI^lamI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x1 x2 ⟶ setsum x2 x3 ∈ lam x0 x1
Known apI^apI : ∀ x0 x1 x2 . setsum x1 x2 ∈ x0 ⟶ x2 ∈ ap x0 x1
Known lamE^lamE : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ lam x0 x1 ⟶ ∀ x3 : ο . (∀ x4 . and (x4 ∈ x0) (∀ x5 : ο . (∀ x6 . and (x6 ∈ x1 x4) (x2 = setsum x4 x6) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3
Known apE^apE : ∀ x0 x1 x2 . x2 ∈ ap x0 x1 ⟶ setsum x1 x2 ∈ x0
Theorem 47a16.. : ∀ x0 x1 . tuple_p x0 x1 ⟶ x1 = lam x0 (ap x1) (proof)
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem 55df5.. : ∀ x0 . ∀ x1 : ι → ι . tuple_p x0 (lam x0 x1) (proof)
Param ordsucc^ordsucc : ι → ι
Param If_i^If_i : ο → ι → ι → ι
Definition 59caa.. := λ x0 . λ x1 : ι → ι . λ x2 . ∀ x3 : ι → ο . (∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . tuple_p (x1 x4) x5 ⟶ (∀ x6 . x6 ∈ x1 x4 ⟶ x3 (ap x5 x6)) ⟶ x3 (lam 2 (λ x6 . If_i (x6 = 0) x4 x5))) ⟶ x3 x2
Theorem 83bd8.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . tuple_p (x1 x2) x3 ⟶ (∀ x4 . x4 ∈ x1 x2 ⟶ 59caa.. x0 x1 (ap x3 x4)) ⟶ 59caa.. x0 x1 (lam 2 (λ x4 . If_i (x4 = 0) x2 x3)) (proof)
Theorem 32b0a.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ο . (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . tuple_p (x1 x3) x4 ⟶ (∀ x5 . x5 ∈ x1 x3 ⟶ 59caa.. x0 x1 (ap x4 x5)) ⟶ (∀ x5 . x5 ∈ x1 x3 ⟶ x2 (ap x4 x5)) ⟶ x2 (lam 2 (λ x5 . If_i (x5 = 0) x3 x4))) ⟶ ∀ x3 . 59caa.. x0 x1 x3 ⟶ x2 x3 (proof)
Param ZF_closed^ZF_closed : ι → ο
Param nat_p^nat_p : ι → ο
Known nat_ind^nat_ind : ∀ x0 : ι → ο . x0 0 ⟶ (∀ x1 . nat_p x1 ⟶ x0 x1 ⟶ x0 (ordsucc x1)) ⟶ ∀ x1 . nat_p x1 ⟶ x0 x1
Known ZF_ordsucc_closed^{ZF_ordsucc_closed} : ∀ x0 . ZF_closed x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ ordsucc x1 ∈ x0
Theorem ebd65.. : ∀ x0 . ZF_closed x0 ⟶ 0 ∈ x0 ⟶ ∀ x1 . nat_p x1 ⟶ x1 ∈ x0 (proof)
Definition TransSet^TransSet := λ x0 . ∀ x1 . x1 ∈ x0 ⟶ x1 ⊆ x0
Known c59b3..^{ZF_Sigma_closed} : ∀ x0 . TransSet x0 ⟶ ZF_closed x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ ∀ x2 : ι → ι . (∀ x3 . x3 ∈ x1 ⟶ x2 x3 ∈ x0) ⟶ lam x1 x2 ∈ x0
Theorem b6a89.. : ∀ x0 . TransSet x0 ⟶ ZF_closed x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . tuple_p x1 x2 ⟶ (∀ x3 . x3 ∈ x1 ⟶ ap x2 x3 ∈ x0) ⟶ x2 ∈ x0 (proof)
Known nat_2^nat_2 : nat_p 2
Known tuple_p_2_tuple^{tuple_p_2_tuple} : ∀ x0 x1 . tuple_p 2 (lam 2 (λ x2 . If_i (x2 = 0) x0 x1))
Known cases_2^cases_2 : ∀ x0 . x0 ∈ 2 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 x0
Known tuple_2_0_eq^tuple_2_0_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 0 = x0
Known tuple_2_1_eq^tuple_2_1_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 1 = x1
Theorem 9f645.. : ∀ x0 . TransSet x0 ⟶ ZF_closed x0 ⟶ 0 ∈ x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ ∀ x2 : ι → ι . (∀ x3 . x3 ∈ x1 ⟶ x2 x3 ∈ x0) ⟶ ∀ x3 . 59caa.. x1 x2 x3 ⟶ x3 ∈ x0 (proof)
Param Sep^Sep : ι → (ι → ο) → ι
Param UPair^UPair : ι → ι → ι
Param famunion^famunion : ι → (ι → ι) → ι
Param Sing^Sing : ι → ι
Definition c8f46.. := λ x0 . λ x1 : ι → ι . Sep (prim6 (UPair x0 (famunion x0 (λ x2 . Sing (x1 x2))))) (59caa.. x0 x1)
Known SepE2^SepE2 : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ Sep x0 x1 ⟶ x1 x2
Theorem 0bd77.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ c8f46.. x0 x1 ⟶ 59caa.. x0 x1 x2 (proof)
Known SepI^SepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ x0 ⟶ x1 x2 ⟶ x2 ∈ Sep x0 x1
Known UnivOf_TransSet^{UnivOf_TransSet} : ∀ x0 . TransSet (prim6 x0)
Known UnivOf_ZF_closed^{UnivOf_ZF_closed} : ∀ x0 . ZF_closed (prim6 x0)
Known 6aa34..^{UnivOf_Subq_closed} : ∀ x0 x1 . x1 ∈ prim6 x0 ⟶ ∀ x2 . x2 ⊆ x1 ⟶ x2 ∈ prim6 x0
Known UnivOf_In^UnivOf_In : ∀ x0 . x0 ∈ prim6 x0
Known Subq_Empty^Subq_Empty : ∀ x0 . 0 ⊆ x0
Known famunionI^famunionI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . x2 ∈ x0 ⟶ x3 ∈ x1 x2 ⟶ x3 ∈ famunion x0 x1
Known SingI^SingI : ∀ x0 . x0 ∈ Sing x0
Known UPairI2^UPairI2 : ∀ x0 x1 . x1 ∈ UPair x0 x1
Known UPairI1^UPairI1 : ∀ x0 x1 . x0 ∈ UPair x0 x1
Theorem 2224e.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . 59caa.. x0 x1 x2 ⟶ x2 ∈ c8f46.. x0 x1 (proof)
Theorem 4db94.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . tuple_p (x1 x2) x3 ⟶ (∀ x4 . x4 ∈ x1 x2 ⟶ ap x3 x4 ∈ c8f46.. x0 x1) ⟶ lam 2 (λ x4 . If_i (x4 = 0) x2 x3) ∈ c8f46.. x0 x1 (proof)
Theorem 34323.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ο . (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . tuple_p (x1 x3) x4 ⟶ (∀ x5 . x5 ∈ x1 x3 ⟶ ap x4 x5 ∈ c8f46.. x0 x1) ⟶ (∀ x5 . x5 ∈ x1 x3 ⟶ x2 (ap x4 x5)) ⟶ x2 (lam 2 (λ x5 . If_i (x5 = 0) x3 x4))) ⟶ ∀ x3 . x3 ∈ c8f46.. x0 x1 ⟶ x2 x3 (proof)
Definition c40a3.. := λ x0 . λ x1 : ι → ι . λ x2 : ι → ι → ι → ι . λ x3 x4 . ∀ x5 : ι → ι → ο . (∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . tuple_p (x1 x6) x7 ⟶ ∀ x8 : ι → ι . (∀ x9 . x9 ∈ x1 x6 ⟶ x5 (ap x7 x9) (x8 x9)) ⟶ x5 (lam 2 (λ x9 . If_i (x9 = 0) x6 x7)) (x2 x6 x7 (lam (x1 x6) x8))) ⟶ x5 x3 x4
Theorem d7522.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ι → ι . ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . tuple_p (x1 x3) x4 ⟶ ∀ x5 : ι → ι . (∀ x6 . x6 ∈ x1 x3 ⟶ c40a3.. x0 x1 x2 (ap x4 x6) (x5 x6)) ⟶ c40a3.. x0 x1 x2 (lam 2 (λ x6 . If_i (x6 = 0) x3 x4)) (x2 x3 x4 (lam (x1 x3) x5)) (proof)
Theorem 0e173.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ι → ι . ∀ x3 : ι → ι → ο . (∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . tuple_p (x1 x4) x5 ⟶ ∀ x6 : ι → ι . (∀ x7 . x7 ∈ x1 x4 ⟶ c40a3.. x0 x1 x2 (ap x5 x7) (x6 x7)) ⟶ (∀ x7 . x7 ∈ x1 x4 ⟶ x3 (ap x5 x7) (x6 x7)) ⟶ x3 (lam 2 (λ x7 . If_i (x7 = 0) x4 x5)) (x2 x4 x5 (lam (x1 x4) x6))) ⟶ ∀ x4 x5 . c40a3.. x0 x1 x2 x4 x5 ⟶ x3 x4 x5 (proof)
Known Eps_i_ex^Eps_i_ex : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . x0 x2 ⟶ x1) ⟶ x1) ⟶ x0 (prim0 x0)
Theorem 4d5b3.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ι → ι . ∀ x3 . x3 ∈ c8f46.. x0 x1 ⟶ ∀ x4 : ο . (∀ x5 . c40a3.. x0 x1 x2 x3 x5 ⟶ x4) ⟶ x4 (proof)
Definition e2778.. := λ x0 . λ x1 : ι → ι . λ x2 : ι → ι → ι → ι . λ x3 . prim0 (c40a3.. x0 x1 x2 x3)
Theorem be97b.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ι → ι . ∀ x3 . x3 ∈ c8f46.. x0 x1 ⟶ c40a3.. x0 x1 x2 x3 (e2778.. x0 x1 x2 x3) (proof)
Known tuple_2_inj^tuple_2_inj : ∀ x0 x1 x2 x3 . lam 2 (λ x5 . If_i (x5 = 0) x0 x1) = lam 2 (λ x5 . If_i (x5 = 0) x2 x3) ⟶ and (x0 = x2) (x1 = x3)
Known encode_u_ext^encode_u_ext : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x1 x3 = x2 x3) ⟶ lam x0 x1 = lam x0 x2
Theorem 9a9e0.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ι → ι . ∀ x3 . x3 ∈ c8f46.. x0 x1 ⟶ ∀ x4 . c40a3.. x0 x1 x2 x3 x4 ⟶ ∀ x5 x6 . c40a3.. x0 x1 x2 x5 x6 ⟶ x3 = x5 ⟶ x4 = x6 (proof)
Theorem 2ca51.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ι → ι . ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . tuple_p (x1 x3) x4 ⟶ (∀ x5 . x5 ∈ x1 x3 ⟶ ap x4 x5 ∈ c8f46.. x0 x1) ⟶ e2778.. x0 x1 x2 (lam 2 (λ x6 . If_i (x6 = 0) x3 x4)) = x2 x3 x4 (lam (x1 x3) (λ x6 . e2778.. x0 x1 x2 (ap x4 x6))) (proof)