Proofgold Proof

pf

Let x0 of type ι be given.

Assume H0: ordinal x0.

Let x1 of type ι → ο be given.

Let x2 of type ι be given.

Assume H1: ordinal x2.

Let x3 of type ι → ο be given.

Assume H2: PNoCutL x0 x1 x2 x3.

Let x4 of type ι be given.

Assume H3: ordinal x4.

Let x5 of type ι → ο be given.

Assume H4: PNoCutR x0 x1 x4 x5.

Apply H2 with PNoLt x2 x3 x4 x5.

Assume H5: x2 ∈ x0.

Assume H6: PNoLt x2 x3 x0 x1.

Apply H4 with PNoLt x2 x3 x4 x5.

Assume H7: x4 ∈ x0.

Assume H8: PNoLt x0 x1 x4 x5.

Apply PNoLt_tra with x2, x0, x4, x3, x1, x5 leaving 5 subgoals.

The subproof is completed by applying H1.

The subproof is completed by applying H0.

The subproof is completed by applying H3.

The subproof is completed by applying H6.

The subproof is completed by applying H8.

■