Theorem drhmsubc

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 division ring homomorphisms is a "subcategory" of the category of (unital) 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	drhmsubc	|- ( U e. V -> J e. ( Subcat ` ( RingCat ` U ) ) )

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	srhmsubc	|- ( U e. V -> J e. ( Subcat ` ( RingCat ` U ) ) )