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

Metamath Proof Explorer

Theorem drngcat

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

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

Proof

Step	Hyp	Ref	Expression
1		drhmsubc.c	$⊢ C = U \cap DivRing$
2		drhmsubc.j	$⊢ J = (r \in C, s \in C ⟼ r RingHom s)$
3		drngring	$⊢ r \in DivRing \to r \in Ring$
4	3	rgen	$⊢ \forall r \in DivRing r \in Ring$
5	4 1 2	sringcat	$⊢ U \in V \to RingCat (U) ↾_{cat} J \in Cat$