Metamath Proof Explorer


Definition df-rngoiso

Description: Define the function which gives the set of ring isomorphisms between two given rings. (Contributed by Jeff Madsen, 16-Jun-2011)

Ref Expression
Assertion df-rngoiso RngIso = ( 𝑟 ∈ RingOps , 𝑠 ∈ RingOps ↦ { 𝑓 ∈ ( 𝑟 RngHom 𝑠 ) ∣ 𝑓 : ran ( 1st𝑟 ) –1-1-onto→ ran ( 1st𝑠 ) } )

Detailed syntax breakdown

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𝑠 ) } )