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

Metamath Proof Explorer

Theorem cringcat

Description: The restriction of the category of (unital) rings to the set of commutative ring homomorphisms is a category, the "category of commutative 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	cringcat	$⊢ U \in V \to RingCat (U) ↾_{cat} J \in Cat$

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		eqid	$⊢ RingCat (U) ↾_{cat} J = RingCat (U) ↾_{cat} J$
4	1 2	crhmsubc	$⊢ U \in V \to J \in Subcat (RingCat (U))$
5	3 4	subccat	$⊢ U \in V \to RingCat (U) ↾_{cat} J \in Cat$