Let x0 of type ι be given.

Assume H0: ordinal x0.

Apply H0 with ∀ x1 . SNo x1 ⟶ SNoLev x1 ∈ ordsucc x0 ⟶ SNoLe x1 x0.

Assume H1: TransSet x0.

Assume H2: ∀ x1 . x1 ∈ x0 ⟶ TransSet x1.

Let x1 of type ι be given.

Assume H3: SNo x1.

Assume H4: SNoLev x1 ∈ ordsucc x0.

Claim L5: SNo x0

Apply ordinal_SNo with x0.

The subproof is completed by applying H0.

Claim L6: SNoLev x0 = x0

Apply ordinal_SNoLev with x0.

The subproof is completed by applying H0.

Apply ordsuccE with x0, SNoLev x1, SNoLe x1 x0 leaving 3 subgoals.

The subproof is completed by applying H4.

Assume H7: SNoLev x1 ∈ x0.

Apply SNoLtLe with x1, x0.

Apply ordinal_SNoLev_max with x0, x1 leaving 3 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H3.

The subproof is completed by applying H7.

Assume H7: SNoLev x1 = x0.

Apply dneg with SNoLe x1 x0.

Assume H8: not (SNoLe x1 x0).

Claim L9: ∀ x2 . ordinal x2 ⟶ x2 ∈ x0 ⟶ x2 ∈ x1

Apply ordinal_ind with λ x2 . x2 ∈ x0 ⟶ x2 ∈ x1.

Let x2 of type ι be given.

Assume H9: ordinal x2.

Assume H10: ∀ x3 . x3 ∈ x2 ⟶ x3 ∈ x0 ⟶ x3 ∈ x1.

Assume H11: x2 ∈ x0.

Apply dneg with x2 ∈ x1.

Assume H12: nIn x2 x1.

Apply H8.

Apply SNoLtLe with x1, x0.

Claim L13: SNo x2

Apply ordinal_SNo with x2.

The subproof is completed by applying H9.

Claim L14: SNoLev x2 = x2

Apply ordinal_SNoLev with x2.

The subproof is completed by applying H9.

Apply SNoLt_tra with x1, x2, x0 leaving 5 subgoals.

The subproof is completed by applying H3.

The subproof is completed by applying L13.

The subproof is completed by applying L5.

Apply SNoLtI3 with x1, x2 leaving 3 subgoals.

Apply L14 with λ x3 x4 . x4 ∈ SNoLev x1.

Apply H7 with λ x3 x4 . x2 ∈ x4.

The subproof is completed by applying H11.

Apply L14 with λ x3 x4 . SNoEq_ x4 x1 x2.

Let x3 of type ι be given.

Assume H15: x3 ∈ x2.

Apply iffI with x3 ∈ x1, x3 ∈ x2 leaving 2 subgoals.

Assume H16: x3 ∈ x1.

The subproof is completed by applying H15.

Assume H16: x3 ∈ x2.

Apply H10 with x3 leaving 2 subgoals.

The subproof is completed by applying H15.

Apply H1 with x2, x3 leaving 2 subgoals.

The subproof is completed by applying H11.

The subproof is completed by applying H15.

Apply L14 with λ x3 x4 . nIn x4 x1.

The subproof is completed by applying H12.

Apply ordinal_In_SNoLt with x0, x2 leaving 2 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H11.

Claim L10: x0 ⊆ x1

Let x2 of type ι be given.

Assume H10: x2 ∈ x0.

Apply L9 with x2 leaving 2 subgoals.

Apply ordinal_Hered with x0, x2 leaving 2 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H10.

Claim L11: x1 = x0

Apply SNo_eq with x1, x0 leaving 4 subgoals.

The subproof is completed by applying H3.

The subproof is completed by applying L5.

Apply L6 with λ x2 x3 . SNoLev x1 = x3.

The subproof is completed by applying H7.

Apply H7 with λ x2 x3 . SNoEq_ x3 x1 x0.

Let x2 of type ι be given.

Assume H11: x2 ∈ x0.

Apply iffI with x2 ∈ x1, x2 ∈ x0 leaving 2 subgoals.

Assume H12: x2 ∈ x1.

The subproof is completed by applying H11.

Assume H12: x2 ∈ x0.

Apply L10 with x2.

The subproof is completed by applying H11.

Apply H8.

Apply L11 with λ x2 x3 . SNoLe x3 x0.

The subproof is completed by applying SNoLe_ref with x0.

■

Proofgold Proof