Proofgold Address

Param lam^Sigma : ι → (ι → ι) → ι
Param ordsucc^ordsucc : ι → ι
Param If_i^If_i : ο → ι → ι → ι
Param setsum^setsum : ι → ι → ι
Known pair_tuple_fun^{pair_tuple_fun} : setsum = λ x1 x2 . lam 2 (λ x3 . If_i (x3 = 0) x1 x2)
Known tupleI0^tupleI0 : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ lam 2 (λ x3 . If_i (x3 = 0) 0 x2) ∈ lam 2 (λ x3 . If_i (x3 = 0) x0 x1)
Theorem a08f4.. : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ lam 2 (λ x3 . If_i (x3 = 0) 0 x2) ∈ setsum x0 x1 (proof)
Known tupleI1^tupleI1 : ∀ x0 x1 x2 . x2 ∈ x1 ⟶ lam 2 (λ x3 . If_i (x3 = 0) 1 x2) ∈ lam 2 (λ x3 . If_i (x3 = 0) x0 x1)
Theorem 40b22.. : ∀ x0 x1 x2 . x2 ∈ x1 ⟶ lam 2 (λ x3 . If_i (x3 = 0) 1 x2) ∈ setsum x0 x1 (proof)
Param Pi^Pi : ι → (ι → ι) → ι
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Known set_ext^set_ext : ∀ x0 x1 . x0 ⊆ x1 ⟶ x1 ⊆ x0 ⟶ x0 = x1
Known Pi_cod_mon^Pi_cod_mon : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x1 x3 ⊆ x2 x3) ⟶ Pi x0 x1 ⊆ Pi x0 x2
Theorem 28e5a.. : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x1 x3 = x2 x3) ⟶ Pi x0 x1 = Pi x0 x2 (proof)
Definition setprod^setprod := λ x0 x1 . lam x0 (λ x2 . x1)
Definition setexp^setexp := λ x0 x1 . Pi x1 (λ x2 . x0)
Param and^and : ο → ο → ο
Definition MetaCat_product_p^product_p := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 x5 x6 x7 x8 . λ x9 : ι → ι → ι → ι . and (and (and (and (and (x0 x4) (x0 x5)) (x0 x6)) (x1 x6 x4 x7)) (x1 x6 x5 x8)) (∀ x10 . x0 x10 ⟶ ∀ x11 x12 . x1 x10 x4 x11 ⟶ x1 x10 x5 x12 ⟶ and (and (and (x1 x10 x6 (x9 x10 x11 x12)) (x3 x10 x6 x4 x7 (x9 x10 x11 x12) = x11)) (x3 x10 x6 x5 x8 (x9 x10 x11 x12) = x12)) (∀ x13 . x1 x10 x6 x13 ⟶ x3 x10 x6 x4 x7 x13 = x11 ⟶ x3 x10 x6 x5 x8 x13 = x12 ⟶ x13 = x9 x10 x11 x12))
Definition MetaCat_product_constr_p^{product_constr_p} := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 x5 x6 : ι → ι → ι . λ x7 : ι → ι → ι → ι → ι → ι . ∀ x8 x9 . x0 x8 ⟶ x0 x9 ⟶ MetaCat_product_p x0 x1 x2 x3 x8 x9 (x4 x8 x9) (x5 x8 x9) (x6 x8 x9) (x7 x8 x9)
Definition MetaCat_exp_p^exponent_p := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 x5 x6 : ι → ι → ι . λ x7 : ι → ι → ι → ι → ι → ι . λ x8 x9 x10 x11 . λ x12 : ι → ι → ι . and (and (and (and (x0 x8) (x0 x9)) (x0 x10)) (x1 (x4 x10 x8) x9 x11)) (∀ x13 . x0 x13 ⟶ ∀ x14 . x1 (x4 x13 x8) x9 x14 ⟶ and (and (x1 x13 x10 (x12 x13 x14)) (x3 (x4 x13 x8) (x4 x10 x8) x9 x11 (x7 x10 x8 (x4 x13 x8) (x3 (x4 x13 x8) x13 x10 (x12 x13 x14) (x5 x13 x8)) (x6 x13 x8)) = x14)) (∀ x15 . x1 x13 x10 x15 ⟶ x3 (x4 x13 x8) (x4 x10 x8) x9 x11 (x7 x10 x8 (x4 x13 x8) (x3 (x4 x13 x8) x13 x10 x15 (x5 x13 x8)) (x6 x13 x8)) = x14 ⟶ x15 = x12 x13 x14))
Definition MetaCat_exp_constr_p^{product_exponent_constr_p} := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 x5 x6 : ι → ι → ι . λ x7 : ι → ι → ι → ι → ι → ι . λ x8 x9 : ι → ι → ι . λ x10 : ι → ι → ι → ι → ι . and (MetaCat_product_constr_p x0 x1 x2 x3 x4 x5 x6 x7) (∀ x11 x12 . x0 x11 ⟶ x0 x12 ⟶ MetaCat_exp_p x0 x1 x2 x3 x4 x5 x6 x7 x11 x12 (x8 x11 x12) (x9 x11 x12) (x10 x11 x12))
Definition HomSet^SetHom := λ x0 x1 x2 . x2 ∈ setexp x1 x0
Param lam_id^lam_id : ι → ι
Param ap^ap : ι → ι → ι
Definition lam_comp^lam_comp := λ x0 x1 x2 . lam x0 (λ x3 . ap x1 (ap x2 x3))
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known and6I^and6I : ∀ x0 x1 x2 x3 x4 x5 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ x5 ⟶ and (and (and (and (and x0 x1) x2) x3) x4) x5
Known lam_Pi^lam_Pi : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x1 x3) ⟶ lam x0 x2 ∈ Pi x0 x1
Known ap0_Sigma^ap0_Sigma : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ lam x0 x1 ⟶ ap x2 0 ∈ x0
Known ap1_Sigma^ap1_Sigma : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ lam x0 x1 ⟶ ap x2 1 ∈ x1 (ap x2 0)
Known and4I^and4I : ∀ x0 x1 x2 x3 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ and (and (and x0 x1) x2) x3
Known encode_u_ext^encode_u_ext : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x1 x3 = x2 x3) ⟶ lam x0 x1 = lam x0 x2
Known beta^beta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ ap (lam x0 x1) x2 = x1 x2
Known tuple_2_0_eq^tuple_2_0_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 0 = x0
Known Pi_eta^Pi_eta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ Pi x0 x1 ⟶ lam x0 (ap x2) = x2
Known tuple_2_1_eq^tuple_2_1_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 1 = x1
Known tuple_Sigma_eta^{tuple_Sigma_eta} : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ lam x0 x1 ⟶ lam 2 (λ x4 . If_i (x4 = 0) (ap x2 0) (ap x2 1)) = x2
Known ap_Pi^ap_Pi : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . x2 ∈ Pi x0 x1 ⟶ x3 ∈ x0 ⟶ ap x2 x3 ∈ x1 x3
Known tuple_2_setprod^{tuple_2_setprod} : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x1 ⟶ lam 2 (λ x4 . If_i (x4 = 0) x2 x3) ∈ setprod x0 x1
Known and5I^and5I : ∀ x0 x1 x2 x3 x4 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ and (and (and (and x0 x1) x2) x3) x4
Known and3I^and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Known 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
Theorem 37ab0..^{MetaCatSet_product_exponent_gen_setprod_setexp} : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ ∀ x2 . x0 x2 ⟶ x0 (setprod x1 x2)) ⟶ (∀ x1 . x0 x1 ⟶ ∀ x2 . x0 x2 ⟶ x0 (setexp x2 x1)) ⟶ MetaCat_exp_constr_p x0 HomSet lam_id (λ x1 x2 x3 . lam_comp x1) setprod (λ x1 x2 . lam (setprod x1 x2) (λ x3 . ap x3 0)) (λ x1 x2 . lam (setprod x1 x2) (λ x3 . ap x3 1)) (λ x1 x2 x3 x4 x5 . lam x3 (λ x6 . lam 2 (λ x7 . If_i (x7 = 0) (ap x4 x6) (ap x5 x6)))) (λ x1 x2 . setexp x2 x1) (λ x1 x2 . lam (setprod (setexp x2 x1) x1) (λ x3 . ap (ap x3 0) (ap x3 1))) (λ x1 x2 x3 x4 . lam x3 (λ x5 . lam x1 (λ x6 . ap x4 (lam 2 (λ x7 . If_i (x7 = 0) x5 x6))))) (proof)
Theorem 32b3d..^{MetaCatSet_product_exponent_gen} : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ ∀ x2 . x0 x2 ⟶ x0 (setprod x1 x2)) ⟶ (∀ x1 . x0 x1 ⟶ ∀ x2 . x0 x2 ⟶ x0 (setexp x2 x1)) ⟶ ∀ x1 : ο . (∀ x2 : ι → ι → ι . (∀ x3 : ο . (∀ x4 : ι → ι → ι . (∀ x5 : ο . (∀ x6 : ι → ι → ι . (∀ x7 : ο . (∀ x8 : ι → ι → ι → ι → ι → ι . (∀ x9 : ο . (∀ x10 : ι → ι → ι . (∀ x11 : ο . (∀ x12 : ι → ι → ι . (∀ x13 : ο . (∀ x14 : ι → ι → ι → ι → ι . MetaCat_exp_constr_p x0 HomSet lam_id (λ x15 x16 x17 . lam_comp x15) x2 x4 x6 x8 x10 x12 x14 ⟶ x13) ⟶ x13) ⟶ x11) ⟶ x11) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3) ⟶ x1) ⟶ x1 (proof)
Definition True^True := ∀ x0 : ο . x0 ⟶ x0
Known TrueI^TrueI : True
Theorem 1810c..^{MetaCatSet_product_exponent} : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . (∀ x8 : ο . (∀ x9 : ι → ι → ι . (∀ x10 : ο . (∀ x11 : ι → ι → ι . (∀ x12 : ο . (∀ x13 : ι → ι → ι → ι → ι . MetaCat_exp_constr_p (λ x14 . True) HomSet lam_id (λ x14 x15 x16 . lam_comp x14) x1 x3 x5 x7 x9 x11 x13 ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Param TransSet^TransSet : ι → ο
Param ZF_closed^ZF_closed : ι → ο
Known 33118..^{ZF_setexp_closed} : ∀ x0 . TransSet x0 ⟶ ZF_closed x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ setexp x2 x1 ∈ x0
Known UnivOf_TransSet^{UnivOf_TransSet} : ∀ x0 . TransSet (prim6 x0)
Known UnivOf_ZF_closed^{UnivOf_ZF_closed} : ∀ x0 . ZF_closed (prim6 x0)
Known ecfb5..^{ZF_setprod_closed} : ∀ x0 . TransSet x0 ⟶ ZF_closed x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ setprod x1 x2 ∈ x0
Theorem 29786..^{MetaCatHFSet_product_exponent} : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . (∀ x8 : ο . (∀ x9 : ι → ι → ι . (∀ x10 : ο . (∀ x11 : ι → ι → ι . (∀ x12 : ο . (∀ x13 : ι → ι → ι → ι → ι . MetaCat_exp_constr_p (λ x14 . x14 ∈ prim6 0) HomSet lam_id (λ x14 x15 x16 . lam_comp x14) x1 x3 x5 x7 x9 x11 x13 ⟶ x12) ⟶ x12) ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)