Definition df-hlg 27543

Description: Define the function producting the relation "belong to the same half-line". (Contributed by Thierry Arnoux, 15-Aug-2020.)

Assertion

Ref	Expression
df-hlg	⊢ hlG = (𝑔 ∈ V ↦ (𝑐 ∈ (Base‘𝑔) ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (Base‘𝑔) ∧ 𝑏 ∈ (Base‘𝑔)) ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐(Itv‘𝑔)𝑏) ∨ 𝑏 ∈ (𝑐(Itv‘𝑔)𝑎))))}))

Distinct variable group:   𝑎,𝑏,𝑐,𝑔

Detailed syntax breakdown of Definition df-hlg

Step	Hyp	Ref	Expression
1		chlg 27542	. 2 class hlG
2		vg	. . 3 setvar 𝑔
3		cvv 3445	. . 3 class V
4		vc	. . . 4 setvar 𝑐
5	2	cv 1540	. . . . 5 class 𝑔
6		cbs 17083	. . . . 5 class Base
7	5, 6	cfv 6496	. . . 4 class (Base‘𝑔)
8		va	. . . . . . . . 9 setvar 𝑎
9	8	cv 1540	. . . . . . . 8 class 𝑎
10	9, 7	wcel 2106	. . . . . . 7 wff 𝑎 ∈ (Base‘𝑔)
11		vb	. . . . . . . . 9 setvar 𝑏
12	11	cv 1540	. . . . . . . 8 class 𝑏
13	12, 7	wcel 2106	. . . . . . 7 wff 𝑏 ∈ (Base‘𝑔)
14	10, 13	wa 396	. . . . . 6 wff (𝑎 ∈ (Base‘𝑔) ∧ 𝑏 ∈ (Base‘𝑔))
15	4	cv 1540	. . . . . . . 8 class 𝑐
16	9, 15	wne 2943	. . . . . . 7 wff 𝑎 ≠ 𝑐
17	12, 15	wne 2943	. . . . . . 7 wff 𝑏 ≠ 𝑐
18		citv 27375	. . . . . . . . . . 11 class Itv
19	5, 18	cfv 6496	. . . . . . . . . 10 class (Itv‘𝑔)
20	15, 12, 19	co 7357	. . . . . . . . 9 class (𝑐(Itv‘𝑔)𝑏)
21	9, 20	wcel 2106	. . . . . . . 8 wff 𝑎 ∈ (𝑐(Itv‘𝑔)𝑏)
22	15, 9, 19	co 7357	. . . . . . . . 9 class (𝑐(Itv‘𝑔)𝑎)
23	12, 22	wcel 2106	. . . . . . . 8 wff 𝑏 ∈ (𝑐(Itv‘𝑔)𝑎)
24	21, 23	wo 845	. . . . . . 7 wff (𝑎 ∈ (𝑐(Itv‘𝑔)𝑏) ∨ 𝑏 ∈ (𝑐(Itv‘𝑔)𝑎))
25	16, 17, 24	w3a 1087	. . . . . 6 wff (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐(Itv‘𝑔)𝑏) ∨ 𝑏 ∈ (𝑐(Itv‘𝑔)𝑎)))
26	14, 25	wa 396	. . . . 5 wff ((𝑎 ∈ (Base‘𝑔) ∧ 𝑏 ∈ (Base‘𝑔)) ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐(Itv‘𝑔)𝑏) ∨ 𝑏 ∈ (𝑐(Itv‘𝑔)𝑎))))
27	26, 8, 11	copab 5167	. . . 4 class {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (Base‘𝑔) ∧ 𝑏 ∈ (Base‘𝑔)) ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐(Itv‘𝑔)𝑏) ∨ 𝑏 ∈ (𝑐(Itv‘𝑔)𝑎))))}
28	4, 7, 27	cmpt 5188	. . 3 class (𝑐 ∈ (Base‘𝑔) ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (Base‘𝑔) ∧ 𝑏 ∈ (Base‘𝑔)) ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐(Itv‘𝑔)𝑏) ∨ 𝑏 ∈ (𝑐(Itv‘𝑔)𝑎))))})
29	2, 3, 28	cmpt 5188	. 2 class (𝑔 ∈ V ↦ (𝑐 ∈ (Base‘𝑔) ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (Base‘𝑔) ∧ 𝑏 ∈ (Base‘𝑔)) ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐(Itv‘𝑔)𝑏) ∨ 𝑏 ∈ (𝑐(Itv‘𝑔)𝑎))))}))
30	1, 29	wceq 1541	1 wff hlG = (𝑔 ∈ V ↦ (𝑐 ∈ (Base‘𝑔) ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (Base‘𝑔) ∧ 𝑏 ∈ (Base‘𝑔)) ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐(Itv‘𝑔)𝑏) ∨ 𝑏 ∈ (𝑐(Itv‘𝑔)𝑎))))}))

This definition is referenced by:  ishlg  27544