Proofgold Proof

pf

Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Assume H0: nat_p x0.

Assume H1: x1 ∈ ordsucc x0.

Assume H2: nat_p x2.

Assume H3: nat_p x1.

Apply SNo__eps_ with x0, exactly1of2 (SetAdjoin x1 (Sing 1) ∈ eps_ x0) (x1 ∈ eps_ x0) leaving 2 subgoals.

Apply nat_p_omega with x0.

The subproof is completed by applying H0.

Assume H4: eps_ x0 ⊆ SNoElts_ (ordsucc x0).

Assume H5: ∀ x3 . x3 ∈ ordsucc x0 ⟶ exactly1of2 (SetAdjoin x3 (Sing 1) ∈ eps_ x0) (x3 ∈ eps_ x0).

Apply H5 with x1.

The subproof is completed by applying H1.

■