Metamath Proof Explorer


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 classRingOps
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 class1st
11 5 10 cfv class1str
12 11 crn classran1str
13 7 10 cfv class1sts
14 13 crn classran1sts
15 12 14 9 wf1o wfff:ran1str1-1 ontoran1sts
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