Let x0 of type ι → ο be given.

Let x1 of type ι → ο be given.

Let x2 of type ι be given.

Assume H0: ordinal x2.

Apply unknownprop_d3eaeaf2c92929364f7d313ca2b01dbaa8e7169d84112bc61a6ed9c6cb0d624a with λ x3 x4 : ι → (ι → ο) → (ι → ο) → ο . ∀ x5 . In x5 x2 ⟶ x4 x5 x0 x1 ⟶ x4 x2 x0 x1.

Let x3 of type ι be given.

Assume H1: In x3 x2.

Assume H2: (λ x4 . λ x5 x6 : ι → ο . ∃ x7 . and (In x7 x4) (and (and (PNoEq_ x7 x5 x6) (not (x5 x7))) (x6 x7))) x3 x0 x1.

Apply H2 with (λ x4 . λ x5 x6 : ι → ο . ∃ x7 . and (In x7 x4) (and (and (PNoEq_ x7 x5 x6) (not (x5 x7))) (x6 x7))) x2 x0 x1.

Let x4 of type ι be given.

Assume H3: (λ x5 . and (In x5 x3) (and (and (PNoEq_ x5 x0 x1) (not (x0 x5))) (x1 x5))) x4.

Apply andE with In x4 x3, and (and (PNoEq_ x4 x0 x1) (not (x0 x4))) (x1 x4), (λ x5 . λ x6 x7 : ι → ο . ∃ x8 . and (In x8 x5) (and (and (PNoEq_ x8 x6 x7) (not (x6 x8))) (x7 x8))) x2 x0 x1 leaving 2 subgoals.

The subproof is completed by applying H3.

Assume H4: In x4 x3.

Assume H5: and (and (PNoEq_ x4 x0 x1) (not (x0 x4))) (x1 x4).

Let x5 of type ο be given.

Assume H6: ∀ x6 . and (In x6 x2) (and (and (PNoEq_ x6 x0 x1) (not (x0 x6))) (x1 x6)) ⟶ x5.

Apply H6 with x4.

Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with In x4 x2, and (and (PNoEq_ x4 x0 x1) (not (x0 x4))) (x1 x4) leaving 2 subgoals.

Apply unknownprop_16d203cf35db7c43083950b8cdf3bc14c48faba5d53a8b40d54b8c3e00a23527 with x2, x3, x4 leaving 3 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H1.

The subproof is completed by applying H4.

The subproof is completed by applying H5.

■

Proofgold Proof