MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-leg Structured version   Visualization version   GIF version

Definition df-leg 26296
Description: Define the less-than relationship between geometric distance congruence classes. See legval 26297. (Contributed by Thierry Arnoux, 21-Jun-2019.)
Assertion
Ref Expression
df-leg ≤G = (𝑔 ∈ V ↦ {⟨𝑒, 𝑓⟩ ∣ [(Base‘𝑔) / 𝑝][(dist‘𝑔) / 𝑑][(Itv‘𝑔) / 𝑖]𝑥𝑝𝑦𝑝 (𝑓 = (𝑥𝑑𝑦) ∧ ∃𝑧𝑝 (𝑧 ∈ (𝑥𝑖𝑦) ∧ 𝑒 = (𝑥𝑑𝑧)))})
Distinct variable group:   𝑒,𝑑,𝑓,𝑔,𝑖,𝑝,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-leg
StepHypRef Expression
1 cleg 26295 . 2 class ≤G
2 vg . . 3 setvar 𝑔
3 cvv 3492 . . 3 class V
4 vf . . . . . . . . . . . 12 setvar 𝑓
54cv 1527 . . . . . . . . . . 11 class 𝑓
6 vx . . . . . . . . . . . . 13 setvar 𝑥
76cv 1527 . . . . . . . . . . . 12 class 𝑥
8 vy . . . . . . . . . . . . 13 setvar 𝑦
98cv 1527 . . . . . . . . . . . 12 class 𝑦
10 vd . . . . . . . . . . . . 13 setvar 𝑑
1110cv 1527 . . . . . . . . . . . 12 class 𝑑
127, 9, 11co 7145 . . . . . . . . . . 11 class (𝑥𝑑𝑦)
135, 12wceq 1528 . . . . . . . . . 10 wff 𝑓 = (𝑥𝑑𝑦)
14 vz . . . . . . . . . . . . . 14 setvar 𝑧
1514cv 1527 . . . . . . . . . . . . 13 class 𝑧
16 vi . . . . . . . . . . . . . . 15 setvar 𝑖
1716cv 1527 . . . . . . . . . . . . . 14 class 𝑖
187, 9, 17co 7145 . . . . . . . . . . . . 13 class (𝑥𝑖𝑦)
1915, 18wcel 2105 . . . . . . . . . . . 12 wff 𝑧 ∈ (𝑥𝑖𝑦)
20 ve . . . . . . . . . . . . . 14 setvar 𝑒
2120cv 1527 . . . . . . . . . . . . 13 class 𝑒
227, 15, 11co 7145 . . . . . . . . . . . . 13 class (𝑥𝑑𝑧)
2321, 22wceq 1528 . . . . . . . . . . . 12 wff 𝑒 = (𝑥𝑑𝑧)
2419, 23wa 396 . . . . . . . . . . 11 wff (𝑧 ∈ (𝑥𝑖𝑦) ∧ 𝑒 = (𝑥𝑑𝑧))
25 vp . . . . . . . . . . . 12 setvar 𝑝
2625cv 1527 . . . . . . . . . . 11 class 𝑝
2724, 14, 26wrex 3136 . . . . . . . . . 10 wff 𝑧𝑝 (𝑧 ∈ (𝑥𝑖𝑦) ∧ 𝑒 = (𝑥𝑑𝑧))
2813, 27wa 396 . . . . . . . . 9 wff (𝑓 = (𝑥𝑑𝑦) ∧ ∃𝑧𝑝 (𝑧 ∈ (𝑥𝑖𝑦) ∧ 𝑒 = (𝑥𝑑𝑧)))
2928, 8, 26wrex 3136 . . . . . . . 8 wff 𝑦𝑝 (𝑓 = (𝑥𝑑𝑦) ∧ ∃𝑧𝑝 (𝑧 ∈ (𝑥𝑖𝑦) ∧ 𝑒 = (𝑥𝑑𝑧)))
3029, 6, 26wrex 3136 . . . . . . 7 wff 𝑥𝑝𝑦𝑝 (𝑓 = (𝑥𝑑𝑦) ∧ ∃𝑧𝑝 (𝑧 ∈ (𝑥𝑖𝑦) ∧ 𝑒 = (𝑥𝑑𝑧)))
312cv 1527 . . . . . . . 8 class 𝑔
32 citv 26149 . . . . . . . 8 class Itv
3331, 32cfv 6348 . . . . . . 7 class (Itv‘𝑔)
3430, 16, 33wsbc 3769 . . . . . 6 wff [(Itv‘𝑔) / 𝑖]𝑥𝑝𝑦𝑝 (𝑓 = (𝑥𝑑𝑦) ∧ ∃𝑧𝑝 (𝑧 ∈ (𝑥𝑖𝑦) ∧ 𝑒 = (𝑥𝑑𝑧)))
35 cds 16562 . . . . . . 7 class dist
3631, 35cfv 6348 . . . . . 6 class (dist‘𝑔)
3734, 10, 36wsbc 3769 . . . . 5 wff [(dist‘𝑔) / 𝑑][(Itv‘𝑔) / 𝑖]𝑥𝑝𝑦𝑝 (𝑓 = (𝑥𝑑𝑦) ∧ ∃𝑧𝑝 (𝑧 ∈ (𝑥𝑖𝑦) ∧ 𝑒 = (𝑥𝑑𝑧)))
38 cbs 16471 . . . . . 6 class Base
3931, 38cfv 6348 . . . . 5 class (Base‘𝑔)
4037, 25, 39wsbc 3769 . . . 4 wff [(Base‘𝑔) / 𝑝][(dist‘𝑔) / 𝑑][(Itv‘𝑔) / 𝑖]𝑥𝑝𝑦𝑝 (𝑓 = (𝑥𝑑𝑦) ∧ ∃𝑧𝑝 (𝑧 ∈ (𝑥𝑖𝑦) ∧ 𝑒 = (𝑥𝑑𝑧)))
4140, 20, 4copab 5119 . . 3 class {⟨𝑒, 𝑓⟩ ∣ [(Base‘𝑔) / 𝑝][(dist‘𝑔) / 𝑑][(Itv‘𝑔) / 𝑖]𝑥𝑝𝑦𝑝 (𝑓 = (𝑥𝑑𝑦) ∧ ∃𝑧𝑝 (𝑧 ∈ (𝑥𝑖𝑦) ∧ 𝑒 = (𝑥𝑑𝑧)))}
422, 3, 41cmpt 5137 . 2 class (𝑔 ∈ V ↦ {⟨𝑒, 𝑓⟩ ∣ [(Base‘𝑔) / 𝑝][(dist‘𝑔) / 𝑑][(Itv‘𝑔) / 𝑖]𝑥𝑝𝑦𝑝 (𝑓 = (𝑥𝑑𝑦) ∧ ∃𝑧𝑝 (𝑧 ∈ (𝑥𝑖𝑦) ∧ 𝑒 = (𝑥𝑑𝑧)))})
431, 42wceq 1528 1 wff ≤G = (𝑔 ∈ V ↦ {⟨𝑒, 𝑓⟩ ∣ [(Base‘𝑔) / 𝑝][(dist‘𝑔) / 𝑑][(Itv‘𝑔) / 𝑖]𝑥𝑝𝑦𝑝 (𝑓 = (𝑥𝑑𝑦) ∧ ∃𝑧𝑝 (𝑧 ∈ (𝑥𝑖𝑦) ∧ 𝑒 = (𝑥𝑑𝑧)))})
Colors of variables: wff setvar class
This definition is referenced by:  legval  26297
  Copyright terms: Public domain W3C validator