This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

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