# Metamath Proof Explorer

## Theorem funcringcsetc

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, 26-Mar-2020)

Ref Expression
Hypotheses funcringcsetc.r
`|- R = ( RingCat ` U )`
funcringcsetc.s
`|- S = ( SetCat ` U )`
funcringcsetc.b
`|- B = ( Base ` R )`
funcringcsetc.u
`|- ( ph -> U e. WUni )`
funcringcsetc.f
`|- ( ph -> F = ( x e. B |-> ( Base ` x ) ) )`
funcringcsetc.g
`|- ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( x RingHom y ) ) ) )`
Assertion funcringcsetc
`|- ( ph -> F ( R Func S ) G )`

### Proof

Step Hyp Ref Expression
1 funcringcsetc.r
` |-  R = ( RingCat ` U )`
2 funcringcsetc.s
` |-  S = ( SetCat ` U )`
3 funcringcsetc.b
` |-  B = ( Base ` R )`
4 funcringcsetc.u
` |-  ( ph -> U e. WUni )`
5 funcringcsetc.f
` |-  ( ph -> F = ( x e. B |-> ( Base ` x ) ) )`
6 funcringcsetc.g
` |-  ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( x RingHom y ) ) ) )`
7 eqid
` |-  ( ExtStrCat ` U ) = ( ExtStrCat ` U )`
8 eqid
` |-  ( Base ` ( ExtStrCat ` U ) ) = ( Base ` ( ExtStrCat ` U ) )`
9 eqid
` |-  ( Base ` S ) = ( Base ` S )`
10 7 4 estrcbas
` |-  ( ph -> U = ( Base ` ( ExtStrCat ` U ) ) )`
11 10 mpteq1d
` |-  ( ph -> ( x e. U |-> ( Base ` x ) ) = ( x e. ( Base ` ( ExtStrCat ` U ) ) |-> ( Base ` x ) ) )`
12 mpoeq12
` |-  ( ( U = ( Base ` ( ExtStrCat ` U ) ) /\ U = ( Base ` ( ExtStrCat ` U ) ) ) -> ( x e. U , y e. U |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) = ( x e. ( Base ` ( ExtStrCat ` U ) ) , y e. ( Base ` ( ExtStrCat ` U ) ) |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) )`
13 10 10 12 syl2anc
` |-  ( ph -> ( x e. U , y e. U |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) = ( x e. ( Base ` ( ExtStrCat ` U ) ) , y e. ( Base ` ( ExtStrCat ` U ) ) |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) )`
14 7 2 8 9 4 11 13 funcestrcsetc
` |-  ( ph -> ( x e. U |-> ( Base ` x ) ) ( ( ExtStrCat ` U ) Func S ) ( x e. U , y e. U |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) )`
15 df-br
` |-  ( ( x e. U |-> ( Base ` x ) ) ( ( ExtStrCat ` U ) Func S ) ( x e. U , y e. U |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) <-> <. ( x e. U |-> ( Base ` x ) ) , ( x e. U , y e. U |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) >. e. ( ( ExtStrCat ` U ) Func S ) )`
16 14 15 sylib
` |-  ( ph -> <. ( x e. U |-> ( Base ` x ) ) , ( x e. U , y e. U |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) >. e. ( ( ExtStrCat ` U ) Func S ) )`
17 eqid
` |-  ( Base ` R ) = ( Base ` R )`
18 1 17 4 ringcbas
` |-  ( ph -> ( Base ` R ) = ( U i^i Ring ) )`
19 incom
` |-  ( U i^i Ring ) = ( Ring i^i U )`
20 18 19 syl6eq
` |-  ( ph -> ( Base ` R ) = ( Ring i^i U ) )`
21 eqid
` |-  ( Hom ` R ) = ( Hom ` R )`
22 1 17 4 21 ringchomfval
` |-  ( ph -> ( Hom ` R ) = ( RingHom |` ( ( Base ` R ) X. ( Base ` R ) ) ) )`
23 7 4 20 22 rhmsubcsetc
` |-  ( ph -> ( Hom ` R ) e. ( Subcat ` ( ExtStrCat ` U ) ) )`
24 16 23 funcres
` |-  ( ph -> ( <. ( x e. U |-> ( Base ` x ) ) , ( x e. U , y e. U |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) >. |`f ( Hom ` R ) ) e. ( ( ( ExtStrCat ` U ) |`cat ( Hom ` R ) ) Func S ) )`
25 mptexg
` |-  ( U e. WUni -> ( x e. U |-> ( Base ` x ) ) e. _V )`
26 4 25 syl
` |-  ( ph -> ( x e. U |-> ( Base ` x ) ) e. _V )`
27 fvex
` |-  ( Hom ` R ) e. _V`
28 27 a1i
` |-  ( ph -> ( Hom ` R ) e. _V )`
29 mpoexga
` |-  ( ( U e. WUni /\ U e. WUni ) -> ( x e. U , y e. U |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) e. _V )`
30 4 4 29 syl2anc
` |-  ( ph -> ( x e. U , y e. U |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) e. _V )`
31 18 22 rhmresfn
` |-  ( ph -> ( Hom ` R ) Fn ( ( Base ` R ) X. ( Base ` R ) ) )`
32 26 28 30 31 resfval2
` |-  ( ph -> ( <. ( x e. U |-> ( Base ` x ) ) , ( x e. U , y e. U |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) >. |`f ( Hom ` R ) ) = <. ( ( x e. U |-> ( Base ` x ) ) |` ( Base ` R ) ) , ( a e. ( Base ` R ) , b e. ( Base ` R ) |-> ( ( a ( x e. U , y e. U |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) b ) |` ( a ( Hom ` R ) b ) ) ) >. )`
33 inss1
` |-  ( U i^i Ring ) C_ U`
34 18 33 eqsstrdi
` |-  ( ph -> ( Base ` R ) C_ U )`
35 34 resmptd
` |-  ( ph -> ( ( x e. U |-> ( Base ` x ) ) |` ( Base ` R ) ) = ( x e. ( Base ` R ) |-> ( Base ` x ) ) )`
36 3 a1i
` |-  ( ph -> B = ( Base ` R ) )`
37 36 mpteq1d
` |-  ( ph -> ( x e. B |-> ( Base ` x ) ) = ( x e. ( Base ` R ) |-> ( Base ` x ) ) )`
38 5 37 eqtr2d
` |-  ( ph -> ( x e. ( Base ` R ) |-> ( Base ` x ) ) = F )`
39 35 38 eqtrd
` |-  ( ph -> ( ( x e. U |-> ( Base ` x ) ) |` ( Base ` R ) ) = F )`
40 oveq1
` |-  ( x = a -> ( x RingHom y ) = ( a RingHom y ) )`
41 40 reseq2d
` |-  ( x = a -> ( _I |` ( x RingHom y ) ) = ( _I |` ( a RingHom y ) ) )`
42 oveq2
` |-  ( y = b -> ( a RingHom y ) = ( a RingHom b ) )`
43 42 reseq2d
` |-  ( y = b -> ( _I |` ( a RingHom y ) ) = ( _I |` ( a RingHom b ) ) )`
44 41 43 cbvmpov
` |-  ( x e. B , y e. B |-> ( _I |` ( x RingHom y ) ) ) = ( a e. B , b e. B |-> ( _I |` ( a RingHom b ) ) )`
45 44 a1i
` |-  ( ph -> ( x e. B , y e. B |-> ( _I |` ( x RingHom y ) ) ) = ( a e. B , b e. B |-> ( _I |` ( a RingHom b ) ) ) )`
46 3 a1i
` |-  ( ( ph /\ a e. B ) -> B = ( Base ` R ) )`
47 eqidd
` |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( x e. U , y e. U |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) = ( x e. U , y e. U |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) )`
48 fveq2
` |-  ( y = b -> ( Base ` y ) = ( Base ` b ) )`
49 fveq2
` |-  ( x = a -> ( Base ` x ) = ( Base ` a ) )`
50 48 49 oveqan12rd
` |-  ( ( x = a /\ y = b ) -> ( ( Base ` y ) ^m ( Base ` x ) ) = ( ( Base ` b ) ^m ( Base ` a ) ) )`
51 50 reseq2d
` |-  ( ( x = a /\ y = b ) -> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) = ( _I |` ( ( Base ` b ) ^m ( Base ` a ) ) ) )`
` |-  ( ( ( ph /\ ( a e. B /\ b e. B ) ) /\ ( x = a /\ y = b ) ) -> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) = ( _I |` ( ( Base ` b ) ^m ( Base ` a ) ) ) )`
53 3 34 eqsstrid
` |-  ( ph -> B C_ U )`
54 53 sseld
` |-  ( ph -> ( a e. B -> a e. U ) )`
55 54 com12
` |-  ( a e. B -> ( ph -> a e. U ) )`
` |-  ( ( a e. B /\ b e. B ) -> ( ph -> a e. U ) )`
57 56 impcom
` |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> a e. U )`
58 53 sseld
` |-  ( ph -> ( b e. B -> b e. U ) )`
` |-  ( ph -> ( ( a e. B /\ b e. B ) -> b e. U ) )`
60 59 imp
` |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> b e. U )`
61 ovexd
` |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( ( Base ` b ) ^m ( Base ` a ) ) e. _V )`
62 61 resiexd
` |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( _I |` ( ( Base ` b ) ^m ( Base ` a ) ) ) e. _V )`
63 47 52 57 60 62 ovmpod
` |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( a ( x e. U , y e. U |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) b ) = ( _I |` ( ( Base ` b ) ^m ( Base ` a ) ) ) )`
64 63 reseq1d
` |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( ( a ( x e. U , y e. U |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) b ) |` ( a ( Hom ` R ) b ) ) = ( ( _I |` ( ( Base ` b ) ^m ( Base ` a ) ) ) |` ( a ( Hom ` R ) b ) ) )`
` |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> U e. WUni )`
66 simprl
` |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> a e. B )`
67 simprr
` |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> b e. B )`
68 1 3 65 21 66 67 ringchom
` |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( a ( Hom ` R ) b ) = ( a RingHom b ) )`
69 68 reseq2d
` |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( ( _I |` ( ( Base ` b ) ^m ( Base ` a ) ) ) |` ( a ( Hom ` R ) b ) ) = ( ( _I |` ( ( Base ` b ) ^m ( Base ` a ) ) ) |` ( a RingHom b ) ) )`
70 eqid
` |-  ( Base ` a ) = ( Base ` a )`
71 eqid
` |-  ( Base ` b ) = ( Base ` b )`
72 70 71 rhmf
` |-  ( f e. ( a RingHom b ) -> f : ( Base ` a ) --> ( Base ` b ) )`
73 fvex
` |-  ( Base ` b ) e. _V`
74 fvex
` |-  ( Base ` a ) e. _V`
75 73 74 pm3.2i
` |-  ( ( Base ` b ) e. _V /\ ( Base ` a ) e. _V )`
76 75 a1i
` |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( ( Base ` b ) e. _V /\ ( Base ` a ) e. _V ) )`
77 elmapg
` |-  ( ( ( Base ` b ) e. _V /\ ( Base ` a ) e. _V ) -> ( f e. ( ( Base ` b ) ^m ( Base ` a ) ) <-> f : ( Base ` a ) --> ( Base ` b ) ) )`
78 76 77 syl
` |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( f e. ( ( Base ` b ) ^m ( Base ` a ) ) <-> f : ( Base ` a ) --> ( Base ` b ) ) )`
79 72 78 syl5ibr
` |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( f e. ( a RingHom b ) -> f e. ( ( Base ` b ) ^m ( Base ` a ) ) ) )`
80 79 ssrdv
` |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( a RingHom b ) C_ ( ( Base ` b ) ^m ( Base ` a ) ) )`
81 80 resabs1d
` |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( ( _I |` ( ( Base ` b ) ^m ( Base ` a ) ) ) |` ( a RingHom b ) ) = ( _I |` ( a RingHom b ) ) )`
82 64 69 81 3eqtrrd
` |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( _I |` ( a RingHom b ) ) = ( ( a ( x e. U , y e. U |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) b ) |` ( a ( Hom ` R ) b ) ) )`
83 36 46 82 mpoeq123dva
` |-  ( ph -> ( a e. B , b e. B |-> ( _I |` ( a RingHom b ) ) ) = ( a e. ( Base ` R ) , b e. ( Base ` R ) |-> ( ( a ( x e. U , y e. U |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) b ) |` ( a ( Hom ` R ) b ) ) ) )`
84 6 45 83 3eqtrrd
` |-  ( ph -> ( a e. ( Base ` R ) , b e. ( Base ` R ) |-> ( ( a ( x e. U , y e. U |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) b ) |` ( a ( Hom ` R ) b ) ) ) = G )`
85 39 84 opeq12d
` |-  ( ph -> <. ( ( x e. U |-> ( Base ` x ) ) |` ( Base ` R ) ) , ( a e. ( Base ` R ) , b e. ( Base ` R ) |-> ( ( a ( x e. U , y e. U |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) b ) |` ( a ( Hom ` R ) b ) ) ) >. = <. F , G >. )`
86 32 85 eqtr2d
` |-  ( ph -> <. F , G >. = ( <. ( x e. U |-> ( Base ` x ) ) , ( x e. U , y e. U |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) >. |`f ( Hom ` R ) ) )`
87 1 4 18 22 ringcval
` |-  ( ph -> R = ( ( ExtStrCat ` U ) |`cat ( Hom ` R ) ) )`
88 87 oveq1d
` |-  ( ph -> ( R Func S ) = ( ( ( ExtStrCat ` U ) |`cat ( Hom ` R ) ) Func S ) )`
89 24 86 88 3eltr4d
` |-  ( ph -> <. F , G >. e. ( R Func S ) )`
90 df-br
` |-  ( F ( R Func S ) G <-> <. F , G >. e. ( R Func S ) )`
91 89 90 sylibr
` |-  ( ph -> F ( R Func S ) G )`