Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

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

Assume H0: In x2 ((λ x3 x4 . binunion x3 (Sing x4)) x0 x1).

Let x3 of type ο be given.

Assume H1: In x2 x0 ⟶ x3.

Assume H2: x2 = x1 ⟶ x3.

Apply unknownprop_a497a9c4fdb392b95b688b10c74f8f445a953a0c88030ccc02fa0b24e4758231 with x0, Sing x1, x2, x3 leaving 3 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H1.

Assume H3: In x2 (Sing x1).

Apply H2.

Apply unknownprop_5b60b98e3f1eb090f9a13c5f00bc0b9619444831e46991a07d9b3c034c70e912 with x1, x2.

The subproof is completed by applying H3.

■

Proofgold Proof