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 ∈ Base g ⟼ a b | a ∈ Base g ∧ b ∈ Base g ∧ a ≠ c ∧ b ≠ c ∧ a ∈ c Itv ⁡ g b ∨ b ∈ c Itv ⁡ g a

Detailed syntax breakdown

Step Hyp Ref Expression
0 chlg class hl 𝒢
1 vg setvar g
2 cvv class V
3 vc setvar c
4 cbs class Base
5 1 cv setvar g
6 5 4 cfv class Base g
7 va setvar a
8 vb setvar b
9 7 cv setvar a
10 9 6 wcel wff a ∈ Base g
11 8 cv setvar b
12 11 6 wcel wff b ∈ Base g
13 10 12 wa wff a ∈ Base g ∧ b ∈ Base g
14 3 cv setvar c
15 9 14 wne wff a ≠ c
16 11 14 wne wff b ≠ c
17 citv class Itv
18 5 17 cfv class Itv ⁡ g
19 14 11 18 co class c Itv ⁡ g b
20 9 19 wcel wff a ∈ c Itv ⁡ g b
21 14 9 18 co class c Itv ⁡ g a
22 11 21 wcel wff b ∈ c Itv ⁡ g a
23 20 22 wo wff a ∈ c Itv ⁡ g b ∨ b ∈ c Itv ⁡ g a
24 15 16 23 w3a wff a ≠ c ∧ b ≠ c ∧ a ∈ c Itv ⁡ g b ∨ b ∈ c Itv ⁡ g a
25 13 24 wa wff a ∈ Base g ∧ b ∈ Base g ∧ a ≠ c ∧ b ≠ c ∧ a ∈ c Itv ⁡ g b ∨ b ∈ c Itv ⁡ g a
26 25 7 8 copab class a b | a ∈ Base g ∧ b ∈ Base g ∧ a ≠ c ∧ b ≠ c ∧ a ∈ c Itv ⁡ g b ∨ b ∈ c Itv ⁡ g a
27 3 6 26 cmpt class c ∈ Base g ⟼ a b | a ∈ Base g ∧ b ∈ Base g ∧ a ≠ c ∧ b ≠ c ∧ a ∈ c Itv ⁡ g b ∨ b ∈ c Itv ⁡ g a
28 1 2 27 cmpt class g ∈ V ⟼ c ∈ Base g ⟼ a b | a ∈ Base g ∧ b ∈ Base g ∧ a ≠ c ∧ b ≠ c ∧ a ∈ c Itv ⁡ g b ∨ b ∈ c Itv ⁡ g a
29 0 28 wceq wff hl 𝒢 = g ∈ V ⟼ c ∈ Base g ⟼ a b | a ∈ Base g ∧ b ∈ Base g ∧ a ≠ c ∧ b ≠ c ∧ a ∈ c Itv ⁡ g b ∨ b ∈ c Itv ⁡ g a