Step | Hyp | Ref
| Expression |
1 | | cthl 21089 |
. 2
class
toHL |
2 | | vh |
. . 3
setvar ℎ |
3 | | cvv 3447 |
. . 3
class
V |
4 | 2 | cv 1541 |
. . . . . 6
class ℎ |
5 | | ccss 21088 |
. . . . . 6
class
ClSubSp |
6 | 4, 5 | cfv 6500 |
. . . . 5
class
(ClSubSp‘ℎ) |
7 | | cipo 18424 |
. . . . 5
class
toInc |
8 | 6, 7 | cfv 6500 |
. . . 4
class
(toInc‘(ClSubSp‘ℎ)) |
9 | | cnx 17073 |
. . . . . 6
class
ndx |
10 | | coc 17149 |
. . . . . 6
class
oc |
11 | 9, 10 | cfv 6500 |
. . . . 5
class
(oc‘ndx) |
12 | | cocv 21087 |
. . . . . 6
class
ocv |
13 | 4, 12 | cfv 6500 |
. . . . 5
class
(ocv‘ℎ) |
14 | 11, 13 | cop 4596 |
. . . 4
class
⟨(oc‘ndx), (ocv‘ℎ)⟩ |
15 | | csts 17043 |
. . . 4
class
sSet |
16 | 8, 14, 15 | co 7361 |
. . 3
class
((toInc‘(ClSubSp‘ℎ)) sSet ⟨(oc‘ndx), (ocv‘ℎ)⟩) |
17 | 2, 3, 16 | cmpt 5192 |
. 2
class (ℎ ∈ V ↦
((toInc‘(ClSubSp‘ℎ)) sSet ⟨(oc‘ndx), (ocv‘ℎ)⟩)) |
18 | 1, 17 | wceq 1542 |
1
wff toHL =
(ℎ ∈ V ↦
((toInc‘(ClSubSp‘ℎ)) sSet ⟨(oc‘ndx), (ocv‘ℎ)⟩)) |