Let x0 of type ι be given.
Apply set_ext with
prim3 x0,
famunion x0 (λ x1 . x1) leaving 2 subgoals.
Let x1 of type ι be given.
Assume H0:
x1 ∈ prim3 x0.
Apply UnionE_impred with
x0,
x1,
x1 ∈ famunion x0 (λ x2 . x2) leaving 2 subgoals.
The subproof is completed by applying H0.
Let x2 of type ι be given.
Assume H1: x1 ∈ x2.
Assume H2: x2 ∈ x0.
Apply famunionI with
x0,
λ x3 . x3,
x2,
x1 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H1.
Let x1 of type ι be given.
Assume H0:
x1 ∈ famunion x0 (λ x2 . x2).
Apply famunionE with
x0,
λ x2 . x2,
x1,
x1 ∈ prim3 x0 leaving 2 subgoals.
The subproof is completed by applying H0.
Let x2 of type ι be given.
Assume H1:
and (x2 ∈ x0) (x1 ∈ x2).
Apply H1 with
x1 ∈ prim3 x0.
Assume H2: x2 ∈ x0.
Assume H3: x1 ∈ x2.
Apply UnionI with
x0,
x1,
x2 leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H2.