Description: The restriction of the category of (unital) rings to the set of division ring homomorphisms is a category, the "category of division rings". (Contributed by AV, 20-Feb-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | drhmsubc.c | |- C = ( U i^i DivRing ) |
|
drhmsubc.j | |- J = ( r e. C , s e. C |-> ( r RingHom s ) ) |
||
Assertion | drngcat | |- ( U e. V -> ( ( RingCat ` U ) |`cat J ) e. Cat ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | drhmsubc.c | |- C = ( U i^i DivRing ) |
|
2 | drhmsubc.j | |- J = ( r e. C , s e. C |-> ( r RingHom s ) ) |
|
3 | drngring | |- ( r e. DivRing -> r e. Ring ) |
|
4 | 3 | rgen | |- A. r e. DivRing r e. Ring |
5 | 4 1 2 | sringcat | |- ( U e. V -> ( ( RingCat ` U ) |`cat J ) e. Cat ) |