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

Metamath Proof Explorer

Theorem rngimf1o

Description: An isomorphism of non-unital rings is a bijection. (Contributed by AV, 23-Feb-2020)

Ref Expression
Hypotheses rnghmf1o.b 
|- B = ( Base ` R )
rnghmf1o.c 
|- C = ( Base ` S )
Assertion rngimf1o 
|- ( F e. ( R RngIso S ) -> F : B -1-1-onto-> C )

Proof

Step Hyp Ref Expression
1 rnghmf1o.b 
 |-  B = ( Base ` R )
2 rnghmf1o.c 
 |-  C = ( Base ` S )
3 rngimrcl 
 |-  ( F e. ( R RngIso S ) -> ( R e. _V /\ S e. _V ) )
4 1 2 isrngim2 
 |-  ( ( R e. _V /\ S e. _V ) -> ( F e. ( R RngIso S ) <-> ( F e. ( R RngHom S ) /\ F : B -1-1-onto-> C ) ) )
5 simpr 
 |-  ( ( F e. ( R RngHom S ) /\ F : B -1-1-onto-> C ) -> F : B -1-1-onto-> C )
6 4 5 biimtrdi 
 |-  ( ( R e. _V /\ S e. _V ) -> ( F e. ( R RngIso S ) -> F : B -1-1-onto-> C ) )
7 3 6 mpcom 
 |-  ( F e. ( R RngIso S ) -> F : B -1-1-onto-> C )