Let x0 of type ι be given.
Let x1 of type ι → ο be given.
Assume H0:
∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3.
Let x2 of type ι be given.
Let x3 of type ι be given.
Let x4 of type ι be given.
Let x5 of type ι be given.
Assume H1: x1 x2.
Let x6 of type ι be given.
Assume H3: x6 ∈ x2.
Apply H2 with
λ x7 x8 . x6 ∈ x7.
Apply binunionI1 with
x2,
{(λ x8 . SetAdjoin x8 x0) x7|x7 ∈ x3},
x6.
The subproof is completed by applying H3.
Apply binunionE with
x4,
{(λ x8 . SetAdjoin x8 x0) x7|x7 ∈ x5},
x6,
x6 ∈ x4 leaving 3 subgoals.
The subproof is completed by applying L4.
Assume H5: x6 ∈ x4.
The subproof is completed by applying H5.
Assume H5:
x6 ∈ {(λ x8 . SetAdjoin x8 x0) x7|x7 ∈ x5}.
Apply FalseE with
x6 ∈ x4.
Apply ReplE_impred with
x5,
λ x7 . (λ x8 . SetAdjoin x8 x0) x7,
x6,
False leaving 2 subgoals.
The subproof is completed by applying H5.
Let x7 of type ι be given.
Assume H6: x7 ∈ x5.
Apply ctagged_notin_F with
x0,
x1,
x2,
x7 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply H7 with
λ x8 x9 . x8 ∈ x2.
The subproof is completed by applying H3.