Metamath Proof Explorer

Theorem rimf1o

Description: An isomorphism of rings is a bijection. (Contributed by AV, 22-Oct-2019)

Ref Expression
Hypotheses rhmf1o.b ⊢ B = Base R
rhmf1o.c ⊢ C = Base S
Assertion rimf1o ⊢ F ∈ R RingIso S → F : B ⟶ 1-1 onto C

Proof

Step Hyp Ref Expression
1 rhmf1o.b ⊢ B = Base R
2 rhmf1o.c ⊢ C = Base S
3 rimrcl ⊢ F ∈ R RingIso S → R ∈ V ∧ S ∈ V
4 1 2 isrim ⊢ R ∈ V ∧ S ∈ V → F ∈ R RingIso S ↔ F ∈ R RingHom S ∧ F : B ⟶ 1-1 onto C
5 simpr ⊢ F ∈ R RingHom S ∧ F : B ⟶ 1-1 onto C → F : B ⟶ 1-1 onto C
6 4 5 syl6bi ⊢ R ∈ V ∧ S ∈ V → F ∈ R RingIso S → F : B ⟶ 1-1 onto C
7 3 6 mpcom ⊢ F ∈ R RingIso S → F : B ⟶ 1-1 onto C