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 ( 1^st ‘ 𝑟 ) –1-1-onto→ ran ( 1^st ‘ 𝑠 ) } )

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	⊢ 1^st
11	5 10	cfv	⊢ ( 1^st ‘ 𝑟 )
12	11	crn	⊢ ran ( 1^st ‘ 𝑟 )
13	7 10	cfv	⊢ ( 1^st ‘ 𝑠 )
14	13	crn	⊢ ran ( 1^st ‘ 𝑠 )
15	12 14 9	wf1o	⊢ 𝑓 : ran ( 1^st ‘ 𝑟 ) –1-1-onto→ ran ( 1^st ‘ 𝑠 )
16	15 4 8	crab	⊢ { 𝑓 ∈ ( 𝑟 RngHom 𝑠 ) ∣ 𝑓 : ran ( 1^st ‘ 𝑟 ) –1-1-onto→ ran ( 1^st ‘ 𝑠 ) }
17	1 3 2 2 16	cmpo	⊢ ( 𝑟 ∈ RingOps , 𝑠 ∈ RingOps ↦ { 𝑓 ∈ ( 𝑟 RngHom 𝑠 ) ∣ 𝑓 : ran ( 1^st ‘ 𝑟 ) –1-1-onto→ ran ( 1^st ‘ 𝑠 ) } )
18	0 17	wceq	⊢ RngIso = ( 𝑟 ∈ RingOps , 𝑠 ∈ RingOps ↦ { 𝑓 ∈ ( 𝑟 RngHom 𝑠 ) ∣ 𝑓 : ran ( 1^st ‘ 𝑟 ) –1-1-onto→ ran ( 1^st ‘ 𝑠 ) } )

Metamath Proof Explorer