Theorem cringcat

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

	Ref	Expression
Hypotheses	crhmsubc.c	⊢ 𝐶 = ( 𝑈 ∩ CRing )
	crhmsubc.j	⊢ 𝐽 = ( 𝑟 ∈ 𝐶 , 𝑠 ∈ 𝐶 ↦ ( 𝑟 RingHom 𝑠 ) )
Assertion	cringcat	⊢ ( 𝑈 ∈ 𝑉 → ( ( RingCat ‘ 𝑈 ) ↾cat 𝐽 ) ∈ Cat )

Proof

Step	Hyp	Ref	Expression
1		crhmsubc.c	⊢ 𝐶 = ( 𝑈 ∩ CRing )
2		crhmsubc.j	⊢ 𝐽 = ( 𝑟 ∈ 𝐶 , 𝑠 ∈ 𝐶 ↦ ( 𝑟 RingHom 𝑠 ) )
3		eqid	⊢ ( ( RingCat ‘ 𝑈 ) ↾cat 𝐽 ) = ( ( RingCat ‘ 𝑈 ) ↾cat 𝐽 )
4	1 2	crhmsubc	⊢ ( 𝑈 ∈ 𝑉 → 𝐽 ∈ ( Subcat ‘ ( RingCat ‘ 𝑈 ) ) )
5	3 4	subccat	⊢ ( 𝑈 ∈ 𝑉 → ( ( RingCat ‘ 𝑈 ) ↾cat 𝐽 ) ∈ Cat )