Definition df-rim

Description: Define the set of ring isomorphisms from r to s . (Contributed by Stefan O'Rear, 7-Mar-2015)

	Ref	Expression
Assertion	df-rim	⊢ RingIso = ( 𝑟 ∈ V , 𝑠 ∈ V ↦ { 𝑓 ∈ ( 𝑟 RingHom 𝑠 ) ∣ ◡ 𝑓 ∈ ( 𝑠 RingHom 𝑟 ) } )

Detailed syntax breakdown

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