Step |
Hyp |
Ref |
Expression |
0 |
|
crrh |
⊢ ℝHom |
1 |
|
vr |
⊢ 𝑟 |
2 |
|
cvv |
⊢ V |
3 |
|
ctg |
⊢ topGen |
4 |
|
cioo |
⊢ (,) |
5 |
4
|
crn |
⊢ ran (,) |
6 |
5 3
|
cfv |
⊢ ( topGen ‘ ran (,) ) |
7 |
|
ccnext |
⊢ CnExt |
8 |
|
ctopn |
⊢ TopOpen |
9 |
1
|
cv |
⊢ 𝑟 |
10 |
9 8
|
cfv |
⊢ ( TopOpen ‘ 𝑟 ) |
11 |
6 10 7
|
co |
⊢ ( ( topGen ‘ ran (,) ) CnExt ( TopOpen ‘ 𝑟 ) ) |
12 |
|
cqqh |
⊢ ℚHom |
13 |
9 12
|
cfv |
⊢ ( ℚHom ‘ 𝑟 ) |
14 |
13 11
|
cfv |
⊢ ( ( ( topGen ‘ ran (,) ) CnExt ( TopOpen ‘ 𝑟 ) ) ‘ ( ℚHom ‘ 𝑟 ) ) |
15 |
1 2 14
|
cmpt |
⊢ ( 𝑟 ∈ V ↦ ( ( ( topGen ‘ ran (,) ) CnExt ( TopOpen ‘ 𝑟 ) ) ‘ ( ℚHom ‘ 𝑟 ) ) ) |
16 |
0 15
|
wceq |
⊢ ℝHom = ( 𝑟 ∈ V ↦ ( ( ( topGen ‘ ran (,) ) CnExt ( TopOpen ‘ 𝑟 ) ) ‘ ( ℚHom ‘ 𝑟 ) ) ) |