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 
|- 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 ) ) ) ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 chlg 
 |-  hlG
1 vg 
 |-  g
2 cvv 
 |-  _V
3 vc 
 |-  c
4 cbs 
 |-  Base
5 1 cv 
 |-  g
6 5 4 cfv 
 |-  ( Base ` g )
7 va 
 |-  a
8 vb 
 |-  b
9 7 cv 
 |-  a
10 9 6 wcel 
 |-  a e. ( Base ` g )
11 8 cv 
 |-  b
12 11 6 wcel 
 |-  b e. ( Base ` g )
13 10 12 wa 
 |-  ( a e. ( Base ` g ) /\ b e. ( Base ` g ) )
14 3 cv 
 |-  c
15 9 14 wne 
 |-  a =/= c
16 11 14 wne 
 |-  b =/= c
17 citv 
 |-  Itv
18 5 17 cfv 
 |-  ( Itv ` g )
19 14 11 18 co 
 |-  ( c ( Itv ` g ) b )
20 9 19 wcel 
 |-  a e. ( c ( Itv ` g ) b )
21 14 9 18 co 
 |-  ( c ( Itv ` g ) a )
22 11 21 wcel 
 |-  b e. ( c ( Itv ` g ) a )
23 20 22 wo 
 |-  ( a e. ( c ( Itv ` g ) b ) \/ b e. ( c ( Itv ` g ) a ) )
24 15 16 23 w3a 
 |-  ( a =/= c /\ b =/= c /\ ( a e. ( c ( Itv ` g ) b ) \/ b e. ( c ( Itv ` g ) a ) ) )
25 13 24 wa 
 |-  ( ( a e. ( Base ` g ) /\ b e. ( Base ` g ) ) /\ ( a =/= c /\ b =/= c /\ ( a e. ( c ( Itv ` g ) b ) \/ b e. ( c ( Itv ` g ) a ) ) ) )
26 25 7 8 copab 
 |-  { <. 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 ) ) ) ) }
27 3 6 26 cmpt 
 |-  ( 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 ) ) ) ) } )
28 1 2 27 cmpt 
 |-  ( 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 ) ) ) ) } ) )
29 0 28 wceq 
 |-  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 ) ) ) ) } ) )