Let x0 of type ι be given.

Assume H0: nat_p x0.

Assume H1: 1 ∈ x0.

Let x1 of type ι be given.

Let x2 of type ι be given.

Let x3 of type ι be given.

Let x4 of type ι be given.

Assume H2: SNo x1.

Assume H3: e9c39.. x0 x1 x2 = e9c39.. x0 x3 x4.

Let x5 of type ι be given.

Assume H4: x5 ∈ x1.

Claim L5: x5 ∈ e9c39.. x0 x3 x4

Apply H3 with λ x6 x7 . x5 ∈ x6.

Apply binunionI1 with x1, {(λ x7 . SetAdjoin x7 (Sing x0)) x6|x6 ∈ x2}, x5.

The subproof is completed by applying H4.

Apply binunionE with x3, {(λ x7 . SetAdjoin x7 (Sing x0)) x6|x6 ∈ x4}, x5, x5 ∈ x3 leaving 3 subgoals.

The subproof is completed by applying L5.

Assume H6: x5 ∈ x3.

The subproof is completed by applying H6.

Assume H6: x5 ∈ {(λ x7 . SetAdjoin x7 (Sing x0)) x6|x6 ∈ x4}.

Apply FalseE with x5 ∈ x3.

Apply ReplE_impred with x4, λ x6 . (λ x7 . SetAdjoin x7 (Sing x0)) x6, x5, False leaving 2 subgoals.

The subproof is completed by applying H6.

Let x6 of type ι be given.

Assume H7: x6 ∈ x4.

Assume H8: x5 = (λ x7 . SetAdjoin x7 (Sing x0)) x6.

Apply unknownprop_b77e4d13156bc801da7c50d615690a07853273eb1e278cd0903fec4370f9e4e2 with x0, x1, x6 leaving 4 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H1.

The subproof is completed by applying H2.

Apply H8 with λ x7 x8 . x7 ∈ x1.

The subproof is completed by applying H4.

■

Proofgold Proof