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 setvar r
2 crngo class RingOps
3 vs setvar s
4 vf setvar f
5 1 cv setvar r
6 crngohom Could not format RingOpsHom : No typesetting found for class RingOpsHom with typecode class
7 3 cv setvar s
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 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 1-1 onto ran 1 st s
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