Metamath Proof Explorer

Theorem rngccat

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

Ref Expression
Hypothesis rngccat.c ⊢ C = RngCat ⁡ U
Assertion rngccat ⊢ U ∈ V → C ∈ Cat

Proof

Step Hyp Ref Expression
1 rngccat.c ⊢ C = RngCat ⁡ U
2 id ⊢ U ∈ V → U ∈ V
3 eqidd ⊢ U ∈ V → U ∩ Rng = U ∩ Rng
4 eqidd ⊢ U ∈ V → RngHomo ↾ U ∩ Rng × U ∩ Rng = RngHomo ↾ U ∩ Rng × U ∩ Rng
5 1 2 3 4 rngcval ⊢ U ∈ V → C = ExtStrCat ⁡ U ↾ cat RngHomo ↾ U ∩ Rng × U ∩ Rng
6 eqid ⊢ ExtStrCat ⁡ U ↾ cat RngHomo ↾ U ∩ Rng × U ∩ Rng = ExtStrCat ⁡ U ↾ cat RngHomo ↾ U ∩ Rng × U ∩ Rng
7 eqid ⊢ ExtStrCat ⁡ U = ExtStrCat ⁡ U
8 eqidd ⊢ U ∈ V → Rng ∩ U = Rng ∩ U
9 incom ⊢ U ∩ Rng = Rng ∩ U
10 9 a1i ⊢ U ∈ V → U ∩ Rng = Rng ∩ U
11 10 sqxpeqd ⊢ U ∈ V → U ∩ Rng × U ∩ Rng = Rng ∩ U × Rng ∩ U
12 11 reseq2d ⊢ U ∈ V → RngHomo ↾ U ∩ Rng × U ∩ Rng = RngHomo ↾ Rng ∩ U × Rng ∩ U
13 7 2 8 12 rnghmsubcsetc ⊢ U ∈ V → RngHomo ↾ U ∩ Rng × U ∩ Rng ∈ Subcat ⁡ ExtStrCat ⁡ U
14 6 13 subccat ⊢ U ∈ V → ExtStrCat ⁡ U ↾ cat RngHomo ↾ U ∩ Rng × U ∩ Rng ∈ Cat
15 5 14 eqeltrd ⊢ U ∈ V → C ∈ Cat