Step | Hyp | Ref
| Expression |
1 | | coch 40206 |
. 2
class
ocH |
2 | | vk |
. . 3
setvar π |
3 | | cvv 3474 |
. . 3
class
V |
4 | | vw |
. . . 4
setvar π€ |
5 | 2 | cv 1540 |
. . . . 5
class π |
6 | | clh 38843 |
. . . . 5
class
LHyp |
7 | 5, 6 | cfv 6540 |
. . . 4
class
(LHypβπ) |
8 | | vx |
. . . . 5
setvar π₯ |
9 | 4 | cv 1540 |
. . . . . . . 8
class π€ |
10 | | cdvh 39937 |
. . . . . . . . 9
class
DVecH |
11 | 5, 10 | cfv 6540 |
. . . . . . . 8
class
(DVecHβπ) |
12 | 9, 11 | cfv 6540 |
. . . . . . 7
class
((DVecHβπ)βπ€) |
13 | | cbs 17140 |
. . . . . . 7
class
Base |
14 | 12, 13 | cfv 6540 |
. . . . . 6
class
(Baseβ((DVecHβπ)βπ€)) |
15 | 14 | cpw 4601 |
. . . . 5
class π«
(Baseβ((DVecHβπ)βπ€)) |
16 | 8 | cv 1540 |
. . . . . . . . . 10
class π₯ |
17 | | vy |
. . . . . . . . . . . 12
setvar π¦ |
18 | 17 | cv 1540 |
. . . . . . . . . . 11
class π¦ |
19 | | cdih 40087 |
. . . . . . . . . . . . 13
class
DIsoH |
20 | 5, 19 | cfv 6540 |
. . . . . . . . . . . 12
class
(DIsoHβπ) |
21 | 9, 20 | cfv 6540 |
. . . . . . . . . . 11
class
((DIsoHβπ)βπ€) |
22 | 18, 21 | cfv 6540 |
. . . . . . . . . 10
class
(((DIsoHβπ)βπ€)βπ¦) |
23 | 16, 22 | wss 3947 |
. . . . . . . . 9
wff π₯ β (((DIsoHβπ)βπ€)βπ¦) |
24 | 5, 13 | cfv 6540 |
. . . . . . . . 9
class
(Baseβπ) |
25 | 23, 17, 24 | crab 3432 |
. . . . . . . 8
class {π¦ β (Baseβπ) β£ π₯ β (((DIsoHβπ)βπ€)βπ¦)} |
26 | | cglb 18259 |
. . . . . . . . 9
class
glb |
27 | 5, 26 | cfv 6540 |
. . . . . . . 8
class
(glbβπ) |
28 | 25, 27 | cfv 6540 |
. . . . . . 7
class
((glbβπ)β{π¦ β (Baseβπ) β£ π₯ β (((DIsoHβπ)βπ€)βπ¦)}) |
29 | | coc 17201 |
. . . . . . . 8
class
oc |
30 | 5, 29 | cfv 6540 |
. . . . . . 7
class
(ocβπ) |
31 | 28, 30 | cfv 6540 |
. . . . . 6
class
((ocβπ)β((glbβπ)β{π¦ β (Baseβπ) β£ π₯ β (((DIsoHβπ)βπ€)βπ¦)})) |
32 | 31, 21 | cfv 6540 |
. . . . 5
class
(((DIsoHβπ)βπ€)β((ocβπ)β((glbβπ)β{π¦ β (Baseβπ) β£ π₯ β (((DIsoHβπ)βπ€)βπ¦)}))) |
33 | 8, 15, 32 | cmpt 5230 |
. . . 4
class (π₯ β π«
(Baseβ((DVecHβπ)βπ€)) β¦ (((DIsoHβπ)βπ€)β((ocβπ)β((glbβπ)β{π¦ β (Baseβπ) β£ π₯ β (((DIsoHβπ)βπ€)βπ¦)})))) |
34 | 4, 7, 33 | cmpt 5230 |
. . 3
class (π€ β (LHypβπ) β¦ (π₯ β π«
(Baseβ((DVecHβπ)βπ€)) β¦ (((DIsoHβπ)βπ€)β((ocβπ)β((glbβπ)β{π¦ β (Baseβπ) β£ π₯ β (((DIsoHβπ)βπ€)βπ¦)}))))) |
35 | 2, 3, 34 | cmpt 5230 |
. 2
class (π β V β¦ (π€ β (LHypβπ) β¦ (π₯ β π«
(Baseβ((DVecHβπ)βπ€)) β¦ (((DIsoHβπ)βπ€)β((ocβπ)β((glbβπ)β{π¦ β (Baseβπ) β£ π₯ β (((DIsoHβπ)βπ€)βπ¦)})))))) |
36 | 1, 35 | wceq 1541 |
1
wff ocH =
(π β V β¦ (π€ β (LHypβπ) β¦ (π₯ β π«
(Baseβ((DVecHβπ)βπ€)) β¦ (((DIsoHβπ)βπ€)β((ocβπ)β((glbβπ)β{π¦ β (Baseβπ) β£ π₯ β (((DIsoHβπ)βπ€)βπ¦)})))))) |