Theorem drngcatALTV

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) (New usage is discouraged.)

	Ref	Expression
Hypotheses	drhmsubcALTV.c	$$⊢C=U\cap \mathrm{DivRing}$$
	drhmsubcALTV.j	$$⊢J=\left(r\in C,s\in C⟼r\mathrm{RingHom}s\right)$$
Assertion	drngcatALTV	$$⊢U\in V\to \mathrm{RingCatALTV}\left(U\right){\upharpoonright }_{\mathrm{cat}}J\in \mathrm{Cat}$$

Proof

Step	Hyp	Ref	Expression
1		drhmsubcALTV.c	$$⊢C=U\cap \mathrm{DivRing}$$
2		drhmsubcALTV.j	$$⊢J=\left(r\in C,s\in C⟼r\mathrm{RingHom}s\right)$$
3		drngring	$$⊢r\in \mathrm{DivRing}\to r\in \mathrm{Ring}$$
4	3	rgen	$$⊢\forall r\in \mathrm{DivRing}r\in \mathrm{Ring}$$
5	4 1 2	sringcatALTV	$$⊢U\in V\to \mathrm{RingCatALTV}\left(U\right){\upharpoonright }_{\mathrm{cat}}J\in \mathrm{Cat}$$