Proofgold Address

Definition d3f3c.. := Power 0
Definition 33cc2.. := Power d3f3c..
Definition 50a6b.. := binrep 33cc2.. 0
Definition 99f52.. := Power 33cc2..
Definition 4cfc8.. := binrep 99f52.. 0
Definition ae183.. := binrep 99f52.. d3f3c..
Definition 803bd.. := binrep ae183.. 0
Definition 568b5.. := Power 50a6b..
Definition 2d4e1.. := binrep 568b5.. 0
Definition c4124.. := binrep 568b5.. d3f3c..
Definition 265be.. := binrep (binrep 568b5.. d3f3c..) 0
Definition c0b45.. := binrep 568b5.. 33cc2..
Definition 2f0db.. := binrep (binrep 568b5.. 33cc2..) 0
Definition 0d915.. := binrep (binrep 568b5.. 33cc2..) d3f3c..
Definition 988b5.. := binrep (binrep (binrep 568b5.. 33cc2..) d3f3c..) 0
Definition 6a551.. := Power 99f52..
Known f2c5c..^equipI : ∀ x0 x1 . ∀ x2 : ι → ι . bij x0 x1 x2 ⟶ equip x0 x1
Known e5c63..^bijI : ∀ x0 x1 . ∀ x2 : ι → ι . inj x0 x1 x2 ⟶ (∀ x3 . In x3 x1 ⟶ ∀ x4 : ο . (∀ x5 . and (In x5 x0) (x2 x5 = x3) ⟶ x4) ⟶ x4) ⟶ bij x0 x1 x2
Known 1796e..^injI : ∀ x0 x1 . ∀ x2 : ι → ι . (∀ x3 . In x3 x0 ⟶ In (x2 x3) x1) ⟶ (∀ x3 . In x3 x0 ⟶ ∀ x4 . In x4 x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4) ⟶ inj x0 x1 x2
Known 93236..^Inj0_setsum : ∀ x0 x1 x2 . In x2 x0 ⟶ In (Inj0 x2) (setsum x0 x1)
Known 9ea3e..^Inj1_setsum : ∀ x0 x1 x2 . In x2 x1 ⟶ In (Inj1 x2) (setsum 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)
Known 49afe..^Inj0_inj : ∀ x0 x1 . Inj0 x0 = Inj0 x1 ⟶ x0 = x1
Known 0139a..^Inj1_inj : ∀ x0 x1 . Inj1 x0 = Inj1 x1 ⟶ x0 = x1
Known 7c02f..^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known d805a..^{combine_funcs_eq2} : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 . combine_funcs x0 x1 x2 x3 (Inj1 x4) = x3 x4
Known 34a93..^{combine_funcs_eq1} : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 . combine_funcs x0 x1 x2 x3 (Inj0 x4) = x2 x4
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
Theorem fcc2b.. : ∀ x0 x1 x2 . equip (setsum (setsum x0 x1) x2) (setsum x0 (setsum x1 x2)) (proof)
Known 367e6..^SubqE : ∀ x0 x1 . Subq x0 x1 ⟶ ∀ x2 . In x2 x0 ⟶ In x2 x1
Known 24526..^nIn_E2 : ∀ x0 x1 . nIn x0 x1 ⟶ In x0 x1 ⟶ False
Known 3ab01..^xmcases_In : ∀ x0 x1 . ∀ x2 : ο . (In x0 x1 ⟶ x2) ⟶ (nIn x0 x1 ⟶ x2) ⟶ x2
Known 626dc..^setminusI : ∀ x0 x1 x2 . In x2 x0 ⟶ nIn x2 x1 ⟶ In x2 (setminus x0 x1)
Known 243aa..^{setminusE_impred} : ∀ x0 x1 x2 . In x2 (setminus x0 x1) ⟶ ∀ x3 : ο . (In x2 x0 ⟶ nIn x2 x1 ⟶ x3) ⟶ x3
Theorem d5a72.. : ∀ x0 x1 . Subq x1 x0 ⟶ equip (setsum x1 (setminus x0 x1)) x0 (proof)
Known 97a83..^{atleastp_E_impred} : ∀ x0 x1 . atleastp x0 x1 ⟶ ∀ x2 : ο . (∀ x3 : ι → ι . inj x0 x1 x3 ⟶ x2) ⟶ x2
Known e6daf..^injE_impred : ∀ x0 x1 . ∀ x2 : ι → ι . inj x0 x1 x2 ⟶ ∀ x3 : ο . ((∀ x4 . In x4 x0 ⟶ In (x2 x4) x1) ⟶ (∀ x4 . In x4 x0 ⟶ ∀ x5 . In x5 x0 ⟶ x2 x4 = x2 x5 ⟶ x4 = x5) ⟶ x3) ⟶ x3
Known b0dce..^SubqI : ∀ x0 x1 . (∀ x2 . In x2 x0 ⟶ In x2 x1) ⟶ Subq x0 x1
Known 0f096..^ReplE2 : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 (Repl x0 x1) ⟶ ∀ x3 : ο . (∀ x4 . In x4 x0 ⟶ x2 = x1 x4 ⟶ x3) ⟶ x3
Known f1bf4..^ReplI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 x0 ⟶ In (x1 x2) (Repl x0 x1)
Theorem 2d714.. : ∀ x0 x1 . atleastp x0 x1 ⟶ ∀ x2 : ο . (∀ x3 . and (Subq x3 x1) (equip x0 x3) ⟶ x2) ⟶ x2 (proof)
Known 95b31..^atleastp_I : ∀ x0 x1 . ∀ x2 : ι → ι . inj x0 x1 x2 ⟶ atleastp x0 x1
Theorem 3394a.. : ∀ x0 x1 x2 . Subq x0 x1 ⟶ atleastp x1 x2 ⟶ atleastp x0 x2 (proof)
Known c9b7c..^{equipE_impred} : ∀ x0 x1 . equip x0 x1 ⟶ ∀ x2 : ο . (∀ x3 : ι → ι . bij x0 x1 x3 ⟶ x2) ⟶ x2
Known 80a11..^bijE_impred : ∀ x0 x1 . ∀ x2 : ι → ι . bij x0 x1 x2 ⟶ ∀ x3 : ο . (inj x0 x1 x2 ⟶ (∀ x4 . In x4 x1 ⟶ ∀ x5 : ο . (∀ x6 . and (In x6 x0) (x2 x6 = x4) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3
Theorem a8ad4.. : ∀ x0 x1 . equip x0 x1 ⟶ atleastp x0 x1 (proof)
Known 54d4b..^equip_ref : ∀ x0 . equip x0 x0
Theorem 5ab24.. : ∀ x0 . atleastp x0 x0 (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 10ff6..^V_E : ∀ x0 x1 . In x0 (V_ x1) ⟶ ∀ x2 : ο . (∀ x3 . In x3 x1 ⟶ Subq x0 (V_ x3) ⟶ x2) ⟶ x2
Known 2901c..^EmptyE : ∀ x0 . In x0 0 ⟶ False
Theorem ed2b7.. : V_ 0 = 0 (proof)
Known 61ad0..^In_ind : ∀ x0 : ι → ο . (∀ x1 . (∀ x2 . In x2 x1 ⟶ x0 x2) ⟶ x0 x1) ⟶ ∀ x1 . x0 x1
Known 79a81..^TransSetI : ∀ x0 . (∀ x1 . In x1 x0 ⟶ Subq x1 x0) ⟶ TransSet x0
Known b5461..^V_I : ∀ x0 x1 x2 . In x1 x2 ⟶ Subq x0 (V_ x1) ⟶ In x0 (V_ x2)
Known 2fc4a..^TransSetE : ∀ x0 . TransSet x0 ⟶ ∀ x1 . In x1 x0 ⟶ Subq x1 x0
Theorem 16197.. : ∀ x0 . TransSet (V_ 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 2d44a..^PowerI : ∀ x0 x1 . Subq x1 x0 ⟶ In x1 (Power x0)
Known b4776..^{ordsuccE_impred} : ∀ x0 x1 . In x1 (ordsucc x0) ⟶ ∀ x2 : ο . (In x1 x0 ⟶ x2) ⟶ (x1 = x0 ⟶ x2) ⟶ x2
Known 2ad64..^Subq_tra : ∀ x0 x1 x2 . Subq x0 x1 ⟶ Subq x1 x2 ⟶ Subq x0 x2
Known 212d0..^V_Subq_2 : ∀ x0 x1 . Subq x0 (V_ x1) ⟶ Subq (V_ x0) (V_ x1)
Known 081f3..^V_Subq : ∀ x0 . Subq x0 (V_ x0)
Known cf025..^ordsuccI2 : ∀ x0 . In x0 (ordsucc x0)
Known ae89b..^PowerE : ∀ x0 x1 . In x1 (Power x0) ⟶ Subq x1 x0
Theorem 0156b.. : ∀ x0 . nat_p x0 ⟶ V_ (ordsucc x0) = Power (V_ x0) (proof)
Known 637fd..^equip_sym : ∀ x0 x1 . equip x0 x1 ⟶ equip x1 x0
Known fa8b5..^Sep_In_Power : ∀ x0 . ∀ x1 : ι → ο . In (Sep x0 x1) (Power x0)
Known eead0..^setexp_ext : ∀ x0 x1 x2 . In x2 (setexp x1 x0) ⟶ ∀ x3 . In x3 (setexp x1 x0) ⟶ (∀ x4 . In x4 x0 ⟶ ap x2 x4 = ap x3 x4) ⟶ x2 = x3
Known 3ad28..^cases_2 : ∀ x0 . In x0 2 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 x0
Known 076ba..^SepE2 : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . In x2 (Sep x0 x1) ⟶ x1 x2
Known dab1f..^SepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . In x2 x0 ⟶ x1 x2 ⟶ In x2 (Sep x0 x1)
Known bc2f0..^ap_setexp : ∀ x0 x1 x2 . In x2 (setexp x1 x0) ⟶ ∀ x3 . In x3 x0 ⟶ In (ap x2 x3) x1
Known 3152e..^lam_setexp : ∀ x0 x1 . ∀ x2 : ι → ι . (∀ x3 . In x3 x0 ⟶ In (x2 x3) x1) ⟶ In (lam x0 x2) (setexp x1 x0)
Known 47706..^xmcases : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (not x0 ⟶ x1) ⟶ x1
Known 0d2f9..^If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0 ⟶ If_i x0 x1 x2 = x1
Known 0a117..^In_1_2 : In 1 2
Known 81513..^If_i_0 : ∀ x0 : ο . ∀ x1 x2 . not x0 ⟶ If_i x0 x1 x2 = x2
Known 0863e..^In_0_2 : In 0 2
Known aa3f4..^SepE_impred : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . In x2 (Sep x0 x1) ⟶ ∀ x3 : ο . (In x2 x0 ⟶ x1 x2 ⟶ x3) ⟶ x3
Known b4782..^contra : ∀ x0 : ο . (not x0 ⟶ False) ⟶ x0
Known e3ec9..^neq_0_1 : not (0 = 1)
Known b515a..^beta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 x0 ⟶ ap (lam x0 x1) x2 = x1 x2
Theorem 56361.. : ∀ x0 . equip (Power x0) (setexp 2 x0) (proof)
Known andE^andE : ∀ x0 x1 : ο . and x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Theorem de142.. : ∀ x0 x1 . equip x0 x1 ⟶ equip (Power x0) (Power x1) (proof)
Known 30edc..^equip_tra : ∀ x0 x1 x2 . equip x0 x1 ⟶ equip x1 x2 ⟶ equip x0 x2
Theorem d80e2.. : ∀ x0 x1 . equip x0 x1 ⟶ equip (Power x0) (setexp 2 x1) (proof)
Known 0978b..^In_0_1 : In 0 1
Known 9ae18..^SingE : ∀ x0 x1 . In x1 (Sing x0) ⟶ x1 = x0
Known 1f15b..^SingI : ∀ x0 . In x0 (Sing x0)
Known e51a8..^cases_1 : ∀ x0 . In x0 1 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 x0
Theorem 2397e.. : ∀ x0 . equip (Sing x0) 1 (proof)
Known 208df..^PiE_impred : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 (Pi x0 x1) ⟶ ∀ x3 : ο . ((∀ x4 . In x4 x2 ⟶ and (setsum_p x4) (In (ap x4 0) x0)) ⟶ (∀ x4 . In x4 x0 ⟶ In (ap x2 x4) (x1 x4)) ⟶ x3) ⟶ x3
Known 4bf71..^setexp_E : ∀ x0 x1 x2 . In x2 (setexp x1 x0) ⟶ In x2 (Pi x0 (λ x3 . x1))
Known 4322e..^setexp_I : ∀ x0 x1 x2 . In x2 (Pi x0 (λ x3 . x1)) ⟶ In x2 (setexp x1 x0)
Known b9bec..^PiI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . (∀ x3 . In x3 x2 ⟶ and (setsum_p x3) (In (ap x3 0) x0)) ⟶ (∀ x3 . In x3 x0 ⟶ In (ap x2 x3) (x1 x3)) ⟶ In x2 (Pi x0 x1)
Theorem fb4a0.. : ∀ x0 . setexp x0 0 = 1 (proof)
Known 08193..^tuple_2_0_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 0 = x0
Known 66870..^tuple_2_1_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 1 = x1
Known c1504..^{tuple_setprod_eta} : ∀ x0 x1 x2 . In x2 (setprod x0 x1) ⟶ lam 2 (λ x4 . If_i (x4 = 0) (ap x2 0) (ap x2 1)) = x2
Known e9b50..^ordsuccI1b : ∀ x0 x1 . In x1 x0 ⟶ In x1 (ordsucc x0)
Known 8106d..^notI : ∀ x0 : ο . (x0 ⟶ False) ⟶ not x0
Known 2a3a3..^In_irref_b : ∀ x0 . In x0 x0 ⟶ False
Known 6789e..^ap1_setprod : ∀ x0 x1 x2 . In x2 (setprod x0 x1) ⟶ In (ap x2 1) x1
Known fe28a..^ap0_setprod : ∀ x0 x1 x2 . In x2 (setprod x0 x1) ⟶ In (ap x2 0) x0
Known e8081..^{tuple_2_setprod} : ∀ x0 x1 x2 . In x2 x0 ⟶ ∀ x3 . In x3 x1 ⟶ In (lam 2 (λ x4 . If_i (x4 = 0) x2 x3)) (setprod x0 x1)
Theorem b8446.. : ∀ x0 x1 . equip (setexp x0 (ordsucc x1)) (setprod (setexp x0 x1) x0) (proof)
Param 69aae..^exp_nat : ι → ι → ι
Known fed08..^nat_ind : ∀ x0 : ι → ο . x0 0 ⟶ (∀ x1 . nat_p x1 ⟶ x0 x1 ⟶ x0 (ordsucc x1)) ⟶ ∀ x1 . nat_p x1 ⟶ x0 x1
Known 94de7..^exp_nat_0 : ∀ x0 . 69aae.. x0 0 = 1
Known f4890..^exp_nat_S : ∀ x0 x1 . nat_p x1 ⟶ 69aae.. x0 (ordsucc x1) = mul_nat x0 (69aae.. x0 x1)
Known d6c64..^mul_nat_com : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ mul_nat x0 x1 = mul_nat x1 x0
Known 912b9..^{equip_setprod_mul_nat_2} : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ ∀ x2 x3 . equip x2 x0 ⟶ equip x3 x1 ⟶ equip (setprod x2 x3) (mul_nat x0 x1)
Known 2f247..^exp_nat_p : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ nat_p (69aae.. x0 x1)
Theorem 98735.. : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ equip (setexp x0 x1) (69aae.. x0 x1) (proof)
Known 08405..^nat_0 : nat_p 0
Known 36841..^nat_2 : nat_p 2
Theorem c8f7e.. : ∀ x0 . nat_p x0 ⟶ ∀ x1 : ο . (∀ x2 . and (nat_p x2) (equip (V_ x0) x2) ⟶ x1) ⟶ x1 (proof)
Known d6778..^{Empty_Subq_eq} : ∀ x0 . Subq x0 0 ⟶ x0 = 0
Known 840d1..^{nat_ordsucc_in_ordsucc} : ∀ x0 . nat_p x0 ⟶ ∀ x1 . In x1 x0 ⟶ In (ordsucc x1) (ordsucc x0)
Known a7773..^{ordsucc_add_nat_1} : ∀ x0 . ordsucc x0 = add_nat x0 1
Known 3fe1c..^add_nat_com : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ add_nat x0 x1 = add_nat x1 x0
Known c7c31..^nat_1 : nat_p 1
Known 56707..^{equip_setsum_add_nat_2} : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ ∀ x2 x3 . equip x2 x0 ⟶ equip x3 x1 ⟶ equip (setsum x2 x3) (add_nat x0 x1)
Known b0a90..^nat_p_trans : ∀ x0 . nat_p x0 ⟶ ∀ x1 . In x1 x0 ⟶ nat_p x1
Known 21479..^nat_ordsucc : ∀ x0 . nat_p x0 ⟶ nat_p (ordsucc x0)
Theorem 0492e.. : ∀ x0 . nat_p x0 ⟶ ∀ x1 . Subq x1 x0 ⟶ ∀ x2 : ο . (∀ x3 . and (In x3 (ordsucc x0)) (equip x1 x3) ⟶ x2) ⟶ x2 (proof)
Theorem ff582.. : ∀ x0 x1 . nat_p x1 ⟶ atleastp x0 x1 ⟶ ∀ x2 : ο . (∀ x3 . and (In x3 (ordsucc x1)) (equip x0 x3) ⟶ x2) ⟶ x2 (proof)
Theorem 19d38.. : ∀ x0 . atleastp x0 0 ⟶ x0 = 0 (proof)
Theorem 82600.. : ∀ x0 . equip x0 0 ⟶ x0 = 0 (proof)
Known ebcfc..^{PigeonHole_nat} : ∀ x0 . nat_p x0 ⟶ ∀ x1 : ι → ι . (∀ x2 . In x2 (ordsucc x0) ⟶ In (x1 x2) x0) ⟶ not (∀ x2 . In x2 (ordsucc x0) ⟶ ∀ x3 . In x3 (ordsucc x0) ⟶ x1 x2 = x1 x3 ⟶ x2 = x3)
Known 26a5d..^{ordinal_ordsucc_In_Subq} : ∀ x0 . ordinal x0 ⟶ ∀ x1 . In x1 x0 ⟶ Subq (ordsucc x1) x0
Known 08dfe..^{nat_p_ordinal} : ∀ x0 . nat_p x0 ⟶ ordinal x0
Theorem ac18f.. : ∀ x0 . nat_p x0 ⟶ ∀ x1 . In x1 x0 ⟶ atleastp x0 x1 ⟶ False (proof)
Known 42117..^{ordinal_trichotomy_or_impred} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ ∀ x2 : ο . (In x0 x1 ⟶ x2) ⟶ (x0 = x1 ⟶ x2) ⟶ (In x1 x0 ⟶ x2) ⟶ x2
Theorem dccf1.. : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ equip x0 x1 ⟶ x0 = x1 (proof)