Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Let x3 of type ι be given.

Assume H0: nIn x2 x1.

Assume H1: nIn x3 x1.

Assume H2: x2 = x3 ⟶ ∀ x4 : ο . x4.

Assume H3: atleastp x0 x1.

Claim L4: binunion x1 (UPair x2 x3) = binunion (binunion x1 (Sing x2)) (Sing x3)

Apply set_ext with binunion x1 (UPair x2 x3), binunion (binunion x1 (Sing x2)) (Sing x3) leaving 2 subgoals.

Apply binunion_Subq_min with x1, UPair x2 x3, binunion (binunion x1 (Sing x2)) (Sing x3) leaving 2 subgoals.

Apply Subq_tra with x1, binunion x1 (Sing x2), binunion (binunion x1 (Sing x2)) (Sing x3) leaving 2 subgoals.

The subproof is completed by applying binunion_Subq_1 with x1, Sing x2.

The subproof is completed by applying binunion_Subq_1 with binunion x1 (Sing x2), Sing x3.

Let x4 of type ι be given.

Assume H4: x4 ∈ UPair x2 x3.

Apply UPairE with x4, x2, x3, x4 ∈ binunion (binunion x1 (Sing x2)) (Sing x3) leaving 3 subgoals.

The subproof is completed by applying H4.

Assume H5: x4 = x2.

Apply H5 with λ x5 x6 . x6 ∈ binunion (binunion x1 (Sing x2)) (Sing x3).

Apply binunionI1 with binunion x1 (Sing x2), Sing x3, x2.

Apply binunionI2 with x1, Sing x2, x2.

The subproof is completed by applying SingI with x2.

Assume H5: x4 = x3.

Apply H5 with λ x5 x6 . x6 ∈ binunion (binunion x1 (Sing x2)) (Sing x3).

Apply binunionI2 with binunion x1 (Sing x2), Sing x3, x3.

The subproof is completed by applying SingI with x3.

Apply binunion_Subq_min with binunion x1 (Sing x2), Sing x3, binunion x1 (UPair x2 x3) leaving 2 subgoals.

Apply binunion_Subq_min with x1, Sing x2, binunion x1 (UPair x2 x3) leaving 2 subgoals.

The subproof is completed by applying binunion_Subq_1 with x1, UPair x2 x3.

Let x4 of type ι be given.

Assume H4: x4 ∈ Sing x2.

Apply SingE with x2, x4, λ x5 x6 . x6 ∈ binunion x1 (UPair x2 x3) leaving 2 subgoals.

The subproof is completed by applying H4.

Apply binunionI2 with x1, UPair x2 x3, x2.

The subproof is completed by applying UPairI1 with x2, x3.

Let x4 of type ι be given.

Assume H4: x4 ∈ Sing x3.

Apply SingE with x3, x4, λ x5 x6 . x6 ∈ binunion x1 (UPair x2 x3) leaving 2 subgoals.

The subproof is completed by applying H4.

Apply binunionI2 with x1, UPair x2 x3, x3.

The subproof is completed by applying UPairI2 with x2, x3.

Apply L4 with λ x4 x5 . atleastp (ordsucc (ordsucc x0)) x5.

Apply unknownprop_11c6158bd93dbd27daaa9a84a43404be6ccbf75f900b1e28dfa453e64ea6c96b with ordsucc x0, binunion x1 (Sing x2), x3 leaving 2 subgoals.

Assume H5: x3 ∈ binunion x1 (Sing x2).

Apply binunionE with x1, Sing x2, x3, False leaving 3 subgoals.

The subproof is completed by applying H5.

The subproof is completed by applying H1.

Assume H6: x3 ∈ Sing x2.

Apply H2.

Let x4 of type ι → ι → ο be given.

Apply SingE with x2, x3, λ x5 x6 . x4 x6 x5.

The subproof is completed by applying H6.

Apply unknownprop_11c6158bd93dbd27daaa9a84a43404be6ccbf75f900b1e28dfa453e64ea6c96b with x0, x1, x2 leaving 2 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H3.

■

Proofgold Proof