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

Step	Hyp	Ref	Expression
1		rnghmf1o.b	$⊢ B = {Base}_{R}$
2		rnghmf1o.c	$⊢ C = {Base}_{S}$
3		rngimrcl	$⊢ F \in (R RngIso S) \to (R \in V \land S \in V)$
4	1 2	isrngim2	$⊢ (R \in V \land S \in V) \to (F \in (R RngIso S) \leftrightarrow (F \in (R RngHom S) \land F : B \underset{1-1 onto}{⟶} C))$
5		simpr	$⊢ (F \in (R RngHom S) \land F : B \underset{1-1 onto}{⟶} C) \to F : B \underset{1-1 onto}{⟶} C$
6	4 5	syl6bi	$⊢ (R \in V \land S \in V) \to (F \in (R RngIso S) \to F : B \underset{1-1 onto}{⟶} C)$
7	3 6	mpcom	$⊢ F \in (R RngIso S) \to F : B \underset{1-1 onto}{⟶} C$

Metamath Proof Explorer