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 R RngIsom 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 R RngIsom S R V S V
4 1 2 isrngim R V S V F R RngIsom S F R RngHomo S F : B 1-1 onto C
5 simpr F R RngHomo S F : B 1-1 onto C F : B 1-1 onto C
6 4 5 syl6bi R V S V F R RngIsom S F : B 1-1 onto C
7 3 6 mpcom F R RngIsom S F : B 1-1 onto C