Step |
Hyp |
Ref |
Expression |
0 |
|
crngiso |
⊢ RngIso |
1 |
|
vr |
⊢ 𝑟 |
2 |
|
crngo |
⊢ RingOps |
3 |
|
vs |
⊢ 𝑠 |
4 |
|
vf |
⊢ 𝑓 |
5 |
1
|
cv |
⊢ 𝑟 |
6 |
|
crnghom |
⊢ RngHom |
7 |
3
|
cv |
⊢ 𝑠 |
8 |
5 7 6
|
co |
⊢ ( 𝑟 RngHom 𝑠 ) |
9 |
4
|
cv |
⊢ 𝑓 |
10 |
|
c1st |
⊢ 1st |
11 |
5 10
|
cfv |
⊢ ( 1st ‘ 𝑟 ) |
12 |
11
|
crn |
⊢ ran ( 1st ‘ 𝑟 ) |
13 |
7 10
|
cfv |
⊢ ( 1st ‘ 𝑠 ) |
14 |
13
|
crn |
⊢ ran ( 1st ‘ 𝑠 ) |
15 |
12 14 9
|
wf1o |
⊢ 𝑓 : ran ( 1st ‘ 𝑟 ) –1-1-onto→ ran ( 1st ‘ 𝑠 ) |
16 |
15 4 8
|
crab |
⊢ { 𝑓 ∈ ( 𝑟 RngHom 𝑠 ) ∣ 𝑓 : ran ( 1st ‘ 𝑟 ) –1-1-onto→ ran ( 1st ‘ 𝑠 ) } |
17 |
1 3 2 2 16
|
cmpo |
⊢ ( 𝑟 ∈ RingOps , 𝑠 ∈ RingOps ↦ { 𝑓 ∈ ( 𝑟 RngHom 𝑠 ) ∣ 𝑓 : ran ( 1st ‘ 𝑟 ) –1-1-onto→ ran ( 1st ‘ 𝑠 ) } ) |
18 |
0 17
|
wceq |
⊢ RngIso = ( 𝑟 ∈ RingOps , 𝑠 ∈ RingOps ↦ { 𝑓 ∈ ( 𝑟 RngHom 𝑠 ) ∣ 𝑓 : ran ( 1st ‘ 𝑟 ) –1-1-onto→ ran ( 1st ‘ 𝑠 ) } ) |