Proofgold Address

Known 3aba6..^{exactly1of2_def} : exactly1of2 = λ x1 x2 : ο . or (and x1 (not x2)) (and (not x1) x2)
Known 37124..^orE : ∀ x0 x1 : ο . or x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known andE^andE : ∀ x0 x1 : ο . and x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Theorem 9001d..^{exactly1of2_E} : ∀ x0 x1 : ο . exactly1of2 x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ not x1 ⟶ x2) ⟶ (not x0 ⟶ x1 ⟶ x2) ⟶ x2 (proof)
Known 71e01..^{exactly1of3_def} : exactly1of3 = λ x1 x2 x3 : ο . or (and (exactly1of2 x1 x2) (not x3)) (and (and (not x1) (not x2)) x3)
Known cd094..^and3E : ∀ x0 x1 x2 : ο . and (and x0 x1) x2 ⟶ ∀ x3 : ο . (x0 ⟶ x1 ⟶ x2 ⟶ x3) ⟶ x3
Theorem 374c9..^{exactly1of3_E} : ∀ x0 x1 x2 : ο . exactly1of3 x0 x1 x2 ⟶ ∀ x3 : ο . (x0 ⟶ not x1 ⟶ not x2 ⟶ x3) ⟶ (not x0 ⟶ x1 ⟶ not x2 ⟶ x3) ⟶ (not x0 ⟶ not x1 ⟶ x2 ⟶ x3) ⟶ x3 (proof)
Known bae00..^exu_i_def : exu_i = λ x1 : ι → ο . and (∀ x2 : ο . (∀ x3 . x1 x3 ⟶ x2) ⟶ x2) (∀ x2 x3 . x1 x2 ⟶ x1 x3 ⟶ x2 = x3)
Known 39854..^andEL : ∀ x0 x1 : ο . and x0 x1 ⟶ x0
Theorem 07bf8..^exu_i_E1 : ∀ x0 : ι → ο . exu_i x0 ⟶ ∀ x1 : ο . (∀ x2 . x0 x2 ⟶ x1) ⟶ x1 (proof)
Known eb789..^andER : ∀ x0 x1 : ο . and x0 x1 ⟶ x1
Theorem 5ab2f..^exu_i_E2 : ∀ x0 : ι → ο . exu_i x0 ⟶ ∀ x1 x2 . x0 x1 ⟶ x0 x2 ⟶ x1 = x2 (proof)
Known 7c02f..^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem 984d6..^exu_i_I : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . x0 x2 ⟶ x1) ⟶ x1) ⟶ (∀ x1 x2 . x0 x1 ⟶ x0 x2 ⟶ x1 = x2) ⟶ exu_i x0 (proof)
Known c0d8d..^atleastp_def : atleastp = λ x1 x2 . ∀ x3 : ο . (∀ x4 : ι → ι . inj x1 x2 x4 ⟶ x3) ⟶ x3
Theorem 95b31..^atleastp_I : ∀ x0 x1 . ∀ x2 : ι → ι . inj x0 x1 x2 ⟶ atleastp x0 x1 (proof)
Theorem 97a83..^{atleastp_E_impred} : ∀ x0 x1 . atleastp x0 x1 ⟶ ∀ x2 : ο . (∀ x3 : ι → ι . inj x0 x1 x3 ⟶ x2) ⟶ x2 (proof)
Known f40a4..^ordinal_def : ordinal = λ x1 . and (TransSet x1) (∀ x2 . In x2 x1 ⟶ TransSet x2)
Theorem 42144..^ordinalI : ∀ x0 . TransSet x0 ⟶ (∀ x1 . In x1 x0 ⟶ TransSet x1) ⟶ ordinal x0 (proof)
Known a0d73..^{reflexive_i_def} : reflexive_i = λ x1 : ι → ι → ο . ∀ x2 . x1 x2 x2
Theorem ca9a0..^{reflexive_i_I} : ∀ x0 : ι → ι → ο . (∀ x1 . x0 x1 x1) ⟶ reflexive_i x0 (proof)
Theorem 02f18..^{reflexive_i_E} : ∀ x0 : ι → ι → ο . reflexive_i x0 ⟶ ∀ x1 . x0 x1 x1 (proof)
Known 405a8..^{irreflexive_i_def} : irreflexive_i = λ x1 : ι → ι → ο . ∀ x2 . not (x1 x2 x2)
Theorem 0881c..^{irreflexive_i_I} : ∀ x0 : ι → ι → ο . (∀ x1 . not (x0 x1 x1)) ⟶ irreflexive_i x0 (proof)
Theorem 69f4a..^{irreflexive_i_E} : ∀ x0 : ι → ι → ο . irreflexive_i x0 ⟶ ∀ x1 . not (x0 x1 x1) (proof)
Known 8f759..^{symmetric_i_def} : symmetric_i = λ x1 : ι → ι → ο . ∀ x2 x3 . x1 x2 x3 ⟶ x1 x3 x2
Theorem c3f98..^{symmetric_i_I} : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1) ⟶ symmetric_i x0 (proof)
Theorem 2acec..^{symmetric_i_E} : ∀ x0 : ι → ι → ο . symmetric_i x0 ⟶ ∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1 (proof)
Known 4b633..^{antisymmetric_i_def} : antisymmetric_i = λ x1 : ι → ι → ο . ∀ x2 x3 . x1 x2 x3 ⟶ x1 x3 x2 ⟶ x2 = x3
Theorem 8fcd7..^{antisymmetric_i_I} : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1 ⟶ x1 = x2) ⟶ antisymmetric_i x0 (proof)
Theorem 892dd..^{antisymmetric_i_E} : ∀ x0 : ι → ι → ο . antisymmetric_i x0 ⟶ ∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1 ⟶ x1 = x2 (proof)
Known ab703..^{transitive_i_def} : transitive_i = λ x1 : ι → ι → ο . ∀ x2 x3 x4 . x1 x2 x3 ⟶ x1 x3 x4 ⟶ x1 x2 x4
Theorem 11ad5..^{transitive_i_I} : ∀ x0 : ι → ι → ο . (∀ x1 x2 x3 . x0 x1 x2 ⟶ x0 x2 x3 ⟶ x0 x1 x3) ⟶ transitive_i x0 (proof)
Theorem 01483..^{transitive_i_E} : ∀ x0 : ι → ι → ο . transitive_i x0 ⟶ ∀ x1 x2 x3 . x0 x1 x2 ⟶ x0 x2 x3 ⟶ x0 x1 x3 (proof)
Known ff0c9..^eqreln_i_def : eqreln_i = λ x1 : ι → ι → ο . and (and (reflexive_i x1) (symmetric_i x1)) (transitive_i x1)
Known f6404..^and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Theorem ab1dd..^eqreln_i_I : ∀ x0 : ι → ι → ο . reflexive_i x0 ⟶ symmetric_i x0 ⟶ transitive_i x0 ⟶ eqreln_i x0 (proof)
Theorem 001b9..^eqreln_i_E : ∀ x0 : ι → ι → ο . eqreln_i x0 ⟶ ∀ x1 : ο . (reflexive_i x0 ⟶ symmetric_i x0 ⟶ transitive_i x0 ⟶ x1) ⟶ x1 (proof)
Known 42cf9..^per_i_def : per_i = λ x1 : ι → ι → ο . and (symmetric_i x1) (transitive_i x1)
Theorem 7c1a4..^per_i_I : ∀ x0 : ι → ι → ο . symmetric_i x0 ⟶ transitive_i x0 ⟶ per_i x0 (proof)
Theorem 14d50..^per_i_E : ∀ x0 : ι → ι → ο . per_i x0 ⟶ ∀ x1 : ο . (symmetric_i x0 ⟶ transitive_i x0 ⟶ x1) ⟶ x1 (proof)
Known 35346..^linear_i_def : linear_i = λ x1 : ι → ι → ο . ∀ x2 x3 . or (x1 x2 x3) (x1 x3 x2)
Theorem c2d56..^linear_i_I : ∀ x0 : ι → ι → ο . (∀ x1 x2 . or (x0 x1 x2) (x0 x2 x1)) ⟶ linear_i x0 (proof)
Theorem 9f4d7..^linear_i_E : ∀ x0 : ι → ι → ο . linear_i x0 ⟶ ∀ x1 x2 . or (x0 x1 x2) (x0 x2 x1) (proof)
Known b6f2a..^{trichotomous_or_i_def} : trichotomous_or_i = λ x1 : ι → ι → ο . ∀ x2 x3 . or (or (x1 x2 x3) (x2 = x3)) (x1 x3 x2)
Theorem e060d..^{trichotomous_or_i_I} : ∀ x0 : ι → ι → ο . (∀ x1 x2 . or (or (x0 x1 x2) (x1 = x2)) (x0 x2 x1)) ⟶ trichotomous_or_i x0 (proof)
Theorem a26a2..^{trichotomous_or_i_E} : ∀ x0 : ι → ι → ο . trichotomous_or_i x0 ⟶ ∀ x1 x2 . or (or (x0 x1 x2) (x1 = x2)) (x0 x2 x1) (proof)
Known 9e965..^{partialorder_i_def} : partialorder_i = λ x1 : ι → ι → ο . and (and (reflexive_i x1) (antisymmetric_i x1)) (transitive_i x1)
Theorem 6ddf4..^{partialorder_i_I} : ∀ x0 : ι → ι → ο . reflexive_i x0 ⟶ antisymmetric_i x0 ⟶ transitive_i x0 ⟶ partialorder_i x0 (proof)
Theorem cef0d..^{partialorder_i_E} : ∀ x0 : ι → ι → ο . partialorder_i x0 ⟶ ∀ x1 : ο . (reflexive_i x0 ⟶ antisymmetric_i x0 ⟶ transitive_i x0 ⟶ x1) ⟶ x1 (proof)
Known 79d4c..^{totalorder_i_def} : totalorder_i = λ x1 : ι → ι → ο . and (partialorder_i x1) (linear_i x1)
Theorem dd535..^{totalorder_i_I} : ∀ x0 : ι → ι → ο . partialorder_i x0 ⟶ linear_i x0 ⟶ totalorder_i x0 (proof)
Theorem 7f7bf..^{totalorder_i_E} : ∀ x0 : ι → ι → ο . totalorder_i x0 ⟶ ∀ x1 : ο . (partialorder_i x0 ⟶ linear_i x0 ⟶ x1) ⟶ x1 (proof)
Known 7f470..^{strictpartialorder_i_def} : strictpartialorder_i = λ x1 : ι → ι → ο . and (irreflexive_i x1) (transitive_i x1)
Theorem ac85b..^{strictpartialorder_i_I} : ∀ x0 : ι → ι → ο . irreflexive_i x0 ⟶ transitive_i x0 ⟶ strictpartialorder_i x0 (proof)
Theorem 0ca41..^{strictpartialorder_i_E} : ∀ x0 : ι → ι → ο . strictpartialorder_i x0 ⟶ ∀ x1 : ο . (irreflexive_i x0 ⟶ transitive_i x0 ⟶ x1) ⟶ x1 (proof)
Known 2c8ff..^{stricttotalorder_i_def} : stricttotalorder_i = λ x1 : ι → ι → ο . and (strictpartialorder_i x1) (trichotomous_or_i x1)
Theorem 757f2..^{stricttotalorder_i_I} : ∀ x0 : ι → ι → ο . strictpartialorder_i x0 ⟶ trichotomous_or_i x0 ⟶ stricttotalorder_i x0 (proof)
Theorem 6dabb..^{stricttotalorder_i_E} : ∀ x0 : ι → ι → ο . stricttotalorder_i x0 ⟶ ∀ x1 : ο . (strictpartialorder_i x0 ⟶ trichotomous_or_i x0 ⟶ x1) ⟶ x1 (proof)
Known 5fc88..^binrep_def : binrep = λ x1 x2 . setsum x1 (Power x2)
Known 93236..^Inj0_setsum : ∀ x0 x1 x2 . In x2 x0 ⟶ In (Inj0 x2) (setsum x0 x1)
Theorem a834f..^binrep_I1 : ∀ x0 x1 x2 . In x2 x0 ⟶ In (Inj0 x2) (binrep x0 x1) (proof)
Known 9ea3e..^Inj1_setsum : ∀ x0 x1 x2 . In x2 x1 ⟶ In (Inj1 x2) (setsum x0 x1)
Known 2d44a..^PowerI : ∀ x0 x1 . Subq x1 x0 ⟶ In x1 (Power x0)
Theorem 2e489..^binrep_I2 : ∀ x0 x1 x2 . Subq x2 x1 ⟶ In (Inj1 x2) (binrep x0 x1) (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 ae89b..^PowerE : ∀ x0 x1 . In x1 (Power x0) ⟶ Subq x1 x0
Theorem e7637..^binrep_E : ∀ x0 x1 x2 . In x2 (binrep x0 x1) ⟶ ∀ x3 : ι → ο . (∀ x4 . In x4 x0 ⟶ x3 (Inj0 x4)) ⟶ (∀ x4 . Subq x4 x1 ⟶ x3 (Inj1 x4)) ⟶ x3 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
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)
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 def11..^tuple_p_def : tuple_p = λ x1 x2 . ∀ x3 . In x3 x2 ⟶ ∀ x4 : ο . (∀ x5 . and (In x5 x1) (∀ x6 : ο . (∀ x7 . x3 = setsum x5 x7 ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4
Theorem d1b61..^tuple_p_I : ∀ x0 x1 . (∀ x2 . In x2 x1 ⟶ ∀ x3 : ο . (∀ x4 . and (In x4 x0) (∀ x5 : ο . (∀ x6 . x2 = setsum x4 x6 ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3) ⟶ tuple_p x0 x1 (proof)
Theorem e716c..^tuple_p_E : ∀ x0 x1 . tuple_p x0 x1 ⟶ ∀ x2 . In x2 x1 ⟶ ∀ x3 : ο . (∀ x4 . and (In x4 x0) (∀ x5 : ο . (∀ x6 . x2 = setsum x4 x6 ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3 (proof)
Known 3c3a9..^setexp_def : setexp = λ x1 x2 . Pi x2 (λ x3 . x1)
Theorem 4322e..^setexp_I : ∀ x0 x1 x2 . In x2 (Pi x0 (λ x3 . x1)) ⟶ In x2 (setexp x1 x0) (proof)
Theorem 4bf71..^setexp_E : ∀ x0 x1 x2 . In x2 (setexp x1 x0) ⟶ In x2 (Pi x0 (λ x3 . x1)) (proof)
Known 244ad..^lam2_def : lam2 = λ x1 . λ x2 : ι → ι . λ x3 : ι → ι → ι . lam x1 (λ x4 . lam (x2 x4) (x3 x4))
Known f9ff3..^lamI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 x0 ⟶ ∀ x3 . In x3 (x1 x2) ⟶ In (setsum x2 x3) (lam x0 x1)
Theorem 935d6..^lam2_I : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ι . ∀ x3 . In x3 x0 ⟶ ∀ x4 . In x4 (x1 x3) ⟶ ∀ x5 . In x5 (x2 x3 x4) ⟶ In (setsum x3 (setsum x4 x5)) (lam2 x0 x1 x2) (proof)
Known 9799b..^lamE_impred : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 (lam x0 x1) ⟶ ∀ x3 : ι → ο . (∀ x4 . In x4 x0 ⟶ ∀ x5 . In x5 (x1 x4) ⟶ x3 (setsum x4 x5)) ⟶ x3 x2
Theorem 69b58..^lam2_E : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ι . ∀ x3 . In x3 (lam2 x0 x1 x2) ⟶ ∀ x4 : ο . (∀ x5 . and (In x5 x0) (∀ x6 : ο . (∀ x7 . and (In x7 (x1 x5)) (∀ x8 : ο . (∀ x9 . and (In x9 (x2 x5 x7)) (x3 = setsum x5 (setsum x7 x9)) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4 (proof)
Theorem 06ef3..^{lam2_E_impred} : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ι . ∀ x3 . In x3 (lam2 x0 x1 x2) ⟶ ∀ x4 : ι → ο . (∀ x5 . In x5 x0 ⟶ ∀ x6 . In x6 (x1 x5) ⟶ ∀ x7 . In x7 (x2 x5 x6) ⟶ x4 (setsum x5 (setsum x6 x7))) ⟶ x4 x3 (proof)
Known 6e7a2..^{pair_tuple_fun} : setsum = λ x1 x2 . lam 2 (λ x3 . If_i (x3 = 0) x1 x2)
Theorem d46d7..^lam2_I2 : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ι . ∀ x3 . In x3 x0 ⟶ ∀ x4 . In x4 (x1 x3) ⟶ ∀ x5 . In x5 (x2 x3 x4) ⟶ In (lam 2 (λ x6 . If_i (x6 = 0) x3 (lam 2 (λ x7 . If_i (x7 = 0) x4 x5)))) (lam2 x0 x1 x2) (proof)
Theorem 809b5..^lam2_E2 : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ι . ∀ x3 . In x3 (lam2 x0 x1 x2) ⟶ ∀ x4 : ο . (∀ x5 . and (In x5 x0) (∀ x6 : ο . (∀ x7 . and (In x7 (x1 x5)) (∀ x8 : ο . (∀ x9 . and (In x9 (x2 x5 x7)) (x3 = lam 2 (λ x11 . If_i (x11 = 0) x5 (lam 2 (λ x12 . If_i (x12 = 0) x7 x9)))) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4 (proof)
Theorem a7e02..^{lam2_E2_impred} : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ι . ∀ x3 . In x3 (lam2 x0 x1 x2) ⟶ ∀ x4 : ι → ο . (∀ x5 . In x5 x0 ⟶ ∀ x6 . In x6 (x1 x5) ⟶ ∀ x7 . In x7 (x2 x5 x6) ⟶ x4 (lam 2 (λ x8 . If_i (x8 = 0) x5 (lam 2 (λ x9 . If_i (x9 = 0) x6 x7))))) ⟶ x4 x3 (proof)
Known c4530..^binop_on_def : binop_on = λ x1 . λ x2 : ι → ι → ι . ∀ x3 . In x3 x1 ⟶ ∀ x4 . In x4 x1 ⟶ In (x2 x3 x4) x1
Theorem 86824..^binop_on_I : ∀ x0 . ∀ x1 : ι → ι → ι . (∀ x2 . In x2 x0 ⟶ ∀ x3 . In x3 x0 ⟶ In (x1 x2 x3) x0) ⟶ binop_on x0 x1 (proof)
Theorem 8b9e9..^binop_on_E : ∀ x0 . ∀ x1 : ι → ι → ι . binop_on x0 x1 ⟶ ∀ x2 . In x2 x0 ⟶ ∀ x3 . In x3 x0 ⟶ In (x1 x2 x3) x0 (proof)