Proofgold Address

Definition and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition bij := λ x0 x1 . λ x2 : ι → ι . and (and (∀ x3 . prim1 x3 x0 ⟶ prim1 (x2 x3) x1) (∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4)) (∀ x3 . prim1 x3 x1 ⟶ ∀ x4 : ο . (∀ x5 . and (prim1 x5 x0) (x2 x5 = x3) ⟶ x4) ⟶ x4)
Definition surj := λ x0 x1 . λ x2 : ι → ι . and (∀ x3 . prim1 x3 x0 ⟶ prim1 (x2 x3) x1) (∀ x3 . prim1 x3 x1 ⟶ ∀ x4 : ο . (∀ x5 . and (prim1 x5 x0) (x2 x5 = x3) ⟶ x4) ⟶ x4)
Known andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem bij_surj : ∀ x0 x1 . ∀ x2 : ι → ι . bij x0 x1 x2 ⟶ surj x0 x1 x2 (proof)
Definition False := ∀ x0 : ο . x0
Definition not := λ x0 : ο . x0 ⟶ False
Param 48ef8.. : ι
Param e5b72.. : ι → ι
Param 1216a.. : ι → (ι → ο) → ι
Definition nIn := λ x0 x1 . not (prim1 x0 x1)
Known b2421.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 x0 ⟶ x1 x2 ⟶ prim1 x2 (1216a.. x0 x1)
Known ac5c1.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 (1216a.. x0 x1) ⟶ x1 x2
Definition Subq := λ x0 x1 . ∀ x2 . prim1 x2 x0 ⟶ prim1 x2 x1
Known 3daee.. : ∀ x0 x1 . Subq x1 x0 ⟶ prim1 x1 (e5b72.. x0)
Known d0a1f.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 (1216a.. x0 x1) ⟶ prim1 x2 x0
Theorem da671.. : ∀ x0 : ι → ι . not (surj 48ef8.. (e5b72.. 48ef8..) x0) (proof)
Param c2e41.. : ι → ι → ο
Known 64d57.. : ∀ x0 x1 . c2e41.. x0 x1 ⟶ ∀ x2 : ο . (∀ x3 : ι → ι . bij x0 x1 x3 ⟶ x2) ⟶ x2
Theorem 86fd0.. : not (c2e41.. 48ef8.. (e5b72.. 48ef8..)) (proof)
Definition inj := λ x0 x1 . λ x2 : ι → ι . and (∀ x3 . prim1 x3 x0 ⟶ prim1 (x2 x3) x1) (∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4)
Param a4c2a.. : ι → (ι → ο) → (ι → ι) → ι
Known e951d.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 : ι → ι . ∀ x3 . prim1 x3 x0 ⟶ x1 x3 ⟶ prim1 (x2 x3) (a4c2a.. x0 x1 x2)
Known 932b3.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 : ι → ι . ∀ x3 . prim1 x3 (a4c2a.. x0 x1 x2) ⟶ ∀ x4 : ο . (∀ x5 . prim1 x5 x0 ⟶ x1 x5 ⟶ x3 = x2 x5 ⟶ x4) ⟶ x4
Theorem 6ec25.. : ∀ x0 : ι → ι . not (inj (e5b72.. 48ef8..) 48ef8.. x0) (proof)