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

Metamath Proof Explorer

Theorem sringcat

Description: The restriction of the category of (unital) rings to the set of special ring homomorphisms is a category. (Contributed by AV, 19-Feb-2020)

	Ref	Expression
Hypotheses	srhmsubc.s	$⊢ \forall r \in S r \in Ring$
	srhmsubc.c	$⊢ C = U \cap S$
	srhmsubc.j	$⊢ J = (r \in C, s \in C ⟼ r RingHom s)$
Assertion	sringcat	$⊢ U \in V \to RingCat (U) ↾_{cat} J \in Cat$

Proof

Step	Hyp	Ref	Expression
1		srhmsubc.s	$⊢ \forall r \in S r \in Ring$
2		srhmsubc.c	$⊢ C = U \cap S$
3		srhmsubc.j	$⊢ J = (r \in C, s \in C ⟼ r RingHom s)$
4		eqid	$⊢ RingCat (U) ↾_{cat} J = RingCat (U) ↾_{cat} J$
5	1 2 3	srhmsubc	$⊢ U \in V \to J \in Subcat (RingCat (U))$
6	4 5	subccat	$⊢ U \in V \to RingCat (U) ↾_{cat} J \in Cat$