Detailed syntax breakdown of Definition df-rngoiso
Step | Hyp | Ref
| Expression |
1 | | crngiso 36098 |
. 2
class
RngIso |
2 | | vr |
. . 3
setvar 𝑟 |
3 | | vs |
. . 3
setvar 𝑠 |
4 | | crngo 36031 |
. . 3
class
RingOps |
5 | 2 | cv 1540 |
. . . . . . 7
class 𝑟 |
6 | | c1st 7815 |
. . . . . . 7
class
1st |
7 | 5, 6 | cfv 6430 |
. . . . . 6
class
(1st ‘𝑟) |
8 | 7 | crn 5589 |
. . . . 5
class ran
(1st ‘𝑟) |
9 | 3 | cv 1540 |
. . . . . . 7
class 𝑠 |
10 | 9, 6 | cfv 6430 |
. . . . . 6
class
(1st ‘𝑠) |
11 | 10 | crn 5589 |
. . . . 5
class ran
(1st ‘𝑠) |
12 | | vf |
. . . . . 6
setvar 𝑓 |
13 | 12 | cv 1540 |
. . . . 5
class 𝑓 |
14 | 8, 11, 13 | wf1o 6429 |
. . . 4
wff 𝑓:ran (1st
‘𝑟)–1-1-onto→ran (1st ‘𝑠) |
15 | | crnghom 36097 |
. . . . 5
class
RngHom |
16 | 5, 9, 15 | co 7268 |
. . . 4
class (𝑟 RngHom 𝑠) |
17 | 14, 12, 16 | crab 3069 |
. . 3
class {𝑓 ∈ (𝑟 RngHom 𝑠) ∣ 𝑓:ran (1st ‘𝑟)–1-1-onto→ran
(1st ‘𝑠)} |
18 | 2, 3, 4, 4, 17 | cmpo 7270 |
. 2
class (𝑟 ∈ RingOps, 𝑠 ∈ RingOps ↦ {𝑓 ∈ (𝑟 RngHom 𝑠) ∣ 𝑓:ran (1st ‘𝑟)–1-1-onto→ran
(1st ‘𝑠)}) |
19 | 1, 18 | wceq 1541 |
1
wff RngIso =
(𝑟 ∈ RingOps, 𝑠 ∈ RingOps ↦ {𝑓 ∈ (𝑟 RngHom 𝑠) ∣ 𝑓:ran (1st ‘𝑟)–1-1-onto→ran
(1st ‘𝑠)}) |