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 = ( 𝑔 ∈ V ↦ ( 𝑐 ∈ ( Base ‘ 𝑔 ) ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( Base ‘ 𝑔 ) ∧ 𝑏 ∈ ( Base ‘ 𝑔 ) ) ∧ ( 𝑎𝑐𝑏𝑐 ∧ ( 𝑎 ∈ ( 𝑐 ( Itv ‘ 𝑔 ) 𝑏 ) ∨ 𝑏 ∈ ( 𝑐 ( Itv ‘ 𝑔 ) 𝑎 ) ) ) ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 chlg hlG
1 vg 𝑔
2 cvv V
3 vc 𝑐
4 cbs Base
5 1 cv 𝑔
6 5 4 cfv ( Base ‘ 𝑔 )
7 va 𝑎
8 vb 𝑏
9 7 cv 𝑎
10 9 6 wcel 𝑎 ∈ ( Base ‘ 𝑔 )
11 8 cv 𝑏
12 11 6 wcel 𝑏 ∈ ( Base ‘ 𝑔 )
13 10 12 wa ( 𝑎 ∈ ( Base ‘ 𝑔 ) ∧ 𝑏 ∈ ( Base ‘ 𝑔 ) )
14 3 cv 𝑐
15 9 14 wne 𝑎𝑐
16 11 14 wne 𝑏𝑐
17 citv Itv
18 5 17 cfv ( Itv ‘ 𝑔 )
19 14 11 18 co ( 𝑐 ( Itv ‘ 𝑔 ) 𝑏 )
20 9 19 wcel 𝑎 ∈ ( 𝑐 ( Itv ‘ 𝑔 ) 𝑏 )
21 14 9 18 co ( 𝑐 ( Itv ‘ 𝑔 ) 𝑎 )
22 11 21 wcel 𝑏 ∈ ( 𝑐 ( Itv ‘ 𝑔 ) 𝑎 )
23 20 22 wo ( 𝑎 ∈ ( 𝑐 ( Itv ‘ 𝑔 ) 𝑏 ) ∨ 𝑏 ∈ ( 𝑐 ( Itv ‘ 𝑔 ) 𝑎 ) )
24 15 16 23 w3a ( 𝑎𝑐𝑏𝑐 ∧ ( 𝑎 ∈ ( 𝑐 ( Itv ‘ 𝑔 ) 𝑏 ) ∨ 𝑏 ∈ ( 𝑐 ( Itv ‘ 𝑔 ) 𝑎 ) ) )
25 13 24 wa ( ( 𝑎 ∈ ( Base ‘ 𝑔 ) ∧ 𝑏 ∈ ( Base ‘ 𝑔 ) ) ∧ ( 𝑎𝑐𝑏𝑐 ∧ ( 𝑎 ∈ ( 𝑐 ( Itv ‘ 𝑔 ) 𝑏 ) ∨ 𝑏 ∈ ( 𝑐 ( Itv ‘ 𝑔 ) 𝑎 ) ) ) )
26 25 7 8 copab { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( Base ‘ 𝑔 ) ∧ 𝑏 ∈ ( Base ‘ 𝑔 ) ) ∧ ( 𝑎𝑐𝑏𝑐 ∧ ( 𝑎 ∈ ( 𝑐 ( Itv ‘ 𝑔 ) 𝑏 ) ∨ 𝑏 ∈ ( 𝑐 ( Itv ‘ 𝑔 ) 𝑎 ) ) ) ) }
27 3 6 26 cmpt ( 𝑐 ∈ ( Base ‘ 𝑔 ) ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( Base ‘ 𝑔 ) ∧ 𝑏 ∈ ( Base ‘ 𝑔 ) ) ∧ ( 𝑎𝑐𝑏𝑐 ∧ ( 𝑎 ∈ ( 𝑐 ( Itv ‘ 𝑔 ) 𝑏 ) ∨ 𝑏 ∈ ( 𝑐 ( Itv ‘ 𝑔 ) 𝑎 ) ) ) ) } )
28 1 2 27 cmpt ( 𝑔 ∈ V ↦ ( 𝑐 ∈ ( Base ‘ 𝑔 ) ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( Base ‘ 𝑔 ) ∧ 𝑏 ∈ ( Base ‘ 𝑔 ) ) ∧ ( 𝑎𝑐𝑏𝑐 ∧ ( 𝑎 ∈ ( 𝑐 ( Itv ‘ 𝑔 ) 𝑏 ) ∨ 𝑏 ∈ ( 𝑐 ( Itv ‘ 𝑔 ) 𝑎 ) ) ) ) } ) )
29 0 28 wceq hlG = ( 𝑔 ∈ V ↦ ( 𝑐 ∈ ( Base ‘ 𝑔 ) ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( Base ‘ 𝑔 ) ∧ 𝑏 ∈ ( Base ‘ 𝑔 ) ) ∧ ( 𝑎𝑐𝑏𝑐 ∧ ( 𝑎 ∈ ( 𝑐 ( Itv ‘ 𝑔 ) 𝑏 ) ∨ 𝑏 ∈ ( 𝑐 ( Itv ‘ 𝑔 ) 𝑎 ) ) ) ) } ) )