Proofgold Address

Known andE^andE : ∀ x0 x1 : ο . and x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Theorem 17e35..^exandE_ii : ∀ x0 x1 : (ι → ι) → ο . (∀ x2 : ο . (∀ x3 : ι → ι . and (x0 x3) (x1 x3) ⟶ x2) ⟶ x2) ⟶ ∀ x2 : ο . (∀ x3 : ι → ι . x0 x3 ⟶ x1 x3 ⟶ x2) ⟶ x2 (proof)
Known 3aba6..^{exactly1of2_def} : exactly1of2 = λ x1 x2 : ο . or (and x1 (not x2)) (and (not x1) x2)
Known 26b88..^tab_pos_or : ∀ x0 x1 : ο . or x0 x1 ⟶ (x0 ⟶ False) ⟶ (x1 ⟶ False) ⟶ False
Theorem 70d65..^{tab_pos_exactly1of2} : ∀ x0 x1 : ο . exactly1of2 x0 x1 ⟶ (x0 ⟶ not x1 ⟶ False) ⟶ (not x0 ⟶ x1 ⟶ False) ⟶ False (proof)
Known 6a5f4..^tab_neg_or : ∀ x0 x1 : ο . not (or x0 x1) ⟶ (not x0 ⟶ not x1 ⟶ False) ⟶ False
Known 77eb0..^tab_neg_and : ∀ x0 x1 : ο . not (and x0 x1) ⟶ (not x0 ⟶ False) ⟶ (not x1 ⟶ False) ⟶ False
Known notE^notE : ∀ x0 : ο . not x0 ⟶ x0 ⟶ False
Known 5f92b..^dneg : ∀ x0 : ο . not (not x0) ⟶ x0
Theorem 6fb1f..^{tab_neg_exactly1of2} : ∀ x0 x1 : ο . not (exactly1of2 x0 x1) ⟶ (x0 ⟶ x1 ⟶ False) ⟶ (not x0 ⟶ not x1 ⟶ False) ⟶ False (proof)
Known 71e01..^{exactly1of3_def} : exactly1of3 = λ x1 x2 x3 : ο . or (and (exactly1of2 x1 x2) (not x3)) (and (and (not x1) (not x2)) x3)
Known 57def..^tab_pos_and : ∀ x0 x1 : ο . and x0 x1 ⟶ (x0 ⟶ x1 ⟶ False) ⟶ False
Theorem 60b29..^{tab_pos_exactly1of3} : ∀ x0 x1 x2 : ο . exactly1of3 x0 x1 x2 ⟶ (x0 ⟶ not x1 ⟶ not x2 ⟶ False) ⟶ (not x0 ⟶ x1 ⟶ not x2 ⟶ False) ⟶ (not x0 ⟶ not x1 ⟶ x2 ⟶ False) ⟶ False (proof)
Theorem e5479..^{tab_neg_exactly1of3} : ∀ x0 x1 x2 : ο . not (exactly1of3 x0 x1 x2) ⟶ (not x0 ⟶ not x1 ⟶ not x2 ⟶ False) ⟶ (x0 ⟶ x1 ⟶ False) ⟶ (x0 ⟶ x2 ⟶ False) ⟶ (x1 ⟶ x2 ⟶ False) ⟶ False (proof)
Known b4782..^contra : ∀ x0 : ο . (not x0 ⟶ False) ⟶ x0
Known 24526..^nIn_E2 : ∀ x0 x1 . nIn x0 x1 ⟶ In x0 x1 ⟶ False
Known 61ad0..^In_ind : ∀ x0 : ι → ο . (∀ x1 . (∀ x2 . In x2 x1 ⟶ x0 x2) ⟶ x0 x1) ⟶ ∀ x1 . x0 x1
Known 9d2e6..^nIn_I2 : ∀ x0 x1 . (In x0 x1 ⟶ False) ⟶ nIn x0 x1
Known 7c02f..^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known 8106d..^notI : ∀ x0 : ο . (x0 ⟶ False) ⟶ not x0
Known 61640..^exandE_i : ∀ x0 x1 : ι → ο . (∀ x2 : ο . (∀ x3 . and (x0 x3) (x1 x3) ⟶ x2) ⟶ x2) ⟶ ∀ x2 : ο . (∀ x3 . x0 x3 ⟶ x1 x3 ⟶ x2) ⟶ x2
Theorem 3903a..^Regularity : ∀ x0 x1 . In x1 x0 ⟶ ∀ x2 : ο . (∀ x3 . and (In x3 x0) (not (∀ x4 : ο . (∀ x5 . and (In x5 x0) (In x5 x3) ⟶ x4) ⟶ x4)) ⟶ x2) ⟶ x2 (proof)
Known 6e0ca..^{In_rec_G_i_def} : In_rec_poly_G_i = λ x1 : ι → (ι → ι) → ι . λ x2 x3 . ∀ x4 : ι → ι → ο . (∀ x5 . ∀ x6 : ι → ι . (∀ x7 . In x7 x5 ⟶ x4 x7 (x6 x7)) ⟶ x4 x5 (x1 x5 x6)) ⟶ x4 x2 x3
Theorem 0857e..^In_rec_G_i_c : ∀ x0 : ι → (ι → ι) → ι . ∀ x1 . ∀ x2 : ι → ι . (∀ x3 . In x3 x1 ⟶ In_rec_poly_G_i x0 x3 (x2 x3)) ⟶ In_rec_poly_G_i x0 x1 (x0 x1 x2) (proof)
Theorem a0610..^{In_rec_G_i_inv} : ∀ x0 : ι → (ι → ι) → ι . ∀ x1 x2 . In_rec_poly_G_i x0 x1 x2 ⟶ ∀ x3 : ο . (∀ x4 : ι → ι . and (∀ x5 . In x5 x1 ⟶ In_rec_poly_G_i x0 x5 (x4 x5)) (x2 = x0 x1 x4) ⟶ x3) ⟶ x3 (proof)
Theorem e5412..^In_rec_G_i_f : ∀ x0 : ι → (ι → ι) → ι . (∀ x1 . ∀ x2 x3 : ι → ι . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 x2 x3 . In_rec_poly_G_i x0 x1 x2 ⟶ In_rec_poly_G_i x0 x1 x3 ⟶ x2 = x3 (proof)
Known 02a06..^In_rec_i_def : In_rec_poly_i = λ x1 : ι → (ι → ι) → ι . λ x2 . Eps_i (In_rec_poly_G_i x1 x2)
Known 4cb75..^Eps_i_R : ∀ x0 : ι → ο . ∀ x1 . x0 x1 ⟶ x0 (Eps_i x0)
Theorem 6f6a6..^{In_rec_G_i_In_rec_i} : ∀ x0 : ι → (ι → ι) → ι . (∀ x1 . ∀ x2 x3 : ι → ι . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . In_rec_poly_G_i x0 x1 (In_rec_poly_i x0 x1) (proof)
Theorem bcc7f..^{In_rec_G_i_In_rec_d} : ∀ x0 : ι → (ι → ι) → ι . (∀ x1 . ∀ x2 x3 : ι → ι . (∀ x4 . In x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . In_rec_poly_G_i x0 x1 (x0 x1 (In_rec_poly_i x0)) (proof)
Theorem 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) (proof)
Known 2cd4b..^Inj1_def : Inj1 = In_rec_poly_i (λ x1 . λ x2 : ι → ι . binunion (Sing 0) (Repl x1 x2))
Known 09697..^ReplEq_ext : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . In x3 x0 ⟶ x1 x3 = x2 x3) ⟶ Repl x0 x1 = Repl x0 x2
Theorem d1941..^Inj1_eq : ∀ x0 . Inj1 x0 = binunion (Sing 0) (Repl x0 Inj1) (proof)
Known 0ce8c..^binunionI1 : ∀ x0 x1 x2 . In x2 x0 ⟶ In x2 (binunion x0 x1)
Known 1f15b..^SingI : ∀ x0 . In x0 (Sing x0)
Theorem 8d83e..^Inj1I1 : ∀ x0 . In 0 (Inj1 x0) (proof)
Known eb8b4..^binunionI2 : ∀ x0 x1 x2 . In x2 x1 ⟶ In x2 (binunion x0 x1)
Known f1bf4..^ReplI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 x0 ⟶ In (x1 x2) (Repl x0 x1)
Theorem 22441..^Inj1I2 : ∀ x0 x1 . In x1 x0 ⟶ In (Inj1 x1) (Inj1 x0) (proof)
Known f9974..^{binunionE_cases} : ∀ x0 x1 x2 . In x2 (binunion x0 x1) ⟶ ∀ x3 : ο . (In x2 x0 ⟶ x3) ⟶ (In x2 x1 ⟶ x3) ⟶ x3
Known dcbd9..^orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Known 9ae18..^SingE : ∀ x0 x1 . In x1 (Sing x0) ⟶ x1 = x0
Known eca40..^orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Known 74a75..^ReplE : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 (Repl x0 x1) ⟶ ∀ x3 : ο . (∀ x4 . and (In x4 x0) (x2 = x1 x4) ⟶ x3) ⟶ x3
Theorem f3200..^Inj1E : ∀ x0 x1 . In x1 (Inj1 x0) ⟶ or (x1 = 0) (∀ x2 : ο . (∀ x3 . and (In x3 x0) (x1 = Inj1 x3) ⟶ x2) ⟶ x2) (proof)
Known 37124..^orE : ∀ x0 x1 : ο . or x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Theorem 474ab..^Inj1E_impred : ∀ x0 x1 . In x1 (Inj1 x0) ⟶ ∀ x2 : ι → ο . x2 0 ⟶ (∀ x3 . In x3 x0 ⟶ x2 (Inj1 x3)) ⟶ x2 x1 (proof)
Known 2901c..^EmptyE : ∀ x0 . In x0 0 ⟶ False
Theorem a1706..^Inj1NE1 : ∀ x0 . not (Inj1 x0 = 0) (proof)
Theorem a6792..^Inj1NE2 : ∀ x0 . nIn (Inj1 x0) (Sing 0) (proof)
Known 4f75b..^Inj0_def : Inj0 = λ x1 . Repl x1 Inj1
Theorem 88e5c..^Inj0I : ∀ x0 x1 . In x1 x0 ⟶ In (Inj1 x1) (Inj0 x0) (proof)
Theorem 0e45c..^Inj0E : ∀ x0 x1 . In x1 (Inj0 x0) ⟶ ∀ x2 : ο . (∀ x3 . and (In x3 x0) (x1 = Inj1 x3) ⟶ x2) ⟶ x2 (proof)
Theorem 5bd6f..^Inj0E_impred : ∀ x0 x1 . In x1 (Inj0 x0) ⟶ ∀ x2 : ι → ο . (∀ x3 . In x3 x0 ⟶ x2 (Inj1 x3)) ⟶ x2 x1 (proof)
Known f7ea7..^Unj_def : Unj = In_rec_poly_i (λ x1 . Repl (setminus x1 (Sing 0)))
Known 54d83..^setminusE1 : ∀ x0 x1 x2 . In x2 (setminus x0 x1) ⟶ In x2 x0
Theorem f52b8..^Unj_eq : ∀ x0 . Unj x0 = Repl (setminus x0 (Sing 0)) Unj (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 0f096..^ReplE2 : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 (Repl x0 x1) ⟶ ∀ x3 : ο . (∀ x4 . In x4 x0 ⟶ x2 = x1 x4 ⟶ x3) ⟶ x3
Known 243aa..^{setminusE_impred} : ∀ x0 x1 x2 . In x2 (setminus x0 x1) ⟶ ∀ x3 : ο . (In x2 x0 ⟶ nIn x2 x1 ⟶ x3) ⟶ x3
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Known 626dc..^setminusI : ∀ x0 x1 x2 . In x2 x0 ⟶ nIn x2 x1 ⟶ In x2 (setminus x0 x1)
Theorem c76aa..^Unj_Inj1_eq : ∀ x0 . Unj (Inj1 x0) = x0 (proof)
Theorem 0139a..^Inj1_inj : ∀ x0 x1 . Inj1 x0 = Inj1 x1 ⟶ x0 = x1 (proof)
Theorem c3d4f..^Unj_Inj0_eq : ∀ x0 . Unj (Inj0 x0) = x0 (proof)
Theorem 49afe..^Inj0_inj : ∀ x0 x1 . Inj0 x0 = Inj0 x1 ⟶ x0 = x1 (proof)
Known 8a1cd..^Repl_Empty : ∀ x0 : ι → ι . Repl 0 x0 = 0
Theorem fc3ab..^Inj0_0 : Inj0 0 = 0 (proof)
Theorem efcec..^{Inj0_Inj1_neq} : ∀ x0 x1 . not (Inj0 x0 = Inj1 x1) (proof)
Known 26db0..^setsum_def : setsum = λ x1 x2 . binunion (Repl x1 Inj0) (Repl x2 Inj1)
Theorem 93236..^Inj0_setsum : ∀ x0 x1 x2 . In x2 x0 ⟶ In (Inj0 x2) (setsum x0 x1) (proof)
Theorem 9ea3e..^Inj1_setsum : ∀ x0 x1 x2 . In x2 x1 ⟶ In (Inj1 x2) (setsum x0 x1) (proof)
Theorem 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) (proof)
Theorem 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 (proof)
Theorem b9c5c..^{Inj0_setsum_0L} : ∀ x0 . setsum 0 x0 = Inj0 x0 (proof)
Known b0dce..^SubqI : ∀ x0 x1 . (∀ x2 . In x2 x0 ⟶ In x2 x1) ⟶ Subq x0 x1
Known 367e6..^SubqE : ∀ x0 x1 . Subq x0 x1 ⟶ ∀ x2 . In x2 x0 ⟶ In x2 x1
Theorem 374e6..^pairSubq : ∀ x0 x1 x2 x3 . Subq x0 x2 ⟶ Subq x1 x3 ⟶ Subq (setsum x0 x1) (setsum x2 x3) (proof)
Known 59a1f..^{combine_funcs_def} : combine_funcs = λ x1 x2 . λ x3 x4 : ι → ι . λ x5 . If_i (x5 = Inj0 (Unj x5)) (x3 (Unj x5)) (x4 (Unj x5))
Known 0d2f9..^If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0 ⟶ If_i x0 x1 x2 = x1
Theorem 34a93..^{combine_funcs_eq1} : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 . combine_funcs x0 x1 x2 x3 (Inj0 x4) = x2 x4 (proof)
Known 81513..^If_i_0 : ∀ x0 : ο . ∀ x1 x2 . not x0 ⟶ If_i x0 x1 x2 = x2
Theorem d805a..^{combine_funcs_eq2} : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 . combine_funcs x0 x1 x2 x3 (Inj1 x4) = x3 x4 (proof)