Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Let x4 of type ι be given.
Let x5 of type ι be given.
Apply H2 with
λ x6 x7 . iff (x6 ∈ x1) (x7 ∈ x1) leaving 4 subgoals.
Let x6 of type ι be given.
Assume H3: x6 ∈ x0.
Apply iffI with
ap x2 x6 ∈ x1,
ap x3 x6 ∈ x1 leaving 2 subgoals.
Assume H4:
ap x2 x6 ∈ x1.
Apply ap_Pi with
x0,
λ x7 . x1,
x3,
x6 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
Assume H4:
ap x3 x6 ∈ x1.
Apply ap_Pi with
x0,
λ x7 . x1,
x2,
x6 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H3.
Let x6 of type ι be given.
The subproof is completed by applying iff_refl with x6 ∈ x1.
Let x6 of type ι be given.
Let x7 of type ι be given.
Assume H3:
iff (x6 ∈ x1) (x7 ∈ x1).
Apply iff_sym with
x6 ∈ x1,
x7 ∈ x1.
The subproof is completed by applying H3.
Let x6 of type ι be given.
Let x7 of type ι be given.
Let x8 of type ι be given.
Assume H3:
iff (x6 ∈ x1) (x7 ∈ x1).
Assume H4:
iff (x7 ∈ x1) (x8 ∈ x1).
Apply iff_trans with
x6 ∈ x1,
x7 ∈ x1,
x8 ∈ x1 leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H4.