Proofgold Address

Known 47706..^xmcases : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (not x0 ⟶ x1) ⟶ x1
Known 81513..^If_i_0 : ∀ x0 : ο . ∀ x1 x2 . not x0 ⟶ If_i x0 x1 x2 = x2
Theorem dbaea..^{nat_primrec_r} : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 . ∀ x3 x4 : ι → ι . (∀ x5 . In x5 x2 ⟶ x3 x5 = x4 x5) ⟶ If_i (In (Union x2) x2) (x1 (Union x2) (x3 (Union x2))) x0 = If_i (In (Union x2) x2) (x1 (Union x2) (x4 (Union x2))) x0 (proof)
Known 1c6cb..^{nat_primrec_def} : nat_primrec = λ x1 . λ x2 : ι → ι → ι . In_rec_poly_i (λ x3 . λ x4 : ι → ι . If_i (In (Union x3) x3) (x2 (Union x3) (x4 (Union x3))) x1)
Known f78bc..^In_rec_i_eq : ∀ x0 : ι → (ι → ι) → ι . (∀ x1 . ∀ x2 x3 : ι → ι . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . In_rec_poly_i x0 x1 = x0 x1 (In_rec_poly_i x0)
Known 8106d..^notI : ∀ x0 : ο . (x0 ⟶ False) ⟶ not x0
Known 2901c..^EmptyE : ∀ x0 . In x0 0 ⟶ False
Theorem 550dc..^{nat_primrec_0} : ∀ x0 . ∀ x1 : ι → ι → ι . nat_primrec x0 x1 0 = x0 (proof)
Known 48ae5..^{Union_ordsucc_eq} : ∀ x0 . nat_p x0 ⟶ Union (ordsucc x0) = x0
Known 0d2f9..^If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0 ⟶ If_i x0 x1 x2 = x1
Known cf025..^ordsuccI2 : ∀ x0 . In x0 (ordsucc x0)
Theorem 12694..^{nat_primrec_S} : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 . nat_p x2 ⟶ nat_primrec x0 x1 (ordsucc x2) = x1 x2 (nat_primrec x0 x1 x2) (proof)
Known 925ca..^add_nat_def : add_nat = λ x1 . nat_primrec x1 (λ x2 . ordsucc)
Theorem 02169..^add_nat_0R : ∀ x0 . add_nat x0 0 = x0 (proof)
Theorem c13d1..^add_nat_SR : ∀ x0 x1 . nat_p x1 ⟶ add_nat x0 (ordsucc x1) = ordsucc (add_nat x0 x1) (proof)
Known fed08..^nat_ind : ∀ x0 : ι → ο . x0 0 ⟶ (∀ x1 . nat_p x1 ⟶ x0 x1 ⟶ x0 (ordsucc x1)) ⟶ ∀ x1 . nat_p x1 ⟶ x0 x1
Known 21479..^nat_ordsucc : ∀ x0 . nat_p x0 ⟶ nat_p (ordsucc x0)
Theorem 56073..^add_nat_p : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ nat_p (add_nat x0 x1) (proof)
Theorem 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) (proof)
Theorem 0dc7e..^add_nat_0L : ∀ x0 . nat_p x0 ⟶ add_nat 0 x0 = x0 (proof)
Theorem 54250..^add_nat_SL : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ add_nat (ordsucc x0) x1 = ordsucc (add_nat x0 x1) (proof)
Theorem 3fe1c..^add_nat_com : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ add_nat x0 x1 = add_nat x1 x0 (proof)
Known 08405..^nat_0 : nat_p 0
Theorem a7773..^{ordsucc_add_nat_1} : ∀ x0 . ordsucc x0 = add_nat x0 1 (proof)
Theorem 26d71..^{add_nat_1_1_2} : add_nat 1 1 = 2 (proof)
Known 6696a..^Subq_ref : ∀ x0 . Subq x0 x0
Known 2ad64..^Subq_tra : ∀ x0 x1 x2 . Subq x0 x1 ⟶ Subq x1 x2 ⟶ Subq x0 x2
Known 165f2..^ordsuccI1 : ∀ x0 . Subq x0 (ordsucc x0)
Theorem 42514..^add_nat_leq : ∀ x0 x1 . nat_p x1 ⟶ Subq x0 (add_nat x0 x1) (proof)
Known 37124..^orE : ∀ x0 x1 : ο . or x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known e9b50..^ordsuccI1b : ∀ x0 x1 . In x1 x0 ⟶ In x1 (ordsucc x0)
Known b651e..^{ordinal_ordsucc_In_eq} : ∀ x0 x1 . ordinal x0 ⟶ In x1 x0 ⟶ or (In (ordsucc x1) x0) (x0 = ordsucc x1)
Known 08dfe..^{nat_p_ordinal} : ∀ x0 . nat_p x0 ⟶ ordinal x0
Theorem 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) (proof)
Known b0a90..^nat_p_trans : ∀ x0 . nat_p x0 ⟶ ∀ x1 . In x1 x0 ⟶ nat_p x1
Theorem 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) (proof)
Known b4776..^{ordsuccE_impred} : ∀ x0 x1 . In x1 (ordsucc x0) ⟶ ∀ x2 : ο . (In x1 x0 ⟶ x2) ⟶ (x1 = x0 ⟶ x2) ⟶ x2
Theorem 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 (proof)
Known 74738..^ordsucc_inj : ∀ x0 x1 . ordsucc x0 = ordsucc x1 ⟶ x0 = x1
Theorem 002a9..^{add_nat_cancelR} : ∀ x0 x1 x2 . nat_p x2 ⟶ add_nat x0 x2 = add_nat x1 x2 ⟶ x0 = x1 (proof)
Theorem 91fe9..^{add_nat_cancelL} : ∀ x0 x1 x2 . nat_p x0 ⟶ nat_p x1 ⟶ nat_p x2 ⟶ add_nat x0 x1 = add_nat x0 x2 ⟶ x1 = x2 (proof)
Known 5f97b..^mul_nat_def : mul_nat = λ x1 . nat_primrec 0 (λ x2 . add_nat x1)
Theorem fad70..^mul_nat_0R : ∀ x0 . mul_nat x0 0 = 0 (proof)
Theorem a6e5c..^mul_nat_SR : ∀ x0 x1 . nat_p x1 ⟶ mul_nat x0 (ordsucc x1) = add_nat x0 (mul_nat x0 x1) (proof)
Theorem 4f633..^mul_nat_p : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ nat_p (mul_nat x0 x1) (proof)
Theorem 0e99e..^mul_nat_0L : ∀ x0 . nat_p x0 ⟶ mul_nat 0 x0 = 0 (proof)
Theorem c8db6..^mul_nat_SL : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ mul_nat (ordsucc x0) x1 = add_nat (mul_nat x0 x1) x1 (proof)
Theorem d6c64..^mul_nat_com : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ mul_nat x0 x1 = mul_nat x1 x0 (proof)
Theorem f0f64..^{mul_add_nat_distrL} : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ ∀ x2 . nat_p x2 ⟶ mul_nat x0 (add_nat x1 x2) = add_nat (mul_nat x0 x1) (mul_nat x0 x2) (proof)
Theorem d18f8..^{mul_add_nat_distrR} : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ ∀ x2 . nat_p x2 ⟶ mul_nat (add_nat x0 x1) x2 = add_nat (mul_nat x0 x2) (mul_nat x1 x2) (proof)
Theorem 7c82a..^mul_nat_asso : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ ∀ x2 . nat_p x2 ⟶ mul_nat (mul_nat x0 x1) x2 = mul_nat x0 (mul_nat x1 x2) (proof)
Definition 69aae..^exp_nat := λ x0 . nat_primrec 1 (λ x1 . mul_nat x0)
Theorem 94de7..^exp_nat_0 : ∀ x0 . 69aae.. x0 0 = 1 (proof)
Theorem f4890..^exp_nat_S : ∀ x0 x1 . nat_p x1 ⟶ 69aae.. x0 (ordsucc x1) = mul_nat x0 (69aae.. x0 x1) (proof)
Known 74fae..^equip_def : equip = λ x1 x2 . ∀ x3 : ο . (∀ x4 : ι → ι . bij x1 x2 x4 ⟶ x3) ⟶ x3
Theorem f2c5c..^equipI : ∀ x0 x1 . ∀ x2 : ι → ι . bij x0 x1 x2 ⟶ equip x0 x1 (proof)
Theorem c9b7c..^{equipE_impred} : ∀ x0 x1 . equip x0 x1 ⟶ ∀ x2 : ο . (∀ x3 : ι → ι . bij x0 x1 x3 ⟶ x2) ⟶ x2 (proof)
Known 3831d..^{equip_mod_def} : equip_mod = λ x1 x2 x3 . ∀ x4 : ο . (∀ x5 . (∀ x6 : ο . (∀ x7 . or (and (equip (setsum x1 x5) x2) (equip (setprod x7 x5) x3)) (and (equip (setsum x2 x5) x1) (equip (setprod x7 x5) x3)) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4
Known dcbd9..^orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Known 7c02f..^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem 429a0..^equip_mod_I1 : ∀ x0 x1 x2 x3 x4 . equip (setsum x0 x3) x1 ⟶ equip (setprod x4 x3) x2 ⟶ equip_mod x0 x1 x2 (proof)
Known eca40..^orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Theorem dd0ac..^equip_mod_I2 : ∀ x0 x1 x2 x3 x4 . equip (setsum x1 x3) x0 ⟶ equip (setprod x4 x3) x2 ⟶ equip_mod x0 x1 x2 (proof)
Known andE^andE : ∀ x0 x1 : ο . and x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Theorem 35d86..^equip_mod_E : ∀ x0 x1 x2 . equip_mod x0 x1 x2 ⟶ ∀ x3 : ο . (∀ x4 x5 . equip (setsum x0 x4) x1 ⟶ equip (setprod x5 x4) x2 ⟶ x3) ⟶ (∀ x4 x5 . equip (setsum x1 x4) x0 ⟶ equip (setprod x5 x4) x2 ⟶ x3) ⟶ x3 (proof)
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 367e6..^SubqE : ∀ x0 x1 . Subq x0 x1 ⟶ ∀ x2 . In x2 x0 ⟶ In x2 x1
Theorem 9da0d..^inj_incl : ∀ x0 x1 . Subq x0 x1 ⟶ inj x0 x1 (λ x2 . x2) (proof)
Theorem d3779..^inj_id : ∀ x0 . inj x0 x0 (λ x1 . x1) (proof)
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
Theorem 505e8..^bij_id : ∀ x0 . bij x0 x0 (λ x1 . x1) (proof)
Definition ed93b..^inv := λ x0 . λ x1 : ι → ι . λ x2 . Eps_i (λ x3 . and (In x3 x0) (x1 x3 = x2))
Known 4cb75..^Eps_i_R : ∀ x0 : ι → ο . ∀ x1 . x0 x1 ⟶ x0 (Eps_i x0)
Theorem 98109..^surj_rinv : ∀ x0 x1 . ∀ x2 : ι → ι . (∀ x3 . In x3 x1 ⟶ ∀ x4 : ο . (∀ x5 . and (In x5 x0) (x2 x5 = x3) ⟶ x4) ⟶ x4) ⟶ ∀ x3 . In x3 x1 ⟶ and (In (ed93b.. x0 x2 x3) x0) (x2 (ed93b.. x0 x2 x3) = x3) (proof)
Theorem 03dfb..^inj_linv : ∀ x0 x1 . ∀ x2 : ι → ι . (∀ x3 . In x3 x0 ⟶ ∀ x4 . In x4 x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4) ⟶ ∀ x3 . In x3 x0 ⟶ ed93b.. x0 x2 (x2 x3) = x3 (proof)
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
Theorem 14b72..^bij_inv : ∀ x0 x1 . ∀ x2 : ι → ι . bij x0 x1 x2 ⟶ bij x1 x0 (ed93b.. x0 x2) (proof)
Theorem 626f8..^inj_comp : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι . inj x0 x1 x3 ⟶ inj x1 x2 x4 ⟶ inj x0 x2 (λ x5 . x4 (x3 x5)) (proof)
Theorem 43d55..^bij_comp : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι . bij x0 x1 x3 ⟶ bij x1 x2 x4 ⟶ bij x0 x2 (λ x5 . x4 (x3 x5)) (proof)
Theorem 54d4b..^equip_ref : ∀ x0 . equip x0 x0 (proof)
Theorem 637fd..^equip_sym : ∀ x0 x1 . equip x0 x1 ⟶ equip x1 x0 (proof)
Theorem 30edc..^equip_tra : ∀ x0 x1 x2 . equip x0 x1 ⟶ equip x1 x2 ⟶ equip x0 x2 (proof)
Known 93236..^Inj0_setsum : ∀ x0 x1 x2 . In x2 x0 ⟶ In (Inj0 x2) (setsum x0 x1)
Known 49afe..^Inj0_inj : ∀ x0 x1 . Inj0 x0 = Inj0 x1 ⟶ x0 = x1
Theorem 81c90..^inj_Inj0 : ∀ x0 x1 . inj x0 (setsum x0 x1) Inj0 (proof)
Known 9ea3e..^Inj1_setsum : ∀ x0 x1 x2 . In x2 x1 ⟶ In (Inj1 x2) (setsum x0 x1)
Known 0139a..^Inj1_inj : ∀ x0 x1 . Inj1 x0 = Inj1 x1 ⟶ x0 = x1
Theorem cad94..^inj_Inj1 : ∀ x0 x1 . inj x1 (setsum x0 x1) Inj1 (proof)
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 FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Theorem c9834..^{equip_setsum_Empty_R} : ∀ x0 . equip (setsum x0 0) 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 0ce8c..^binunionI1 : ∀ x0 x1 x2 . In x2 x0 ⟶ In x2 (binunion x0 x1)
Known f9974..^{binunionE_cases} : ∀ x0 x1 x2 . In x2 (binunion x0 x1) ⟶ ∀ x3 : ο . (In x2 x0 ⟶ x3) ⟶ (In x2 x1 ⟶ x3) ⟶ x3
Known eb8b4..^binunionI2 : ∀ x0 x1 x2 . In x2 x1 ⟶ In x2 (binunion x0 x1)
Theorem 976df..^{setsum_binunion_distrR} : ∀ x0 x1 x2 . setsum x0 (binunion x1 x2) = binunion (setsum x0 x1) (setsum x0 x2) (proof)
Known 34a93..^{combine_funcs_eq1} : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 . combine_funcs x0 x1 x2 x3 (Inj0 x4) = x2 x4
Known d805a..^{combine_funcs_eq2} : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 . combine_funcs x0 x1 x2 x3 (Inj1 x4) = x3 x4
Known 24526..^nIn_E2 : ∀ x0 x1 . nIn x0 x1 ⟶ In x0 x1 ⟶ False
Known e85f6..^In_irref : ∀ x0 . nIn x0 x0
Theorem 4d857..^{equip_setsum_add_nat} : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ equip (setsum x0 x1) (add_nat x0 x1) (proof)
Theorem 95550..^{combine_funcs_fun} : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι . (∀ x5 . In x5 x0 ⟶ In (x3 x5) x2) ⟶ (∀ x5 . In x5 x1 ⟶ In (x4 x5) x2) ⟶ ∀ x5 . In x5 (setsum x0 x1) ⟶ In (combine_funcs x0 x1 x3 x4 x5) x2 (proof)
Known notE^notE : ∀ x0 : ο . not x0 ⟶ x0 ⟶ False
Theorem 9d9c7..^{combine_funcs_inj} : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι . inj x0 x2 x3 ⟶ inj x1 x2 x4 ⟶ (∀ x5 . In x5 x0 ⟶ ∀ x6 . In x6 x1 ⟶ not (x3 x5 = x4 x6)) ⟶ inj (setsum x0 x1) x2 (combine_funcs x0 x1 x3 x4) (proof)
Theorem 81c90..^inj_Inj0 : ∀ x0 x1 . inj x0 (setsum x0 x1) Inj0 (proof)
Theorem cad94..^inj_Inj1 : ∀ x0 x1 . inj x1 (setsum x0 x1) Inj1 (proof)
Known efcec..^{Inj0_Inj1_neq} : ∀ x0 x1 . not (Inj0 x0 = Inj1 x1)
Theorem 0b5e2..^{equip_setsum_cong} : ∀ x0 x1 x2 x3 . equip x0 x2 ⟶ equip x1 x3 ⟶ equip (setsum x0 x1) (setsum x2 x3) (proof)
Theorem 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) (proof)