Proofgold Asset

Param 4402e.. : ι → (ι → ι → ο) → ο
Param cf2df.. : ι → (ι → ι → ο) → ο
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Param setminus^setminus : ι → ι → ι
Param Sing^Sing : ι → ι
Param 07080.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο
Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Definition 6799e.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . ∀ x14 : ο . (07080.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ (x1 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x2 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x8 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x9 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x10 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x11 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x12 = x13 ⟶ ∀ x15 : ο . x15) ⟶ x0 x1 x13 ⟶ x0 x2 x13 ⟶ not (x0 x3 x13) ⟶ x0 x4 x13 ⟶ not (x0 x5 x13) ⟶ not (x0 x6 x13) ⟶ not (x0 x7 x13) ⟶ not (x0 x8 x13) ⟶ not (x0 x9 x13) ⟶ not (x0 x10 x13) ⟶ x0 x11 x13 ⟶ not (x0 x12 x13) ⟶ x14) ⟶ x14
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition nIn^nIn := λ x0 x1 . not (x0 ∈ x1)
Known setminusE^setminusE : ∀ x0 x1 x2 . x2 ∈ setminus x0 x1 ⟶ and (x2 ∈ x0) (nIn x2 x1)
Known 123e7.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ x2 x3 x4 ⟶ x2 x4 x3) ⟶ 4402e.. x1 x2 ⟶ cf2df.. x1 x2 ⟶ ∀ x3 . x3 ∈ x1 ⟶ x0 ⊆ setminus x1 (Sing x3) ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ ∀ x13 . x13 ∈ x0 ⟶ ∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ 07080.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 ⟶ ∀ x16 : ο . (x2 x4 x3 ⟶ x2 x5 x3 ⟶ not (x2 x6 x3) ⟶ x2 x7 x3 ⟶ not (x2 x8 x3) ⟶ not (x2 x9 x3) ⟶ not (x2 x10 x3) ⟶ not (x2 x11 x3) ⟶ not (x2 x12 x3) ⟶ not (x2 x13 x3) ⟶ x2 x14 x3 ⟶ not (x2 x15 x3) ⟶ x16) ⟶ x16
Known SingI^SingI : ∀ x0 . x0 ∈ Sing x0
Theorem 30440.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ x2 x3 x4 ⟶ x2 x4 x3) ⟶ 4402e.. x1 x2 ⟶ cf2df.. x1 x2 ⟶ ∀ x3 . x3 ∈ x1 ⟶ x0 ⊆ setminus x1 (Sing x3) ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ ∀ x11 . x11 ∈ x0 ⟶ ∀ x12 . x12 ∈ x0 ⟶ ∀ x13 . x13 ∈ x0 ⟶ ∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ 07080.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 ⟶ 6799e.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x3 (proof)