Definition 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	Could not format assertion : No typesetting found for |- RingOpsIso = ( r e. RingOps , s e. RingOps |-> { f e. ( r RingOpsHom s ) | f : ran ( 1st ` r ) -1-1-onto-> ran ( 1st ` s ) } ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crngoiso	Could not format RingOpsIso : No typesetting found for class RingOpsIso with typecode class
1		vr	$$setvarr$$
2		crngo	$$class\mathrm{RingOps}$$
3		vs	$$setvars$$
4		vf	$$setvarf$$
5	1	cv	$$setvarr$$
6		crngohom	Could not format RingOpsHom : No typesetting found for class RingOpsHom with typecode class
7	3	cv	$$setvars$$
8	5 7 6	co	Could not format ( r RingOpsHom s ) : No typesetting found for class ( r RingOpsHom s ) with typecode class
9	4	cv	$$setvarf$$
10		c1st	$$class{1}^{st}$$
11	5 10	cfv	$$class{1}^{st}\left(r\right)$$
12	11	crn	$$class\mathrm{ran}{1}^{st}\left(r\right)$$
13	7 10	cfv	$$class{1}^{st}\left(s\right)$$
14	13	crn	$$class\mathrm{ran}{1}^{st}\left(s\right)$$
15	12 14 9	wf1o	$$wfff:\mathrm{ran}{1}^{st}\left(r\right)\underset{1-1\; onto}{⟶}\mathrm{ran}{1}^{st}\left(s\right)$$
16	15 4 8	crab	Could not format { f e. ( r RingOpsHom s ) | f : ran ( 1st ` r ) -1-1-onto-> ran ( 1st ` s ) } : No typesetting found for class { f e. ( r RingOpsHom s ) | f : ran ( 1st ` r ) -1-1-onto-> ran ( 1st ` s ) } with typecode class
17	1 3 2 2 16	cmpo	Could not format ( r e. RingOps , s e. RingOps |-> { f e. ( r RingOpsHom s ) | f : ran ( 1st ` r ) -1-1-onto-> ran ( 1st ` s ) } ) : No typesetting found for class ( r e. RingOps , s e. RingOps |-> { f e. ( r RingOpsHom s ) | f : ran ( 1st ` r ) -1-1-onto-> ran ( 1st ` s ) } ) with typecode class
18	0 17	wceq	Could not format RingOpsIso = ( r e. RingOps , s e. RingOps |-> { f e. ( r RingOpsHom s ) | f : ran ( 1st ` r ) -1-1-onto-> ran ( 1st ` s ) } ) : No typesetting found for wff RingOpsIso = ( r e. RingOps , s e. RingOps |-> { f e. ( r RingOpsHom s ) | f : ran ( 1st ` r ) -1-1-onto-> ran ( 1st ` s ) } ) with typecode wff