| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | legval.l | . 2
⊢  ≤ =
(≤G‘𝐺) | 
| 2 |  | legval.g | . . 3
⊢ (𝜑 → 𝐺 ∈ TarskiG) | 
| 3 |  | elex 3501 | . . 3
⊢ (𝐺 ∈ TarskiG → 𝐺 ∈ V) | 
| 4 |  | legval.p | . . . . . 6
⊢ 𝑃 = (Base‘𝐺) | 
| 5 |  | legval.d | . . . . . 6
⊢  − =
(dist‘𝐺) | 
| 6 |  | legval.i | . . . . . 6
⊢ 𝐼 = (Itv‘𝐺) | 
| 7 |  | simp1 1137 | . . . . . . . 8
⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → 𝑝 = 𝑃) | 
| 8 | 7 | eqcomd 2743 | . . . . . . 7
⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → 𝑃 = 𝑝) | 
| 9 |  | simp2 1138 | . . . . . . . . . . . 12
⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → 𝑑 = − ) | 
| 10 | 9 | eqcomd 2743 | . . . . . . . . . . 11
⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → − = 𝑑) | 
| 11 | 10 | oveqd 7448 | . . . . . . . . . 10
⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (𝑥 − 𝑦) = (𝑥𝑑𝑦)) | 
| 12 | 11 | eqeq2d 2748 | . . . . . . . . 9
⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (𝑓 = (𝑥 − 𝑦) ↔ 𝑓 = (𝑥𝑑𝑦))) | 
| 13 |  | simp3 1139 | . . . . . . . . . . . . . 14
⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → 𝑖 = 𝐼) | 
| 14 | 13 | eqcomd 2743 | . . . . . . . . . . . . 13
⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → 𝐼 = 𝑖) | 
| 15 | 14 | oveqd 7448 | . . . . . . . . . . . 12
⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (𝑥𝐼𝑦) = (𝑥𝑖𝑦)) | 
| 16 | 15 | eleq2d 2827 | . . . . . . . . . . 11
⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (𝑧 ∈ (𝑥𝐼𝑦) ↔ 𝑧 ∈ (𝑥𝑖𝑦))) | 
| 17 | 10 | oveqd 7448 | . . . . . . . . . . . 12
⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (𝑥 − 𝑧) = (𝑥𝑑𝑧)) | 
| 18 | 17 | eqeq2d 2748 | . . . . . . . . . . 11
⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (𝑒 = (𝑥 − 𝑧) ↔ 𝑒 = (𝑥𝑑𝑧))) | 
| 19 | 16, 18 | anbi12d 632 | . . . . . . . . . 10
⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → ((𝑧 ∈ (𝑥𝐼𝑦) ∧ 𝑒 = (𝑥 − 𝑧)) ↔ (𝑧 ∈ (𝑥𝑖𝑦) ∧ 𝑒 = (𝑥𝑑𝑧)))) | 
| 20 | 8, 19 | rexeqbidv 3347 | . . . . . . . . 9
⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (∃𝑧 ∈ 𝑃 (𝑧 ∈ (𝑥𝐼𝑦) ∧ 𝑒 = (𝑥 − 𝑧)) ↔ ∃𝑧 ∈ 𝑝 (𝑧 ∈ (𝑥𝑖𝑦) ∧ 𝑒 = (𝑥𝑑𝑧)))) | 
| 21 | 12, 20 | anbi12d 632 | . . . . . . . 8
⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → ((𝑓 = (𝑥 − 𝑦) ∧ ∃𝑧 ∈ 𝑃 (𝑧 ∈ (𝑥𝐼𝑦) ∧ 𝑒 = (𝑥 − 𝑧))) ↔ (𝑓 = (𝑥𝑑𝑦) ∧ ∃𝑧 ∈ 𝑝 (𝑧 ∈ (𝑥𝑖𝑦) ∧ 𝑒 = (𝑥𝑑𝑧))))) | 
| 22 | 8, 21 | rexeqbidv 3347 | . . . . . . 7
⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (∃𝑦 ∈ 𝑃 (𝑓 = (𝑥 − 𝑦) ∧ ∃𝑧 ∈ 𝑃 (𝑧 ∈ (𝑥𝐼𝑦) ∧ 𝑒 = (𝑥 − 𝑧))) ↔ ∃𝑦 ∈ 𝑝 (𝑓 = (𝑥𝑑𝑦) ∧ ∃𝑧 ∈ 𝑝 (𝑧 ∈ (𝑥𝑖𝑦) ∧ 𝑒 = (𝑥𝑑𝑧))))) | 
| 23 | 8, 22 | rexeqbidv 3347 | . . . . . 6
⊢ ((𝑝 = 𝑃 ∧ 𝑑 = − ∧ 𝑖 = 𝐼) → (∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑓 = (𝑥 − 𝑦) ∧ ∃𝑧 ∈ 𝑃 (𝑧 ∈ (𝑥𝐼𝑦) ∧ 𝑒 = (𝑥 − 𝑧))) ↔ ∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 (𝑓 = (𝑥𝑑𝑦) ∧ ∃𝑧 ∈ 𝑝 (𝑧 ∈ (𝑥𝑖𝑦) ∧ 𝑒 = (𝑥𝑑𝑧))))) | 
| 24 | 4, 5, 6, 23 | sbcie3s 17199 | . . . . 5
⊢ (𝑔 = 𝐺 → ([(Base‘𝑔) / 𝑝][(dist‘𝑔) / 𝑑][(Itv‘𝑔) / 𝑖]∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 (𝑓 = (𝑥𝑑𝑦) ∧ ∃𝑧 ∈ 𝑝 (𝑧 ∈ (𝑥𝑖𝑦) ∧ 𝑒 = (𝑥𝑑𝑧))) ↔ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑓 = (𝑥 − 𝑦) ∧ ∃𝑧 ∈ 𝑃 (𝑧 ∈ (𝑥𝐼𝑦) ∧ 𝑒 = (𝑥 − 𝑧))))) | 
| 25 | 24 | opabbidv 5209 | . . . 4
⊢ (𝑔 = 𝐺 → {〈𝑒, 𝑓〉 ∣ [(Base‘𝑔) / 𝑝][(dist‘𝑔) / 𝑑][(Itv‘𝑔) / 𝑖]∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 (𝑓 = (𝑥𝑑𝑦) ∧ ∃𝑧 ∈ 𝑝 (𝑧 ∈ (𝑥𝑖𝑦) ∧ 𝑒 = (𝑥𝑑𝑧)))} = {〈𝑒, 𝑓〉 ∣ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑓 = (𝑥 − 𝑦) ∧ ∃𝑧 ∈ 𝑃 (𝑧 ∈ (𝑥𝐼𝑦) ∧ 𝑒 = (𝑥 − 𝑧)))}) | 
| 26 |  | df-leg 28591 | . . . 4
⊢ ≤G =
(𝑔 ∈ V ↦
{〈𝑒, 𝑓〉 ∣
[(Base‘𝑔) /
𝑝][(dist‘𝑔) / 𝑑][(Itv‘𝑔) / 𝑖]∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 (𝑓 = (𝑥𝑑𝑦) ∧ ∃𝑧 ∈ 𝑝 (𝑧 ∈ (𝑥𝑖𝑦) ∧ 𝑒 = (𝑥𝑑𝑧)))}) | 
| 27 | 5 | fvexi 6920 | . . . . . . . . 9
⊢  − ∈
V | 
| 28 | 27 | imaex 7936 | . . . . . . . 8
⊢ ( − “
(𝑃 × 𝑃)) ∈ V | 
| 29 |  | p0ex 5384 | . . . . . . . 8
⊢ {∅}
∈ V | 
| 30 | 28, 29 | unex 7764 | . . . . . . 7
⊢ (( − “
(𝑃 × 𝑃)) ∪ {∅}) ∈
V | 
| 31 | 30 | a1i 11 | . . . . . 6
⊢ (⊤
→ (( − “ (𝑃 × 𝑃)) ∪ {∅}) ∈
V) | 
| 32 |  | simprr 773 | . . . . . . . . . . . . 13
⊢
(((((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃) ∧ (𝑓 = (𝑥 − 𝑦) ∧ ∃𝑧 ∈ 𝑃 (𝑧 ∈ (𝑥𝐼𝑦) ∧ 𝑒 = (𝑥 − 𝑧)))) ∧ 𝑑 ∈ 𝑃) ∧ (𝑑 ∈ (𝑥𝐼𝑦) ∧ 𝑒 = (𝑥 − 𝑑))) → 𝑒 = (𝑥 − 𝑑)) | 
| 33 |  | ovima0 7612 | . . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝑃 ∧ 𝑑 ∈ 𝑃) → (𝑥 − 𝑑) ∈ (( − “ (𝑃 × 𝑃)) ∪ {∅})) | 
| 34 | 33 | ad5ant14 758 | . . . . . . . . . . . . 13
⊢
(((((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃) ∧ (𝑓 = (𝑥 − 𝑦) ∧ ∃𝑧 ∈ 𝑃 (𝑧 ∈ (𝑥𝐼𝑦) ∧ 𝑒 = (𝑥 − 𝑧)))) ∧ 𝑑 ∈ 𝑃) ∧ (𝑑 ∈ (𝑥𝐼𝑦) ∧ 𝑒 = (𝑥 − 𝑑))) → (𝑥 − 𝑑) ∈ (( − “ (𝑃 × 𝑃)) ∪ {∅})) | 
| 35 | 32, 34 | eqeltrd 2841 | . . . . . . . . . . . 12
⊢
(((((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃) ∧ (𝑓 = (𝑥 − 𝑦) ∧ ∃𝑧 ∈ 𝑃 (𝑧 ∈ (𝑥𝐼𝑦) ∧ 𝑒 = (𝑥 − 𝑧)))) ∧ 𝑑 ∈ 𝑃) ∧ (𝑑 ∈ (𝑥𝐼𝑦) ∧ 𝑒 = (𝑥 − 𝑑))) → 𝑒 ∈ (( − “ (𝑃 × 𝑃)) ∪ {∅})) | 
| 36 |  | simpllr 776 | . . . . . . . . . . . . . 14
⊢
(((((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃) ∧ (𝑓 = (𝑥 − 𝑦) ∧ ∃𝑧 ∈ 𝑃 (𝑧 ∈ (𝑥𝐼𝑦) ∧ 𝑒 = (𝑥 − 𝑧)))) ∧ 𝑑 ∈ 𝑃) ∧ (𝑑 ∈ (𝑥𝐼𝑦) ∧ 𝑒 = (𝑥 − 𝑑))) → (𝑓 = (𝑥 − 𝑦) ∧ ∃𝑧 ∈ 𝑃 (𝑧 ∈ (𝑥𝐼𝑦) ∧ 𝑒 = (𝑥 − 𝑧)))) | 
| 37 | 36 | simpld 494 | . . . . . . . . . . . . 13
⊢
(((((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃) ∧ (𝑓 = (𝑥 − 𝑦) ∧ ∃𝑧 ∈ 𝑃 (𝑧 ∈ (𝑥𝐼𝑦) ∧ 𝑒 = (𝑥 − 𝑧)))) ∧ 𝑑 ∈ 𝑃) ∧ (𝑑 ∈ (𝑥𝐼𝑦) ∧ 𝑒 = (𝑥 − 𝑑))) → 𝑓 = (𝑥 − 𝑦)) | 
| 38 |  | ovima0 7612 | . . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃) → (𝑥 − 𝑦) ∈ (( − “ (𝑃 × 𝑃)) ∪ {∅})) | 
| 39 | 38 | ad3antrrr 730 | . . . . . . . . . . . . 13
⊢
(((((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃) ∧ (𝑓 = (𝑥 − 𝑦) ∧ ∃𝑧 ∈ 𝑃 (𝑧 ∈ (𝑥𝐼𝑦) ∧ 𝑒 = (𝑥 − 𝑧)))) ∧ 𝑑 ∈ 𝑃) ∧ (𝑑 ∈ (𝑥𝐼𝑦) ∧ 𝑒 = (𝑥 − 𝑑))) → (𝑥 − 𝑦) ∈ (( − “ (𝑃 × 𝑃)) ∪ {∅})) | 
| 40 | 37, 39 | eqeltrd 2841 | . . . . . . . . . . . 12
⊢
(((((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃) ∧ (𝑓 = (𝑥 − 𝑦) ∧ ∃𝑧 ∈ 𝑃 (𝑧 ∈ (𝑥𝐼𝑦) ∧ 𝑒 = (𝑥 − 𝑧)))) ∧ 𝑑 ∈ 𝑃) ∧ (𝑑 ∈ (𝑥𝐼𝑦) ∧ 𝑒 = (𝑥 − 𝑑))) → 𝑓 ∈ (( − “ (𝑃 × 𝑃)) ∪ {∅})) | 
| 41 | 35, 40 | jca 511 | . . . . . . . . . . 11
⊢
(((((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃) ∧ (𝑓 = (𝑥 − 𝑦) ∧ ∃𝑧 ∈ 𝑃 (𝑧 ∈ (𝑥𝐼𝑦) ∧ 𝑒 = (𝑥 − 𝑧)))) ∧ 𝑑 ∈ 𝑃) ∧ (𝑑 ∈ (𝑥𝐼𝑦) ∧ 𝑒 = (𝑥 − 𝑑))) → (𝑒 ∈ (( − “ (𝑃 × 𝑃)) ∪ {∅}) ∧ 𝑓 ∈ (( − “ (𝑃 × 𝑃)) ∪ {∅}))) | 
| 42 |  | simprr 773 | . . . . . . . . . . . 12
⊢ (((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃) ∧ (𝑓 = (𝑥 − 𝑦) ∧ ∃𝑧 ∈ 𝑃 (𝑧 ∈ (𝑥𝐼𝑦) ∧ 𝑒 = (𝑥 − 𝑧)))) → ∃𝑧 ∈ 𝑃 (𝑧 ∈ (𝑥𝐼𝑦) ∧ 𝑒 = (𝑥 − 𝑧))) | 
| 43 |  | eleq1w 2824 | . . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑑 → (𝑧 ∈ (𝑥𝐼𝑦) ↔ 𝑑 ∈ (𝑥𝐼𝑦))) | 
| 44 |  | oveq2 7439 | . . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑑 → (𝑥 − 𝑧) = (𝑥 − 𝑑)) | 
| 45 | 44 | eqeq2d 2748 | . . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑑 → (𝑒 = (𝑥 − 𝑧) ↔ 𝑒 = (𝑥 − 𝑑))) | 
| 46 | 43, 45 | anbi12d 632 | . . . . . . . . . . . . 13
⊢ (𝑧 = 𝑑 → ((𝑧 ∈ (𝑥𝐼𝑦) ∧ 𝑒 = (𝑥 − 𝑧)) ↔ (𝑑 ∈ (𝑥𝐼𝑦) ∧ 𝑒 = (𝑥 − 𝑑)))) | 
| 47 | 46 | cbvrexvw 3238 | . . . . . . . . . . . 12
⊢
(∃𝑧 ∈
𝑃 (𝑧 ∈ (𝑥𝐼𝑦) ∧ 𝑒 = (𝑥 − 𝑧)) ↔ ∃𝑑 ∈ 𝑃 (𝑑 ∈ (𝑥𝐼𝑦) ∧ 𝑒 = (𝑥 − 𝑑))) | 
| 48 | 42, 47 | sylib 218 | . . . . . . . . . . 11
⊢ (((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃) ∧ (𝑓 = (𝑥 − 𝑦) ∧ ∃𝑧 ∈ 𝑃 (𝑧 ∈ (𝑥𝐼𝑦) ∧ 𝑒 = (𝑥 − 𝑧)))) → ∃𝑑 ∈ 𝑃 (𝑑 ∈ (𝑥𝐼𝑦) ∧ 𝑒 = (𝑥 − 𝑑))) | 
| 49 | 41, 48 | r19.29a 3162 | . . . . . . . . . 10
⊢ (((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃) ∧ (𝑓 = (𝑥 − 𝑦) ∧ ∃𝑧 ∈ 𝑃 (𝑧 ∈ (𝑥𝐼𝑦) ∧ 𝑒 = (𝑥 − 𝑧)))) → (𝑒 ∈ (( − “ (𝑃 × 𝑃)) ∪ {∅}) ∧ 𝑓 ∈ (( − “ (𝑃 × 𝑃)) ∪ {∅}))) | 
| 50 | 49 | ex 412 | . . . . . . . . 9
⊢ ((𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃) → ((𝑓 = (𝑥 − 𝑦) ∧ ∃𝑧 ∈ 𝑃 (𝑧 ∈ (𝑥𝐼𝑦) ∧ 𝑒 = (𝑥 − 𝑧))) → (𝑒 ∈ (( − “ (𝑃 × 𝑃)) ∪ {∅}) ∧ 𝑓 ∈ (( − “ (𝑃 × 𝑃)) ∪ {∅})))) | 
| 51 | 50 | rexlimivv 3201 | . . . . . . . 8
⊢
(∃𝑥 ∈
𝑃 ∃𝑦 ∈ 𝑃 (𝑓 = (𝑥 − 𝑦) ∧ ∃𝑧 ∈ 𝑃 (𝑧 ∈ (𝑥𝐼𝑦) ∧ 𝑒 = (𝑥 − 𝑧))) → (𝑒 ∈ (( − “ (𝑃 × 𝑃)) ∪ {∅}) ∧ 𝑓 ∈ (( − “ (𝑃 × 𝑃)) ∪ {∅}))) | 
| 52 | 51 | adantl 481 | . . . . . . 7
⊢
((⊤ ∧ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑓 = (𝑥 − 𝑦) ∧ ∃𝑧 ∈ 𝑃 (𝑧 ∈ (𝑥𝐼𝑦) ∧ 𝑒 = (𝑥 − 𝑧)))) → (𝑒 ∈ (( − “ (𝑃 × 𝑃)) ∪ {∅}) ∧ 𝑓 ∈ (( − “ (𝑃 × 𝑃)) ∪ {∅}))) | 
| 53 | 52 | simpld 494 | . . . . . 6
⊢
((⊤ ∧ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑓 = (𝑥 − 𝑦) ∧ ∃𝑧 ∈ 𝑃 (𝑧 ∈ (𝑥𝐼𝑦) ∧ 𝑒 = (𝑥 − 𝑧)))) → 𝑒 ∈ (( − “ (𝑃 × 𝑃)) ∪ {∅})) | 
| 54 | 52 | simprd 495 | . . . . . 6
⊢
((⊤ ∧ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑓 = (𝑥 − 𝑦) ∧ ∃𝑧 ∈ 𝑃 (𝑧 ∈ (𝑥𝐼𝑦) ∧ 𝑒 = (𝑥 − 𝑧)))) → 𝑓 ∈ (( − “ (𝑃 × 𝑃)) ∪ {∅})) | 
| 55 | 31, 31, 53, 54 | opabex2 8082 | . . . . 5
⊢ (⊤
→ {〈𝑒, 𝑓〉 ∣ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑓 = (𝑥 − 𝑦) ∧ ∃𝑧 ∈ 𝑃 (𝑧 ∈ (𝑥𝐼𝑦) ∧ 𝑒 = (𝑥 − 𝑧)))} ∈ V) | 
| 56 | 55 | mptru 1547 | . . . 4
⊢
{〈𝑒, 𝑓〉 ∣ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑓 = (𝑥 − 𝑦) ∧ ∃𝑧 ∈ 𝑃 (𝑧 ∈ (𝑥𝐼𝑦) ∧ 𝑒 = (𝑥 − 𝑧)))} ∈ V | 
| 57 | 25, 26, 56 | fvmpt 7016 | . . 3
⊢ (𝐺 ∈ V →
(≤G‘𝐺) =
{〈𝑒, 𝑓〉 ∣ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑓 = (𝑥 − 𝑦) ∧ ∃𝑧 ∈ 𝑃 (𝑧 ∈ (𝑥𝐼𝑦) ∧ 𝑒 = (𝑥 − 𝑧)))}) | 
| 58 | 2, 3, 57 | 3syl 18 | . 2
⊢ (𝜑 → (≤G‘𝐺) = {〈𝑒, 𝑓〉 ∣ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑓 = (𝑥 − 𝑦) ∧ ∃𝑧 ∈ 𝑃 (𝑧 ∈ (𝑥𝐼𝑦) ∧ 𝑒 = (𝑥 − 𝑧)))}) | 
| 59 | 1, 58 | eqtrid 2789 | 1
⊢ (𝜑 → ≤ = {〈𝑒, 𝑓〉 ∣ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑓 = (𝑥 − 𝑦) ∧ ∃𝑧 ∈ 𝑃 (𝑧 ∈ (𝑥𝐼𝑦) ∧ 𝑒 = (𝑥 − 𝑧)))}) |