Metamath Proof Explorer


Theorem rngcrescrhm

Description: The category of non-unital rings (in a universe) restricted to the ring homomorphisms between unital rings (in the same universe). (Contributed by AV, 1-Mar-2020)

Ref Expression
Hypotheses rngcrescrhm.u φUV
rngcrescrhm.c C=RngCatU
rngcrescrhm.r φR=RingU
rngcrescrhm.h H=RingHomR×R
Assertion rngcrescrhm φCcatH=C𝑠RsSetHomndxH

Proof

Step Hyp Ref Expression
1 rngcrescrhm.u φUV
2 rngcrescrhm.c C=RngCatU
3 rngcrescrhm.r φR=RingU
4 rngcrescrhm.h H=RingHomR×R
5 eqid CcatH=CcatH
6 2 fvexi CV
7 6 a1i φCV
8 incom RingU=URing
9 3 8 eqtrdi φR=URing
10 inex1g UVURingV
11 1 10 syl φURingV
12 9 11 eqeltrd φRV
13 inss1 RingURing
14 3 13 eqsstrdi φRRing
15 xpss12 RRingRRingR×RRing×Ring
16 14 14 15 syl2anc φR×RRing×Ring
17 rhmfn RingHomFnRing×Ring
18 fnssresb RingHomFnRing×RingRingHomR×RFnR×RR×RRing×Ring
19 17 18 mp1i φRingHomR×RFnR×RR×RRing×Ring
20 16 19 mpbird φRingHomR×RFnR×R
21 4 fneq1i HFnR×RRingHomR×RFnR×R
22 20 21 sylibr φHFnR×R
23 5 7 12 22 rescval2 φCcatH=C𝑠RsSetHomndxH