Let x0 of type ι be given.
Let x1 of type ι → ι be given.
Let x2 of type ι be given.
Apply SepI with
prim6 (UPair x0 (famunion x0 (λ x3 . Sing (x1 x3)))),
λ x3 . 59caa.. x0 x1 x3,
x2 leaving 2 subgoals.
The subproof is completed by applying UnivOf_In with
UPair x0 (famunion x0 (λ x3 . Sing (x1 x3))).
Apply UnivOf_TransSet with
UPair x0 (famunion x0 (λ x3 . Sing (x1 x3))),
UPair x0 (famunion x0 (λ x3 . Sing (x1 x3))),
x0 leaving 2 subgoals.
The subproof is completed by applying L1.
The subproof is completed by applying UPairI1 with
x0,
famunion x0 (λ x3 . Sing (x1 x3)).
Apply UnivOf_TransSet with
UPair x0 (famunion x0 (λ x3 . Sing (x1 x3))),
UPair x0 (famunion x0 (λ x3 . Sing (x1 x3))),
famunion x0 (λ x3 . Sing (x1 x3)) leaving 2 subgoals.
The subproof is completed by applying L1.
The subproof is completed by applying UPairI2 with
x0,
famunion x0 (λ x3 . Sing (x1 x3)).
Let x3 of type ι be given.
Assume H4: x3 ∈ x0.
Apply UnivOf_TransSet with
UPair x0 (famunion x0 (λ x4 . Sing (x1 x4))),
famunion x0 (λ x4 . Sing (x1 x4)),
x1 x3 leaving 2 subgoals.
The subproof is completed by applying L3.
Apply famunionI with
x0,
λ x4 . Sing (x1 x4),
x3,
x1 x3 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying SingI with x1 x3.
Apply unknownprop_1bcb0376aad766d016ee9f0693d3212cc24924141721dea50bf523c306096bab with
UPair x0 (famunion x0 (λ x3 . Sing (x1 x3))),
UPair x0 (famunion x0 (λ x3 . Sing (x1 x3))),
0 leaving 2 subgoals.
The subproof is completed by applying UnivOf_In with
UPair x0 (famunion x0 (λ x3 . Sing (x1 x3))).
The subproof is completed by applying Subq_Empty with
UPair x0 (famunion x0 (λ x3 . Sing (x1 x3))).
Apply unknownprop_01e489ef49a5abff8a57f5263f07314025d4dc630bb6e2f317e9171009ca8dc8 with
prim6 (UPair x0 (famunion x0 (λ x3 . Sing (x1 x3)))),
x0,
x1,
x2 leaving 6 subgoals.
The subproof is completed by applying UnivOf_TransSet with
UPair x0 (famunion x0 (λ x3 . Sing (x1 x3))).
The subproof is completed by applying UnivOf_ZF_closed with
UPair x0 (famunion x0 (λ x3 . Sing (x1 x3))).
The subproof is completed by applying L5.
The subproof is completed by applying L2.
The subproof is completed by applying L4.
The subproof is completed by applying H0.
The subproof is completed by applying H0.