isrngoiso

Description: The predicate "is a ring isomorphism between R and S ". (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	isrngoiso	$⊢ (R \in RingOps \land S \in RingOps) \to (F \in (R RngIso S) \leftrightarrow (F \in (R RngHom S) \land 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	rngoisoval	$⊢ (R \in RingOps \land S \in RingOps) \to R RngIso S = \{f \in (R RngHom S) \| f : X \underset{1-1 onto}{⟶} Y\}$
6	5	eleq2d	$⊢ (R \in RingOps \land S \in RingOps) \to (F \in (R RngIso S) \leftrightarrow F \in \{f \in (R RngHom 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 RngHom S) \| f : X \underset{1-1 onto}{⟶} Y\} \leftrightarrow (F \in (R RngHom S) \land F : X \underset{1-1 onto}{⟶} Y)$
9	6 8	bitrdi	$⊢ (R \in RingOps \land S \in RingOps) \to (F \in (R RngIso S) \leftrightarrow (F \in (R RngHom S) \land F : X \underset{1-1 onto}{⟶} Y))$

Metamath Proof Explorer