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: SNo x0.

Assume H1: SNo_pair x0 x1 = SNo_pair x2 x3.

Let x4 of type ι be given.

Assume H2: x4 ∈ x0.

Claim L3: x4 ∈ SNo_pair x2 x3

Apply H1 with λ x5 x6 . x4 ∈ x5.

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

The subproof is completed by applying H2.

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

The subproof is completed by applying L3.

Assume H4: x4 ∈ x2.

The subproof is completed by applying H4.

Assume H4: x4 ∈ {(λ x6 . SetAdjoin x6 (Sing 2)) x5|x5 ∈ x3}.

Apply FalseE with x4 ∈ x2.

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

The subproof is completed by applying H4.

Let x5 of type ι be given.

Assume H5: x5 ∈ x3.

Assume H6: x4 = (λ x6 . SetAdjoin x6 (Sing 2)) x5.

Apply ctagged_notin_SNo with x0, x5 leaving 2 subgoals.

The subproof is completed by applying H0.

Apply H6 with λ x6 x7 . x6 ∈ x0.

The subproof is completed by applying H2.

■

Proofgold Proof