Definition df-hlg 25496

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 = ( g e. _V |-> ( c e. ( Base ` g ) |-> { <. a , b >. | ( ( a e. ( Base ` g ) /\ b e. ( Base ` g ) ) /\ ( a =/= c /\ b =/= c /\ ( a e. ( c (Itv ` g ) b ) \/ b e. ( c (Itv ` g ) a ) ) ) ) } ) )

Distinct variable group:   a, b, c, g

Detailed syntax breakdown of Definition df-hlg

Step	Hyp	Ref	Expression
1		chlg 25495	. 2 class hlG
2		vg	. . 3 setvar g
3		cvv 3200	. . 3 class _V
4		vc	. . . 4 setvar c
5	2	cv 1482	. . . . 5 class g
6		cbs 15857	. . . . 5 class Base
7	5, 6	cfv 5888	. . . 4 class ( Base ` g )
8		va	. . . . . . . . 9 setvar a
9	8	cv 1482	. . . . . . . 8 class a
10	9, 7	wcel 1990	. . . . . . 7 wff a e. ( Base ` g )
11		vb	. . . . . . . . 9 setvar b
12	11	cv 1482	. . . . . . . 8 class b
13	12, 7	wcel 1990	. . . . . . 7 wff b e. ( Base ` g )
14	10, 13	wa 384	. . . . . 6 wff ( a e. ( Base ` g ) /\ b e. ( Base ` g ) )
15	4	cv 1482	. . . . . . . 8 class c
16	9, 15	wne 2794	. . . . . . 7 wff a =/= c
17	12, 15	wne 2794	. . . . . . 7 wff b =/= c
18		citv 25335	. . . . . . . . . . 11 class Itv
19	5, 18	cfv 5888	. . . . . . . . . 10 class (Itv ` g )
20	15, 12, 19	co 6650	. . . . . . . . 9 class ( c (Itv ` g ) b )
21	9, 20	wcel 1990	. . . . . . . 8 wff a e. ( c (Itv ` g ) b )
22	15, 9, 19	co 6650	. . . . . . . . 9 class ( c (Itv ` g ) a )
23	12, 22	wcel 1990	. . . . . . . 8 wff b e. ( c (Itv ` g ) a )
24	21, 23	wo 383	. . . . . . 7 wff ( a e. ( c (Itv ` g ) b ) \/ b e. ( c (Itv ` g ) a ) )
25	16, 17, 24	w3a 1037	. . . . . 6 wff ( a =/= c /\ b =/= c /\ ( a e. ( c (Itv ` g ) b ) \/ b e. ( c (Itv ` g ) a ) ) )
26	14, 25	wa 384	. . . . 5 wff ( ( a e. ( Base ` g ) /\ b e. ( Base ` g ) ) /\ ( a =/= c /\ b =/= c /\ ( a e. ( c (Itv ` g ) b ) \/ b e. ( c (Itv ` g ) a ) ) ) )
27	26, 8, 11	copab 4712	. . . 4 class { <. a , b >. | ( ( a e. ( Base ` g ) /\ b e. ( Base ` g ) ) /\ ( a =/= c /\ b =/= c /\ ( a e. ( c (Itv ` g ) b ) \/ b e. ( c (Itv ` g ) a ) ) ) ) }
28	4, 7, 27	cmpt 4729	. . 3 class ( c e. ( Base ` g ) |-> { <. a , b >. | ( ( a e. ( Base ` g ) /\ b e. ( Base ` g ) ) /\ ( a =/= c /\ b =/= c /\ ( a e. ( c (Itv ` g ) b ) \/ b e. ( c (Itv ` g ) a ) ) ) ) } )
29	2, 3, 28	cmpt 4729	. 2 class ( g e. _V |-> ( c e. ( Base ` g ) |-> { <. a , b >. | ( ( a e. ( Base ` g ) /\ b e. ( Base ` g ) ) /\ ( a =/= c /\ b =/= c /\ ( a e. ( c (Itv ` g ) b ) \/ b e. ( c (Itv ` g ) a ) ) ) ) } ) )
30	1, 29	wceq 1483	1 wff hlG = ( g e. _V |-> ( c e. ( Base ` g ) |-> { <. a , b >. | ( ( a e. ( Base ` g ) /\ b e. ( Base ` g ) ) /\ ( a =/= c /\ b =/= c /\ ( a e. ( c (Itv ` g ) b ) \/ b e. ( c (Itv ` g ) a ) ) ) ) } ) )

This definition is referenced by:  ishlg  25497