Metamath Proof Explorer


Theorem drngcat

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 )

Proof

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 )