Let x0 of type ι → ι → ο be given.
Assume H0: ∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1.
Assume H1:
not (or (∃ x1 . and (x1 ⊆ u9) (and (equip u3 x1) (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3))) (∃ x1 . and (x1 ⊆ u9) (and (equip u4 x1) (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3))))).
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Let x4 of type ι be given.
Let x5 of type ι be given.
Assume H8: x1 = x2 ⟶ ∀ x6 : ο . x6.
Assume H9: x1 = x3 ⟶ ∀ x6 : ο . x6.
Assume H10: x1 = x4 ⟶ ∀ x6 : ο . x6.
Assume H11: x1 = x5 ⟶ ∀ x6 : ο . x6.
Assume H12: x2 = x3 ⟶ ∀ x6 : ο . x6.
Assume H13: x2 = x4 ⟶ ∀ x6 : ο . x6.
Assume H14: x2 = x5 ⟶ ∀ x6 : ο . x6.
Assume H15: x3 = x4 ⟶ ∀ x6 : ο . x6.
Assume H16: x3 = x5 ⟶ ∀ x6 : ο . x6.
Assume H17: x4 = x5 ⟶ ∀ x6 : ο . x6.
Assume H18: x0 x1 x2.
Assume H19: x0 x1 x3.
Assume H20: x0 x1 x4.
Assume H21:
not (x0 x2 x3).
Assume H22:
not (x0 x2 x4).
Assume H23:
not (x0 x3 x4).
Assume H24: x0 x5 x2.
Assume H25: x0 x5 x3.
Assume H26: x0 x5 x4.
Apply unknownprop_45d11dce2d0b092bd17c01d64c29c5885c90b43dc7cb762c6d6ada999ea508c5 with
u3,
setminus u9 (SetAdjoin (SetAdjoin (SetAdjoin (UPair x1 x2) x3) x4) x5),
False leaving 3 subgoals.
The subproof is completed by applying nat_3.
Apply unknownprop_8a6bdce060c93f04626730b6e01b099cc0487102a697e253c81b39b9a082262d with
u8 leaving 2 subgoals.
The subproof is completed by applying nat_8.