Step | Hyp | Ref
| Expression |
1 | | crngcALTV 46409 |
. 2
class
RngCatALTV |
2 | | vu |
. . 3
setvar π’ |
3 | | cvv 3459 |
. . 3
class
V |
4 | | vb |
. . . 4
setvar π |
5 | 2 | cv 1540 |
. . . . 5
class π’ |
6 | | crng 46325 |
. . . . 5
class
Rng |
7 | 5, 6 | cin 3927 |
. . . 4
class (π’ β© Rng) |
8 | | cnx 17091 |
. . . . . . 7
class
ndx |
9 | | cbs 17109 |
. . . . . . 7
class
Base |
10 | 8, 9 | cfv 6516 |
. . . . . 6
class
(Baseβndx) |
11 | 4 | cv 1540 |
. . . . . 6
class π |
12 | 10, 11 | cop 4612 |
. . . . 5
class
β¨(Baseβndx), πβ© |
13 | | chom 17173 |
. . . . . . 7
class
Hom |
14 | 8, 13 | cfv 6516 |
. . . . . 6
class (Hom
βndx) |
15 | | vx |
. . . . . . 7
setvar π₯ |
16 | | vy |
. . . . . . 7
setvar π¦ |
17 | 15 | cv 1540 |
. . . . . . . 8
class π₯ |
18 | 16 | cv 1540 |
. . . . . . . 8
class π¦ |
19 | | crngh 46336 |
. . . . . . . 8
class
RngHomo |
20 | 17, 18, 19 | co 7377 |
. . . . . . 7
class (π₯ RngHomo π¦) |
21 | 15, 16, 11, 11, 20 | cmpo 7379 |
. . . . . 6
class (π₯ β π, π¦ β π β¦ (π₯ RngHomo π¦)) |
22 | 14, 21 | cop 4612 |
. . . . 5
class
β¨(Hom βndx), (π₯ β π, π¦ β π β¦ (π₯ RngHomo π¦))β© |
23 | | cco 17174 |
. . . . . . 7
class
comp |
24 | 8, 23 | cfv 6516 |
. . . . . 6
class
(compβndx) |
25 | | vv |
. . . . . . 7
setvar π£ |
26 | | vz |
. . . . . . 7
setvar π§ |
27 | 11, 11 | cxp 5651 |
. . . . . . 7
class (π Γ π) |
28 | | vg |
. . . . . . . 8
setvar π |
29 | | vf |
. . . . . . . 8
setvar π |
30 | 25 | cv 1540 |
. . . . . . . . . 10
class π£ |
31 | | c2nd 7940 |
. . . . . . . . . 10
class
2nd |
32 | 30, 31 | cfv 6516 |
. . . . . . . . 9
class
(2nd βπ£) |
33 | 26 | cv 1540 |
. . . . . . . . 9
class π§ |
34 | 32, 33, 19 | co 7377 |
. . . . . . . 8
class
((2nd βπ£) RngHomo π§) |
35 | | c1st 7939 |
. . . . . . . . . 10
class
1st |
36 | 30, 35 | cfv 6516 |
. . . . . . . . 9
class
(1st βπ£) |
37 | 36, 32, 19 | co 7377 |
. . . . . . . 8
class
((1st βπ£) RngHomo (2nd βπ£)) |
38 | 28 | cv 1540 |
. . . . . . . . 9
class π |
39 | 29 | cv 1540 |
. . . . . . . . 9
class π |
40 | 38, 39 | ccom 5657 |
. . . . . . . 8
class (π β π) |
41 | 28, 29, 34, 37, 40 | cmpo 7379 |
. . . . . . 7
class (π β ((2nd
βπ£) RngHomo π§), π β ((1st βπ£) RngHomo (2nd
βπ£)) β¦ (π β π)) |
42 | 25, 26, 27, 11, 41 | cmpo 7379 |
. . . . . 6
class (π£ β (π Γ π), π§ β π β¦ (π β ((2nd βπ£) RngHomo π§), π β ((1st βπ£) RngHomo (2nd
βπ£)) β¦ (π β π))) |
43 | 24, 42 | cop 4612 |
. . . . 5
class
β¨(compβndx), (π£ β (π Γ π), π§ β π β¦ (π β ((2nd βπ£) RngHomo π§), π β ((1st βπ£) RngHomo (2nd
βπ£)) β¦ (π β π)))β© |
44 | 12, 22, 43 | ctp 4610 |
. . . 4
class
{β¨(Baseβndx), πβ©, β¨(Hom βndx), (π₯ β π, π¦ β π β¦ (π₯ RngHomo π¦))β©, β¨(compβndx), (π£ β (π Γ π), π§ β π β¦ (π β ((2nd βπ£) RngHomo π§), π β ((1st βπ£) RngHomo (2nd
βπ£)) β¦ (π β π)))β©} |
45 | 4, 7, 44 | csb 3873 |
. . 3
class
β¦(π’
β© Rng) / πβ¦{β¨(Baseβndx), πβ©, β¨(Hom βndx),
(π₯ β π, π¦ β π β¦ (π₯ RngHomo π¦))β©, β¨(compβndx), (π£ β (π Γ π), π§ β π β¦ (π β ((2nd βπ£) RngHomo π§), π β ((1st βπ£) RngHomo (2nd
βπ£)) β¦ (π β π)))β©} |
46 | 2, 3, 45 | cmpt 5208 |
. 2
class (π’ β V β¦
β¦(π’ β©
Rng) / πβ¦{β¨(Baseβndx), πβ©, β¨(Hom βndx),
(π₯ β π, π¦ β π β¦ (π₯ RngHomo π¦))β©, β¨(compβndx), (π£ β (π Γ π), π§ β π β¦ (π β ((2nd βπ£) RngHomo π§), π β ((1st βπ£) RngHomo (2nd
βπ£)) β¦ (π β π)))β©}) |
47 | 1, 46 | wceq 1541 |
1
wff RngCatALTV
= (π’ β V β¦
β¦(π’ β©
Rng) / πβ¦{β¨(Baseβndx), πβ©, β¨(Hom βndx),
(π₯ β π, π¦ β π β¦ (π₯ RngHomo π¦))β©, β¨(compβndx), (π£ β (π Γ π), π§ β π β¦ (π β ((2nd βπ£) RngHomo π§), π β ((1st βπ£) RngHomo (2nd
βπ£)) β¦ (π β π)))β©}) |