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 ) ) |