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 i^i DivRing )
	drhmsubcALTV.j	|- J = ( r e. C , s e. C |-> ( r RingHom s ) )
Assertion	drngcatALTV	|- ( U e. V -> ( ( RingCatALTV ` U ) |`cat J ) e. Cat )

Proof

Step	Hyp	Ref	Expression
1		drhmsubcALTV.c	|- C = ( U i^i DivRing )
2		drhmsubcALTV.j	|- J = ( r e. C , s e. C |-> ( r RingHom s ) )
3		drngring	|- ( r e. DivRing -> r e. Ring )
4	3	rgen	|- A. r e. DivRing r e. Ring
5	4 1 2	sringcatALTV	|- ( U e. V -> ( ( RingCatALTV ` U ) |`cat J ) e. Cat )