Step | Hyp | Ref
| Expression |
1 | | cqqh 32952 |
. 2
class
βHom |
2 | | vr |
. . 3
setvar π |
3 | | cvv 3475 |
. . 3
class
V |
4 | | vx |
. . . . 5
setvar π₯ |
5 | | vy |
. . . . 5
setvar π¦ |
6 | | cz 12558 |
. . . . 5
class
β€ |
7 | 2 | cv 1541 |
. . . . . . . 8
class π |
8 | | czrh 21049 |
. . . . . . . 8
class
β€RHom |
9 | 7, 8 | cfv 6544 |
. . . . . . 7
class
(β€RHomβπ) |
10 | 9 | ccnv 5676 |
. . . . . 6
class β‘(β€RHomβπ) |
11 | | cui 20169 |
. . . . . . 7
class
Unit |
12 | 7, 11 | cfv 6544 |
. . . . . 6
class
(Unitβπ) |
13 | 10, 12 | cima 5680 |
. . . . 5
class (β‘(β€RHomβπ) β (Unitβπ)) |
14 | 4 | cv 1541 |
. . . . . . 7
class π₯ |
15 | 5 | cv 1541 |
. . . . . . 7
class π¦ |
16 | | cdiv 11871 |
. . . . . . 7
class
/ |
17 | 14, 15, 16 | co 7409 |
. . . . . 6
class (π₯ / π¦) |
18 | 14, 9 | cfv 6544 |
. . . . . . 7
class
((β€RHomβπ)βπ₯) |
19 | 15, 9 | cfv 6544 |
. . . . . . 7
class
((β€RHomβπ)βπ¦) |
20 | | cdvr 20214 |
. . . . . . . 8
class
/r |
21 | 7, 20 | cfv 6544 |
. . . . . . 7
class
(/rβπ) |
22 | 18, 19, 21 | co 7409 |
. . . . . 6
class
(((β€RHomβπ)βπ₯)(/rβπ)((β€RHomβπ)βπ¦)) |
23 | 17, 22 | cop 4635 |
. . . . 5
class
β¨(π₯ / π¦), (((β€RHomβπ)βπ₯)(/rβπ)((β€RHomβπ)βπ¦))β© |
24 | 4, 5, 6, 13, 23 | cmpo 7411 |
. . . 4
class (π₯ β β€, π¦ β (β‘(β€RHomβπ) β (Unitβπ)) β¦ β¨(π₯ / π¦), (((β€RHomβπ)βπ₯)(/rβπ)((β€RHomβπ)βπ¦))β©) |
25 | 24 | crn 5678 |
. . 3
class ran
(π₯ β β€, π¦ β (β‘(β€RHomβπ) β (Unitβπ)) β¦ β¨(π₯ / π¦), (((β€RHomβπ)βπ₯)(/rβπ)((β€RHomβπ)βπ¦))β©) |
26 | 2, 3, 25 | cmpt 5232 |
. 2
class (π β V β¦ ran (π₯ β β€, π¦ β (β‘(β€RHomβπ) β (Unitβπ)) β¦ β¨(π₯ / π¦), (((β€RHomβπ)βπ₯)(/rβπ)((β€RHomβπ)βπ¦))β©)) |
27 | 1, 26 | wceq 1542 |
1
wff βHom
= (π β V β¦ ran
(π₯ β β€, π¦ β (β‘(β€RHomβπ) β (Unitβπ)) β¦ β¨(π₯ / π¦), (((β€RHomβπ)βπ₯)(/rβπ)((β€RHomβπ)βπ¦))β©)) |