Proofgold Address

Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Param lam^Sigma : ι → (ι → ι) → ι
Definition setprod^setprod := λ x0 x1 . lam x0 (λ x2 . x1)
Known Sigma_mon^Sigma_mon : ∀ x0 x1 . x0 ⊆ x1 ⟶ ∀ x2 x3 : ι → ι . (∀ x4 . x4 ∈ x0 ⟶ x2 x4 ⊆ x3 x4) ⟶ lam x0 x2 ⊆ lam x1 x3
Theorem setprod_mon^setprod_mon : ∀ x0 x1 . x0 ⊆ x1 ⟶ ∀ x2 x3 . x2 ⊆ x3 ⟶ setprod x0 x2 ⊆ setprod x1 x3 (proof)
Known Sigma_mon0^Sigma_mon0 : ∀ x0 x1 . x0 ⊆ x1 ⟶ ∀ x2 : ι → ι . lam x0 x2 ⊆ lam x1 x2
Theorem setprod_mon0^setprod_mon0 : ∀ x0 x1 . x0 ⊆ x1 ⟶ ∀ x2 . setprod x0 x2 ⊆ setprod x1 x2 (proof)
Known Subq_ref^Subq_ref : ∀ x0 . x0 ⊆ x0
Theorem setprod_mon1^setprod_mon1 : ∀ x0 x1 x2 . x1 ⊆ x2 ⟶ setprod x0 x1 ⊆ setprod x0 x2 (proof)
Param setsum^setsum : ι → ι → ι
Param ap^ap : ι → ι → ι
Param ordsucc^ordsucc : ι → ι
Param proj0^proj0 : ι → ι
Known proj0_ap_0^proj0_ap_0 : ∀ x0 . proj0 x0 = ap x0 0
Param proj1^proj1 : ι → ι
Known proj1_ap_1^proj1_ap_1 : ∀ x0 . proj1 x0 = ap x0 1
Known pair_eta_Subq_proj^{pair_eta_Subq_proj} : ∀ x0 . setsum (proj0 x0) (proj1 x0) ⊆ x0
Theorem pair_eta_Subq^{pair_eta_Subq} : ∀ x0 . setsum (ap x0 0) (ap x0 1) ⊆ x0 (proof)
Known proj_Sigma_eta^{proj_Sigma_eta} : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ lam x0 x1 ⟶ setsum (proj0 x2) (proj1 x2) = x2
Theorem Sigma_eta^Sigma_eta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ lam x0 x1 ⟶ setsum (ap x2 0) (ap x2 1) = x2 (proof)
Known ReplEq_ext^ReplEq_ext : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x1 x3 = x2 x3) ⟶ prim5 x0 x1 = prim5 x0 x2
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)
Theorem ReplEq_setprod_ext^{ReplEq_setprod_ext} : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . (∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x1 ⟶ x2 x4 x5 = x3 x4 x5) ⟶ {x2 (ap x5 0) (ap x5 1)|x5 ∈ setprod x0 x1} = {x3 (ap x5 0) (ap x5 1)|x5 ∈ setprod x0 x1} (proof)
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
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 If_i^If_i : ο → ι → ι → ι
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 andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and 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
Theorem tuple_p_3_tuple^{tuple_p_3_tuple} : ∀ x0 x1 x2 . tuple_p 3 (lam 3 (λ x3 . If_i (x3 = 0) x0 (If_i (x3 = 1) x1 x2))) (proof)
Theorem tuple_p_4_tuple^{tuple_p_4_tuple} : ∀ x0 x1 x2 x3 . tuple_p 4 (lam 4 (λ x4 . If_i (x4 = 0) x0 (If_i (x4 = 1) x1 (If_i (x4 = 2) x2 x3)))) (proof)
Param Pi^Pi : ι → (ι → ι) → ι
Known PowerI^PowerI : ∀ x0 x1 . x1 ⊆ x0 ⟶ x1 ∈ prim4 x0
Known In_0_1^In_0_1 : 0 ∈ 1
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
Definition pair_p^pair_p := λ x0 . setsum (ap x0 0) (ap x0 1) = x0
Known 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)
Param Sing^Sing : ι → ι
Known EmptyE^EmptyE : ∀ x0 . nIn x0 0
Known apI^apI : ∀ x0 x1 x2 . setsum x1 x2 ∈ x0 ⟶ x2 ∈ ap x0 x1
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 Pi_Power_1^Pi_Power_1 : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . x2 ∈ x0 ⟶ x1 x2 ∈ prim4 1) ⟶ Pi x0 x1 ∈ prim4 1 (proof)
Known 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
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known xm^xm : ∀ x0 : ο . or x0 (not x0)
Known Pi_eta^Pi_eta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ Pi x0 x1 ⟶ lam x0 (ap x2) = x2
Known beta0^beta0 : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . nIn x2 x0 ⟶ ap (lam x0 x1) x2 = 0
Theorem Pi_0_dom_mon^Pi_0_dom_mon : ∀ x0 x1 . ∀ x2 : ι → ι . x0 ⊆ x1 ⟶ (∀ x3 . x3 ∈ x1 ⟶ nIn x3 x0 ⟶ 0 ∈ x2 x3) ⟶ Pi x0 x2 ⊆ Pi x1 x2 (proof)
Theorem Pi_cod_mon^Pi_cod_mon : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x1 x3 ⊆ x2 x3) ⟶ Pi x0 x1 ⊆ Pi x0 x2 (proof)
Known Subq_tra^Subq_tra : ∀ x0 x1 x2 . x0 ⊆ x1 ⟶ x1 ⊆ x2 ⟶ x0 ⊆ x2
Theorem Pi_0_mon^Pi_0_mon : ∀ x0 x1 . ∀ x2 x3 : ι → ι . (∀ x4 . x4 ∈ x0 ⟶ x2 x4 ⊆ x3 x4) ⟶ x0 ⊆ x1 ⟶ (∀ x4 . x4 ∈ x1 ⟶ nIn x4 x0 ⟶ 0 ∈ x3 x4) ⟶ Pi x0 x2 ⊆ Pi x1 x3 (proof)
Definition setexp^setexp := λ x0 x1 . Pi x1 (λ x2 . x0)
Known set_ext^set_ext : ∀ x0 x1 . x0 ⊆ x1 ⟶ x1 ⊆ x0 ⟶ x0 = x1
Known and3E^and3E : ∀ x0 x1 x2 : ο . and (and x0 x1) x2 ⟶ ∀ x3 : ο . (x0 ⟶ x1 ⟶ x2 ⟶ x3) ⟶ x3
Known 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))
Known tuple_pair^tuple_pair : ∀ x0 x1 . setsum x0 x1 = lam 2 (λ x3 . If_i (x3 = 0) x0 x1)
Known lam_Pi^lam_Pi : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x1 x3) ⟶ lam x0 x2 ∈ Pi x0 x1
Known If_i_or^If_i_or : ∀ x0 : ο . ∀ x1 x2 . or (If_i x0 x1 x2 = x1) (If_i x0 x1 x2 = x2)
Known lamI^lamI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x1 x2 ⟶ setsum x2 x3 ∈ lam x0 x1
Known In_0_2^In_0_2 : 0 ∈ 2
Known In_1_2^In_1_2 : 1 ∈ 2
Known pair_p_I2^pair_p_I2 : ∀ x0 . (∀ x1 . x1 ∈ x0 ⟶ and (pair_p x1) (ap x1 0 ∈ 2)) ⟶ pair_p x0
Theorem setexp_2_eq^setexp_2_eq : ∀ x0 . setprod x0 x0 = setexp x0 2 (proof)
Theorem setexp_0_dom_mon^{setexp_0_dom_mon} : ∀ x0 . 0 ∈ x0 ⟶ ∀ x1 x2 . x1 ⊆ x2 ⟶ setexp x0 x1 ⊆ setexp x0 x2 (proof)
Theorem setexp_0_mon^setexp_0_mon : ∀ x0 x1 x2 x3 . 0 ∈ x3 ⟶ x2 ⊆ x3 ⟶ x0 ⊆ x1 ⟶ setexp x2 x0 ⊆ setexp x3 x1 (proof)
Param nat_p^nat_p : ι → ο
Known nat_trans^nat_trans : ∀ x0 . nat_p x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ x1 ⊆ x0
Theorem nat_in_setexp_mon^{nat_in_setexp_mon} : ∀ x0 . 0 ∈ x0 ⟶ ∀ x1 . nat_p x1 ⟶ ∀ x2 . x2 ∈ x1 ⟶ setexp x0 x2 ⊆ setexp x0 x1 (proof)
Known pair_tuple_fun^{pair_tuple_fun} : setsum = λ x1 x2 . lam 2 (λ x3 . If_i (x3 = 0) x1 x2)
Known pairI0^pairI0 : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ setsum 0 x2 ∈ setsum x0 x1
Theorem 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) (proof)
Known pairI1^pairI1 : ∀ x0 x1 x2 . x2 ∈ x1 ⟶ setsum 1 x2 ∈ setsum x0 x1
Theorem 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) (proof)
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)
Theorem tupleE^tupleE : ∀ x0 x1 x2 . x2 ∈ lam 2 (λ x3 . If_i (x3 = 0) x0 x1) ⟶ or (∀ x3 : ο . (∀ x4 . and (x4 ∈ x0) (x2 = lam 2 (λ x6 . If_i (x6 = 0) 0 x4)) ⟶ x3) ⟶ x3) (∀ x3 : ο . (∀ x4 . and (x4 ∈ x1) (x2 = lam 2 (λ x6 . If_i (x6 = 0) 1 x4)) ⟶ x3) ⟶ x3) (proof)
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 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 (proof)
Theorem 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 (proof)
Theorem apI2^apI2 : ∀ x0 x1 x2 . lam 2 (λ x3 . If_i (x3 = 0) x1 x2) ∈ x0 ⟶ x2 ∈ ap x0 x1 (proof)
Known apE^apE : ∀ x0 x1 x2 . x2 ∈ ap x0 x1 ⟶ setsum x1 x2 ∈ x0
Theorem apE2^apE2 : ∀ x0 x1 x2 . x2 ∈ ap x0 x1 ⟶ lam 2 (λ x3 . If_i (x3 = 0) x1 x2) ∈ x0 (proof)
Known Empty_Subq_eq^{Empty_Subq_eq} : ∀ x0 . x0 ⊆ 0 ⟶ x0 = 0
Theorem ap_const_0^ap_const_0 : ∀ x0 . ap 0 x0 = 0 (proof)
Known 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)
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 tuple_2_in_A_2^{tuple_2_in_A_2} : ∀ x0 x1 x2 . x0 ∈ x2 ⟶ x1 ∈ x2 ⟶ lam 2 (λ x3 . If_i (x3 = 0) x0 x1) ∈ setexp x2 2 (proof)
Param bij^bij : ι → ι → (ι → ι) → ο
Known PigeonHole_nat_bij^{PigeonHole_nat_bij} : ∀ x0 . nat_p x0 ⟶ ∀ x1 : ι → ι . (∀ x2 . x2 ∈ x0 ⟶ x1 x2 ∈ x0) ⟶ (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 = x1 x3 ⟶ x2 = x3) ⟶ bij x0 x0 x1
Known nat_2^nat_2 : nat_p 2
Theorem tuple_2_bij_2^{tuple_2_bij_2} : ∀ x0 x1 . x0 ∈ 2 ⟶ x1 ∈ 2 ⟶ (x0 = x1 ⟶ ∀ x2 : ο . x2) ⟶ bij 2 2 (ap (lam 2 (λ x2 . If_i (x2 = 0) x0 x1))) (proof)