Proofgold Signed Transaction

Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition MetaCat_equalizer_p^equalizer_p := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 x5 x6 x7 x8 x9 . λ x10 : ι → ι → ι . and (and (and (and (and (and (and (x0 x4) (x0 x5)) (x1 x4 x5 x6)) (x1 x4 x5 x7)) (x0 x8)) (x1 x8 x4 x9)) (x3 x8 x4 x5 x6 x9 = x3 x8 x4 x5 x7 x9)) (∀ x11 . x0 x11 ⟶ ∀ x12 . x1 x11 x4 x12 ⟶ x3 x11 x4 x5 x6 x12 = x3 x11 x4 x5 x7 x12 ⟶ and (and (x1 x11 x8 (x10 x11 x12)) (x3 x11 x8 x4 x9 (x10 x11 x12) = x12)) (∀ x13 . x1 x11 x8 x13 ⟶ x3 x11 x8 x4 x9 x13 = x12 ⟶ x13 = x10 x11 x12))
Definition MetaCat_equalizer_struct_p^{equalizer_constr_p} := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 x5 : ι → ι → ι → ι → ι . λ x6 : ι → ι → ι → ι → ι → ι → ι . ∀ x7 x8 . x0 x7 ⟶ x0 x8 ⟶ ∀ x9 x10 . x1 x7 x8 x9 ⟶ x1 x7 x8 x10 ⟶ MetaCat_equalizer_p x0 x1 x2 x3 x7 x8 x9 x10 (x4 x7 x8 x9 x10) (x5 x7 x8 x9 x10) (x6 x7 x8 x9 x10)
Param Pi^Pi : ι → (ι → ι) → ι
Definition setexp^setexp := λ x0 x1 . Pi x1 (λ x2 . x0)
Definition HomSet^SetHom := λ x0 x1 x2 . x2 ∈ setexp x1 x0
Param lam^Sigma : ι → (ι → ι) → ι
Definition lam_id^lam_id := λ x0 . lam x0 (λ x1 . x1)
Param ap^ap : ι → ι → ι
Definition lam_comp^lam_comp := λ x0 x1 x2 . lam x0 (λ x3 . ap x1 (ap x2 x3))
Param Sep^Sep : ι → (ι → ο) → ι
Known 41253..^and8I : ∀ x0 x1 x2 x3 x4 x5 x6 x7 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ x5 ⟶ x6 ⟶ x7 ⟶ and (and (and (and (and (and (and x0 x1) x2) x3) x4) x5) x6) x7
Known Sep_Subq^Sep_Subq : ∀ x0 . ∀ x1 : ι → ο . Sep x0 x1 ⊆ x0
Known lam_Pi^lam_Pi : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x1 x3) ⟶ lam x0 x2 ∈ Pi x0 x1
Known SepE1^SepE1 : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ Sep x0 x1 ⟶ x2 ∈ x0
Known encode_u_ext^encode_u_ext : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x1 x3 = x2 x3) ⟶ lam x0 x1 = lam x0 x2
Known SepE2^SepE2 : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ Sep x0 x1 ⟶ x1 x2
Known and3I^and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Known SepI^SepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ x0 ⟶ x1 x2 ⟶ x2 ∈ Sep x0 x1
Known ap_Pi^ap_Pi : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . x2 ∈ Pi x0 x1 ⟶ x3 ∈ x0 ⟶ ap x2 x3 ∈ x1 x3
Known beta^beta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ ap (lam x0 x1) x2 = x1 x2
Known Pi_eta^Pi_eta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ Pi x0 x1 ⟶ lam x0 (ap x2) = x2
Theorem ae25c..^{MetaCatSet_equalizer_gen} : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ ∀ x2 . x2 ⊆ x1 ⟶ x0 x2) ⟶ ∀ x1 : ο . (∀ x2 : ι → ι → ι → ι → ι . (∀ x3 : ο . (∀ x4 : ι → ι → ι → ι → ι . (∀ x5 : ο . (∀ x6 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_struct_p x0 HomSet lam_id (λ x7 x8 x9 . lam_comp x7) x2 x4 x6 ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3) ⟶ x1) ⟶ x1 (proof)
Param ZF_closed^ZF_closed : ι → ο
Param Union_closed^Union_closed : ι → ο
Definition Power_closed^Power_closed := λ x0 . ∀ x1 . x1 ∈ x0 ⟶ prim4 x1 ∈ x0
Param Repl_closed^Repl_closed : ι → ο
Known ZF_closed_E^ZF_closed_E : ∀ x0 . ZF_closed x0 ⟶ ∀ x1 : ο . (Union_closed x0 ⟶ Power_closed x0 ⟶ Repl_closed x0 ⟶ x1) ⟶ x1
Known UnivOf_ZF_closed^{UnivOf_ZF_closed} : ∀ x0 . ZF_closed (prim6 x0)
Definition TransSet^TransSet := λ x0 . ∀ x1 . x1 ∈ x0 ⟶ x1 ⊆ x0
Known UnivOf_TransSet^{UnivOf_TransSet} : ∀ x0 . TransSet (prim6 x0)
Known PowerI^PowerI : ∀ x0 x1 . x1 ⊆ x0 ⟶ x1 ∈ prim4 x0
Theorem 03706..^{MetaCatHFSet_equalizer_gen} : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ ∀ x2 . x2 ⊆ x1 ⟶ x0 x2) ⟶ ∀ x1 : ο . (∀ x2 : ι → ι → ι → ι → ι . (∀ x3 : ο . (∀ x4 : ι → ι → ι → ι → ι . (∀ x5 : ο . (∀ x6 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_struct_p (λ x7 . x7 ∈ prim6 0) HomSet lam_id (λ x7 x8 x9 . lam_comp x7) x2 x4 x6 ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3) ⟶ x1) ⟶ x1 (proof)
Theorem 3d3ca..^{MetaCatSmallSet_equalizer_gen} : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ ∀ x2 . x2 ⊆ x1 ⟶ x0 x2) ⟶ ∀ x1 : ο . (∀ x2 : ι → ι → ι → ι → ι . (∀ x3 : ο . (∀ x4 : ι → ι → ι → ι → ι . (∀ x5 : ο . (∀ x6 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_struct_p (λ x7 . x7 ∈ prim6 (prim6 0)) HomSet lam_id (λ x7 x8 x9 . lam_comp x7) x2 x4 x6 ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3) ⟶ x1) ⟶ x1 (proof)
Param MetaCat^MetaCat : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → ο
Param setprod^setprod : ι → ι → ι
Param MetaCat_pullback_struct_p^{pullback_constr_p} : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι → ι → ι) → ο
Param MetaCat_product_constr_p^{product_constr_p} : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → ο
Known ed2b0..^{product_equalizer_pullback_constr_ex} : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . MetaCat x0 x1 x2 x3 ⟶ (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι . (∀ x8 : ο . (∀ x9 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_struct_p x0 x1 x2 x3 x5 x7 x9 ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι . (∀ x8 : ο . (∀ x9 : ι → ι → ι . (∀ x10 : ο . (∀ x11 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p x0 x1 x2 x3 x5 x7 x9 x11 ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ ∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . (∀ x8 : ο . (∀ x9 : ι → ι → ι → ι → ι → ι . (∀ x10 : ο . (∀ x11 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pullback_struct_p x0 x1 x2 x3 x5 x7 x9 x11 ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4
Known 21e78..^{MetaCatSet_product_gen} : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ ∀ x2 . x0 x2 ⟶ x0 (setprod x1 x2)) ⟶ ∀ x1 : ο . (∀ x2 : ι → ι → ι . (∀ x3 : ο . (∀ x4 : ι → ι → ι . (∀ x5 : ο . (∀ x6 : ι → ι → ι . (∀ x7 : ο . (∀ x8 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p x0 HomSet (λ x9 . lam x9 (λ x10 . x10)) (λ x9 x10 x11 x12 x13 . lam x9 (λ x14 . ap x12 (ap x13 x14))) x2 x4 x6 x8 ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3) ⟶ x1) ⟶ x1
Theorem a53be..^{MetaCatSet_pullback_gen} : ∀ x0 : ι → ο . MetaCat x0 HomSet lam_id (λ x1 x2 x3 . lam_comp x1) ⟶ (∀ x1 . x0 x1 ⟶ ∀ x2 . x2 ⊆ x1 ⟶ x0 x2) ⟶ (∀ x1 . x0 x1 ⟶ ∀ x2 . x0 x2 ⟶ x0 (setprod x1 x2)) ⟶ ∀ x1 : ο . (∀ x2 : ι → ι → ι → ι → ι → ι . (∀ x3 : ο . (∀ x4 : ι → ι → ι → ι → ι → ι . (∀ x5 : ο . (∀ x6 : ι → ι → ι → ι → ι → ι . (∀ x7 : ο . (∀ x8 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pullback_struct_p x0 HomSet lam_id (λ x9 x10 x11 . lam_comp x9) x2 x4 x6 x8 ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3) ⟶ x1) ⟶ x1 (proof)
Definition True^True := ∀ x0 : ο . x0 ⟶ x0
Known e4125..^MetaCatSet : MetaCat (λ x0 . True) HomSet lam_id (λ x0 x1 x2 . lam_comp x0)
Known TrueI^TrueI : True
Theorem fcaee..^{MetaCatSet_pullback} : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pullback_struct_p (λ x8 . True) HomSet lam_id (λ x8 x9 x10 . lam_comp x8) x1 x3 x5 x7 ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Known 2fb6a..^MetaCatHFSet : MetaCat (λ x0 . x0 ∈ prim6 0) HomSet lam_id (λ x0 x1 x2 . lam_comp x0)
Known ecfb5..^{ZF_setprod_closed} : ∀ x0 . TransSet x0 ⟶ ZF_closed x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ setprod x1 x2 ∈ x0
Theorem 2e08d..^{MetaCatHFSet_pullback} : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pullback_struct_p (λ x8 . x8 ∈ prim6 0) HomSet lam_id (λ x8 x9 x10 . lam_comp x8) x1 x3 x5 x7 ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Known 68978..^{MetaCatSmallSet} : MetaCat (λ x0 . x0 ∈ prim6 (prim6 0)) HomSet lam_id (λ x0 x1 x2 . lam_comp x0)
Theorem 596e3..^{MetaCatSmallSet_pullback} : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pullback_struct_p (λ x8 . x8 ∈ prim6 (prim6 0)) HomSet lam_id (λ x8 x9 x10 . lam_comp x8) x1 x3 x5 x7 ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Param ordsucc^ordsucc : ι → ι
Definition MetaCat_terminal_p^terminal_p := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 . λ x5 : ι → ι . and (x0 x4) (∀ x6 . x0 x6 ⟶ and (x1 x6 x4 (x5 x6)) (∀ x7 . x1 x6 x4 x7 ⟶ x7 = x5 x6))
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known In_0_1^In_0_1 : 0 ∈ 1
Param Sing^Sing : ι → ι
Known SingE^SingE : ∀ x0 x1 . x1 ∈ Sing x0 ⟶ x1 = x0
Known eq_1_Sing0^eq_1_Sing0 : 1 = Sing 0
Theorem ad19c.. : ∀ x0 : ι → ο . x0 1 ⟶ MetaCat_terminal_p x0 HomSet (λ x1 . lam x1 (λ x2 . x2)) (λ x1 x2 x3 x4 x5 . lam x1 (λ x6 . ap x4 (ap x5 x6))) 1 (λ x1 . lam x1 (λ x2 . 0)) (proof)
Definition MetaCat_monic_p^monic := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 x5 x6 . and (and (and (x0 x4) (x0 x5)) (x1 x4 x5 x6)) (∀ x7 . x0 x7 ⟶ ∀ x8 x9 . x1 x7 x4 x8 ⟶ x1 x7 x4 x9 ⟶ x3 x7 x4 x5 x6 x8 = x3 x7 x4 x5 x6 x9 ⟶ x8 = x9)
Definition MetaCat_pullback_p^pullback_p := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 x5 x6 x7 x8 x9 x10 x11 . λ x12 : ι → ι → ι → ι . and (and (and (and (and (and (and (and (and (x0 x4) (x0 x5)) (x0 x6)) (x1 x4 x6 x7)) (x1 x5 x6 x8)) (x0 x9)) (x1 x9 x4 x10)) (x1 x9 x5 x11)) (x3 x9 x4 x6 x7 x10 = x3 x9 x5 x6 x8 x11)) (∀ x13 . x0 x13 ⟶ ∀ x14 . x1 x13 x4 x14 ⟶ ∀ x15 . x1 x13 x5 x15 ⟶ x3 x13 x4 x6 x7 x14 = x3 x13 x5 x6 x8 x15 ⟶ and (and (and (x1 x13 x9 (x12 x13 x14 x15)) (x3 x13 x9 x4 x10 (x12 x13 x14 x15) = x14)) (x3 x13 x9 x5 x11 (x12 x13 x14 x15) = x15)) (∀ x16 . x1 x13 x9 x16 ⟶ x3 x13 x9 x4 x10 x16 = x14 ⟶ x3 x13 x9 x5 x11 x16 = x15 ⟶ x16 = x12 x13 x14 x15))
Definition MetaCat_subobject_classifier_p^{subobject_classifier_p} := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 . λ x5 : ι → ι . λ x6 x7 . λ x8 : ι → ι → ι → ι . λ x9 : ι → ι → ι → ι → ι → ι → ι . and (and (and (MetaCat_terminal_p x0 x1 x2 x3 x4 x5) (x0 x6)) (x1 x4 x6 x7)) (∀ x10 x11 x12 . MetaCat_monic_p x0 x1 x2 x3 x10 x11 x12 ⟶ and (x1 x11 x6 (x8 x10 x11 x12)) (MetaCat_pullback_p x0 x1 x2 x3 x4 x11 x6 x7 (x8 x10 x11 x12) x10 (x5 x10) x12 (x9 x10 x11 x12)))
Param If_i^If_i : ο → ι → ι → ι
Param inv^inv : ι → (ι → ι) → ι → ι
Known and4I^and4I : ∀ x0 x1 x2 x3 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ and (and (and x0 x1) x2) x3
Known In_1_2^In_1_2 : 1 ∈ 2
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known If_i_or^If_i_or : ∀ x0 : ο . ∀ x1 x2 . or (If_i x0 x1 x2 = x1) (If_i x0 x1 x2 = x2)
Known In_0_2^In_0_2 : 0 ∈ 2
Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Known 19e22..^and10I : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ x5 ⟶ x6 ⟶ x7 ⟶ x8 ⟶ x9 ⟶ and (and (and (and (and (and (and (and (and x0 x1) x2) x3) x4) x5) x6) x7) x8) x9
Known inj_linv^inj_linv : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 = x1 x3 ⟶ x2 = x3) ⟶ ∀ x2 . x2 ∈ x0 ⟶ inv x0 x1 (x1 x2) = x2
Known cases_1^cases_1 : ∀ x0 . x0 ∈ 1 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 x0
Known neq_0_1^neq_0_1 : 0 = 1 ⟶ ∀ x0 : ο . x0
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Known If_i_correct^If_i_correct : ∀ x0 : ο . ∀ x1 x2 . or (and x0 (If_i x0 x1 x2 = x1)) (and (not x0) (If_i x0 x1 x2 = x2))
Known orIL^orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Known orIR^orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Theorem bd9cd..^{MetaCatSet_subobject_classifier_gen} : ∀ x0 : ι → ο . x0 1 ⟶ x0 2 ⟶ MetaCat_subobject_classifier_p x0 HomSet lam_id (λ x1 x2 x3 . lam_comp x1) 1 (λ x1 . lam x1 (λ x2 . 0)) 2 (lam 1 (λ x1 . 1)) (λ x1 x2 x3 . lam x2 (λ x4 . If_i (∀ x5 : ο . (∀ x6 . and (x6 ∈ x1) (ap x3 x6 = x4) ⟶ x5) ⟶ x5) 1 0)) (λ x1 x2 x3 x4 x5 x6 . lam x4 (λ x7 . inv x1 (ap x3) (ap x6 x7))) (proof)
Theorem e5b47..^{MetaCatSet_subobject_classifier_gen_ex} : ∀ x0 : ι → ο . x0 1 ⟶ x0 2 ⟶ ∀ x1 : ο . (∀ x2 . (∀ x3 : ο . (∀ x4 : ι → ι . (∀ x5 : ο . (∀ x6 . (∀ x7 : ο . (∀ x8 . (∀ x9 : ο . (∀ x10 : ι → ι → ι → ι . (∀ x11 : ο . (∀ x12 : ι → ι → ι → ι → ι → ι → ι . MetaCat_subobject_classifier_p x0 HomSet lam_id (λ x13 x14 x15 . lam_comp x13) x2 x4 x6 x8 x10 x12 ⟶ x11) ⟶ x11) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3) ⟶ x1) ⟶ x1 (proof)
Theorem 25c26..^{MetaCatSet_subobject_classifier} : ∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . (∀ x4 : ο . (∀ x5 . (∀ x6 : ο . (∀ x7 . (∀ x8 : ο . (∀ x9 : ι → ι → ι → ι . (∀ x10 : ο . (∀ x11 : ι → ι → ι → ι → ι → ι → ι . MetaCat_subobject_classifier_p (λ x12 . True) HomSet lam_id (λ x12 x13 x14 . lam_comp x12) x1 x3 x5 x7 x9 x11 ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Param nat_p^nat_p : ι → ο
Known nat_p_UnivOf_Empty^{nat_p_UnivOf_Empty} : ∀ x0 . nat_p x0 ⟶ x0 ∈ prim6 0
Known nat_2^nat_2 : nat_p 2
Known nat_1^nat_1 : nat_p 1
Theorem 341a1..^{MetaCatHFSet_subobject_classifier} : ∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . (∀ x4 : ο . (∀ x5 . (∀ x6 : ο . (∀ x7 . (∀ x8 : ο . (∀ x9 : ι → ι → ι → ι . (∀ x10 : ο . (∀ x11 : ι → ι → ι → ι → ι → ι → ι . MetaCat_subobject_classifier_p (λ x12 . x12 ∈ prim6 0) HomSet lam_id (λ x12 x13 x14 . lam_comp x12) x1 x3 x5 x7 x9 x11 ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Known UnivOf_In^UnivOf_In : ∀ x0 . x0 ∈ prim6 x0
Theorem e892d.. : 1 ∈ prim6 (prim6 0) (proof)
Theorem f6173.. : 2 ∈ prim6 (prim6 0) (proof)
Theorem 7223a..^{MetaCatSmallSet_subobject_classifier} : ∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . (∀ x4 : ο . (∀ x5 . (∀ x6 : ο . (∀ x7 . (∀ x8 : ο . (∀ x9 : ι → ι → ι → ι . (∀ x10 : ο . (∀ x11 : ι → ι → ι → ι → ι → ι → ι . MetaCat_subobject_classifier_p (λ x12 . x12 ∈ prim6 (prim6 0)) HomSet lam_id (λ x12 x13 x14 . lam_comp x12) x1 x3 x5 x7 x9 x11 ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Param omega^omega : ι
Definition MetaCat_nno_p^nno_p := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 . λ x5 : ι → ι . λ x6 x7 x8 . λ x9 : ι → ι → ι → ι . and (and (and (and (MetaCat_terminal_p x0 x1 x2 x3 x4 x5) (x0 x6)) (x1 x4 x6 x7)) (x1 x6 x6 x8)) (∀ x10 x11 x12 . x0 x10 ⟶ x1 x4 x10 x11 ⟶ x1 x10 x10 x12 ⟶ and (and (and (x1 x6 x10 (x9 x10 x11 x12)) (x3 x4 x6 x10 (x9 x10 x11 x12) x7 = x11)) (x3 x6 x6 x10 (x9 x10 x11 x12) x8 = x3 x6 x10 x10 x12 (x9 x10 x11 x12))) (∀ x13 . x1 x6 x10 x13 ⟶ x3 x4 x6 x10 x13 x7 = x11 ⟶ x3 x6 x6 x10 x13 x8 = x3 x6 x10 x10 x12 x13 ⟶ x13 = x9 x10 x11 x12))
Param nat_primrec^nat_primrec : ι → (ι → ι → ι) → ι → ι
Known and5I^and5I : ∀ x0 x1 x2 x3 x4 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ and (and (and (and x0 x1) x2) x3) x4
Known omega_ordsucc^{omega_ordsucc} : ∀ x0 . x0 ∈ omega ⟶ ordsucc x0 ∈ omega
Known omega_nat_p^omega_nat_p : ∀ x0 . x0 ∈ omega ⟶ nat_p x0
Known nat_ind^nat_ind : ∀ x0 : ι → ο . x0 0 ⟶ (∀ x1 . nat_p x1 ⟶ x0 x1 ⟶ x0 (ordsucc x1)) ⟶ ∀ x1 . nat_p x1 ⟶ x0 x1
Known nat_primrec_0^{nat_primrec_0} : ∀ x0 . ∀ x1 : ι → ι → ι . nat_primrec x0 x1 0 = x0
Known nat_primrec_S^{nat_primrec_S} : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 . nat_p x2 ⟶ nat_primrec x0 x1 (ordsucc x2) = x1 x2 (nat_primrec x0 x1 x2)
Known nat_p_omega^nat_p_omega : ∀ x0 . nat_p x0 ⟶ x0 ∈ omega
Known nat_0^nat_0 : nat_p 0
Theorem ea037..^{MetaCatSet_nno_gen} : ∀ x0 : ι → ο . x0 1 ⟶ x0 omega ⟶ MetaCat_nno_p x0 HomSet lam_id (λ x1 x2 x3 . lam_comp x1) 1 (λ x1 . lam x1 (λ x2 . 0)) omega (lam 1 (λ x1 . 0)) (lam omega ordsucc) (λ x1 x2 x3 . lam omega (nat_primrec (ap x2 0) (λ x4 . ap x3))) (proof)
Theorem 1051b..^{MetaCatSet_nno_gen_ex} : ∀ x0 : ι → ο . x0 1 ⟶ x0 omega ⟶ ∀ x1 : ο . (∀ x2 . (∀ x3 : ο . (∀ x4 : ι → ι . (∀ x5 : ο . (∀ x6 . (∀ x7 : ο . (∀ x8 . (∀ x9 : ο . (∀ x10 . (∀ x11 : ο . (∀ x12 : ι → ι → ι → ι . MetaCat_nno_p x0 HomSet lam_id (λ x13 x14 x15 . lam_comp x13) x2 x4 x6 x8 x10 x12 ⟶ x11) ⟶ x11) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3) ⟶ x1) ⟶ x1 (proof)
Theorem 0e563..^{MetaCatSet_nno} : ∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . (∀ x4 : ο . (∀ x5 . (∀ x6 : ο . (∀ x7 . (∀ x8 : ο . (∀ x9 . (∀ x10 : ο . (∀ x11 : ι → ι → ι → ι . MetaCat_nno_p (λ x12 . True) HomSet lam_id (λ x12 x13 x14 . lam_comp x12) x1 x3 x5 x7 x9 x11 ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Theorem 7b79d.. : omega ∈ prim6 (prim6 0) (proof)
Theorem 833b6..^{MetaCatSmallSet_nno} : ∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . (∀ x4 : ο . (∀ x5 . (∀ x6 : ο . (∀ x7 . (∀ x8 : ο . (∀ x9 . (∀ x10 : ο . (∀ x11 : ι → ι → ι → ι . MetaCat_nno_p (λ x12 . x12 ∈ prim6 (prim6 0)) HomSet lam_id (λ x12 x13 x14 . lam_comp x12) x1 x3 x5 x7 x9 x11 ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)