Proofgold Address

Known 535f2..^set_ext_2 : ∀ x0 x1 . (∀ x2 . In x2 x0 ⟶ In x2 x1) ⟶ (∀ x2 . In x2 x1 ⟶ In x2 x0) ⟶ x0 = x1
Known 970d5..^apI : ∀ x0 x1 x2 . In (setsum x1 x2) x0 ⟶ In x2 (ap x0 x1)
Known 88f5c..^proj0E : ∀ x0 x1 . In x1 (proj0 x0) ⟶ In (setsum 0 x1) x0
Known afc0a..^proj0I : ∀ x0 x1 . In (setsum 0 x1) x0 ⟶ In x1 (proj0 x0)
Known 0bd41..^apE : ∀ x0 x1 x2 . In x2 (ap x0 x1) ⟶ In (setsum x1 x2) x0
Theorem 82f37..^proj0_ap_0 : ∀ x0 . proj0 x0 = ap x0 0 (proof)
Known 13e9e..^proj1E : ∀ x0 x1 . In x1 (proj1 x0) ⟶ In (setsum 1 x1) x0
Known 16411..^proj1I : ∀ x0 x1 . In (setsum 1 x1) x0 ⟶ In x1 (proj1 x0)
Theorem 3342b..^proj1_ap_1 : ∀ x0 . proj1 x0 = ap x0 1 (proof)
Known d6e1a..^{proj0_pair_eq} : ∀ x0 x1 . proj0 (setsum x0 x1) = x0
Theorem ca18d..^pair_ap_0 : ∀ x0 x1 . ap (setsum x0 x1) 0 = x0 (proof)
Known b8fac..^{proj1_pair_eq} : ∀ x0 x1 . proj1 (setsum x0 x1) = x1
Theorem dcb97..^pair_ap_1 : ∀ x0 x1 . ap (setsum x0 x1) 1 = x1 (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 37124..^orE : ∀ x0 x1 : ο . or x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known 2ce7d..^pairE : ∀ x0 x1 x2 . In x2 (setsum x0 x1) ⟶ or (∀ x3 : ο . (∀ x4 . and (In x4 x0) (x2 = setsum 0 x4) ⟶ x3) ⟶ x3) (∀ x3 : ο . (∀ x4 . and (In x4 x1) (x2 = setsum 1 x4) ⟶ x3) ⟶ x3)
Known 61640..^exandE_i : ∀ x0 x1 : ι → ο . (∀ x2 : ο . (∀ x3 . and (x0 x3) (x1 x3) ⟶ x2) ⟶ x2) ⟶ ∀ x2 : ο . (∀ x3 . x0 x3 ⟶ x1 x3 ⟶ x2) ⟶ x2
Known 24526..^nIn_E2 : ∀ x0 x1 . nIn x0 x1 ⟶ In x0 x1 ⟶ False
Known 39854..^andEL : ∀ x0 x1 : ο . and x0 x1 ⟶ x0
Known a1bad..^pair_inj : ∀ x0 x1 x2 x3 . setsum x0 x1 = setsum x2 x3 ⟶ and (x0 = x2) (x1 = x3)
Known 0863e..^In_0_2 : In 0 2
Known 0a117..^In_1_2 : In 1 2
Theorem e90b3..^pair_ap_n2 : ∀ x0 x1 x2 . nIn x2 2 ⟶ ap (setsum x0 x1) x2 = 0 (proof)
Known 8da7f..^{pair_eta_Subq_proj} : ∀ x0 . Subq (setsum (proj0 x0) (proj1 x0)) x0
Theorem 2aea4..^{pair_eta_Subq} : ∀ x0 . Subq (setsum (ap x0 0) (ap x0 1)) x0 (proof)
Known 3057f..^proj0_Sigma : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 (lam x0 x1) ⟶ In (proj0 x2) x0
Theorem 1194c..^ap0_Sigma : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 (lam x0 x1) ⟶ In (ap x2 0) x0 (proof)
Known 6bfcf..^proj1_Sigma : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 (lam x0 x1) ⟶ In (proj1 x2) (x1 (proj0 x2))
Theorem a6609..^ap1_Sigma : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 (lam x0 x1) ⟶ In (ap x2 1) (x1 (ap x2 0)) (proof)
Known 413ee..^{proj_Sigma_eta} : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 (lam x0 x1) ⟶ setsum (proj0 x2) (proj1 x2) = x2
Theorem 43d10..^Sigma_eta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 (lam x0 x1) ⟶ setsum (ap x2 0) (ap x2 1) = x2 (proof)
Known 09697..^ReplEq_ext : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . In x3 x0 ⟶ x1 x3 = x2 x3) ⟶ Repl x0 x1 = Repl x0 x2
Known ad99c..^setprod_def : setprod = λ x1 x2 . lam x1 (λ x3 . x2)
Theorem 5fe5d..^{ReplEq_setprod_ext} : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . (∀ x4 . In x4 x0 ⟶ ∀ x5 . In x5 x1 ⟶ x2 x4 x5 = x3 x4 x5) ⟶ Repl (setprod x0 x1) (λ x5 . x2 (ap x5 0) (ap x5 1)) = Repl (setprod x0 x1) (λ x5 . x3 (ap x5 0) (ap x5 1)) (proof)
Known fb6e4..^setsum_p_def : setsum_p = λ x1 . setsum (ap x1 0) (ap x1 1) = x1
Theorem d0663..^setsum_p_E : ∀ x0 . setsum_p x0 ⟶ ∀ x1 : ι → ο . (∀ x2 x3 . x1 (setsum x2 x3)) ⟶ x1 x0 (proof)
Theorem b2553..^setsum_p_I : ∀ x0 x1 . setsum_p (setsum x0 x1) (proof)
Known 2a3f2..^pairE_impred : ∀ x0 x1 x2 . In x2 (setsum x0 x1) ⟶ ∀ x3 : ι → ο . (∀ x4 . In x4 x0 ⟶ x3 (setsum 0 x4)) ⟶ (∀ x4 . In x4 x1 ⟶ x3 (setsum 1 x4)) ⟶ x3 x2
Known 65d0d..^{ReplSepE_impred} : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 : ι → ι . ∀ x3 . In x3 (ReplSep x0 x1 x2) ⟶ ∀ x4 : ο . (∀ x5 . In x5 x0 ⟶ x1 x5 ⟶ x3 = x2 x5 ⟶ x4) ⟶ x4
Known andE^andE : ∀ x0 x1 : ο . and x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Known 7aad1..^UPairE_cases : ∀ x0 x1 x2 . In x0 (UPair x1 x2) ⟶ ∀ x3 : ο . (x0 = x1 ⟶ x3) ⟶ (x0 = x2 ⟶ x3) ⟶ x3
Known 65c61..^pairI0 : ∀ x0 x1 x2 . In x2 x0 ⟶ In (setsum 0 x2) (setsum x0 x1)
Known 9fdc4..^ReplSepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 : ι → ι . ∀ x3 . In x3 x0 ⟶ x1 x3 ⟶ In (x2 x3) (ReplSep x0 x1 x2)
Known 77980..^pairI1 : ∀ x0 x1 x2 . In x2 x1 ⟶ In (setsum 1 x2) (setsum x0 x1)
Known 367e6..^SubqE : ∀ x0 x1 . Subq x0 x1 ⟶ ∀ x2 . In x2 x0 ⟶ In x2 x1
Known 8fa42..^{Subq_2_UPair01} : Subq 2 (UPair 0 1)
Theorem b4313..^setsum_p_I2 : ∀ x0 . (∀ x1 . In x1 x0 ⟶ and (setsum_p x1) (In (ap x1 0) 2)) ⟶ setsum_p x0 (proof)
Theorem f8570..^{setsum_p_In_ap} : ∀ x0 x1 . setsum_p x0 ⟶ In x0 x1 ⟶ In (ap x0 1) (ap x1 (ap x0 0)) (proof)
Known prop_ext_2^prop_ext_2 : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ x0 = x1
Theorem pred_ext_2^pred_ext_i : ∀ x0 x1 : ι → ο . (∀ x2 . x0 x2 ⟶ x1 x2) ⟶ (∀ x2 . x1 x2 ⟶ x0 x2) ⟶ x0 = x1 (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
Known 7c02f..^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem 47657..^{setsum_p_tuple2} : setsum_p = tuple_p 2 (proof)
Known e3e5f..^lamE : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 (lam x0 x1) ⟶ ∀ x3 : ο . (∀ x4 . and (In x4 x0) (∀ x5 : ο . (∀ x6 . and (In x6 (x1 x4)) (x2 = setsum x4 x6) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3
Theorem 1cbf4..^{tuple_p_2_tuple} : ∀ x0 x1 . tuple_p 2 (lam 2 (λ x2 . If_i (x2 = 0) x0 x1)) (proof)
Theorem bd5ac..^{tuple_p_3_tuple} : ∀ x0 x1 x2 . tuple_p 3 (lam 3 (λ x3 . If_i (x3 = 0) x0 (If_i (x3 = 1) x1 x2))) (proof)
Theorem 6947c..^{tuple_p_4_tuple} : ∀ x0 x1 x2 x3 . tuple_p 4 (lam 4 (λ x4 . If_i (x4 = 0) x0 (If_i (x4 = 1) x1 (If_i (x4 = 2) x2 x3)))) (proof)
Known f9ff3..^lamI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 x0 ⟶ ∀ x3 . In x3 (x1 x2) ⟶ In (setsum x2 x3) (lam x0 x1)
Known 0d2f9..^If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0 ⟶ If_i x0 x1 x2 = x1
Known 81513..^If_i_0 : ∀ x0 : ο . ∀ x1 x2 . not x0 ⟶ If_i x0 x1 x2 = x2
Known a871f..^neq_1_0 : not (1 = 0)
Theorem 7fead..^tuple_pair : ∀ x0 x1 . setsum x0 x1 = lam 2 (λ x3 . If_i (x3 = 0) x0 x1) (proof)
Known ca1b6..^Pi_def : Pi = λ x1 . λ x2 : ι → ι . Sep (Power (lam x1 (λ x3 . Union (x2 x3)))) (λ x3 . ∀ x4 . In x4 x1 ⟶ In (ap x3 x4) (x2 x4))
Known dab1f..^SepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . In x2 x0 ⟶ x1 x2 ⟶ In x2 (Sep x0 x1)
Known 2d44a..^PowerI : ∀ x0 x1 . Subq x1 x0 ⟶ In x1 (Power x0)
Known b0dce..^SubqI : ∀ x0 x1 . (∀ x2 . In x2 x0 ⟶ In x2 x1) ⟶ Subq x0 x1
Known a4d26..^UnionI : ∀ x0 x1 x2 . In x1 x2 ⟶ In x2 x0 ⟶ In x1 (Union x0)
Theorem 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) (proof)
Known aa3f4..^SepE_impred : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . In x2 (Sep x0 x1) ⟶ ∀ x3 : ο . (In x2 x0 ⟶ x1 x2 ⟶ x3) ⟶ x3
Known ae89b..^PowerE : ∀ x0 x1 . In x1 (Power x0) ⟶ Subq x1 x0
Theorem 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 (proof)
Theorem 8dccb..^PiE : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 (Pi x0 x1) ⟶ and (∀ x3 . In x3 x2 ⟶ and (setsum_p x3) (In (ap x3 0) x0)) (∀ x3 . In x3 x0 ⟶ In (ap x2 x3) (x1 x3)) (proof)
Known 32c82..^iffI : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ iff x0 x1
Theorem cab70..^PiEq : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . iff (In x2 (Pi x0 x1)) (and (∀ x3 . In x3 x2 ⟶ and (setsum_p x3) (In (ap x3 0) x0)) (∀ x3 . In x3 x0 ⟶ In (ap x2 x3) (x1 x3))) (proof)
Known b515a..^beta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 x0 ⟶ ap (lam x0 x1) x2 = x1 x2
Theorem 25543..^lam_Pi : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . In x3 x0 ⟶ In (x2 x3) (x1 x3)) ⟶ In (lam x0 x2) (Pi x0 x1) (proof)
Known 076ba..^SepE2 : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . In x2 (Sep x0 x1) ⟶ x1 x2
Theorem 31c25..^ap_Pi : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . In x2 (Pi x0 x1) ⟶ In x3 x0 ⟶ In (ap x2 x3) (x1 x3) (proof)
Theorem 44e63..^Pi_ext_Subq : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 (Pi x0 x1) ⟶ ∀ x3 . In x3 (Pi x0 x1) ⟶ (∀ x4 . In x4 x0 ⟶ Subq (ap x2 x4) (ap x3 x4)) ⟶ Subq x2 x3 (proof)
Known b3824..^set_ext : ∀ x0 x1 . Subq x0 x1 ⟶ Subq x1 x0 ⟶ x0 = x1
Known 6696a..^Subq_ref : ∀ x0 . Subq x0 x0
Theorem 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 (proof)
Theorem eb933..^Pi_eta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 (Pi x0 x1) ⟶ lam x0 (ap x2) = x2 (proof)
Known 0978b..^In_0_1 : In 0 1
Known 2901c..^EmptyE : ∀ x0 . In x0 0 ⟶ False
Known 9ae18..^SingE : ∀ x0 x1 . In x1 (Sing x0) ⟶ x1 = x0
Known 830d8..^Subq_1_Sing0 : Subq 1 (Sing 0)
Theorem 99b3b..^Pi_Power_1 : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . In x2 x0 ⟶ In (x1 x2) (Power 1)) ⟶ In (Pi x0 x1) (Power 1) (proof)
Known 3ab01..^xmcases_In : ∀ x0 x1 . ∀ x2 : ο . (In x0 x1 ⟶ x2) ⟶ (nIn x0 x1 ⟶ x2) ⟶ x2
Known 4862c..^beta0 : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . nIn x2 x0 ⟶ ap (lam x0 x1) x2 = 0
Theorem 53cbb..^Pi_0_dom_mon : ∀ x0 x1 . ∀ x2 : ι → ι . Subq x0 x1 ⟶ (∀ x3 . In x3 x1 ⟶ nIn x3 x0 ⟶ In 0 (x2 x3)) ⟶ Subq (Pi x0 x2) (Pi x1 x2) (proof)
Theorem 82f9f..^Pi_cod_mon : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . In x3 x0 ⟶ Subq (x1 x3) (x2 x3)) ⟶ Subq (Pi x0 x1) (Pi x0 x2) (proof)
Known 2ad64..^Subq_tra : ∀ x0 x1 x2 . Subq x0 x1 ⟶ Subq x1 x2 ⟶ Subq x0 x2
Theorem 755f8..^Pi_0_mon : ∀ x0 x1 . ∀ x2 x3 : ι → ι . (∀ x4 . In x4 x0 ⟶ Subq (x2 x4) (x3 x4)) ⟶ Subq x0 x1 ⟶ (∀ x4 . In x4 x1 ⟶ nIn x4 x0 ⟶ In 0 (x3 x4)) ⟶ Subq (Pi x0 x2) (Pi x1 x3) (proof)
Known 3c3a9..^setexp_def : setexp = λ x1 x2 . Pi x2 (λ x3 . x1)
Known cd094..^and3E : ∀ x0 x1 x2 : ο . and (and x0 x1) x2 ⟶ ∀ x3 : ο . (x0 ⟶ x1 ⟶ x2 ⟶ x3) ⟶ x3
Known 56f17..^{Sigma_eta_proj0_proj1} : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 (lam x0 x1) ⟶ and (and (setsum (proj0 x2) (proj1 x2) = x2) (In (proj0 x2) x0)) (In (proj1 x2) (x1 (proj0 x2)))
Known e01bb..^If_i_or : ∀ x0 : ο . ∀ x1 x2 . or (If_i x0 x1 x2 = x1) (If_i x0 x1 x2 = x2)
Theorem 4c66a..^setexp_2_eq : ∀ x0 . setprod x0 x0 = setexp x0 2 (proof)
Theorem 49ee1..^{setexp_0_dom_mon} : ∀ x0 . In 0 x0 ⟶ ∀ x1 x2 . Subq x1 x2 ⟶ Subq (setexp x0 x1) (setexp x0 x2) (proof)
Theorem ad21b..^setexp_0_mon : ∀ x0 x1 x2 x3 . In 0 x3 ⟶ Subq x2 x3 ⟶ Subq x0 x1 ⟶ Subq (setexp x2 x0) (setexp x3 x1) (proof)
Known 80da5..^nat_trans : ∀ x0 . nat_p x0 ⟶ ∀ x1 . In x1 x0 ⟶ Subq x1 x0
Theorem 5ac7b..^{nat_in_setexp_mon} : ∀ x0 . In 0 x0 ⟶ ∀ x1 . nat_p x1 ⟶ ∀ x2 . In x2 x1 ⟶ Subq (setexp x0 x2) (setexp x0 x1) (proof)
Theorem 08193..^tuple_2_0_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 0 = x0 (proof)
Theorem 66870..^tuple_2_1_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 1 = x1 (proof)
Known 82574..^In_0_3 : In 0 3
Theorem bfdfa..^tuple_3_0_eq : ∀ x0 x1 x2 . ap (lam 3 (λ x4 . If_i (x4 = 0) x0 (If_i (x4 = 1) x1 x2))) 0 = x0 (proof)
Known f0f3e..^In_1_3 : In 1 3
Theorem 96b06..^tuple_3_1_eq : ∀ x0 x1 x2 . ap (lam 3 (λ x4 . If_i (x4 = 0) x0 (If_i (x4 = 1) x1 x2))) 1 = x1 (proof)
Known b5e95..^In_2_3 : In 2 3
Known db5d7..^neq_2_0 : not (2 = 0)
Known 56778..^neq_2_1 : not (2 = 1)
Theorem 1edca..^tuple_3_2_eq : ∀ x0 x1 x2 . ap (lam 3 (λ x4 . If_i (x4 = 0) x0 (If_i (x4 = 1) x1 x2))) 2 = x2 (proof)
Theorem 6e7a2..^{pair_tuple_fun} : setsum = λ x1 x2 . lam 2 (λ x3 . If_i (x3 = 0) x1 x2) (proof)
Theorem 51f9a..^tupleI0 : ∀ x0 x1 x2 . In x2 x0 ⟶ In (lam 2 (λ x3 . If_i (x3 = 0) 0 x2)) (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) (proof)
Theorem 6975b..^tupleI1 : ∀ x0 x1 x2 . In x2 x1 ⟶ In (lam 2 (λ x3 . If_i (x3 = 0) 1 x2)) (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) (proof)
Theorem bc7d4..^tupleE : ∀ x0 x1 x2 . In x2 (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) ⟶ or (∀ x3 : ο . (∀ x4 . and (In x4 x0) (x2 = lam 2 (λ x6 . If_i (x6 = 0) 0 x4)) ⟶ x3) ⟶ x3) (∀ x3 : ο . (∀ x4 . and (In x4 x1) (x2 = lam 2 (λ x6 . If_i (x6 = 0) 1 x4)) ⟶ x3) ⟶ x3) (proof)
Theorem 7b362..^tuple_2_inj : ∀ x0 x1 x2 x3 . lam 2 (λ x5 . If_i (x5 = 0) x0 x1) = lam 2 (λ x5 . If_i (x5 = 0) x2 x3) ⟶ and (x0 = x2) (x1 = x3) (proof)
Theorem 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 (proof)
Theorem 77775..^lamI2 : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 x0 ⟶ ∀ x3 . In x3 (x1 x2) ⟶ In (lam 2 (λ x4 . If_i (x4 = 0) x2 x3)) (lam x0 x1) (proof)
Theorem 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) (proof)
Theorem 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 (proof)
Theorem 77775..^lamI2 : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 x0 ⟶ ∀ x3 . In x3 (x1 x2) ⟶ In (lam 2 (λ x4 . If_i (x4 = 0) x2 x3)) (lam x0 x1) (proof)
Theorem 8eec4..^lamE2 : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 (lam x0 x1) ⟶ ∀ x3 : ο . (∀ x4 . and (In x4 x0) (∀ x5 : ο . (∀ x6 . and (In x6 (x1 x4)) (x2 = lam 2 (λ x8 . If_i (x8 = 0) x4 x6)) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3 (proof)
Theorem 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 (proof)
Theorem 2c78e..^lamE2_impred : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 (lam x0 x1) ⟶ ∀ x3 : ι → ο . (∀ x4 . In x4 x0 ⟶ ∀ x5 . In x5 (x1 x4) ⟶ x3 (lam 2 (λ x6 . If_i (x6 = 0) x4 x5))) ⟶ x3 x2 (proof)
Theorem cc0cc..^apI2 : ∀ x0 x1 x2 . In (lam 2 (λ x3 . If_i (x3 = 0) x1 x2)) x0 ⟶ In x2 (ap x0 x1) (proof)
Theorem 35c18..^apE2 : ∀ x0 x1 x2 . In x2 (ap x0 x1) ⟶ In (lam 2 (λ x3 . If_i (x3 = 0) x1 x2)) x0 (proof)
Known d6778..^{Empty_Subq_eq} : ∀ x0 . Subq x0 0 ⟶ x0 = 0
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Theorem 3b6b2..^ap_const_0 : ∀ x0 . ap 0 x0 = 0 (proof)
Theorem 1a8aa..^lam_ext_sub : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . In x3 x0 ⟶ x1 x3 = x2 x3) ⟶ Subq (lam x0 x1) (lam x0 x2) (proof)
Theorem 08153..^lam_ext : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . In x3 x0 ⟶ x1 x3 = x2 x3) ⟶ lam x0 x1 = lam x0 x2 (proof)
Theorem 38435..^lam_eta : ∀ x0 . ∀ x1 : ι → ι . lam x0 (ap (lam x0 x1)) = lam x0 x1 (proof)
Theorem d583c..^tuple_2_eta : ∀ x0 x1 . lam 2 (ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1))) = lam 2 (λ x3 . If_i (x3 = 0) x0 x1) (proof)
Theorem b4c59..^tuple_3_eta : ∀ x0 x1 x2 . lam 3 (ap (lam 3 (λ x4 . If_i (x4 = 0) x0 (If_i (x4 = 1) x1 x2)))) = lam 3 (λ x4 . If_i (x4 = 0) x0 (If_i (x4 = 1) x1 x2)) (proof)
Theorem 2d998..^tuple_4_eta : ∀ x0 x1 x2 x3 . lam 4 (ap (lam 4 (λ x5 . If_i (x5 = 0) x0 (If_i (x5 = 1) x1 (If_i (x5 = 2) x2 x3))))) = lam 4 (λ x5 . If_i (x5 = 0) x0 (If_i (x5 = 1) x1 (If_i (x5 = 2) x2 x3))) (proof)
Known 8bb76..^Sep2_def : Sep2 = λ x1 . λ x2 : ι → ι . λ x3 : ι → ι → ο . Sep (lam x1 x2) (λ x4 . x3 (ap x4 0) (ap x4 1))
Theorem 3212f..^Sep2I : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 . In x3 x0 ⟶ ∀ x4 . In x4 (x1 x3) ⟶ x2 x3 x4 ⟶ In (lam 2 (λ x5 . If_i (x5 = 0) x3 x4)) (Sep2 x0 x1 x2) (proof)
Theorem 67445..^Sep2E_impred : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 . In x3 (Sep2 x0 x1 x2) ⟶ ∀ x4 : ι → ο . (∀ x5 . In x5 x0 ⟶ ∀ x6 . In x6 (x1 x5) ⟶ x2 x5 x6 ⟶ x4 (lam 2 (λ x7 . If_i (x7 = 0) x5 x6))) ⟶ x4 x3 (proof)
Theorem c083f..^Sep2E : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 . In x3 (Sep2 x0 x1 x2) ⟶ ∀ x4 : ο . (∀ x5 . and (In x5 x0) (∀ x6 : ο . (∀ x7 . and (In x7 (x1 x5)) (and (x3 = lam 2 (λ x9 . If_i (x9 = 0) x5 x7)) (x2 x5 x7)) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4 (proof)
Theorem f69a3..^Sep2E_impred : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 x4 . In (lam 2 (λ x5 . If_i (x5 = 0) x3 x4)) (Sep2 x0 x1 x2) ⟶ ∀ x5 : ο . (In x3 x0 ⟶ In x4 (x1 x3) ⟶ x2 x3 x4 ⟶ x5) ⟶ x5 (proof)
Theorem 63884..^Sep2E1 : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 x4 . In (lam 2 (λ x5 . If_i (x5 = 0) x3 x4)) (Sep2 x0 x1 x2) ⟶ In x3 x0 (proof)
Theorem f1aba..^Sep2E2 : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 x4 . In (lam 2 (λ x5 . If_i (x5 = 0) x3 x4)) (Sep2 x0 x1 x2) ⟶ In x4 (x1 x3) (proof)
Theorem 1861a..^Sep2E3 : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 x4 . In (lam 2 (λ x5 . If_i (x5 = 0) x3 x4)) (Sep2 x0 x1 x2) ⟶ x2 x3 x4 (proof)
Known 4e628..^{set_of_pairs_def} : set_of_pairs = λ x1 . ∀ x2 . In x2 x1 ⟶ ∀ x3 : ο . (∀ x4 . (∀ x5 : ο . (∀ x6 . x2 = lam 2 (λ x8 . If_i (x8 = 0) x4 x6) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3
Known d182e..^iffE : ∀ x0 x1 : ο . iff x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ (not x0 ⟶ not x1 ⟶ x2) ⟶ x2
Known notE^notE : ∀ x0 : ο . not x0 ⟶ x0 ⟶ False
Theorem 51150..^{set_of_pairs_ext} : ∀ x0 x1 . set_of_pairs x0 ⟶ set_of_pairs x1 ⟶ (∀ x2 x3 . iff (In (lam 2 (λ x4 . If_i (x4 = 0) x2 x3)) x0) (In (lam 2 (λ x4 . If_i (x4 = 0) x2 x3)) x1)) ⟶ x0 = x1 (proof)
Theorem 9a832..^{Sep2_set_of_pairs} : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . set_of_pairs (Sep2 x0 x1 x2) (proof)
Theorem 1b318..^Sep2_ext : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 : ι → ι → ο . (∀ x4 . In x4 x0 ⟶ ∀ x5 . In x5 (x1 x4) ⟶ iff (x2 x4 x5) (x3 x4 x5)) ⟶ Sep2 x0 x1 x2 = Sep2 x0 x1 x3 (proof)
Known 244ad..^lam2_def : lam2 = λ x1 . λ x2 : ι → ι . λ x3 : ι → ι → ι . lam x1 (λ x4 . lam (x2 x4) (x3 x4))
Theorem 0c386..^beta2 : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ι . ∀ x3 . In x3 x0 ⟶ ∀ x4 . In x4 (x1 x3) ⟶ ap (ap (lam2 x0 x1 x2) x3) x4 = x2 x3 x4 (proof)
Theorem 0c69a..^lam2_ext : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 : ι → ι → ι . (∀ x4 . In x4 x0 ⟶ ∀ x5 . In x5 (x1 x4) ⟶ x2 x4 x5 = x3 x4 x5) ⟶ lam2 x0 x1 x2 = lam2 x0 x1 x3 (proof)
Known 3ad28..^cases_2 : ∀ x0 . In x0 2 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 x0
Theorem b5384..^{tuple_2_in_A_2} : ∀ x0 x1 x2 . In x0 x2 ⟶ In x1 x2 ⟶ In (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) (setexp x2 2) (proof)
Known 416bd..^cases_3 : ∀ x0 . In x0 3 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 2 ⟶ x1 x0
Theorem 42b05..^{tuple_3_in_A_3} : ∀ x0 x1 x2 x3 . In x0 x3 ⟶ In x1 x3 ⟶ In x2 x3 ⟶ In (lam 3 (λ x4 . If_i (x4 = 0) x0 (If_i (x4 = 1) x1 x2))) (setexp x3 3) (proof)
Known 480eb..^inj_def : inj = λ x1 x2 . λ x3 : ι → ι . and (∀ x4 . In x4 x1 ⟶ In (x3 x4) x2) (∀ x4 . In x4 x1 ⟶ ∀ x5 . In x5 x1 ⟶ x3 x4 = x3 x5 ⟶ x4 = x5)
Theorem 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 (proof)
Theorem 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 (proof)
Known 9276c..^bij_def : bij = λ x1 x2 . λ x3 : ι → ι . and (inj x1 x2 x3) (∀ x4 . In x4 x2 ⟶ ∀ x5 : ο . (∀ x6 . and (In x6 x1) (x3 x6 = x4) ⟶ x5) ⟶ x5)
Theorem 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 (proof)
Theorem 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 (proof)
Known fed08..^nat_ind : ∀ x0 : ι → ο . x0 0 ⟶ (∀ x1 . nat_p x1 ⟶ x0 x1 ⟶ x0 (ordsucc x1)) ⟶ ∀ x1 . nat_p x1 ⟶ x0 x1
Known 8106d..^notI : ∀ x0 : ο . (x0 ⟶ False) ⟶ not x0
Known 47706..^xmcases : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (not x0 ⟶ x1) ⟶ x1
Known 74738..^ordsucc_inj : ∀ x0 x1 . ordsucc x0 = ordsucc x1 ⟶ x0 = x1
Known 165f2..^ordsuccI1 : ∀ x0 . Subq x0 (ordsucc x0)
Known 840d1..^{nat_ordsucc_in_ordsucc} : ∀ x0 . nat_p x0 ⟶ ∀ x1 . In x1 x0 ⟶ In (ordsucc x1) (ordsucc x0)
Known 21479..^nat_ordsucc : ∀ x0 . nat_p x0 ⟶ nat_p (ordsucc x0)
Known b4776..^{ordsuccE_impred} : ∀ x0 x1 . In x1 (ordsucc x0) ⟶ ∀ x2 : ο . (In x1 x0 ⟶ x2) ⟶ (x1 = x0 ⟶ x2) ⟶ x2
Known e85f6..^In_irref : ∀ x0 . nIn x0 x0
Known cf025..^ordsuccI2 : ∀ x0 . In x0 (ordsucc x0)
Theorem 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) (proof)
Known b4782..^contra : ∀ x0 : ο . (not x0 ⟶ False) ⟶ x0
Theorem 398e3..^{PigeonHole_nat_bij} : ∀ x0 . nat_p x0 ⟶ ∀ x1 : ι → ι . (∀ x2 . In x2 x0 ⟶ In (x1 x2) x0) ⟶ (∀ x2 . In x2 x0 ⟶ ∀ x3 . In x3 x0 ⟶ x1 x2 = x1 x3 ⟶ x2 = x3) ⟶ bij x0 x0 x1 (proof)
Known 36841..^nat_2 : nat_p 2
Theorem 32c65..^{tuple_2_bij_2} : ∀ x0 x1 . In x0 2 ⟶ In x1 2 ⟶ not (x0 = x1) ⟶ bij 2 2 (ap (lam 2 (λ x2 . If_i (x2 = 0) x0 x1))) (proof)
Theorem c1fe0..^{tuple_3_bij_3} : ∀ x0 x1 x2 . In x0 3 ⟶ In x1 3 ⟶ In x2 3 ⟶ not (x0 = x1) ⟶ not (x0 = x2) ⟶ not (x1 = x2) ⟶ bij 3 3 (ap (lam 3 (λ x3 . If_i (x3 = 0) x0 (If_i (x3 = 1) x1 x2)))) (proof)