Metamath Proof Explorer

Definition df-hlg

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

Ref Expression
Assertion df-hlg ⊢hl𝒢=g∈V⟼c∈Baseg⟼ab|a∈Baseg∧b∈Baseg∧a≠c∧b≠c∧a∈cItv⁡gb∨b∈cItv⁡ga

Detailed syntax breakdown

Step Hyp Ref Expression
0 chlg classhl𝒢
1 vg setvarg
2 cvv classV
3 vc setvarc
4 cbs classBase
5 1 cv setvarg
6 5 4 cfv classBaseg
7 va setvara
8 vb setvarb
9 7 cv setvara
10 9 6 wcel wffa∈Baseg
11 8 cv setvarb
12 11 6 wcel wffb∈Baseg
13 10 12 wa wffa∈Baseg∧b∈Baseg
14 3 cv setvarc
15 9 14 wne wffa≠c
16 11 14 wne wffb≠c
17 citv classItv
18 5 17 cfv classItv⁡g
19 14 11 18 co classcItv⁡gb
20 9 19 wcel wffa∈cItv⁡gb
21 14 9 18 co classcItv⁡ga
22 11 21 wcel wffb∈cItv⁡ga
23 20 22 wo wffa∈cItv⁡gb∨b∈cItv⁡ga
24 15 16 23 w3a wffa≠c∧b≠c∧a∈cItv⁡gb∨b∈cItv⁡ga
25 13 24 wa wffa∈Baseg∧b∈Baseg∧a≠c∧b≠c∧a∈cItv⁡gb∨b∈cItv⁡ga
26 25 7 8 copab classab|a∈Baseg∧b∈Baseg∧a≠c∧b≠c∧a∈cItv⁡gb∨b∈cItv⁡ga
27 3 6 26 cmpt classc∈Baseg⟼ab|a∈Baseg∧b∈Baseg∧a≠c∧b≠c∧a∈cItv⁡gb∨b∈cItv⁡ga
28 1 2 27 cmpt classg∈V⟼c∈Baseg⟼ab|a∈Baseg∧b∈Baseg∧a≠c∧b≠c∧a∈cItv⁡gb∨b∈cItv⁡ga
29 0 28 wceq wffhl𝒢=g∈V⟼c∈Baseg⟼ab|a∈Baseg∧b∈Baseg∧a≠c∧b≠c∧a∈cItv⁡gb∨b∈cItv⁡ga