Let x0 of type ι → ι → ο be given.
Assume H0: ∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1.
Assume H2:
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.
Assume H7: x1 = x2 ⟶ ∀ x5 : ο . x5.
Assume H8: x1 = x3 ⟶ ∀ x5 : ο . x5.
Assume H9: x1 = x4 ⟶ ∀ x5 : ο . x5.
Assume H10: x2 = x3 ⟶ ∀ x5 : ο . x5.
Assume H11: x2 = x4 ⟶ ∀ x5 : ο . x5.
Assume H12: x3 = x4 ⟶ ∀ x5 : ο . x5.
Assume H13: x0 x1 x2.
Assume H14: x0 x1 x3.
Assume H15: x0 x1 x4.
Apply unknownprop_f0014261a073154b27e42b7a2586bc3123c4455a00f08c2d90b89b2c21d8c9c7 with
x0,
x1,
x2,
x3,
∀ x5 . x5 ∈ u9 ⟶ x0 x1 x5 ⟶ x5 ∈ SetAdjoin (SetAdjoin (UPair x1 x2) x3) x4 leaving 11 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
The subproof is completed by applying H7.
The subproof is completed by applying H8.
The subproof is completed by applying H10.
The subproof is completed by applying H13.
The subproof is completed by applying H14.
Let x5 of type ι be given.
Assume H17: x1 = x5 ⟶ ∀ x6 : ο . x6.
Assume H18: x2 = x5 ⟶ ∀ x6 : ο . x6.
Assume H19: x3 = x5 ⟶ ∀ x6 : ο . x6.
Assume H20: x0 x1 x5.
Assume H21:
not (x0 x2 x5).
Assume H22:
not (x0 x3 x5).
Apply binunionE with
SetAdjoin (UPair x1 x2) x3,
Sing x5,
x4,
∀ x6 . x6 ∈ u9 ⟶ x0 x1 x6 ⟶ x6 ∈ SetAdjoin (SetAdjoin (UPair x1 x2) x3) x4 leaving 3 subgoals.
Apply H23 with
x4 leaving 2 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying H15.
Apply FalseE with
∀ x6 . x6 ∈ u9 ⟶ x0 x1 x6 ⟶ x6 ∈ SetAdjoin (SetAdjoin (UPair x1 x2) x3) x4.
Apply binunionE with
UPair x1 x2,
Sing x3,
x4,
False leaving 3 subgoals.
The subproof is completed by applying H24.
Assume H25:
x4 ∈ UPair x1 x2.
Apply UPairE with
x4,
x1,
x2,
False leaving 3 subgoals.
The subproof is completed by applying H25.
Assume H26: x4 = x1.
Apply H9.
Let x6 of type ι → ι → ο be given.
The subproof is completed by applying H26 with λ x7 x8 . x6 x8 x7.