Step | Hyp | Ref
| Expression |
1 | | crngiso 36423 |
. 2
class
RngIso |
2 | | vr |
. . 3
setvar π |
3 | | vs |
. . 3
setvar π |
4 | | crngo 36356 |
. . 3
class
RingOps |
5 | 2 | cv 1541 |
. . . . . . 7
class π |
6 | | c1st 7920 |
. . . . . . 7
class
1st |
7 | 5, 6 | cfv 6497 |
. . . . . 6
class
(1st βπ) |
8 | 7 | crn 5635 |
. . . . 5
class ran
(1st βπ) |
9 | 3 | cv 1541 |
. . . . . . 7
class π |
10 | 9, 6 | cfv 6497 |
. . . . . 6
class
(1st βπ ) |
11 | 10 | crn 5635 |
. . . . 5
class ran
(1st βπ ) |
12 | | vf |
. . . . . 6
setvar π |
13 | 12 | cv 1541 |
. . . . 5
class π |
14 | 8, 11, 13 | wf1o 6496 |
. . . 4
wff π:ran (1st
βπ)β1-1-ontoβran (1st βπ ) |
15 | | crnghom 36422 |
. . . . 5
class
RngHom |
16 | 5, 9, 15 | co 7358 |
. . . 4
class (π RngHom π ) |
17 | 14, 12, 16 | crab 3408 |
. . 3
class {π β (π RngHom π ) β£ π:ran (1st βπ)β1-1-ontoβran
(1st βπ )} |
18 | 2, 3, 4, 4, 17 | cmpo 7360 |
. 2
class (π β RingOps, π β RingOps β¦ {π β (π RngHom π ) β£ π:ran (1st βπ)β1-1-ontoβran
(1st βπ )}) |
19 | 1, 18 | wceq 1542 |
1
wff RngIso =
(π β RingOps, π β RingOps β¦ {π β (π RngHom π ) β£ π:ran (1st βπ)β1-1-ontoβran
(1st βπ )}) |