Apply nat_ind with λ x0 . ∀ x1 . x1 ⊆ x0 ⟶ ∃ x2 . and (and (nat_p x2) (x2 ⊆ x0)) (equip x1 x2) leaving 2 subgoals.

Let x0 of type ι be given.

Assume H0: x0 ⊆ 0.

Let x1 of type ο be given.

Assume H1: ∀ x2 . and (and (nat_p x2) (x2 ⊆ 0)) (equip x0 x2) ⟶ x1.

Apply H1 with 0.

Apply and3I with nat_p 0, 0 ⊆ 0, equip x0 0 leaving 3 subgoals.

The subproof is completed by applying nat_0.

The subproof is completed by applying Subq_ref with 0.

Apply Empty_Subq_eq with x0, λ x2 x3 . equip x3 0 leaving 2 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying equip_ref with 0.

Let x0 of type ι be given.

Assume H0: nat_p x0.

Assume H1: ∀ x1 . x1 ⊆ x0 ⟶ ∃ x2 . and (and (nat_p x2) (x2 ⊆ x0)) (equip x1 x2).

Let x1 of type ι be given.

Assume H2: x1 ⊆ ordsucc x0.

Apply xm with x0 ∈ x1, ∃ x2 . and (and (nat_p x2) (x2 ⊆ ordsucc x0)) (equip x1 x2) leaving 2 subgoals.

Assume H3: x0 ∈ x1.

Claim L4: setminus x1 (Sing x0) ⊆ x0

Let x2 of type ι be given.

Assume H4: x2 ∈ setminus x1 (Sing x0).

Apply setminusE with x1, Sing x0, x2, x2 ∈ x0 leaving 2 subgoals.

The subproof is completed by applying H4.

Assume H5: x2 ∈ x1.

Assume H6: nIn x2 (Sing x0).

Apply ordsuccE with x0, x2, x2 ∈ ... leaving 3 subgoals.

...

Apply H1 with setminus x1 (Sing x0), ∃ x2 . and (and (nat_p x2) (x2 ⊆ ordsucc x0)) (equip x1 x2) leaving 2 subgoals.

The subproof is completed by applying L4.

Let x2 of type ι be given.

Assume H5: (λ x3 . and (and (nat_p x3) (x3 ⊆ x0)) (equip (setminus x1 (Sing x0)) x3)) x2.

Apply H5 with ∃ x3 . and (and (nat_p x3) (x3 ⊆ ordsucc x0)) (equip x1 x3).

Assume H6: and (nat_p x2) (x2 ⊆ x0).

Apply H6 with equip (setminus x1 (Sing x0)) x2 ⟶ ∃ x3 . and (and (nat_p x3) (x3 ⊆ ordsucc x0)) (equip x1 x3).

Assume H7: nat_p x2.

Assume H8: x2 ⊆ x0.

Assume H9: equip (setminus x1 (Sing x0)) x2.

Let x3 of type ο be given.

Assume H10: ∀ x4 . and (and (nat_p x4) (x4 ⊆ ordsucc x0)) (equip x1 x4) ⟶ x3.

Apply H10 with ordsucc x2.

Apply and3I with nat_p (ordsucc x2), ordsucc x2 ⊆ ordsucc x0, equip x1 (ordsucc x2) leaving 3 subgoals.

Apply nat_ordsucc with x2.

The subproof is completed by applying H7.

Apply unknownprop_ad830447e2a256c0fa48f150ede5366d23a389e771f030df6830dfe0d4977bf6 with x2, x0 leaving 3 subgoals.

The subproof is completed by applying H7.

The subproof is completed by applying H0.

The subproof is completed by applying H8.

Apply equip_sym with ordsucc x2, x1.

Apply unknownprop_20fce6fc7f2e036c1229cbf996632439eddb19cfae541105a83e5be9c65bc111 with x1, x0, λ x4 x5 . equip (ordsucc x2) x5 leaving 2 subgoals.

The subproof is completed by applying H3.

Apply unknownprop_eab190d6552dbda6c7d00c3e93c1ad9385698a8d73462a2a4e5795b67701610d with x2, setminus x1 (Sing x0), x0 leaving 2 subgoals.

Apply setminus_nIn_I2 with x1, Sing x0, x0.

The subproof is completed by applying SingI with x0.

Apply equip_sym with setminus x1 (Sing x0), x2.

The subproof is completed by applying H9.

...

■

Proofgold Proof