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

Metamath Proof Explorer

Theorem drhmsubc

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 division ring homomorphisms is a "subcategory" of the category of (unital) 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	drhmsubc	$⊢ U \in V \to J \in Subcat (RingCat (U))$

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	srhmsubc	$⊢ U \in V \to J \in Subcat (RingCat (U))$