Metamath Proof Explorer


Theorem rngcbas

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

Ref Expression
Hypotheses rngcbas.c C=RngCatU
rngcbas.b B=BaseC
rngcbas.u φUV
Assertion rngcbas φB=URng

Proof

Step Hyp Ref Expression
1 rngcbas.c C=RngCatU
2 rngcbas.b B=BaseC
3 rngcbas.u φUV
4 eqidd φURng=URng
5 eqidd φRngHomoURng×URng=RngHomoURng×URng
6 1 3 4 5 rngcval φC=ExtStrCatUcatRngHomoURng×URng
7 6 fveq2d φBaseC=BaseExtStrCatUcatRngHomoURng×URng
8 2 a1i φB=BaseC
9 eqid ExtStrCatUcatRngHomoURng×URng=ExtStrCatUcatRngHomoURng×URng
10 eqid BaseExtStrCatU=BaseExtStrCatU
11 fvexd φExtStrCatUV
12 4 5 rnghmresfn φRngHomoURng×URngFnURng×URng
13 inss1 URngU
14 eqid ExtStrCatU=ExtStrCatU
15 14 3 estrcbas φU=BaseExtStrCatU
16 13 15 sseqtrid φURngBaseExtStrCatU
17 9 10 11 12 16 rescbas φURng=BaseExtStrCatUcatRngHomoURng×URng
18 7 8 17 3eqtr4d φB=URng