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

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 \in (R RingIso S) \to F : B \underset{1-1 onto}{⟶} C$

Step	Hyp	Ref	Expression
1		rhmf1o.b	$⊢ B = {Base}_{R}$
2		rhmf1o.c	$⊢ C = {Base}_{S}$
3	1 2	isrim	$⊢ F \in (R RingIso S) \leftrightarrow (F \in (R RingHom S) \land F : B \underset{1-1 onto}{⟶} C)$
4	3	simprbi	$⊢ F \in (R RingIso S) \to F : B \underset{1-1 onto}{⟶} C$