Metamath Proof Explorer


Theorem sringcatALTV

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

Ref Expression
Hypotheses srhmsubcALTV.s 𝑟𝑆 𝑟 ∈ Ring
srhmsubcALTV.c 𝐶 = ( 𝑈𝑆 )
srhmsubcALTV.j 𝐽 = ( 𝑟𝐶 , 𝑠𝐶 ↦ ( 𝑟 RingHom 𝑠 ) )
Assertion sringcatALTV ( 𝑈𝑉 → ( ( RingCatALTV ‘ 𝑈 ) ↾cat 𝐽 ) ∈ Cat )

Proof

Step Hyp Ref Expression
1 srhmsubcALTV.s 𝑟𝑆 𝑟 ∈ Ring
2 srhmsubcALTV.c 𝐶 = ( 𝑈𝑆 )
3 srhmsubcALTV.j 𝐽 = ( 𝑟𝐶 , 𝑠𝐶 ↦ ( 𝑟 RingHom 𝑠 ) )
4 eqid ( ( RingCatALTV ‘ 𝑈 ) ↾cat 𝐽 ) = ( ( RingCatALTV ‘ 𝑈 ) ↾cat 𝐽 )
5 1 2 3 srhmsubcALTV ( 𝑈𝑉𝐽 ∈ ( Subcat ‘ ( RingCatALTV ‘ 𝑈 ) ) )
6 4 5 subccat ( 𝑈𝑉 → ( ( RingCatALTV ‘ 𝑈 ) ↾cat 𝐽 ) ∈ Cat )