Proofgold Address

Known ad99c..^setprod_def : setprod = λ x1 x2 . lam x1 (λ x3 . x2)
Theorem 3a5bf..^setprod_I : ∀ x0 x1 x2 . In x2 (lam x0 (λ x3 . x1)) ⟶ In x2 (setprod x0 x1) (proof)
Theorem e9adc..^setprod_E : ∀ x0 x1 x2 . In x2 (setprod x0 x1) ⟶ In x2 (lam x0 (λ x3 . x1)) (proof)
Known 1194c..^ap0_Sigma : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 (lam x0 x1) ⟶ In (ap x2 0) x0
Theorem fe28a..^ap0_setprod : ∀ x0 x1 x2 . In x2 (setprod x0 x1) ⟶ In (ap x2 0) x0 (proof)
Known a6609..^ap1_Sigma : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 (lam x0 x1) ⟶ In (ap x2 1) (x1 (ap x2 0))
Theorem 6789e..^ap1_setprod : ∀ x0 x1 x2 . In x2 (setprod x0 x1) ⟶ In (ap x2 1) x1 (proof)
Known f1e40..^{tuple_Sigma_eta} : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 (lam x0 x1) ⟶ lam 2 (λ x4 . If_i (x4 = 0) (ap x2 0) (ap x2 1)) = x2
Theorem 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 (proof)
Known 4322e..^setexp_I : ∀ x0 x1 x2 . In x2 (Pi x0 (λ x3 . x1)) ⟶ In x2 (setexp x1 x0)
Known 25543..^lam_Pi : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . In x3 x0 ⟶ In (x2 x3) (x1 x3)) ⟶ In (lam x0 x2) (Pi x0 x1)
Theorem 3152e..^lam_setexp : ∀ x0 x1 . ∀ x2 : ι → ι . (∀ x3 . In x3 x0 ⟶ In (x2 x3) x1) ⟶ In (lam x0 x2) (setexp x1 x0) (proof)
Known 31c25..^ap_Pi : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . In x2 (Pi x0 x1) ⟶ In x3 x0 ⟶ In (ap x2 x3) (x1 x3)
Known 4bf71..^setexp_E : ∀ x0 x1 x2 . In x2 (setexp x1 x0) ⟶ In x2 (Pi x0 (λ x3 . x1))
Theorem bc2f0..^ap_setexp : ∀ x0 x1 x2 . In x2 (setexp x1 x0) ⟶ ∀ x3 . In x3 x0 ⟶ In (ap x2 x3) x1 (proof)
Known 3c3a9..^setexp_def : setexp = λ x1 x2 . Pi x2 (λ x3 . x1)
Known 552ff..^Pi_ext : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 (Pi x0 x1) ⟶ ∀ x3 . In x3 (Pi x0 x1) ⟶ (∀ x4 . In x4 x0 ⟶ ap x2 x4 = ap x3 x4) ⟶ x2 = x3
Theorem 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 (proof)
Known eb933..^Pi_eta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 (Pi x0 x1) ⟶ lam x0 (ap x2) = x2
Theorem 09a68..^setexp_eta : ∀ x0 x1 x2 . In x2 (setexp x1 x0) ⟶ lam x0 (ap x2) = x2 (proof)
Known a6e5c..^mul_nat_SR : ∀ x0 x1 . nat_p x1 ⟶ mul_nat x0 (ordsucc x1) = add_nat x0 (mul_nat x0 x1)
Known 08405..^nat_0 : nat_p 0
Known fad70..^mul_nat_0R : ∀ x0 . mul_nat x0 0 = 0
Known 02169..^add_nat_0R : ∀ x0 . add_nat x0 0 = x0
Theorem 9b388..^mul_nat_1R : ∀ x0 . mul_nat x0 1 = x0 (proof)
Known d6c64..^mul_nat_com : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ mul_nat x0 x1 = mul_nat x1 x0
Known c7c31..^nat_1 : nat_p 1
Theorem e6942..^mul_nat_1L : ∀ x0 . nat_p x0 ⟶ mul_nat 1 x0 = 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 4f633..^mul_nat_p : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ nat_p (mul_nat x0 x1)
Theorem 2f247..^exp_nat_p : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ nat_p (69aae.. x0 x1) (proof)
Theorem 37c59..^exp_nat_1 : ∀ x0 . 69aae.. x0 1 = x0 (proof)
Theorem 8271b..^{exp_nat_2_mul_nat} : ∀ x0 . 69aae.. x0 2 = mul_nat x0 x0 (proof)
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 andE^andE : ∀ x0 x1 : ο . and x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Theorem 5f4e5..^{nat_inv_impred} : ∀ x0 . nat_p x0 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ (∀ x2 . nat_p x2 ⟶ x0 = ordsucc x2 ⟶ x1 (ordsucc x2)) ⟶ x1 x0 (proof)
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Known 2901c..^EmptyE : ∀ x0 . In x0 0 ⟶ False
Theorem bce4a..^{pos_nat_inv_impred} : ∀ x0 . nat_p x0 ⟶ ∀ x1 . In x1 x0 ⟶ ∀ x2 : ι → ο . (∀ x3 . nat_p x3 ⟶ x0 = ordsucc x3 ⟶ x2 (ordsucc x3)) ⟶ x2 x0 (proof)
Known 3e9a7..^{ordinal_In_Or_Subq} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ or (In x0 x1) (Subq x1 x0)
Known 80da5..^nat_trans : ∀ x0 . nat_p x0 ⟶ ∀ x1 . In x1 x0 ⟶ Subq x1 x0
Known ba2b3..^add_nat_ltL : ∀ x0 . nat_p x0 ⟶ ∀ x1 . In x1 x0 ⟶ ∀ x2 . nat_p x2 ⟶ In (add_nat x1 x2) (add_nat x0 x2)
Known 56073..^add_nat_p : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ nat_p (add_nat x0 x1)
Known 6696a..^Subq_ref : ∀ x0 . Subq x0 x0
Known b3824..^set_ext : ∀ x0 x1 . Subq x0 x1 ⟶ Subq x1 x0 ⟶ x0 = x1
Known 08dfe..^{nat_p_ordinal} : ∀ x0 . nat_p x0 ⟶ ordinal x0
Theorem 3d240..^add_nat_leL : ∀ x0 x1 x2 . nat_p x0 ⟶ nat_p x1 ⟶ Subq x0 x1 ⟶ nat_p x2 ⟶ Subq (add_nat x0 x2) (add_nat x1 x2) (proof)
Known 3fe1c..^add_nat_com : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ add_nat x0 x1 = add_nat x1 x0
Theorem 6f7bf..^add_nat_leR : ∀ x0 x1 x2 . nat_p x0 ⟶ nat_p x1 ⟶ nat_p x2 ⟶ Subq x1 x2 ⟶ Subq (add_nat x0 x1) (add_nat x0 x2) (proof)
Known 0dc7e..^add_nat_0L : ∀ x0 . nat_p x0 ⟶ add_nat 0 x0 = x0
Known b41a2..^Subq_Empty : ∀ x0 . Subq 0 x0
Theorem 791c2..^{add_nat_leL_2} : ∀ x0 x1 . nat_p x0 ⟶ nat_p x1 ⟶ Subq x0 (add_nat x1 x0) (proof)
Theorem 10d71..^{add_nat_leR_2} : ∀ x0 x1 . nat_p x0 ⟶ nat_p x1 ⟶ Subq x0 (add_nat x0 x1) (proof)
Known 1cf88..^{ordinal_TransSet_b} : ∀ x0 . ordinal x0 ⟶ ∀ x1 . In x1 x0 ⟶ ∀ x2 . In x2 x1 ⟶ In x2 x0
Known 428f7..^add_nat_ltR : ∀ x0 . nat_p x0 ⟶ ∀ x1 . In x1 x0 ⟶ ∀ x2 . nat_p x2 ⟶ In (add_nat x2 x1) (add_nat x2 x0)
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 d3280..^mul_nat_ltL : ∀ x0 . nat_p x0 ⟶ ∀ x1 . In x1 x0 ⟶ ∀ x2 . nat_p x2 ⟶ In (mul_nat x1 (ordsucc x2)) (mul_nat x0 (ordsucc x2)) (proof)
Theorem b01a1..^mul_nat_ltR : ∀ x0 . nat_p x0 ⟶ ∀ x1 . In x1 x0 ⟶ ∀ x2 . nat_p x2 ⟶ In (mul_nat (ordsucc x2) x1) (mul_nat (ordsucc x2) x0) (proof)
Known 2ad64..^Subq_tra : ∀ x0 x1 x2 . Subq x0 x1 ⟶ Subq x1 x2 ⟶ Subq x0 x2
Theorem e93e8..^mul_nat_leL : ∀ x0 x1 . nat_p x0 ⟶ nat_p x1 ⟶ Subq x0 x1 ⟶ ∀ x2 . nat_p x2 ⟶ Subq (mul_nat x0 x2) (mul_nat x1 x2) (proof)
Theorem 4d5cb..^mul_nat_leR : ∀ x0 x1 x2 . nat_p x0 ⟶ nat_p x1 ⟶ nat_p x2 ⟶ Subq x1 x2 ⟶ Subq (mul_nat x0 x1) (mul_nat x0 x2) (proof)
Known 61737..^{add_nat_mem_impred} : ∀ x0 x1 . nat_p x1 ⟶ ∀ x2 . In x2 (add_nat x0 x1) ⟶ ∀ x3 : ο . (In x2 x0 ⟶ x3) ⟶ (∀ x4 . In x4 x1 ⟶ x2 = add_nat x0 x4 ⟶ x3) ⟶ x3
Known 7bd16..^{nat_0_in_ordsucc} : ∀ x0 . nat_p x0 ⟶ In 0 (ordsucc x0)
Known 0e99e..^mul_nat_0L : ∀ x0 . nat_p x0 ⟶ mul_nat 0 x0 = 0
Known 7c02f..^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known c8db6..^mul_nat_SL : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ mul_nat (ordsucc x0) x1 = add_nat (mul_nat x0 x1) x1
Known 2a3a3..^In_irref_b : ∀ x0 . In x0 x0 ⟶ False
Known 367e6..^SubqE : ∀ x0 x1 . Subq x0 x1 ⟶ ∀ x2 . In x2 x0 ⟶ In x2 x1
Known 840d1..^{nat_ordsucc_in_ordsucc} : ∀ x0 . nat_p x0 ⟶ ∀ x1 . In x1 x0 ⟶ In (ordsucc x1) (ordsucc x0)
Known 47f74..^add_nat_asso : ∀ x0 x1 . nat_p x1 ⟶ ∀ x2 . nat_p x2 ⟶ add_nat (add_nat x0 x1) x2 = add_nat x0 (add_nat x1 x2)
Known 002a9..^{add_nat_cancelR} : ∀ x0 x1 x2 . nat_p x2 ⟶ add_nat x0 x2 = add_nat x1 x2 ⟶ x0 = x1
Known cf025..^ordsuccI2 : ∀ x0 . In x0 (ordsucc x0)
Known 8cf6a..^{nat_ordsucc_trans} : ∀ x0 . nat_p x0 ⟶ ∀ x1 . In x1 (ordsucc x0) ⟶ Subq x1 x0
Theorem 1c648..^{quot_rem_nat_impred} : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ ∀ x2 . In x2 (mul_nat x0 x1) ⟶ ∀ x3 : ο . (∀ x4 . In x4 x0 ⟶ ∀ x5 . In x5 x1 ⟶ x2 = add_nat x4 (mul_nat x5 x0) ⟶ (∀ x6 . In x6 x0 ⟶ ∀ x7 . In x7 x1 ⟶ x2 = add_nat x6 (mul_nat x7 x0) ⟶ and (x6 = x4) (x7 = x5)) ⟶ x3) ⟶ x3 (proof)
Known b4776..^{ordsuccE_impred} : ∀ x0 x1 . In x1 (ordsucc x0) ⟶ ∀ x2 : ο . (In x1 x0 ⟶ x2) ⟶ (x1 = x0 ⟶ x2) ⟶ x2
Theorem 5fcca..^{add_mul_nat_lt} : ∀ x0 x1 . nat_p x0 ⟶ nat_p x1 ⟶ ∀ x2 . In x2 x0 ⟶ ∀ x3 . In x3 x1 ⟶ In (add_nat x2 (mul_nat x3 x0)) (mul_nat x0 x1) (proof)
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 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)
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
Theorem ff088..^{equip_setprod_mul_nat} : ∀ x0 x1 . nat_p x0 ⟶ nat_p x1 ⟶ equip (setprod x0 x1) (mul_nat x0 x1) (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
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 abe40..^{tuple_2_inj_impred} : ∀ x0 x1 x2 x3 . lam 2 (λ x5 . If_i (x5 = 0) x0 x1) = lam 2 (λ x5 . If_i (x5 = 0) x2 x3) ⟶ ∀ x4 : ο . (x0 = x2 ⟶ x1 = x3 ⟶ x4) ⟶ x4
Theorem a3135..^{equip_setprod_cong} : ∀ x0 x1 x2 x3 . equip x0 x2 ⟶ equip x1 x3 ⟶ equip (setprod x0 x1) (setprod x2 x3) (proof)
Known 30edc..^equip_tra : ∀ x0 x1 x2 . equip x0 x1 ⟶ equip x1 x2 ⟶ equip x0 x2
Theorem 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) (proof)
Known 4c66a..^setexp_2_eq : ∀ x0 . setprod x0 x0 = setexp x0 2
Theorem 6d8a0..^{equip_setexp_2} : ∀ x0 . nat_p x0 ⟶ ∀ x1 . equip x1 x0 ⟶ equip (setexp x1 2) (mul_nat x0 x0) (proof)
Theorem 857de..^{equip_setexp_2b} : ∀ x0 . nat_p x0 ⟶ ∀ x1 . equip x1 x0 ⟶ equip (setexp x1 2) (69aae.. x0 2) (proof)
Known e9b50..^ordsuccI1b : ∀ x0 x1 . In x1 x0 ⟶ In x1 (ordsucc x0)
Known b515a..^beta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 x0 ⟶ ap (lam x0 x1) x2 = x1 x2
Known 81513..^If_i_0 : ∀ x0 : ο . ∀ x1 x2 . not x0 ⟶ If_i x0 x1 x2 = x2
Known 8106d..^notI : ∀ x0 : ο . (x0 ⟶ False) ⟶ not x0
Known 0d2f9..^If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0 ⟶ If_i x0 x1 x2 = x1
Theorem d5467..^{equip_setexp_ordsucc_setprod} : ∀ x0 x1 . equip (setexp x1 (ordsucc x0)) (setprod x1 (setexp x1 x0)) (proof)
Known 36841..^nat_2 : nat_p 2
Theorem 21472..^{equip_setexp_3} : ∀ x0 . nat_p x0 ⟶ ∀ x1 . equip x1 x0 ⟶ equip (setexp x1 3) (69aae.. x0 3) (proof)