Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι → ι → ο be given.
Let x1 of type ι → ι be given.
Assume H0: ∀ x2 . x2 ∈ u12 ⟶ x1 x2 ∈ u12.
Assume H1: ∀ x2 . x2 ∈ u12 ⟶ ∀ x3 . x3 ∈ u12 ⟶ x1 x2 = x1 x3 ⟶ x2 = x3.
Assume H2: ∀ x2 . x2 ∈ u12 ⟶ ∀ x3 . x3 ∈ u12 ⟶ x0 (x1 x2) (x1 x3) ⟶ x0 x2 x3.
Assume H3: x1 u9 = u8.
Assume H4: x1 u10 = u11.
Assume H5: x1 u11 = u9.
Assume H6: x0 u8 u11.
Let x2 of type ι be given.
Assume H7: x2 ⊆ u12.
Assume H8: atleastp u5 x2.
Assume H9: ∀ x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ∈ x2 ⟶ not (x0 x3 x4).
Assume H10: atleastp u2 (setminus x2 u8).
Let x3 of type ο be given.
Assume H11: ∀ x4 . x4 ⊆ u12 ⟶ atleastp u5 x4 ⟶ (∀ x5 . x5 ∈ x4 ⟶ ∀ x6 . x6 ∈ x4 ⟶ not (x0 x5 x6)) ⟶ u8 ∈ x4 ⟶ u9 ∈ x4 ⟶ x3.
Assume H12: ∀ x4 . x4 ⊆ u12 ⟶ atleastp u5 x4 ⟶ (∀ x5 . x5 ∈ x4 ⟶ ∀ x6 . x6 ∈ x4 ⟶ not (x0 x5 x6)) ⟶ u8 ∈ x4 ⟶ u10 ∈ x4 ⟶ x3.
Assume H13: ∀ x4 . x4 ⊆ u12 ⟶ atleastp u5 x4 ⟶ (∀ x5 . x5 ∈ x4 ⟶ ∀ x6 . x6 ∈ x4 ⟶ not (x0 x5 x6)) ⟶ u9 ∈ x4 ⟶ u10 ∈ x4 ⟶ x3.
Claim L14: ...
...
Claim L15: ...
...
Claim L16: ...
...
Claim L17: ...
...
Claim L18: ...
...
Claim L19: ...
...
Claim L20: ...
...
Claim L21: ...
...
Apply unknownprop_8d334858d1804afd99b1b9082715c7f916daee31e697b66b5c752e0c8756ebae with setminus x2 u8, x3 leaving 2 subgoals.
The subproof is completed by applying H10.
Apply L15 with x3.
Let x4 of type ι be given.
Assume H22: x4 ∈ setminus x2 u8.
Let x5 of type ι be given.
Assume H23: x5 ∈ setminus x2 u8.
Assume H24: x4 ∈ x5.
Apply setminusE with x2, u8, x4, x3 leaving 2 subgoals.
The subproof is completed by applying H22.
Assume H25: x4 ∈ x2.
Assume H26: nIn x4 u8.
Apply setminusE with x2, u8, x5, x3 leaving 2 subgoals.
The subproof is completed by applying H23.
Assume H27: x5 ∈ x2.
Assume H28: nIn x5 u8.
Apply L14 with x4, x3 leaving 6 subgoals.
Apply H7 with x4.
The subproof is completed by applying H25.
Assume H29: x4 ∈ u8.
Apply FalseE with x3.
Apply H26.
The subproof is completed by applying H29.
Assume H29: x4 = u8.
Apply L14 with x5, x3 leaving 6 subgoals.
Apply H7 with x5.
The subproof is completed by applying H27.
Assume H30: x5 ∈ u8.
Apply FalseE with x3.
Apply H28.
The subproof is completed by applying H30.
Assume H30: x5 = u8.
Apply FalseE with x3.
Apply In_irref with x4.
Apply H29 with λ x6 x7 . x4 ∈ x7.
Apply H30 with λ x6 x7 . x4 ∈ x6.
The subproof is completed by applying H24.
Assume H30: x5 = u9.
Apply H11 with x2 leaving 5 subgoals.
The subproof is completed by applying H7.
The subproof is completed by applying H8.
The subproof is completed by applying H9.
Apply H29 with λ x6 x7 . x6 ∈ x2.
The subproof is completed by applying H25.
Apply H30 with λ x6 x7 . x6 ∈ x2.
The subproof is completed by applying H27.
Assume H30: x5 = u10.
Apply H12 with x2 leaving 5 subgoals.
The subproof is completed by applying H7.
The subproof is completed by applying H8.
The subproof is completed by applying H9.
Apply H29 with λ x6 x7 . x6 ∈ x2.
The subproof is completed by applying H25.
Apply H30 with λ x6 x7 . x6 ∈ x2.
The subproof is completed by applying H27.
Assume H30: ....
...
...
...
...
■