Metamath Proof Explorer


Theorem ringcbasALTV

Description: Set of objects of the category of rings (in a universe). (Contributed by AV, 13-Feb-2020) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 ringcbasALTV.c
 |-  C = ( RingCatALTV ` U )
2 ringcbasALTV.b
 |-  B = ( Base ` C )
3 ringcbasALTV.u
 |-  ( ph -> U e. V )
4 eqidd
 |-  ( ph -> ( U i^i Ring ) = ( U i^i Ring ) )
5 eqidd
 |-  ( ph -> ( x e. ( U i^i Ring ) , y e. ( U i^i Ring ) |-> ( x RingHom y ) ) = ( x e. ( U i^i Ring ) , y e. ( U i^i Ring ) |-> ( x RingHom y ) ) )
6 eqidd
 |-  ( ph -> ( v e. ( ( U i^i Ring ) X. ( U i^i Ring ) ) , z e. ( U i^i Ring ) |-> ( f e. ( ( 2nd ` v ) RingHom z ) , g e. ( ( 1st ` v ) RingHom ( 2nd ` v ) ) |-> ( f o. g ) ) ) = ( v e. ( ( U i^i Ring ) X. ( U i^i Ring ) ) , z e. ( U i^i Ring ) |-> ( f e. ( ( 2nd ` v ) RingHom z ) , g e. ( ( 1st ` v ) RingHom ( 2nd ` v ) ) |-> ( f o. g ) ) ) )
7 1 3 4 5 6 ringcvalALTV
 |-  ( ph -> C = { <. ( Base ` ndx ) , ( U i^i Ring ) >. , <. ( Hom ` ndx ) , ( x e. ( U i^i Ring ) , y e. ( U i^i Ring ) |-> ( x RingHom y ) ) >. , <. ( comp ` ndx ) , ( v e. ( ( U i^i Ring ) X. ( U i^i Ring ) ) , z e. ( U i^i Ring ) |-> ( f e. ( ( 2nd ` v ) RingHom z ) , g e. ( ( 1st ` v ) RingHom ( 2nd ` v ) ) |-> ( f o. g ) ) ) >. } )
8 catstr
 |-  { <. ( Base ` ndx ) , ( U i^i Ring ) >. , <. ( Hom ` ndx ) , ( x e. ( U i^i Ring ) , y e. ( U i^i Ring ) |-> ( x RingHom y ) ) >. , <. ( comp ` ndx ) , ( v e. ( ( U i^i Ring ) X. ( U i^i Ring ) ) , z e. ( U i^i Ring ) |-> ( f e. ( ( 2nd ` v ) RingHom z ) , g e. ( ( 1st ` v ) RingHom ( 2nd ` v ) ) |-> ( f o. g ) ) ) >. } Struct <. 1 , ; 1 5 >.
9 baseid
 |-  Base = Slot ( Base ` ndx )
10 snsstp1
 |-  { <. ( Base ` ndx ) , ( U i^i Ring ) >. } C_ { <. ( Base ` ndx ) , ( U i^i Ring ) >. , <. ( Hom ` ndx ) , ( x e. ( U i^i Ring ) , y e. ( U i^i Ring ) |-> ( x RingHom y ) ) >. , <. ( comp ` ndx ) , ( v e. ( ( U i^i Ring ) X. ( U i^i Ring ) ) , z e. ( U i^i Ring ) |-> ( f e. ( ( 2nd ` v ) RingHom z ) , g e. ( ( 1st ` v ) RingHom ( 2nd ` v ) ) |-> ( f o. g ) ) ) >. }
11 inex1g
 |-  ( U e. V -> ( U i^i Ring ) e. _V )
12 3 11 syl
 |-  ( ph -> ( U i^i Ring ) e. _V )
13 7 8 9 10 12 2 strfv3
 |-  ( ph -> B = ( U i^i Ring ) )