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 ⊢ 𝐶 = ( RngCat ‘ 𝑈 )
Assertion rngccat ( 𝑈 ∈ 𝑉 → 𝐶 ∈ Cat )

Proof

Step Hyp Ref Expression
1 rngccat.c ⊢ 𝐶 = ( RngCat ‘ 𝑈 )
2 id ⊢ ( 𝑈 ∈ 𝑉 → 𝑈 ∈ 𝑉 )
3 eqidd ⊢ ( 𝑈 ∈ 𝑉 → ( 𝑈 ∩ Rng ) = ( 𝑈 ∩ Rng ) )
4 eqidd ⊢ ( 𝑈 ∈ 𝑉 → ( RngHom ↾ ( ( 𝑈 ∩ Rng ) × ( 𝑈 ∩ Rng ) ) ) = ( RngHom ↾ ( ( 𝑈 ∩ Rng ) × ( 𝑈 ∩ Rng ) ) ) )
5 1 2 3 4 rngcval ⊢ ( 𝑈 ∈ 𝑉 → 𝐶 = ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( RngHom ↾ ( ( 𝑈 ∩ Rng ) × ( 𝑈 ∩ Rng ) ) ) ) )
6 eqid ⊢ ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( RngHom ↾ ( ( 𝑈 ∩ Rng ) × ( 𝑈 ∩ Rng ) ) ) ) = ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( RngHom ↾ ( ( 𝑈 ∩ Rng ) × ( 𝑈 ∩ Rng ) ) ) )
7 eqid ⊢ ( ExtStrCat ‘ 𝑈 ) = ( ExtStrCat ‘ 𝑈 )
8 eqidd ⊢ ( 𝑈 ∈ 𝑉 → ( Rng ∩ 𝑈 ) = ( Rng ∩ 𝑈 ) )
9 incom ⊢ ( 𝑈 ∩ Rng ) = ( Rng ∩ 𝑈 )
10 9 a1i ⊢ ( 𝑈 ∈ 𝑉 → ( 𝑈 ∩ Rng ) = ( Rng ∩ 𝑈 ) )
11 10 sqxpeqd ⊢ ( 𝑈 ∈ 𝑉 → ( ( 𝑈 ∩ Rng ) × ( 𝑈 ∩ Rng ) ) = ( ( Rng ∩ 𝑈 ) × ( Rng ∩ 𝑈 ) ) )
12 11 reseq2d ⊢ ( 𝑈 ∈ 𝑉 → ( RngHom ↾ ( ( 𝑈 ∩ Rng ) × ( 𝑈 ∩ Rng ) ) ) = ( RngHom ↾ ( ( Rng ∩ 𝑈 ) × ( Rng ∩ 𝑈 ) ) ) )
13 7 2 8 12 rnghmsubcsetc ⊢ ( 𝑈 ∈ 𝑉 → ( RngHom ↾ ( ( 𝑈 ∩ Rng ) × ( 𝑈 ∩ Rng ) ) ) ∈ ( Subcat ‘ ( ExtStrCat ‘ 𝑈 ) ) )
14 6 13 subccat ⊢ ( 𝑈 ∈ 𝑉 → ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( RngHom ↾ ( ( 𝑈 ∩ Rng ) × ( 𝑈 ∩ Rng ) ) ) ) ∈ Cat )
15 5 14 eqeltrd ⊢ ( 𝑈 ∈ 𝑉 → 𝐶 ∈ Cat )