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.
Assume H5: x1 = x2 ⟶ ∀ x3 : ο . x3.
Assume H6: x0 x1 x2.
Let x3 of type ο be given.
Assume H7:
∀ x4 . x4 ∈ u9 ⟶ ∀ x5 . x5 ∈ u9 ⟶ (x1 = x4 ⟶ ∀ x6 : ο . x6) ⟶ (x1 = x5 ⟶ ∀ x6 : ο . x6) ⟶ (x2 = x4 ⟶ ∀ x6 : ο . x6) ⟶ (x2 = x5 ⟶ ∀ x6 : ο . x6) ⟶ (x4 = x5 ⟶ ∀ x6 : ο . x6) ⟶ x0 x1 x4 ⟶ x0 x1 x5 ⟶ not (x0 x2 x4) ⟶ not (x0 x2 x5) ⟶ not (x0 x4 x5) ⟶ (∀ x6 . x6 ∈ u9 ⟶ x0 x1 x6 ⟶ x6 ∈ SetAdjoin (SetAdjoin (UPair x1 x2) x4) x5) ⟶ x3.
Apply unknownprop_15d48b0d93044e45e1d5f0b67d2878c4ac013f81cd695d89157633dd4a764e14 with
x0,
x1,
x3 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
Let x4 of type ι be given.
Let x5 of type ι be given.
Let x6 of type ι be given.
Assume H11: x1 = x4 ⟶ ∀ x7 : ο . x7.
Assume H12: x1 = x5 ⟶ ∀ x7 : ο . x7.
Assume H13: x1 = x6 ⟶ ∀ x7 : ο . x7.
Assume H14: x4 = x5 ⟶ ∀ x7 : ο . x7.
Assume H15: x4 = x6 ⟶ ∀ x7 : ο . x7.
Assume H16: x5 = x6 ⟶ ∀ x7 : ο . x7.
Assume H17: x0 x1 x4.
Assume H18: x0 x1 x5.
Assume H19: x0 x1 x6.
Assume H20:
not (x0 x4 x5).
Assume H21:
not (x0 x4 x6).
Assume H22:
not (x0 x5 x6).
Apply L24 leaving 3 subgoals.
Assume H25: x2 = x4.
Apply H25 with
λ x7 x8 . ∀ x9 . ... ⟶ ... ⟶ ... ∈ ....
Apply H7 with
x5,
x6 leaving 13 subgoals.
The subproof is completed by applying H9.
The subproof is completed by applying H10.
The subproof is completed by applying H12.
The subproof is completed by applying H13.
The subproof is completed by applying L26.
The subproof is completed by applying L27.
The subproof is completed by applying H16.
The subproof is completed by applying H18.
The subproof is completed by applying H19.
The subproof is completed by applying L28.
The subproof is completed by applying L29.
The subproof is completed by applying H22.
The subproof is completed by applying L30.