Proofgold Address

Param famunion^famunion : ι → (ι → ι) → ι
Param setsum^setsum : ι → ι → ι
Definition lam^Sigma := λ x0 . λ x1 : ι → ι . famunion x0 (λ x2 . prim5 (x1 x2) (setsum x2))
Known famunionI^famunionI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . x2 ∈ x0 ⟶ x3 ∈ x1 x2 ⟶ x3 ∈ famunion x0 x1
Known ReplI^ReplI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ x1 x2 ∈ prim5 x0 x1
Theorem lamI^lamI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x1 x2 ⟶ setsum x2 x3 ∈ lam x0 x1 (proof)
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Param proj0^proj0 : ι → ι
Param proj1^proj1 : ι → ι
Known exandE_i^exandE_i : ∀ x0 x1 : ι → ο . (∀ x2 : ο . (∀ x3 . and (x0 x3) (x1 x3) ⟶ x2) ⟶ x2) ⟶ ∀ x2 : ο . (∀ x3 . x0 x3 ⟶ x1 x3 ⟶ x2) ⟶ x2
Known ReplE_impred^ReplE_impred : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ prim5 x0 x1 ⟶ ∀ x3 : ο . (∀ x4 . x4 ∈ x0 ⟶ x2 = x1 x4 ⟶ x3) ⟶ x3
Known proj0_pair_eq^{proj0_pair_eq} : ∀ x0 x1 . proj0 (setsum x0 x1) = x0
Known proj1_pair_eq^{proj1_pair_eq} : ∀ x0 x1 . proj1 (setsum x0 x1) = x1
Known and3I^and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Known famunionE^famunionE : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ famunion x0 x1 ⟶ ∀ x3 : ο . (∀ x4 . and (x4 ∈ x0) (x2 ∈ x1 x4) ⟶ x3) ⟶ x3
Theorem Sigma_eta_proj0_proj1^{Sigma_eta_proj0_proj1} : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ lam x0 x1 ⟶ and (and (setsum (proj0 x2) (proj1 x2) = x2) (proj0 x2 ∈ x0)) (proj1 x2 ∈ x1 (proj0 x2)) (proof)
Known and3E^and3E : ∀ x0 x1 x2 : ο . and (and x0 x1) x2 ⟶ ∀ x3 : ο . (x0 ⟶ x1 ⟶ x2 ⟶ x3) ⟶ x3
Theorem proj_Sigma_eta^{proj_Sigma_eta} : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ lam x0 x1 ⟶ setsum (proj0 x2) (proj1 x2) = x2 (proof)
Theorem proj0_Sigma^proj0_Sigma : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ lam x0 x1 ⟶ proj0 x2 ∈ x0 (proof)
Theorem proj1_Sigma^proj1_Sigma : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ lam x0 x1 ⟶ proj1 x2 ∈ x1 (proj0 x2) (proof)
Theorem pair_Sigma_E0^{pair_Sigma_E0} : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . setsum x2 x3 ∈ lam x0 x1 ⟶ x2 ∈ x0 (proof)
Theorem pair_Sigma_E1^{pair_Sigma_E1} : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . setsum x2 x3 ∈ lam x0 x1 ⟶ x3 ∈ x1 x2 (proof)
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem 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 (proof)
Definition iff^iff := λ x0 x1 : ο . and (x0 ⟶ x1) (x1 ⟶ x0)
Known iffI^iffI : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ iff x0 x1
Theorem lamEq^lamEq : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . iff (x2 ∈ lam x0 x1) (∀ x3 : ο . (∀ x4 . and (x4 ∈ x0) (∀ x5 : ο . (∀ x6 . and (x6 ∈ x1 x4) (x2 = setsum x4 x6) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3) (proof)
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Theorem Sigma_mon^Sigma_mon : ∀ x0 x1 . x0 ⊆ x1 ⟶ ∀ x2 x3 : ι → ι . (∀ x4 . x4 ∈ x0 ⟶ x2 x4 ⊆ x3 x4) ⟶ lam x0 x2 ⊆ lam x1 x3 (proof)
Known Subq_ref^Subq_ref : ∀ x0 . x0 ⊆ x0
Theorem Sigma_mon0^Sigma_mon0 : ∀ x0 x1 . x0 ⊆ x1 ⟶ ∀ x2 : ι → ι . lam x0 x2 ⊆ lam x1 x2 (proof)
Theorem Sigma_mon1^Sigma_mon1 : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x1 x3 ⊆ x2 x3) ⟶ lam x0 x1 ⊆ lam x0 x2 (proof)
Param ordsucc^ordsucc : ι → ι
Known PowerI^PowerI : ∀ x0 x1 . x1 ⊆ x0 ⟶ x1 ∈ prim4 x0
Known In_0_1^In_0_1 : 0 ∈ 1
Known setsum_0_0^setsum_0_0 : setsum 0 0 = 0
Param Sing^Sing : ι → ι
Known SingE^SingE : ∀ x0 x1 . x1 ∈ Sing x0 ⟶ x1 = x0
Known Subq_1_Sing0^Subq_1_Sing0 : 1 ⊆ Sing 0
Known PowerE^PowerE : ∀ x0 x1 . x1 ∈ prim4 x0 ⟶ x1 ⊆ x0
Theorem Sigma_Power_1^{Sigma_Power_1} : ∀ x0 . x0 ∈ prim4 1 ⟶ ∀ x1 : ι → ι . (∀ x2 . x2 ∈ x0 ⟶ x1 x2 ∈ prim4 1) ⟶ lam x0 x1 ∈ prim4 1 (proof)
Definition setprod^setprod := λ x0 x1 . lam x0 (λ x2 . x1)
Theorem pair_setprod^pair_setprod : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x1 ⟶ setsum x2 x3 ∈ setprod x0 x1 (proof)
Theorem proj0_setprod^{proj0_setprod} : ∀ x0 x1 x2 . x2 ∈ setprod x0 x1 ⟶ proj0 x2 ∈ x0 (proof)
Theorem proj1_setprod^{proj1_setprod} : ∀ x0 x1 x2 . x2 ∈ setprod x0 x1 ⟶ proj1 x2 ∈ x1 (proof)
Theorem pair_setprod_E0^{pair_setprod_E0} : ∀ x0 x1 x2 x3 . setsum x2 x3 ∈ setprod x0 x1 ⟶ x2 ∈ x0 (proof)
Theorem pair_setprod_E1^{pair_setprod_E1} : ∀ x0 x1 x2 x3 . setsum x2 x3 ∈ setprod x0 x1 ⟶ x3 ∈ x1 (proof)
Param ReplSep^ReplSep : ι → (ι → ο) → (ι → ι) → ι
Definition ap^ap := λ x0 x1 . ReplSep x0 (λ x2 . ∀ x3 : ο . (∀ x4 . x2 = setsum x1 x4 ⟶ x3) ⟶ x3) proj1
Known ReplSepI^ReplSepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 : ι → ι . ∀ x3 . x3 ∈ x0 ⟶ x1 x3 ⟶ x2 x3 ∈ ReplSep x0 x1 x2
Theorem apI^apI : ∀ x0 x1 x2 . setsum x1 x2 ∈ x0 ⟶ x2 ∈ ap x0 x1 (proof)
Known ReplSepE_impred^{ReplSepE_impred} : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 : ι → ι . ∀ x3 . x3 ∈ ReplSep x0 x1 x2 ⟶ ∀ x4 : ο . (∀ x5 . x5 ∈ x0 ⟶ x1 x5 ⟶ x3 = x2 x5 ⟶ x4) ⟶ x4
Theorem apE^apE : ∀ x0 x1 x2 . x2 ∈ ap x0 x1 ⟶ setsum x1 x2 ∈ x0 (proof)
Theorem apEq^apEq : ∀ x0 x1 x2 . iff (x2 ∈ ap x0 x1) (setsum x1 x2 ∈ x0) (proof)
Known set_ext^set_ext : ∀ x0 x1 . x0 ⊆ x1 ⟶ x1 ⊆ x0 ⟶ x0 = x1
Theorem beta^beta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ ap (lam x0 x1) x2 = x1 x2 (proof)
Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Definition nIn^nIn := λ x0 x1 . not (x0 ∈ x1)
Known Empty_eq^Empty_eq : ∀ x0 . (∀ x1 . nIn x1 x0) ⟶ x0 = 0
Theorem beta0^beta0 : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . nIn x2 x0 ⟶ ap (lam x0 x1) x2 = 0 (proof)
Known proj0E^proj0E : ∀ x0 x1 . x1 ∈ proj0 x0 ⟶ setsum 0 x1 ∈ x0
Known proj0I^proj0I : ∀ x0 x1 . setsum 0 x1 ∈ x0 ⟶ x1 ∈ proj0 x0
Theorem proj0_ap_0^proj0_ap_0 : ∀ x0 . proj0 x0 = ap x0 0 (proof)
Known proj1E^proj1E : ∀ x0 x1 . x1 ∈ proj1 x0 ⟶ setsum 1 x1 ∈ x0
Known proj1I^proj1I : ∀ x0 x1 . setsum 1 x1 ∈ x0 ⟶ x1 ∈ proj1 x0
Theorem proj1_ap_1^proj1_ap_1 : ∀ x0 . proj1 x0 = ap x0 1 (proof)
Theorem pair_ap_0^pair_ap_0 : ∀ x0 x1 . ap (setsum x0 x1) 0 = x0 (proof)
Theorem pair_ap_1^pair_ap_1 : ∀ x0 x1 . ap (setsum x0 x1) 1 = x1 (proof)
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known pairE^pairE : ∀ x0 x1 x2 . x2 ∈ setsum x0 x1 ⟶ or (∀ x3 : ο . (∀ x4 . and (x4 ∈ x0) (x2 = setsum 0 x4) ⟶ x3) ⟶ x3) (∀ x3 : ο . (∀ x4 . and (x4 ∈ x1) (x2 = setsum 1 x4) ⟶ x3) ⟶ x3)
Known pair_inj^pair_inj : ∀ x0 x1 x2 x3 . setsum x0 x1 = setsum x2 x3 ⟶ and (x0 = x2) (x1 = x3)
Known In_0_2^In_0_2 : 0 ∈ 2
Known In_1_2^In_1_2 : 1 ∈ 2
Theorem pair_ap_n2^pair_ap_n2 : ∀ x0 x1 x2 . nIn x2 2 ⟶ ap (setsum x0 x1) x2 = 0 (proof)
Theorem ap0_Sigma^ap0_Sigma : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ lam x0 x1 ⟶ ap x2 0 ∈ x0 (proof)
Theorem ap1_Sigma^ap1_Sigma : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ lam x0 x1 ⟶ ap x2 1 ∈ x1 (ap x2 0) (proof)
Definition pair_p^pair_p := λ x0 . setsum (ap x0 0) (ap x0 1) = x0
Theorem pair_p_I^pair_p_I : ∀ x0 x1 . pair_p (setsum x0 x1) (proof)
Param UPair^UPair : ι → ι → ι
Known UPairE^UPairE : ∀ x0 x1 x2 . x0 ∈ UPair x1 x2 ⟶ or (x0 = x1) (x0 = x2)
Known pairI0^pairI0 : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ setsum 0 x2 ∈ setsum x0 x1
Known pairI1^pairI1 : ∀ x0 x1 x2 . x2 ∈ x1 ⟶ setsum 1 x2 ∈ setsum x0 x1
Known Subq_2_UPair01^{Subq_2_UPair01} : 2 ⊆ UPair 0 1
Theorem pair_p_I2^pair_p_I2 : ∀ x0 . (∀ x1 . x1 ∈ x0 ⟶ and (pair_p x1) (ap x1 0 ∈ 2)) ⟶ pair_p x0 (proof)
Theorem pair_p_In_ap^pair_p_In_ap : ∀ x0 x1 . pair_p x0 ⟶ x0 ∈ x1 ⟶ ap x0 1 ∈ ap x1 (ap x0 0) (proof)
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
Known pred_ext_2^pred_ext_2 : ∀ x0 x1 : ι → ο . (∀ x2 . x0 x2 ⟶ x1 x2) ⟶ (∀ x2 . x1 x2 ⟶ x0 x2) ⟶ x0 = x1
Theorem pair_p_tuple2^{pair_p_tuple2} : pair_p = tuple_p 2 (proof)
Param If_i^If_i : ο → ι → ι → ι
Theorem tuple_p_2_tuple^{tuple_p_2_tuple} : ∀ x0 x1 . tuple_p 2 (lam 2 (λ x2 . If_i (x2 = 0) x0 x1)) (proof)
Known If_i_1^If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0 ⟶ If_i x0 x1 x2 = x1
Known If_i_0^If_i_0 : ∀ x0 : ο . ∀ x1 x2 . not x0 ⟶ If_i x0 x1 x2 = x2
Known neq_1_0^neq_1_0 : 1 = 0 ⟶ ∀ x0 : ο . x0
Theorem tuple_pair^tuple_pair : ∀ x0 x1 . setsum x0 x1 = lam 2 (λ x3 . If_i (x3 = 0) x0 x1) (proof)
Param Sep^Sep : ι → (ι → ο) → ι
Definition Pi^Pi := λ x0 . λ x1 : ι → ι . {x2 ∈ prim4 (lam x0 (λ x2 . prim3 (x1 x2)))|∀ x3 . x3 ∈ x0 ⟶ ap x2 x3 ∈ x1 x3}
Known SepI^SepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ x0 ⟶ x1 x2 ⟶ x2 ∈ Sep x0 x1
Known UnionI^UnionI : ∀ x0 x1 x2 . x1 ∈ x2 ⟶ x2 ∈ x0 ⟶ x1 ∈ prim3 x0
Theorem PiI^PiI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . (∀ x3 . x3 ∈ x2 ⟶ and (pair_p x3) (ap x3 0 ∈ x0)) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ap x2 x3 ∈ x1 x3) ⟶ x2 ∈ Pi x0 x1 (proof)
Known SepE^SepE : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ Sep x0 x1 ⟶ and (x2 ∈ x0) (x1 x2)
Theorem PiE^PiE : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ Pi x0 x1 ⟶ and (∀ x3 . x3 ∈ x2 ⟶ and (pair_p x3) (ap x3 0 ∈ x0)) (∀ x3 . x3 ∈ x0 ⟶ ap x2 x3 ∈ x1 x3) (proof)
Theorem PiEq^PiEq : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . iff (x2 ∈ Pi x0 x1) (and (∀ x3 . x3 ∈ x2 ⟶ and (pair_p x3) (ap x3 0 ∈ x0)) (∀ x3 . x3 ∈ x0 ⟶ ap x2 x3 ∈ x1 x3)) (proof)
Theorem lam_Pi^lam_Pi : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x1 x3) ⟶ lam x0 x2 ∈ Pi x0 x1 (proof)
Known SepE2^SepE2 : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ Sep x0 x1 ⟶ x1 x2
Theorem ap_Pi^ap_Pi : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . x2 ∈ Pi x0 x1 ⟶ x3 ∈ x0 ⟶ ap x2 x3 ∈ x1 x3 (proof)
Theorem Pi_ext_Subq^Pi_ext_Subq : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ Pi x0 x1 ⟶ ∀ x3 . x3 ∈ Pi x0 x1 ⟶ (∀ x4 . x4 ∈ x0 ⟶ ap x2 x4 ⊆ ap x3 x4) ⟶ x2 ⊆ x3 (proof)
Theorem Pi_ext^Pi_ext : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ Pi x0 x1 ⟶ ∀ x3 . x3 ∈ Pi x0 x1 ⟶ (∀ x4 . x4 ∈ x0 ⟶ ap x2 x4 = ap x3 x4) ⟶ x2 = x3 (proof)
Theorem Pi_eta^Pi_eta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ Pi x0 x1 ⟶ lam x0 (ap x2) = x2 (proof)
Definition setexp^setexp := λ x0 x1 . Pi x1 (λ x2 . x0)
Theorem pair_tuple_fun^{pair_tuple_fun} : setsum = λ x1 x2 . lam 2 (λ x3 . If_i (x3 = 0) x1 x2) (proof)
Theorem tuple_2_Sigma^{tuple_2_Sigma} : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x1 x2 ⟶ lam 2 (λ x4 . If_i (x4 = 0) x2 x3) ∈ lam x0 x1 (proof)
Theorem lamE2^lamE2 : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ lam x0 x1 ⟶ ∀ x3 : ο . (∀ x4 . and (x4 ∈ x0) (∀ x5 : ο . (∀ x6 . and (x6 ∈ x1 x4) (x2 = lam 2 (λ x8 . If_i (x8 = 0) x4 x6)) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3 (proof)
Theorem 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) (proof)
Theorem tuple_2_0_eq^tuple_2_0_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 0 = x0 (proof)
Theorem tuple_2_1_eq^tuple_2_1_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 1 = x1 (proof)
Definition Sep2^Sep2 := λ x0 . λ x1 : ι → ι . λ x2 : ι → ι → ο . {x3 ∈ lam x0 x1|x2 (ap x3 0) (ap x3 1)}
Theorem Sep2I^Sep2I : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x1 x3 ⟶ x2 x3 x4 ⟶ lam 2 (λ x5 . If_i (x5 = 0) x3 x4) ∈ Sep2 x0 x1 x2 (proof)
Theorem Sep2E^Sep2E : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 . x3 ∈ Sep2 x0 x1 x2 ⟶ ∀ x4 : ο . (∀ x5 . and (x5 ∈ x0) (∀ x6 : ο . (∀ x7 . and (x7 ∈ x1 x5) (and (x3 = lam 2 (λ x9 . If_i (x9 = 0) x5 x7)) (x2 x5 x7)) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4 (proof)
Theorem Sep2E'^Sep2E : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 x4 . lam 2 (λ x5 . If_i (x5 = 0) x3 x4) ∈ Sep2 x0 x1 x2 ⟶ and (and (x3 ∈ x0) (x4 ∈ x1 x3)) (x2 x3 x4) (proof)
Theorem Sep2E'1^Sep2E1 : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 x4 . lam 2 (λ x5 . If_i (x5 = 0) x3 x4) ∈ Sep2 x0 x1 x2 ⟶ x3 ∈ x0 (proof)
Theorem Sep2E'2^Sep2E2 : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 x4 . lam 2 (λ x5 . If_i (x5 = 0) x3 x4) ∈ Sep2 x0 x1 x2 ⟶ x4 ∈ x1 x3 (proof)
Theorem Sep2E'3^Sep2E3 : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 x4 . lam 2 (λ x5 . If_i (x5 = 0) x3 x4) ∈ Sep2 x0 x1 x2 ⟶ x2 x3 x4 (proof)
Definition set_of_pairs^set_of_pairs := λ x0 . ∀ x1 . x1 ∈ x0 ⟶ ∀ x2 : ο . (∀ x3 . (∀ x4 : ο . (∀ x5 . x1 = lam 2 (λ x7 . If_i (x7 = 0) x3 x5) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2
Theorem set_of_pairs_ext^{set_of_pairs_ext} : ∀ x0 x1 . set_of_pairs x0 ⟶ set_of_pairs x1 ⟶ (∀ x2 x3 . iff (lam 2 (λ x4 . If_i (x4 = 0) x2 x3) ∈ x0) (lam 2 (λ x4 . If_i (x4 = 0) x2 x3) ∈ x1)) ⟶ x0 = x1 (proof)
Theorem Sep2_set_of_pairs^{Sep2_set_of_pairs} : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . set_of_pairs (Sep2 x0 x1 x2) (proof)
Theorem Sep2_ext^Sep2_ext : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 : ι → ι → ο . (∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x1 x4 ⟶ iff (x2 x4 x5) (x3 x4 x5)) ⟶ Sep2 x0 x1 x2 = Sep2 x0 x1 x3 (proof)
Theorem lam_ext_sub^lam_ext_sub : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x1 x3 = x2 x3) ⟶ lam x0 x1 ⊆ lam x0 x2 (proof)
Theorem encode_u_ext^encode_u_ext : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x1 x3 = x2 x3) ⟶ lam x0 x1 = lam x0 x2 (proof)
Theorem lam_eta^lam_eta : ∀ x0 . ∀ x1 : ι → ι . lam x0 (ap (lam x0 x1)) = lam x0 x1 (proof)
Theorem tuple_2_eta^tuple_2_eta : ∀ x0 x1 . lam 2 (ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1))) = lam 2 (λ x3 . If_i (x3 = 0) x0 x1) (proof)
Definition lam2^lam2 := λ x0 . λ x1 : ι → ι . λ x2 : ι → ι → ι . lam x0 (λ x3 . lam (x1 x3) (x2 x3))
Theorem beta2^beta2 : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ι . ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x1 x3 ⟶ ap (ap (lam2 x0 x1 x2) x3) x4 = x2 x3 x4 (proof)
Theorem lam2_ext^lam2_ext : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 : ι → ι → ι . (∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x1 x4 ⟶ x2 x4 x5 = x3 x4 x5) ⟶ lam2 x0 x1 x2 = lam2 x0 x1 x3 (proof)
Definition lam^Sigma := lam
Definition ap^ap := ap
Definition encode_b^encode_b := λ x0 . lam2 x0 (λ x1 . x0)
Definition decode_b^decode_b := λ x0 x1 . ap (ap x0 x1)
Definition decode_p^decode_p := λ x0 x1 . x1 ∈ x0
Definition encode_r^encode_r := λ x0 . Sep2 x0 (λ x1 . x0)
Definition decode_r^decode_r := λ x0 x1 x2 . lam 2 (λ x3 . If_i (x3 = 0) x1 x2) ∈ x0
Definition encode_c^encode_c := λ x0 . λ x1 : (ι → ο) → ο . {x2 ∈ prim4 x0|x1 (λ x3 . x3 ∈ x2)}
Definition decode_c^decode_c := λ x0 . λ x1 : ι → ο . ∀ x2 : ο . (∀ x3 . and (∀ x4 . iff (x1 x4) (x4 ∈ x3)) (x3 ∈ x0) ⟶ x2) ⟶ x2
Theorem decode_encode_b^{decode_encode_b} : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ decode_b (encode_b x0 x1) x2 x3 = x1 x2 x3 (proof)
Theorem encode_b_ext^encode_b_ext : ∀ x0 . ∀ x1 x2 : ι → ι → ι . (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x1 x3 x4 = x2 x3 x4) ⟶ encode_b x0 x1 = encode_b x0 x2 (proof)
Known prop_ext_2^prop_ext_2 : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ x0 = x1
Theorem decode_encode_p^{decode_encode_p} : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ x0 ⟶ decode_p (Sep x0 x1) x2 = x1 x2 (proof)
Theorem encode_p_ext^encode_p_ext : ∀ x0 . ∀ x1 x2 : ι → ο . (∀ x3 . x3 ∈ x0 ⟶ iff (x1 x3) (x2 x3)) ⟶ Sep x0 x1 = Sep x0 x2 (proof)
Theorem decode_encode_r^{decode_encode_r} : ∀ x0 . ∀ x1 : ι → ι → ο . ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ decode_r (encode_r x0 x1) x2 x3 = x1 x2 x3 (proof)
Theorem encode_r_ext^encode_r_ext : ∀ x0 . ∀ x1 x2 : ι → ι → ο . (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ iff (x1 x3 x4) (x2 x3 x4)) ⟶ encode_r x0 x1 = encode_r x0 x2 (proof)
Known Sep_In_Power^Sep_In_Power : ∀ x0 . ∀ x1 : ι → ο . Sep x0 x1 ∈ prim4 x0
Theorem decode_encode_c^{decode_encode_c} : ∀ x0 . ∀ x1 : (ι → ο) → ο . ∀ x2 : ι → ο . (∀ x3 . x2 x3 ⟶ x3 ∈ x0) ⟶ decode_c (encode_c x0 x1) x2 = x1 x2 (proof)
Theorem encode_c_ext^encode_c_ext : ∀ x0 . ∀ x1 x2 : (ι → ο) → ο . (∀ x3 : ι → ο . (∀ x4 . x3 x4 ⟶ x4 ∈ x0) ⟶ iff (x1 x3) (x2 x3)) ⟶ encode_c x0 x1 = encode_c x0 x2 (proof)