Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: x1 ∈ x0.
Apply dneg with
∃ x2 . and (x2 ∈ x0) (not (∃ x3 . and (x3 ∈ x0) (x3 ∈ x2))).
Assume H1:
not (∃ x2 . and (x2 ∈ x0) (not (∃ x3 . and (x3 ∈ x0) (x3 ∈ x2)))).
Claim L2:
∀ x2 . nIn x2 x0Apply In_ind with
λ x2 . nIn x2 x0.
Let x2 of type ι be given.
Assume H2:
∀ x3 . x3 ∈ x2 ⟶ nIn x3 x0.
Assume H3: x2 ∈ x0.
Apply H1.
Let x3 of type ο be given.
Assume H4:
∀ x4 . and (x4 ∈ x0) (not (∃ x5 . and (x5 ∈ x0) (x5 ∈ x4))) ⟶ x3.
Apply H4 with
x2.
Apply andI with
x2 ∈ x0,
not (∃ x4 . and (x4 ∈ x0) (x4 ∈ x2)) leaving 2 subgoals.
The subproof is completed by applying H3.
Assume H5:
∃ x4 . and (x4 ∈ x0) (x4 ∈ x2).
Apply H5 with
False.
Let x4 of type ι be given.
Assume H6:
(λ x5 . and (x5 ∈ x0) (x5 ∈ x2)) x4.
Apply H6 with
False.
Assume H7: x4 ∈ x0.
Assume H8: x4 ∈ x2.
Apply H2 with
x4 leaving 2 subgoals.
The subproof is completed by applying H8.
The subproof is completed by applying H7.
Apply L2 with
x1.
The subproof is completed by applying H0.