Metamath Proof Explorer

Theorem ringcbas

Description: Set of objects of the category of unital rings (in a universe). (Contributed by AV, 13-Feb-2020) (Revised by AV, 8-Mar-2020)

Ref Expression
Hypotheses ringcbas.c 
|- C = ( RingCat ` U )
ringcbas.b 
|- B = ( Base ` C )
ringcbas.u 
|- ( ph -> U e. V )
Assertion ringcbas 
|- ( ph -> B = ( U i^i Ring ) )

Proof

Step Hyp Ref Expression
1 ringcbas.c 
 |-  C = ( RingCat ` U )
2 ringcbas.b 
 |-  B = ( Base ` C )
3 ringcbas.u 
 |-  ( ph -> U e. V )
4 eqidd 
 |-  ( ph -> ( U i^i Ring ) = ( U i^i Ring ) )
5 eqidd 
 |-  ( ph -> ( RingHom |` ( ( U i^i Ring ) X. ( U i^i Ring ) ) ) = ( RingHom |` ( ( U i^i Ring ) X. ( U i^i Ring ) ) ) )
6 1 3 4 5 ringcval 
 |-  ( ph -> C = ( ( ExtStrCat ` U ) |`cat ( RingHom |` ( ( U i^i Ring ) X. ( U i^i Ring ) ) ) ) )
7 6 fveq2d 
 |-  ( ph -> ( Base ` C ) = ( Base ` ( ( ExtStrCat ` U ) |`cat ( RingHom |` ( ( U i^i Ring ) X. ( U i^i Ring ) ) ) ) ) )
8 2 a1i 
 |-  ( ph -> B = ( Base ` C ) )
9 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 ) ) ) )
10 eqid 
 |-  ( Base ` ( ExtStrCat ` U ) ) = ( Base ` ( ExtStrCat ` U ) )
11 fvexd 
 |-  ( ph -> ( ExtStrCat ` U ) e. _V )
12 4 5 rhmresfn 
 |-  ( ph -> ( RingHom |` ( ( U i^i Ring ) X. ( U i^i Ring ) ) ) Fn ( ( U i^i Ring ) X. ( U i^i Ring ) ) )
13 inss1 
 |-  ( U i^i Ring ) C_ U
14 eqid 
 |-  ( ExtStrCat ` U ) = ( ExtStrCat ` U )
15 14 3 estrcbas 
 |-  ( ph -> U = ( Base ` ( ExtStrCat ` U ) ) )
16 13 15 sseqtrid 
 |-  ( ph -> ( U i^i Ring ) C_ ( Base ` ( ExtStrCat ` U ) ) )
17 9 10 11 12 16 rescbas 
 |-  ( ph -> ( U i^i Ring ) = ( Base ` ( ( ExtStrCat ` U ) |`cat ( RingHom |` ( ( U i^i Ring ) X. ( U i^i Ring ) ) ) ) ) )
18 7 8 17 3eqtr4d 
 |-  ( ph -> B = ( U i^i Ring ) )