# 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}=\mathrm{RingCat}\left({U}\right)$
funcringcsetc.s ${⊢}{S}=\mathrm{SetCat}\left({U}\right)$
funcringcsetc.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
funcringcsetc.u ${⊢}{\phi }\to {U}\in \mathrm{WUni}$
funcringcsetc.f ${⊢}{\phi }\to {F}=\left({x}\in {B}⟼{\mathrm{Base}}_{{x}}\right)$
funcringcsetc.g ${⊢}{\phi }\to {G}=\left({x}\in {B},{y}\in {B}⟼{\mathrm{I}↾}_{\left({x}\mathrm{RingHom}{y}\right)}\right)$
Assertion funcringcsetc ${⊢}{\phi }\to {F}\left({R}\mathrm{Func}{S}\right){G}$

### Proof

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