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 ‘ 𝑔 ) 𝑎 ) ) ) ) } ) )