Metamath Proof Explorer

Theorem isrngoiso

Description: Obsolete theorem, use isrim instead. The predicate "is a ring isomorphism between R and S ". (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	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))$

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	rngoisoval	$⊢ (R \in RingOps \land S \in RingOps) \to R RingOpsIso S = \{f \in (R RingOpsHom S) \| f : X \underset{1-1 onto}{⟶} Y\}$
6	5	eleq2d	$⊢ (R \in RingOps \land S \in RingOps) \to (F \in (R RingOpsIso S) \leftrightarrow F \in \{f \in (R RingOpsHom S) \| f : X \underset{1-1 onto}{⟶} Y\})$
7		f1oeq1	$⊢ f = F \to (f : X \underset{1-1 onto}{⟶} Y \leftrightarrow F : X \underset{1-1 onto}{⟶} Y)$
8	7	elrab	$⊢ F \in \{f \in (R RingOpsHom S) \| f : X \underset{1-1 onto}{⟶} Y\} \leftrightarrow (F \in (R RingOpsHom S) \land F : X \underset{1-1 onto}{⟶} Y)$
9	6 8	bitrdi	$⊢ (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))$