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