Definition df-leg 26953

Description: Define the less-than relationship between geometric distance congruence classes. See legval 26954. (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

Step	Hyp	Ref	Expression
1		cleg 26952	. 2 class ≤G
2		vg	. . 3 setvar 𝑔
3		cvv 3433	. . 3 class V
4		vf	. . . . . . . . . . . 12 setvar 𝑓
5	4	cv 1538	. . . . . . . . . . 11 class 𝑓
6		vx	. . . . . . . . . . . . 13 setvar 𝑥
7	6	cv 1538	. . . . . . . . . . . 12 class 𝑥
8		vy	. . . . . . . . . . . . 13 setvar 𝑦
9	8	cv 1538	. . . . . . . . . . . 12 class 𝑦
10		vd	. . . . . . . . . . . . 13 setvar 𝑑
11	10	cv 1538	. . . . . . . . . . . 12 class 𝑑
12	7, 9, 11	co 7284	. . . . . . . . . . 11 class (𝑥𝑑𝑦)
13	5, 12	wceq 1539	. . . . . . . . . 10 wff 𝑓 = (𝑥𝑑𝑦)
14		vz	. . . . . . . . . . . . . 14 setvar 𝑧
15	14	cv 1538	. . . . . . . . . . . . 13 class 𝑧
16		vi	. . . . . . . . . . . . . . 15 setvar 𝑖
17	16	cv 1538	. . . . . . . . . . . . . 14 class 𝑖
18	7, 9, 17	co 7284	. . . . . . . . . . . . 13 class (𝑥𝑖𝑦)
19	15, 18	wcel 2107	. . . . . . . . . . . 12 wff 𝑧 ∈ (𝑥𝑖𝑦)
20		ve	. . . . . . . . . . . . . 14 setvar 𝑒
21	20	cv 1538	. . . . . . . . . . . . 13 class 𝑒
22	7, 15, 11	co 7284	. . . . . . . . . . . . 13 class (𝑥𝑑𝑧)
23	21, 22	wceq 1539	. . . . . . . . . . . 12 wff 𝑒 = (𝑥𝑑𝑧)
24	19, 23	wa 396	. . . . . . . . . . 11 wff (𝑧 ∈ (𝑥𝑖𝑦) ∧ 𝑒 = (𝑥𝑑𝑧))
25		vp	. . . . . . . . . . . 12 setvar 𝑝
26	25	cv 1538	. . . . . . . . . . 11 class 𝑝
27	24, 14, 26	wrex 3066	. . . . . . . . . 10 wff ∃𝑧 ∈ 𝑝 (𝑧 ∈ (𝑥𝑖𝑦) ∧ 𝑒 = (𝑥𝑑𝑧))
28	13, 27	wa 396	. . . . . . . . 9 wff (𝑓 = (𝑥𝑑𝑦) ∧ ∃𝑧 ∈ 𝑝 (𝑧 ∈ (𝑥𝑖𝑦) ∧ 𝑒 = (𝑥𝑑𝑧)))
29	28, 8, 26	wrex 3066	. . . . . . . 8 wff ∃𝑦 ∈ 𝑝 (𝑓 = (𝑥𝑑𝑦) ∧ ∃𝑧 ∈ 𝑝 (𝑧 ∈ (𝑥𝑖𝑦) ∧ 𝑒 = (𝑥𝑑𝑧)))
30	29, 6, 26	wrex 3066	. . . . . . 7 wff ∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 (𝑓 = (𝑥𝑑𝑦) ∧ ∃𝑧 ∈ 𝑝 (𝑧 ∈ (𝑥𝑖𝑦) ∧ 𝑒 = (𝑥𝑑𝑧)))
31	2	cv 1538	. . . . . . . 8 class 𝑔
32		citv 26803	. . . . . . . 8 class Itv
33	31, 32	cfv 6437	. . . . . . 7 class (Itv‘𝑔)
34	30, 16, 33	wsbc 3717	. . . . . 6 wff [(Itv‘𝑔) / 𝑖]∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 (𝑓 = (𝑥𝑑𝑦) ∧ ∃𝑧 ∈ 𝑝 (𝑧 ∈ (𝑥𝑖𝑦) ∧ 𝑒 = (𝑥𝑑𝑧)))
35		cds 16980	. . . . . . 7 class dist
36	31, 35	cfv 6437	. . . . . 6 class (dist‘𝑔)
37	34, 10, 36	wsbc 3717	. . . . 5 wff [(dist‘𝑔) / 𝑑][(Itv‘𝑔) / 𝑖]∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 (𝑓 = (𝑥𝑑𝑦) ∧ ∃𝑧 ∈ 𝑝 (𝑧 ∈ (𝑥𝑖𝑦) ∧ 𝑒 = (𝑥𝑑𝑧)))
38		cbs 16921	. . . . . 6 class Base
39	31, 38	cfv 6437	. . . . 5 class (Base‘𝑔)
40	37, 25, 39	wsbc 3717	. . . 4 wff [(Base‘𝑔) / 𝑝][(dist‘𝑔) / 𝑑][(Itv‘𝑔) / 𝑖]∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 (𝑓 = (𝑥𝑑𝑦) ∧ ∃𝑧 ∈ 𝑝 (𝑧 ∈ (𝑥𝑖𝑦) ∧ 𝑒 = (𝑥𝑑𝑧)))
41	40, 20, 4	copab 5137	. . 3 class {⟨𝑒, 𝑓⟩ ∣ [(Base‘𝑔) / 𝑝][(dist‘𝑔) / 𝑑][(Itv‘𝑔) / 𝑖]∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 (𝑓 = (𝑥𝑑𝑦) ∧ ∃𝑧 ∈ 𝑝 (𝑧 ∈ (𝑥𝑖𝑦) ∧ 𝑒 = (𝑥𝑑𝑧)))}
42	2, 3, 41	cmpt 5158	. 2 class (𝑔 ∈ V ↦ {⟨𝑒, 𝑓⟩ ∣ [(Base‘𝑔) / 𝑝][(dist‘𝑔) / 𝑑][(Itv‘𝑔) / 𝑖]∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 (𝑓 = (𝑥𝑑𝑦) ∧ ∃𝑧 ∈ 𝑝 (𝑧 ∈ (𝑥𝑖𝑦) ∧ 𝑒 = (𝑥𝑑𝑧)))})
43	1, 42	wceq 1539	1 wff ≤G = (𝑔 ∈ V ↦ {⟨𝑒, 𝑓⟩ ∣ [(Base‘𝑔) / 𝑝][(dist‘𝑔) / 𝑑][(Itv‘𝑔) / 𝑖]∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 (𝑓 = (𝑥𝑑𝑦) ∧ ∃𝑧 ∈ 𝑝 (𝑧 ∈ (𝑥𝑖𝑦) ∧ 𝑒 = (𝑥𝑑𝑧)))})

This definition is referenced by:  legval  26954