Metamath Proof Explorer

Theorem rngoiso1o

Description: Obsolete theorem, use rimf1o instead. A ring isomorphism is a bijection. (Contributed by Jeff Madsen, 16-Jun-2011) (Proof modification is discouraged.) (New usage is discouraged.)

		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$

Proof

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$