Metamath Proof Explorer


Theorem funcringcsetcALTV2

Description: The "natural forgetful functor" from the category of unital rings into the category of sets which sends each ring to its underlying set (base set) and the morphisms (ring homomorphisms) to mappings of the corresponding base sets. (Contributed by AV, 16-Feb-2020) (New usage is discouraged.)

Ref Expression
Hypotheses funcringcsetcALTV2.r R=RingCatU
funcringcsetcALTV2.s S=SetCatU
funcringcsetcALTV2.b B=BaseR
funcringcsetcALTV2.c C=BaseS
funcringcsetcALTV2.u φUWUni
funcringcsetcALTV2.f φF=xBBasex
funcringcsetcALTV2.g φG=xB,yBIxRingHomy
Assertion funcringcsetcALTV2 φFRFuncSG

Proof

Step Hyp Ref Expression
1 funcringcsetcALTV2.r R=RingCatU
2 funcringcsetcALTV2.s S=SetCatU
3 funcringcsetcALTV2.b B=BaseR
4 funcringcsetcALTV2.c C=BaseS
5 funcringcsetcALTV2.u φUWUni
6 funcringcsetcALTV2.f φF=xBBasex
7 funcringcsetcALTV2.g φG=xB,yBIxRingHomy
8 eqid HomR=HomR
9 eqid HomS=HomS
10 eqid IdR=IdR
11 eqid IdS=IdS
12 eqid compR=compR
13 eqid compS=compS
14 1 ringccat UWUniRCat
15 5 14 syl φRCat
16 2 setccat UWUniSCat
17 5 16 syl φSCat
18 1 2 3 4 5 6 funcringcsetcALTV2lem3 φF:BC
19 1 2 3 4 5 6 7 funcringcsetcALTV2lem4 φGFnB×B
20 1 2 3 4 5 6 7 funcringcsetcALTV2lem8 φaBbBaGb:aHomRbFaHomSFb
21 1 2 3 4 5 6 7 funcringcsetcALTV2lem7 φaBaGaIdRa=IdSFa
22 1 2 3 4 5 6 7 funcringcsetcALTV2lem9 φaBbBcBhaHomRbkbHomRcaGckabcompRch=bGckFaFbcompSFcaGbh
23 3 4 8 9 10 11 12 13 15 17 18 19 20 21 22 isfuncd φFRFuncSG