Metamath Proof Explorer


Definition df-rngim

Description: Define the set of non-unital ring isomorphisms from r to s . (Contributed by AV, 20-Feb-2020)

Ref Expression
Assertion df-rngim RngIso = ( 𝑟 ∈ V , 𝑠 ∈ V ↦ { 𝑓 ∈ ( 𝑟 RngHom 𝑠 ) ∣ 𝑓 ∈ ( 𝑠 RngHom 𝑟 ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 crngim RngIso
1 vr 𝑟
2 cvv V
3 vs 𝑠
4 vf 𝑓
5 1 cv 𝑟
6 crnghm RngHom
7 3 cv 𝑠
8 5 7 6 co ( 𝑟 RngHom 𝑠 )
9 4 cv 𝑓
10 9 ccnv 𝑓
11 7 5 6 co ( 𝑠 RngHom 𝑟 )
12 10 11 wcel 𝑓 ∈ ( 𝑠 RngHom 𝑟 )
13 12 4 8 crab { 𝑓 ∈ ( 𝑟 RngHom 𝑠 ) ∣ 𝑓 ∈ ( 𝑠 RngHom 𝑟 ) }
14 1 3 2 2 13 cmpo ( 𝑟 ∈ V , 𝑠 ∈ V ↦ { 𝑓 ∈ ( 𝑟 RngHom 𝑠 ) ∣ 𝑓 ∈ ( 𝑠 RngHom 𝑟 ) } )
15 0 14 wceq RngIso = ( 𝑟 ∈ V , 𝑠 ∈ V ↦ { 𝑓 ∈ ( 𝑟 RngHom 𝑠 ) ∣ 𝑓 ∈ ( 𝑠 RngHom 𝑟 ) } )