df-rngoiso

Description: Define the function which gives the set of ring isomorphisms between two given rings. (Contributed by Jeff Madsen, 16-Jun-2011)

		Ref	Expression
	Assertion	df-rngoiso	$⊢ RngIso = (r \in RingOps, s \in RingOps ⟼ \{f \in (r RngHom s) \| f : ran 1^{st} (r) \underset{1-1 onto}{⟶} ran 1^{st} (s)\})$

Step	Hyp	Ref	Expression
0		crngiso	$class RngIso$
1		vr	$setvar r$
2		crngo	$class RingOps$
3		vs	$setvar s$
4		vf	$setvar f$
5	1	cv	$setvar r$
6		crnghom	$class RngHom$
7	3	cv	$setvar s$
8	5 7 6	co	$class (r RngHom s)$
9	4	cv	$setvar f$
10		c1st	$class 1^{st}$
11	5 10	cfv	$class 1^{st} (r)$
12	11	crn	$class ran 1^{st} (r)$
13	7 10	cfv	$class 1^{st} (s)$
14	13	crn	$class ran 1^{st} (s)$
15	12 14 9	wf1o	$wff f : ran 1^{st} (r) \underset{1-1 onto}{⟶} ran 1^{st} (s)$
16	15 4 8	crab	$class \{f \in (r RngHom s) \| f : ran 1^{st} (r) \underset{1-1 onto}{⟶} ran 1^{st} (s)\}$
17	1 3 2 2 16	cmpo	$class (r \in RingOps, s \in RingOps ⟼ \{f \in (r RngHom s) \| f : ran 1^{st} (r) \underset{1-1 onto}{⟶} ran 1^{st} (s)\})$
18	0 17	wceq	$wff RngIso = (r \in RingOps, s \in RingOps ⟼ \{f \in (r RngHom s) \| f : ran 1^{st} (r) \underset{1-1 onto}{⟶} ran 1^{st} (s)\})$

Metamath Proof Explorer