Let x0 of type ι be given.

Assume H0: nat_p x0.

Assume H1: 1 ∈ x0.

Let x1 of type ι be given.

Assume H2: ordinal ((λ x2 . SetAdjoin x2 (Sing x0)) x1).

Claim L3: Sing x0 ∈ (λ x2 . SetAdjoin x2 (Sing x0)) x1

Apply binunionI2 with x1, Sing (Sing x0), Sing x0.

The subproof is completed by applying SingI with Sing x0.

Apply not_ordinal_Sing_tagn with x0 leaving 3 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H1.

Apply ordinal_Hered with (λ x2 . SetAdjoin x2 (Sing x0)) x1, Sing x0 leaving 2 subgoals.

The subproof is completed by applying H2.

The subproof is completed by applying L3.

■

Proofgold Proof