Theorem rngcbasALTV

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

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

Proof

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