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