Theorem ringccat

Description: The category of unital rings is a category. (Contributed by AV, 14-Feb-2020) (Revised by AV, 9-Mar-2020)

	Ref	Expression
Hypothesis	ringccat.c	⊢ 𝐶 = ( RingCat ‘ 𝑈 )
Assertion	ringccat	⊢ ( 𝑈 ∈ 𝑉 → 𝐶 ∈ Cat )

Proof

Step	Hyp	Ref	Expression
1		ringccat.c	⊢ 𝐶 = ( RingCat ‘ 𝑈 )
2		id	⊢ ( 𝑈 ∈ 𝑉 → 𝑈 ∈ 𝑉 )
3		eqidd	⊢ ( 𝑈 ∈ 𝑉 → ( 𝑈 ∩ Ring ) = ( 𝑈 ∩ Ring ) )
4		eqidd	⊢ ( 𝑈 ∈ 𝑉 → ( RingHom ↾ ( ( 𝑈 ∩ Ring ) × ( 𝑈 ∩ Ring ) ) ) = ( RingHom ↾ ( ( 𝑈 ∩ Ring ) × ( 𝑈 ∩ Ring ) ) ) )
5	1 2 3 4	ringcval	⊢ ( 𝑈 ∈ 𝑉 → 𝐶 = ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( RingHom ↾ ( ( 𝑈 ∩ Ring ) × ( 𝑈 ∩ Ring ) ) ) ) )
6		eqid	⊢ ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( RingHom ↾ ( ( 𝑈 ∩ Ring ) × ( 𝑈 ∩ Ring ) ) ) ) = ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( RingHom ↾ ( ( 𝑈 ∩ Ring ) × ( 𝑈 ∩ Ring ) ) ) )
7		eqid	⊢ ( ExtStrCat ‘ 𝑈 ) = ( ExtStrCat ‘ 𝑈 )
8		eqidd	⊢ ( 𝑈 ∈ 𝑉 → ( Ring ∩ 𝑈 ) = ( Ring ∩ 𝑈 ) )
9		incom	⊢ ( 𝑈 ∩ Ring ) = ( Ring ∩ 𝑈 )
10	9	a1i	⊢ ( 𝑈 ∈ 𝑉 → ( 𝑈 ∩ Ring ) = ( Ring ∩ 𝑈 ) )
11	10	sqxpeqd	⊢ ( 𝑈 ∈ 𝑉 → ( ( 𝑈 ∩ Ring ) × ( 𝑈 ∩ Ring ) ) = ( ( Ring ∩ 𝑈 ) × ( Ring ∩ 𝑈 ) ) )
12	11	reseq2d	⊢ ( 𝑈 ∈ 𝑉 → ( RingHom ↾ ( ( 𝑈 ∩ Ring ) × ( 𝑈 ∩ Ring ) ) ) = ( RingHom ↾ ( ( Ring ∩ 𝑈 ) × ( Ring ∩ 𝑈 ) ) ) )
13	7 2 8 12	rhmsubcsetc	⊢ ( 𝑈 ∈ 𝑉 → ( RingHom ↾ ( ( 𝑈 ∩ Ring ) × ( 𝑈 ∩ Ring ) ) ) ∈ ( Subcat ‘ ( ExtStrCat ‘ 𝑈 ) ) )
14	6 13	subccat	⊢ ( 𝑈 ∈ 𝑉 → ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( RingHom ↾ ( ( 𝑈 ∩ Ring ) × ( 𝑈 ∩ Ring ) ) ) ) ∈ Cat )
15	5 14	eqeltrd	⊢ ( 𝑈 ∈ 𝑉 → 𝐶 ∈ Cat )