rngoiso1o

Description: A ring isomorphism is a bijection. (Contributed by Jeff Madsen, 16-Jun-2011)

	Ref	Expression
Hypotheses	rngisoval.1	$⊢ G = 1^{st} (R)$
	rngisoval.2	$⊢ X = ran G$
	rngisoval.3	$⊢ J = 1^{st} (S)$
	rngisoval.4	$⊢ Y = ran J$
Assertion	rngoiso1o	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RingOpsIso S)) \to F : X \underset{1-1 onto}{⟶} Y$

Step	Hyp	Ref	Expression
1		rngisoval.1	$⊢ G = 1^{st} (R)$
2		rngisoval.2	$⊢ X = ran G$
3		rngisoval.3	$⊢ J = 1^{st} (S)$
4		rngisoval.4	$⊢ Y = ran J$
5	1 2 3 4	isrngoiso	$⊢ (R \in RingOps \land S \in RingOps) \to (F \in (R RingOpsIso S) \leftrightarrow (F \in (R RingOpsHom S) \land F : X \underset{1-1 onto}{⟶} Y))$
6	5	simplbda	$⊢ ((R \in RingOps \land S \in RingOps) \land F \in (R RingOpsIso S)) \to F : X \underset{1-1 onto}{⟶} Y$
7	6	3impa	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RingOpsIso S)) \to F : X \underset{1-1 onto}{⟶} Y$

Metamath Proof Explorer