Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι → ι → ο be given.
Assume H0: ∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1.
Claim L1: ...
...
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.
Assume H3: x1 ∈ u9.
Let x2 of type ο be given.
Assume H4: ∀ x3 . x3 ∈ u9 ⟶ ∀ x4 . x4 ∈ u9 ⟶ ∀ x5 . x5 ∈ u9 ⟶ (x1 = x3 ⟶ ∀ x6 : ο . x6) ⟶ (x1 = x4 ⟶ ∀ x6 : ο . x6) ⟶ (x1 = x5 ⟶ ∀ x6 : ο . x6) ⟶ (x3 = x4 ⟶ ∀ x6 : ο . x6) ⟶ (x3 = x5 ⟶ ∀ x6 : ο . x6) ⟶ (x4 = x5 ⟶ ∀ x6 : ο . x6) ⟶ x0 x1 x3 ⟶ x0 x1 x4 ⟶ x0 x1 x5 ⟶ not (x0 x3 x4) ⟶ not (x0 x3 x5) ⟶ not (x0 x4 x5) ⟶ (∀ x6 . x6 ∈ u9 ⟶ x0 x1 x6 ⟶ x6 ∈ SetAdjoin (SetAdjoin (UPair x1 x3) x4) x5) ⟶ x2.
Apply unknownprop_452df11b965aa438aa496a76fcdf27f39965839d9f9a8a70e5fe6b3a61f5a4ef with x0, x1, x2 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 x3 of type ι be given.
Assume H5: x3 ∈ u9.
Let x4 of type ι be given.
Assume H6: x4 ∈ u9.
Let x5 of type ι be given.
Assume H7: x5 ∈ u9.
Assume H8: x1 = x3 ⟶ ∀ x6 : ο . x6.
Assume H9: x1 = x4 ⟶ ∀ x6 : ο . x6.
Assume H10: x1 = x5 ⟶ ∀ x6 : ο . x6.
Assume H11: x3 = x4 ⟶ ∀ x6 : ο . x6.
Assume H12: x3 = x5 ⟶ ∀ x6 : ο . x6.
Assume H13: x4 = x5 ⟶ ∀ x6 : ο . x6.
Assume H14: x0 x1 x3.
Assume H15: x0 x1 x4.
Assume H16: x0 x1 x5.
Claim L17: ...
...
Claim L18: ...
...
Claim L19: ...
...
Apply H4 with x3, x4, x5 leaving 16 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H6.
The subproof is completed by applying H7.
The subproof is completed by applying H8.
The subproof is completed by applying H9.
The subproof is completed by applying H10.
The subproof is completed by applying H11.
The subproof is completed by applying H12.
The subproof is completed by applying H13.
The subproof is completed by applying H14.
The subproof is completed by applying H15.
The subproof is completed by applying H16.
The subproof is completed by applying L17.
The subproof is completed by applying L18.
The subproof is completed by applying L19.
Let x6 of type ι be given.
Assume H20: x6 ∈ u9.
Assume H21: x0 x1 x6.
Apply dneg with x6 ∈ SetAdjoin (SetAdjoin (UPair x1 x3) x4) x5.
Assume H22: nIn x6 (SetAdjoin (SetAdjoin (UPair x1 x3) x4) x5).
Claim L23: ...
...
Claim L24: ...
...
Claim L25: ...
...
Apply H2.
Apply orIR with ∃ x7 . and (x7 ⊆ u9) (and (equip u3 x7) (∀ x8 . x8 ∈ x7 ⟶ ∀ x9 . x9 ∈ x7 ⟶ (x8 = x9 ⟶ ∀ x10 : ο . x10) ⟶ x0 x8 x9)), ∃ x7 . and ... ....
...
■