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 e. V -> C e. Cat )

Proof

Step Hyp Ref Expression
1 rngccat.c 
 |-  C = ( RngCat ` U )
2 id 
 |-  ( U e. V -> U e. V )
3 eqidd 
 |-  ( U e. V -> ( U i^i Rng ) = ( U i^i Rng ) )
4 eqidd 
 |-  ( U e. V -> ( RngHom |` ( ( U i^i Rng ) X. ( U i^i Rng ) ) ) = ( RngHom |` ( ( U i^i Rng ) X. ( U i^i Rng ) ) ) )
5 1 2 3 4 rngcval 
 |-  ( U e. V -> C = ( ( ExtStrCat ` U ) |`cat ( RngHom |` ( ( U i^i Rng ) X. ( U i^i Rng ) ) ) ) )
6 eqid 
 |-  ( ( ExtStrCat ` U ) |`cat ( RngHom |` ( ( U i^i Rng ) X. ( U i^i Rng ) ) ) ) = ( ( ExtStrCat ` U ) |`cat ( RngHom |` ( ( U i^i Rng ) X. ( U i^i Rng ) ) ) )
7 eqid 
 |-  ( ExtStrCat ` U ) = ( ExtStrCat ` U )
8 eqidd 
 |-  ( U e. V -> ( Rng i^i U ) = ( Rng i^i U ) )
9 incom 
 |-  ( U i^i Rng ) = ( Rng i^i U )
10 9 a1i 
 |-  ( U e. V -> ( U i^i Rng ) = ( Rng i^i U ) )
11 10 sqxpeqd 
 |-  ( U e. V -> ( ( U i^i Rng ) X. ( U i^i Rng ) ) = ( ( Rng i^i U ) X. ( Rng i^i U ) ) )
12 11 reseq2d 
 |-  ( U e. V -> ( RngHom |` ( ( U i^i Rng ) X. ( U i^i Rng ) ) ) = ( RngHom |` ( ( Rng i^i U ) X. ( Rng i^i U ) ) ) )
13 7 2 8 12 rnghmsubcsetc 
 |-  ( U e. V -> ( RngHom |` ( ( U i^i Rng ) X. ( U i^i Rng ) ) ) e. ( Subcat ` ( ExtStrCat ` U ) ) )
14 6 13 subccat 
 |-  ( U e. V -> ( ( ExtStrCat ` U ) |`cat ( RngHom |` ( ( U i^i Rng ) X. ( U i^i Rng ) ) ) ) e. Cat )
15 5 14 eqeltrd 
 |-  ( U e. V -> C e. Cat )