Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ο be given.

Assume H0: Subq x1 (SNoElts_ x0) ⟶ (∀ x3 . In x3 x0 ⟶ exactly1of2 (In ((λ x4 . SetAdjoin x4 (Sing 1)) x3) x1) (In x3 x1)) ⟶ x2.

Apply unknownprop_e27cc1084b79022284e382e1b6bc2015115f79977a5cda617e7753aa1838b538 with λ x3 x4 : ι → ι → ο . x4 x0 x1 ⟶ x2.

Assume H1: (λ x3 x4 . and (Subq x4 (SNoElts_ x3)) (∀ x5 . In x5 x3 ⟶ exactly1of2 (In (SetAdjoin x5 (Sing 1)) x4) (In x5 x4))) x0 x1.

Apply andE with Subq x1 (SNoElts_ x0), ∀ x3 . In x3 x0 ⟶ exactly1of2 (In ((λ x4 . SetAdjoin x4 (Sing 1)) x3) x1) (In x3 x1), x2 leaving 2 subgoals.

The subproof is completed by applying H1.

The subproof is completed by applying H0.

■

Proofgold Proof