Proofgold Address

Known 2d44a..^PowerI : ∀ x0 x1 . Subq x1 x0 ⟶ In x1 (Power x0)
Known b0dce..^SubqI : ∀ x0 x1 . (∀ x2 . In x2 x0 ⟶ In x2 x1) ⟶ Subq x0 x1
Theorem bcb61..^PowerI2 : ∀ x0 x1 . (∀ x2 . In x2 x1 ⟶ In x2 x0) ⟶ In x1 (Power x0) (proof)
Known 367e6..^SubqE : ∀ x0 x1 . Subq x0 x1 ⟶ ∀ x2 . In x2 x0 ⟶ In x2 x1
Known ae89b..^PowerE : ∀ x0 x1 . In x1 (Power x0) ⟶ Subq x1 x0
Theorem decfb..^PowerE2 : ∀ x0 x1 . In x1 (Power x0) ⟶ ∀ x2 . In x2 x1 ⟶ In x2 x0 (proof)
Known 535f2..^set_ext_2 : ∀ x0 x1 . (∀ x2 . In x2 x0 ⟶ In x2 x1) ⟶ (∀ x2 . In x2 x1 ⟶ In x2 x0) ⟶ x0 = x1
Known 351c1..^{setsum_Inj_inv_impred} : ∀ x0 x1 x2 . In x2 (setsum x0 x1) ⟶ ∀ x3 : ι → ο . (∀ x4 . In x4 x0 ⟶ x3 (Inj0 x4)) ⟶ (∀ x4 . In x4 x1 ⟶ x3 (Inj1 x4)) ⟶ x3 x2
Known fc3ab..^Inj0_0 : Inj0 0 = 0
Known 8d83e..^Inj1I1 : ∀ x0 . In 0 (Inj1 x0)
Known 9ae18..^SingE : ∀ x0 x1 . In x1 (Sing x0) ⟶ x1 = x0
Known 830d8..^Subq_1_Sing0 : Subq 1 (Sing 0)
Known 22441..^Inj1I2 : ∀ x0 x1 . In x1 x0 ⟶ In (Inj1 x1) (Inj1 x0)
Known 474ab..^Inj1E_impred : ∀ x0 x1 . In x1 (Inj1 x0) ⟶ ∀ x2 : ι → ο . x2 0 ⟶ (∀ x3 . In x3 x0 ⟶ x2 (Inj1 x3)) ⟶ x2 x1
Known 93236..^Inj0_setsum : ∀ x0 x1 x2 . In x2 x0 ⟶ In (Inj0 x2) (setsum x0 x1)
Known 0978b..^In_0_1 : In 0 1
Known 9ea3e..^Inj1_setsum : ∀ x0 x1 x2 . In x2 x1 ⟶ In (Inj1 x2) (setsum x0 x1)
Theorem 412eb..^{Inj1_setsum_1L} : ∀ x0 . setsum 1 x0 = Inj1 x0 (proof)
Known 92870..^{nat_complete_ind} : ∀ x0 : ι → ο . (∀ x1 . nat_p x1 ⟶ (∀ x2 . In x2 x1 ⟶ x0 x2) ⟶ x0 x1) ⟶ ∀ x1 . nat_p x1 ⟶ x0 x1
Known 7bd16..^{nat_0_in_ordsucc} : ∀ x0 . nat_p x0 ⟶ In 0 (ordsucc x0)
Known 840d1..^{nat_ordsucc_in_ordsucc} : ∀ x0 . nat_p x0 ⟶ ∀ x1 . In x1 x0 ⟶ In (ordsucc x1) (ordsucc x0)
Known b4776..^{ordsuccE_impred} : ∀ x0 x1 . In x1 (ordsucc x0) ⟶ ∀ x2 : ο . (In x1 x0 ⟶ x2) ⟶ (x1 = x0 ⟶ x2) ⟶ x2
Known 37124..^orE : ∀ x0 x1 : ο . or x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known c7246..^nat_inv : ∀ x0 . nat_p x0 ⟶ or (x0 = 0) (∀ x1 : ο . (∀ x2 . and (nat_p x2) (x0 = ordsucc x2) ⟶ x1) ⟶ x1)
Known b0a90..^nat_p_trans : ∀ x0 . nat_p x0 ⟶ ∀ x1 . In x1 x0 ⟶ nat_p x1
Known 61640..^exandE_i : ∀ x0 x1 : ι → ο . (∀ x2 : ο . (∀ x3 . and (x0 x3) (x1 x3) ⟶ x2) ⟶ x2) ⟶ ∀ x2 : ο . (∀ x3 . x0 x3 ⟶ x1 x3 ⟶ x2) ⟶ x2
Known 80da5..^nat_trans : ∀ x0 . nat_p x0 ⟶ ∀ x1 . In x1 x0 ⟶ Subq x1 x0
Known cf025..^ordsuccI2 : ∀ x0 . In x0 (ordsucc x0)
Theorem 0e046..^{nat_pair1_ordsucc} : ∀ x0 . nat_p x0 ⟶ setsum 1 x0 = ordsucc x0 (proof)
Known b9c5c..^{Inj0_setsum_0L} : ∀ x0 . setsum 0 x0 = Inj0 x0
Theorem 52346..^pair_0_0 : setsum 0 0 = 0 (proof)
Known 08405..^nat_0 : nat_p 0
Theorem c6ede..^pair_1_0_1 : setsum 1 0 = 1 (proof)
Known c7c31..^nat_1 : nat_p 1
Theorem 9eb99..^pair_1_1_2 : setsum 1 1 = 2 (proof)
Theorem 52346..^pair_0_0 : setsum 0 0 = 0 (proof)
Theorem c6ede..^pair_1_0_1 : setsum 1 0 = 1 (proof)
Theorem 9eb99..^pair_1_1_2 : setsum 1 1 = 2 (proof)
Theorem 0e046..^{nat_pair1_ordsucc} : ∀ x0 . nat_p x0 ⟶ setsum 1 x0 = ordsucc x0 (proof)
Known 15e97..^eq_sym_i : ∀ x0 x1 . x0 = x1 ⟶ x1 = x0
Theorem dfb4d..^{Inj0_pair_0_eq} : Inj0 = setsum 0 (proof)
Theorem 715b1..^{Inj1_pair_1_eq} : Inj1 = setsum 1 (proof)
Theorem 65c61..^pairI0 : ∀ x0 x1 x2 . In x2 x0 ⟶ In (setsum 0 x2) (setsum x0 x1) (proof)
Theorem 77980..^pairI1 : ∀ x0 x1 x2 . In x2 x1 ⟶ In (setsum 1 x2) (setsum x0 x1) (proof)
Known 76cef..^{setsum_Inj_inv} : ∀ x0 x1 x2 . In x2 (setsum x0 x1) ⟶ or (∀ x3 : ο . (∀ x4 . and (In x4 x0) (x2 = Inj0 x4) ⟶ x3) ⟶ x3) (∀ x3 : ο . (∀ x4 . and (In x4 x1) (x2 = Inj1 x4) ⟶ x3) ⟶ x3)
Theorem 2ce7d..^pairE : ∀ x0 x1 x2 . In x2 (setsum x0 x1) ⟶ or (∀ x3 : ο . (∀ x4 . and (In x4 x0) (x2 = setsum 0 x4) ⟶ x3) ⟶ x3) (∀ x3 : ο . (∀ x4 . and (In x4 x1) (x2 = setsum 1 x4) ⟶ x3) ⟶ x3) (proof)
Known andE^andE : ∀ x0 x1 : ο . and x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Theorem 2a3f2..^pairE_impred : ∀ x0 x1 x2 . In x2 (setsum x0 x1) ⟶ ∀ x3 : ι → ο . (∀ x4 . In x4 x0 ⟶ x3 (setsum 0 x4)) ⟶ (∀ x4 . In x4 x1 ⟶ x3 (setsum 1 x4)) ⟶ x3 x2 (proof)
Known 49afe..^Inj0_inj : ∀ x0 x1 . Inj0 x0 = Inj0 x1 ⟶ x0 = x1
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Known notE^notE : ∀ x0 : ο . not x0 ⟶ x0 ⟶ False
Known efcec..^{Inj0_Inj1_neq} : ∀ x0 x1 . not (Inj0 x0 = Inj1 x1)
Theorem d321a..^pairE0 : ∀ x0 x1 x2 . In (setsum 0 x2) (setsum x0 x1) ⟶ In x2 x0 (proof)
Known 0139a..^Inj1_inj : ∀ x0 x1 . Inj1 x0 = Inj1 x1 ⟶ x0 = x1
Theorem 861bf..^pairE1 : ∀ x0 x1 x2 . In (setsum 1 x2) (setsum x0 x1) ⟶ In x2 x1 (proof)
Known 32c82..^iffI : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ iff x0 x1
Theorem 2a16a..^pairEq : ∀ x0 x1 x2 . iff (In x2 (setsum x0 x1)) (or (∀ x3 : ο . (∀ x4 . and (In x4 x0) (x2 = setsum 0 x4) ⟶ x3) ⟶ x3) (∀ x3 : ο . (∀ x4 . and (In x4 x1) (x2 = setsum 1 x4) ⟶ x3) ⟶ x3)) (proof)
Theorem 374e6..^pairSubq : ∀ x0 x1 x2 x3 . Subq x0 x2 ⟶ Subq x1 x3 ⟶ Subq (setsum x0 x1) (setsum x2 x3) (proof)
Known 92282..^proj0_def : proj0 = λ x1 . ReplSep x1 (λ x2 . ∀ x3 : ο . (∀ x4 . Inj0 x4 = x2 ⟶ x3) ⟶ x3) Unj
Known c3d4f..^Unj_Inj0_eq : ∀ x0 . Unj (Inj0 x0) = x0
Known 9fdc4..^ReplSepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 : ι → ι . ∀ x3 . In x3 x0 ⟶ x1 x3 ⟶ In (x2 x3) (ReplSep x0 x1 x2)
Theorem afc0a..^proj0I : ∀ x0 x1 . In (setsum 0 x1) x0 ⟶ In x1 (proj0 x0) (proof)
Known 65d0d..^{ReplSepE_impred} : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 : ι → ι . ∀ x3 . In x3 (ReplSep x0 x1 x2) ⟶ ∀ x4 : ο . (∀ x5 . In x5 x0 ⟶ x1 x5 ⟶ x3 = x2 x5 ⟶ x4) ⟶ x4
Theorem 88f5c..^proj0E : ∀ x0 x1 . In x1 (proj0 x0) ⟶ In (setsum 0 x1) x0 (proof)
Known c65ed..^proj1_def : proj1 = λ x1 . ReplSep x1 (λ x2 . ∀ x3 : ο . (∀ x4 . Inj1 x4 = x2 ⟶ x3) ⟶ x3) Unj
Known c76aa..^Unj_Inj1_eq : ∀ x0 . Unj (Inj1 x0) = x0
Theorem 16411..^proj1I : ∀ x0 x1 . In (setsum 1 x1) x0 ⟶ In x1 (proj1 x0) (proof)
Theorem 13e9e..^proj1E : ∀ x0 x1 . In x1 (proj1 x0) ⟶ In (setsum 1 x1) x0 (proof)
Theorem d6e1a..^{proj0_pair_eq} : ∀ x0 x1 . proj0 (setsum x0 x1) = x0 (proof)
Theorem b8fac..^{proj1_pair_eq} : ∀ x0 x1 . proj1 (setsum x0 x1) = x1 (proof)
Known 7c02f..^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem a1bad..^pair_inj : ∀ x0 x1 x2 x3 . setsum x0 x1 = setsum x2 x3 ⟶ and (x0 = x2) (x1 = x3) (proof)
Theorem 8da7f..^{pair_eta_Subq_proj} : ∀ x0 . Subq (setsum (proj0 x0) (proj1 x0)) x0 (proof)
Known 04d4d..^lam_def : lam = λ x1 . λ x2 : ι → ι . famunion x1 (λ x3 . Repl (x2 x3) (setsum x3))
Known 8f8c2..^famunionI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . In x2 x0 ⟶ In x3 (x1 x2) ⟶ In x3 (famunion x0 x1)
Known f1bf4..^ReplI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 x0 ⟶ In (x1 x2) (Repl x0 x1)
Theorem f9ff3..^lamI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 x0 ⟶ ∀ x3 . In x3 (x1 x2) ⟶ In (setsum x2 x3) (lam x0 x1) (proof)
Known 7b31d..^famunionE2 : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 (famunion x0 x1) ⟶ ∀ x3 : ο . (∀ x4 . In x4 x0 ⟶ In x2 (x1 x4) ⟶ x3) ⟶ x3
Known 0f096..^ReplE2 : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 (Repl x0 x1) ⟶ ∀ x3 : ο . (∀ x4 . In x4 x0 ⟶ x2 = x1 x4 ⟶ x3) ⟶ x3
Known f6404..^and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Theorem 56f17..^{Sigma_eta_proj0_proj1} : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 (lam x0 x1) ⟶ and (and (setsum (proj0 x2) (proj1 x2) = x2) (In (proj0 x2) x0)) (In (proj1 x2) (x1 (proj0 x2))) (proof)
Known cd094..^and3E : ∀ x0 x1 x2 : ο . and (and x0 x1) x2 ⟶ ∀ x3 : ο . (x0 ⟶ x1 ⟶ x2 ⟶ x3) ⟶ x3
Theorem 413ee..^{proj_Sigma_eta} : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 (lam x0 x1) ⟶ setsum (proj0 x2) (proj1 x2) = x2 (proof)
Theorem 3057f..^proj0_Sigma : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 (lam x0 x1) ⟶ In (proj0 x2) x0 (proof)
Theorem 6bfcf..^proj1_Sigma : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 (lam x0 x1) ⟶ In (proj1 x2) (x1 (proj0 x2)) (proof)
Theorem 1d863..^{pair_Sigma_E0} : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . In (setsum x2 x3) (lam x0 x1) ⟶ In x2 x0 (proof)
Theorem be650..^{pair_Sigma_E1} : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . In (setsum x2 x3) (lam x0 x1) ⟶ In x3 (x1 x2) (proof)
Theorem e3e5f..^lamE : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 (lam x0 x1) ⟶ ∀ x3 : ο . (∀ x4 . and (In x4 x0) (∀ x5 : ο . (∀ x6 . and (In x6 (x1 x4)) (x2 = setsum x4 x6) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3 (proof)
Theorem efa2b..^lamEq : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . iff (In x2 (lam x0 x1)) (∀ x3 : ο . (∀ x4 . and (In x4 x0) (∀ x5 : ο . (∀ x6 . and (In x6 (x1 x4)) (x2 = setsum x4 x6) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3) (proof)
Theorem 1587f..^Sigma_mon : ∀ x0 x1 . Subq x0 x1 ⟶ ∀ x2 x3 : ι → ι . (∀ x4 . In x4 x0 ⟶ Subq (x2 x4) (x3 x4)) ⟶ Subq (lam x0 x2) (lam x1 x3) (proof)
Known 6696a..^Subq_ref : ∀ x0 . Subq x0 x0
Theorem 01b21..^Sigma_mon0 : ∀ x0 x1 . Subq x0 x1 ⟶ ∀ x2 : ι → ι . Subq (lam x0 x2) (lam x1 x2) (proof)
Theorem 251f7..^Sigma_mon1 : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . In x3 x0 ⟶ Subq (x1 x3) (x2 x3)) ⟶ Subq (lam x0 x1) (lam x0 x2) (proof)
Theorem 71581..^{Sigma_Power_1} : ∀ x0 . In x0 (Power 1) ⟶ ∀ x1 : ι → ι . (∀ x2 . In x2 x0 ⟶ In (x1 x2) (Power 1)) ⟶ In (lam x0 x1) (Power 1) (proof)
Known ad99c..^setprod_def : setprod = λ x1 x2 . lam x1 (λ x3 . x2)
Theorem 07808..^pair_setprod : ∀ x0 x1 x2 . In x2 x0 ⟶ ∀ x3 . In x3 x1 ⟶ In (setsum x2 x3) (setprod x0 x1) (proof)
Theorem 681fa..^{proj0_setprod} : ∀ x0 x1 x2 . In x2 (setprod x0 x1) ⟶ In (proj0 x2) x0 (proof)
Theorem 1cfb6..^{proj1_setprod} : ∀ x0 x1 x2 . In x2 (setprod x0 x1) ⟶ In (proj1 x2) x1 (proof)
Theorem 40531..^setprod_mon : ∀ x0 x1 . Subq x0 x1 ⟶ ∀ x2 x3 . Subq x2 x3 ⟶ Subq (setprod x0 x2) (setprod x1 x3) (proof)
Theorem b327e..^setprod_mon0 : ∀ x0 x1 . Subq x0 x1 ⟶ ∀ x2 . Subq (setprod x0 x2) (setprod x1 x2) (proof)
Theorem 3ea93..^setprod_mon1 : ∀ x0 x1 x2 . Subq x1 x2 ⟶ Subq (setprod x0 x1) (setprod x0 x2) (proof)
Theorem 98421..^{pair_setprod_E0} : ∀ x0 x1 x2 x3 . In (setsum x2 x3) (setprod x0 x1) ⟶ In x2 x0 (proof)
Theorem c6ec6..^{pair_setprod_E1} : ∀ x0 x1 x2 x3 . In (setsum x2 x3) (setprod x0 x1) ⟶ In x3 x1 (proof)
Theorem f9ff3..^lamI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 x0 ⟶ ∀ x3 . In x3 (x1 x2) ⟶ In (setsum x2 x3) (lam x0 x1) (proof)
Theorem e3e5f..^lamE : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 (lam x0 x1) ⟶ ∀ x3 : ο . (∀ x4 . and (In x4 x0) (∀ x5 : ο . (∀ x6 . and (In x6 (x1 x4)) (x2 = setsum x4 x6) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3 (proof)
Theorem efa2b..^lamEq : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . iff (In x2 (lam x0 x1)) (∀ x3 : ο . (∀ x4 . and (In x4 x0) (∀ x5 : ο . (∀ x6 . and (In x6 (x1 x4)) (x2 = setsum x4 x6) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3) (proof)
Known 043f7..^ap_def : ap = λ x1 x2 . ReplSep x1 (λ x3 . ∀ x4 : ο . (∀ x5 . x3 = setsum x2 x5 ⟶ x4) ⟶ x4) proj1
Theorem 970d5..^apI : ∀ x0 x1 x2 . In (setsum x1 x2) x0 ⟶ In x2 (ap x0 x1) (proof)
Theorem 0bd41..^apE : ∀ x0 x1 x2 . In x2 (ap x0 x1) ⟶ In (setsum x1 x2) x0 (proof)
Theorem d1a05..^apEq : ∀ x0 x1 x2 . iff (In x2 (ap x0 x1)) (In (setsum x1 x2) x0) (proof)
Theorem b515a..^beta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 x0 ⟶ ap (lam x0 x1) x2 = x1 x2 (proof)
Known d0de4..^Empty_eq : ∀ x0 . (∀ x1 . nIn x1 x0) ⟶ x0 = 0
Known 9d2e6..^nIn_I2 : ∀ x0 x1 . (In x0 x1 ⟶ False) ⟶ nIn x0 x1
Known 24526..^nIn_E2 : ∀ x0 x1 . nIn x0 x1 ⟶ In x0 x1 ⟶ False
Theorem 4862c..^beta0 : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . nIn x2 x0 ⟶ ap (lam x0 x1) x2 = 0 (proof)