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	|- G = ( 1st ` R )
	rngisoval.2	|- X = ran G
	rngisoval.3	|- J = ( 1st ` S )
	rngisoval.4	|- Y = ran J
Assertion	isrngoiso	|- ( ( R e. RingOps /\ S e. RingOps ) -> ( F e. ( R RingOpsIso S ) <-> ( F e. ( R RingOpsHom S ) /\ F : X -1-1-onto-> Y ) ) )

Proof

Step	Hyp	Ref	Expression
1		rngisoval.1	|- G = ( 1st ` R )
2		rngisoval.2	|- X = ran G
3		rngisoval.3	|- J = ( 1st ` S )
4		rngisoval.4	|- Y = ran J
5	1 2 3 4	rngoisoval	|- ( ( R e. RingOps /\ S e. RingOps ) -> ( R RingOpsIso S ) = { f e. ( R RingOpsHom S ) | f : X -1-1-onto-> Y } )
6	5	eleq2d	|- ( ( R e. RingOps /\ S e. RingOps ) -> ( F e. ( R RingOpsIso S ) <-> F e. { f e. ( R RingOpsHom S ) | f : X -1-1-onto-> Y } ) )
7		f1oeq1	|- ( f = F -> ( f : X -1-1-onto-> Y <-> F : X -1-1-onto-> Y ) )
8	7	elrab	|- ( F e. { f e. ( R RingOpsHom S ) | f : X -1-1-onto-> Y } <-> ( F e. ( R RingOpsHom S ) /\ F : X -1-1-onto-> Y ) )
9	6 8	bitrdi	|- ( ( R e. RingOps /\ S e. RingOps ) -> ( F e. ( R RingOpsIso S ) <-> ( F e. ( R RingOpsHom S ) /\ F : X -1-1-onto-> Y ) ) )