Let x0 of type ι → (ι → ο) → ο be given.

Let x1 of type ι → (ι → ο) → ο be given.

Let x2 of type ι be given.

Let x3 of type ι → ο be given.

Let x4 of type ι → ο be given.

Assume H0: ordinal x2.

Assume H1: TransSet x2.

Assume H2: ∀ x5 . x5 ∈ x2 ⟶ ∀ x6 : ι → ο . not (PNo_strict_imv x0 x1 x5 x6).

Assume H3: PNo_strict_lowerbd x1 x2 x3.

Assume H4: PNo_strict_upperbd x0 x2 x4.

Assume H5: PNo_strict_lowerbd x1 x2 x4.

Assume H6: ∀ x5 . ordinal x5 ⟶ x5 ∈ x2 ⟶ iff (x3 x5) (x4 x5).

Let x5 of type ι be given.

Assume H7: x5 ∈ x2.

Claim L8: ordinal x5

Apply ordinal_Hered with x2, x5 leaving 2 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H7.

Apply H6 with x5 leaving 2 subgoals.

The subproof is completed by applying L8.

The subproof is completed by applying H7.

■

Proofgold Proof