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

Proof

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