Theorem isrngoiso

Description: The predicate "is a ring isomorphism between R and S ". (Contributed by Jeff Madsen, 16-Jun-2011)

	Ref	Expression
Hypotheses	rngisoval.1	⊢ 𝐺 = ( 1st ‘ 𝑅 )
	rngisoval.2	⊢ 𝑋 = ran 𝐺
	rngisoval.3	⊢ 𝐽 = ( 1st ‘ 𝑆 )
	rngisoval.4	⊢ 𝑌 = ran 𝐽
Assertion	isrngoiso	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) → ( 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ↔ ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rngisoval.1	⊢ 𝐺 = ( 1st ‘ 𝑅 )
2		rngisoval.2	⊢ 𝑋 = ran 𝐺
3		rngisoval.3	⊢ 𝐽 = ( 1st ‘ 𝑆 )
4		rngisoval.4	⊢ 𝑌 = ran 𝐽
5	1 2 3 4	rngoisoval	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) → ( 𝑅 RngIso 𝑆 ) = { 𝑓 ∈ ( 𝑅 RngHom 𝑆 ) ∣ 𝑓 : 𝑋 –1-1-onto→ 𝑌 } )
6	5	eleq2d	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) → ( 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ↔ 𝐹 ∈ { 𝑓 ∈ ( 𝑅 RngHom 𝑆 ) ∣ 𝑓 : 𝑋 –1-1-onto→ 𝑌 } ) )
7		f1oeq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 : 𝑋 –1-1-onto→ 𝑌 ↔ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) )
8	7	elrab	⊢ ( 𝐹 ∈ { 𝑓 ∈ ( 𝑅 RngHom 𝑆 ) ∣ 𝑓 : 𝑋 –1-1-onto→ 𝑌 } ↔ ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) )
9	6 8	bitrdi	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) → ( 𝐹 ∈ ( 𝑅 RngIso 𝑆 ) ↔ ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ) )