This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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