Metamath Proof Explorer


Theorem crhmsubc

Description: According to df-subc , the subcategories ( SubcatC ) of a category C are subsets of the homomorphisms of C (see subcssc and subcss2 ). Therefore, the set of commutative ring homomorphisms (i.e. ring homomorphisms from a commutative ring to a commutative ring) is a "subcategory" of the category of (unital) rings. (Contributed by AV, 19-Feb-2020)

Ref Expression
Hypotheses crhmsubc.c
|- C = ( U i^i CRing )
crhmsubc.j
|- J = ( r e. C , s e. C |-> ( r RingHom s ) )
Assertion crhmsubc
|- ( U e. V -> J e. ( Subcat ` ( RingCat ` U ) ) )

Proof

Step Hyp Ref Expression
1 crhmsubc.c
 |-  C = ( U i^i CRing )
2 crhmsubc.j
 |-  J = ( r e. C , s e. C |-> ( r RingHom s ) )
3 crngring
 |-  ( r e. CRing -> r e. Ring )
4 3 rgen
 |-  A. r e. CRing r e. Ring
5 4 1 2 srhmsubc
 |-  ( U e. V -> J e. ( Subcat ` ( RingCat ` U ) ) )