Proofgold Address

Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition bij^bij := λ x0 x1 . λ x2 : ι → ι . and (and (∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x1) (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4)) (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 : ο . (∀ x5 . and (x5 ∈ x0) (x2 x5 = x3) ⟶ x4) ⟶ x4)
Definition equip^equip := λ x0 x1 . ∀ x2 : ο . (∀ x3 : ι → ι . bij x0 x1 x3 ⟶ x2) ⟶ x2
Param ordsucc^ordsucc : ι → ι
Param setminus^setminus : ι → ι → ι
Param UPair^UPair : ι → ι → ι
Param Sing^Sing : ι → ι
Known 9c223..^{equip_ordsucc_remove1} : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ equip x0 (ordsucc x1) ⟶ equip (setminus x0 (Sing x2)) x1
Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Definition nIn^nIn := λ x0 x1 . not (x0 ∈ x1)
Known setminusI^setminusI : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ nIn x2 x1 ⟶ x2 ∈ setminus x0 x1
Known SingE^SingE : ∀ x0 x1 . x1 ∈ Sing x0 ⟶ x1 = x0
Param binunion^binunion : ι → ι → ι
Known setminus_binunion^{setminus_binunion} : ∀ x0 x1 x2 . setminus x0 (binunion x1 x2) = setminus (setminus x0 x1) x2
Known cbaf1.. : ∀ x0 x1 . UPair x0 x1 = binunion (Sing x0) (Sing x1)
Theorem 185e6.. : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ equip x0 (ordsucc (ordsucc x1)) ⟶ equip (setminus x0 (UPair x2 x3)) x1 (proof)
Definition SetAdjoin^SetAdjoin := λ x0 x1 . binunion x0 (Sing x1)
Known 1aece.. : ∀ x0 x1 x2 x3 x4 . x4 ∈ SetAdjoin (SetAdjoin (UPair x0 x1) x2) x3 ⟶ ∀ x5 : ι → ο . x5 x0 ⟶ x5 x1 ⟶ x5 x2 ⟶ x5 x3 ⟶ x5 x4
Theorem 8698a.. : ∀ x0 x1 x2 x3 . ∀ x4 : ι → ο . x4 x0 ⟶ x4 x1 ⟶ x4 x2 ⟶ x4 x3 ⟶ ∀ x5 . x5 ∈ SetAdjoin (SetAdjoin (UPair x0 x1) x2) x3 ⟶ x4 x5 (proof)
Known 3cea6.. : ∀ x0 x1 x2 x3 x4 x5 . x5 ∈ SetAdjoin (SetAdjoin (SetAdjoin (UPair x0 x1) x2) x3) x4 ⟶ ∀ x6 : ι → ο . x6 x0 ⟶ x6 x1 ⟶ x6 x2 ⟶ x6 x3 ⟶ x6 x4 ⟶ x6 x5
Theorem 9b26d.. : ∀ x0 x1 x2 x3 x4 . ∀ x5 : ι → ο . x5 x0 ⟶ x5 x1 ⟶ x5 x2 ⟶ x5 x3 ⟶ x5 x4 ⟶ ∀ x6 . x6 ∈ SetAdjoin (SetAdjoin (SetAdjoin (UPair x0 x1) x2) x3) x4 ⟶ x5 x6 (proof)
Definition inj^inj := λ x0 x1 . λ x2 : ι → ι . and (∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x1) (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4)
Definition atleastp^atleastp := λ x0 x1 . ∀ x2 : ο . (∀ x3 : ι → ι . inj x0 x1 x3 ⟶ x2) ⟶ x2
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known ReplI^ReplI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ x1 x2 ∈ prim5 x0 x1
Theorem 13005.. : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 = x1 x3 ⟶ x2 = x3) ⟶ atleastp x0 (prim5 x0 x1) (proof)
Known bijI^bijI : ∀ x0 x1 . ∀ x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x1) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4) ⟶ (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 : ο . (∀ x5 . and (x5 ∈ x0) (x2 x5 = x3) ⟶ x4) ⟶ x4) ⟶ bij x0 x1 x2
Known ReplE_impred^ReplE_impred : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ prim5 x0 x1 ⟶ ∀ x3 : ο . (∀ x4 . x4 ∈ x0 ⟶ x2 = x1 x4 ⟶ x3) ⟶ x3
Theorem d2050.. : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 = x1 x3 ⟶ x2 = x3) ⟶ equip x0 (prim5 x0 x1) (proof)
Param omega^omega : ι
Definition finite^finite := λ x0 . ∀ x1 : ο . (∀ x2 . and (x2 ∈ omega) (equip x0 x2) ⟶ x1) ⟶ x1
Definition u1 := 1
Param nat_p^nat_p : ι → ο
Known nat_p_omega^nat_p_omega : ∀ x0 . nat_p x0 ⟶ x0 ∈ omega
Known nat_1^nat_1 : nat_p 1
Known 5169f..^equip_Sing_1 : ∀ x0 . equip (Sing x0) u1
Theorem 28148..^Sing_finite : ∀ x0 . finite (Sing x0) (proof)
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known xm^xm : ∀ x0 : ο . or x0 (not x0)
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Known set_ext^set_ext : ∀ x0 x1 . x0 ⊆ x1 ⟶ x1 ⊆ x0 ⟶ x0 = x1
Known UPairE^UPairE : ∀ x0 x1 x2 . x0 ∈ UPair x1 x2 ⟶ or (x0 = x1) (x0 = x2)
Known SingI^SingI : ∀ x0 . x0 ∈ Sing x0
Known 6cd03.. : ∀ x0 x1 . x1 ∈ x0 ⟶ Sing x1 ⊆ x0
Known UPairI1^UPairI1 : ∀ x0 x1 . x0 ∈ UPair x0 x1
Definition u2 := ordsucc u1
Known nat_2^nat_2 : nat_p 2
Known ced33.. : ∀ x0 x1 . (x0 = x1 ⟶ ∀ x2 : ο . x2) ⟶ equip (UPair x0 x1) u2
Theorem 92c81.. : ∀ x0 x1 . finite (UPair x0 x1) (proof)
Known bijE^bijE : ∀ x0 x1 . ∀ x2 : ι → ι . bij x0 x1 x2 ⟶ ∀ x3 : ο . ((∀ x4 . x4 ∈ x0 ⟶ x2 x4 ∈ x1) ⟶ (∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ x2 x4 = x2 x5 ⟶ x4 = x5) ⟶ (∀ x4 . x4 ∈ x1 ⟶ ∀ x5 : ο . (∀ x6 . and (x6 ∈ x0) (x2 x6 = x4) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3
Known PigeonHole_nat_bij^{PigeonHole_nat_bij} : ∀ x0 . nat_p x0 ⟶ ∀ x1 : ι → ι . (∀ x2 . x2 ∈ x0 ⟶ x1 x2 ∈ x0) ⟶ (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 = x1 x3 ⟶ x2 = x3) ⟶ bij x0 x0 x1
Known omega_nat_p^omega_nat_p : ∀ x0 . x0 ∈ omega ⟶ nat_p x0
Known equip_sym^equip_sym : ∀ x0 x1 . equip x0 x1 ⟶ equip x1 x0
Theorem 1b508.. : ∀ x0 x1 . finite x0 ⟶ atleastp x1 x0 ⟶ x0 ⊆ x1 ⟶ x0 = x1 (proof)
Known inj_comp^inj_comp : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι . inj x0 x1 x3 ⟶ inj x1 x2 x4 ⟶ inj x0 x2 (λ x5 . x4 (x3 x5))
Theorem 77ee8.. : ∀ x0 x1 x2 . ∀ x3 : ι → ι . nat_p x0 ⟶ equip x1 x0 ⟶ equip x2 x0 ⟶ inj x1 x2 x3 ⟶ bij x1 x2 x3 (proof)
Definition u3 := ordsucc u2
Param Sep^Sep : ι → (ι → ο) → ι
Param ap^ap : ι → ι → ι
Param lam^Sigma : ι → (ι → ι) → ι
Param If_i^If_i : ο → ι → ι → ι
Known cases_3^cases_3 : ∀ x0 . x0 ∈ 3 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 2 ⟶ x1 x0
Known tuple_3_0_eq^tuple_3_0_eq : ∀ x0 x1 x2 . ap (lam 3 (λ x4 . If_i (x4 = 0) x0 (If_i (x4 = 1) x1 x2))) 0 = x0
Known SepI^SepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ x0 ⟶ x1 x2 ⟶ x2 ∈ Sep x0 x1
Known PowerI^PowerI : ∀ x0 x1 . x1 ⊆ x0 ⟶ x1 ∈ prim4 x0
Known In_0_3^In_0_3 : 0 ∈ 3
Known In_1_3^In_1_3 : 1 ∈ 3
Known neq_0_1^neq_0_1 : 0 = 1 ⟶ ∀ x0 : ο . x0
Known tuple_3_1_eq^tuple_3_1_eq : ∀ x0 x1 x2 . ap (lam 3 (λ x4 . If_i (x4 = 0) x0 (If_i (x4 = 1) x1 x2))) 1 = x1
Known In_2_3^In_2_3 : 2 ∈ 3
Known neq_0_2^neq_0_2 : 0 = 2 ⟶ ∀ x0 : ο . x0
Known tuple_3_2_eq^tuple_3_2_eq : ∀ x0 x1 x2 . ap (lam 3 (λ x4 . If_i (x4 = 0) x0 (If_i (x4 = 1) x1 x2))) 2 = x2
Known neq_1_2^neq_1_2 : 1 = 2 ⟶ ∀ x0 : ο . x0
Known In_irref^In_irref : ∀ x0 . nIn x0 x0
Known eq_2_UPair01^eq_2_UPair01 : 2 = UPair 0 1
Known UPairI2^UPairI2 : ∀ x0 x1 . x1 ∈ UPair x0 x1
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Known SepE^SepE : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ Sep x0 x1 ⟶ and (x2 ∈ x0) (x1 x2)
Known atleastp_tra^atleastp_tra : ∀ x0 x1 x2 . atleastp x0 x1 ⟶ atleastp x1 x2 ⟶ atleastp x0 x2
Known equip_atleastp^{equip_atleastp} : ∀ x0 x1 . equip x0 x1 ⟶ atleastp x0 x1
Known PowerE^PowerE : ∀ x0 x1 . x1 ∈ prim4 x0 ⟶ x1 ⊆ x0
Known In_0_1^In_0_1 : 0 ∈ 1
Known In_0_2^In_0_2 : 0 ∈ 2
Theorem 72ea6.. : bij u3 {x0 ∈ prim4 u3|equip x0 u2} (ap (lam 3 (λ x0 . If_i (x0 = 0) (UPair 0 u1) (If_i (x0 = 1) (UPair 0 u2) (UPair u1 u2))))) (proof)
Known equip_tra^equip_tra : ∀ x0 x1 x2 . equip x0 x1 ⟶ equip x1 x2 ⟶ equip x0 x2
Param inv^inv : ι → (ι → ι) → ι → ι
Known surj_rinv^surj_rinv : ∀ x0 x1 . ∀ x2 : ι → ι . (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 : ο . (∀ x5 . and (x5 ∈ x0) (x2 x5 = x3) ⟶ x4) ⟶ x4) ⟶ ∀ x3 . x3 ∈ x1 ⟶ and (inv x0 x2 x3 ∈ x0) (x2 (inv x0 x2 x3) = x3)
Known bij_inv^bij_inv : ∀ x0 x1 . ∀ x2 : ι → ι . bij x0 x1 x2 ⟶ bij x1 x0 (inv x0 x2)
Theorem da3b9.. : ∀ x0 . equip x0 u3 ⟶ equip {x1 ∈ prim4 x0|equip x1 u2} u3 (proof)
Known binunionE^binunionE : ∀ x0 x1 x2 . x2 ∈ binunion x0 x1 ⟶ or (x2 ∈ x0) (x2 ∈ x1)
Known binunionI1^binunionI1 : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ x2 ∈ binunion x0 x1
Known binunionI2^binunionI2 : ∀ x0 x1 x2 . x2 ∈ x1 ⟶ x2 ∈ binunion x0 x1
Theorem 6a935.. : ∀ x0 x1 x2 . SetAdjoin (UPair x0 x1) x2 ⊆ SetAdjoin (UPair x0 x2) x1 (proof)
Theorem 166d0.. : ∀ x0 x1 x2 . SetAdjoin (UPair x0 x1) x2 = SetAdjoin (UPair x0 x2) x1 (proof)
Known binunion_asso^{binunion_asso} : ∀ x0 x1 x2 . binunion x0 (binunion x1 x2) = binunion (binunion x0 x1) x2
Known binunion_com^binunion_com : ∀ x0 x1 . binunion x0 x1 = binunion x1 x0
Theorem 50015.. : ∀ x0 x1 x2 x3 . SetAdjoin (SetAdjoin (UPair x0 x1) x2) x3 = SetAdjoin (SetAdjoin (UPair x0 x1) x3) x2 (proof)
Theorem e488c.. : ∀ x0 x1 x2 x3 x4 . SetAdjoin (SetAdjoin (SetAdjoin (UPair x0 x1) x2) x3) x4 = SetAdjoin (SetAdjoin (SetAdjoin (UPair x0 x1) x4) x2) x3 (proof)