Metamath Proof Explorer

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 ⊢ C = RingCat ⁡ U
Assertion ringccat ⊢ U ∈ V → C ∈ Cat

Proof

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