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=RingCatALTVU
ringcbasALTV.b B=BaseC
ringcbasALTV.u φUV
Assertion ringcbasALTV φB=URing

Proof

Step Hyp Ref Expression
1 ringcbasALTV.c C=RingCatALTVU
2 ringcbasALTV.b B=BaseC
3 ringcbasALTV.u φUV
4 eqidd φURing=URing
5 eqidd φxURing,yURingxRingHomy=xURing,yURingxRingHomy
6 eqidd φvURing×URing,zURingf2ndvRingHomz,g1stvRingHom2ndvfg=vURing×URing,zURingf2ndvRingHomz,g1stvRingHom2ndvfg
7 1 3 4 5 6 ringcvalALTV φC=BasendxURingHomndxxURing,yURingxRingHomycompndxvURing×URing,zURingf2ndvRingHomz,g1stvRingHom2ndvfg
8 catstr BasendxURingHomndxxURing,yURingxRingHomycompndxvURing×URing,zURingf2ndvRingHomz,g1stvRingHom2ndvfgStruct115
9 baseid Base=SlotBasendx
10 snsstp1 BasendxURingBasendxURingHomndxxURing,yURingxRingHomycompndxvURing×URing,zURingf2ndvRingHomz,g1stvRingHom2ndvfg
11 inex1g UVURingV
12 3 11 syl φURingV
13 7 8 9 10 12 2 strfv3 φB=URing