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\cap \mathrm{CRing}$$
	crhmsubc.j	$$⊢J=\left(r\in C,s\in C⟼r\mathrm{RingHom}s\right)$$
Assertion	crhmsubc	$$⊢U\in V\to J\in \mathrm{Subcat}\left(\mathrm{RingCat}\left(U\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		crhmsubc.c	$$⊢C=U\cap \mathrm{CRing}$$
2		crhmsubc.j	$$⊢J=\left(r\in C,s\in C⟼r\mathrm{RingHom}s\right)$$
3		crngring	$$⊢r\in \mathrm{CRing}\to r\in \mathrm{Ring}$$
4	3	rgen	$$⊢\forall r\in \mathrm{CRing}r\in \mathrm{Ring}$$
5	4 1 2	srhmsubc	$$⊢U\in V\to J\in \mathrm{Subcat}\left(\mathrm{RingCat}\left(U\right)\right)$$