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}\upharpoonright }_{\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}\upharpoonright }_{\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}\upharpoonright }_{\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}\upharpoonright }_{\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}\upharpoonright }_{\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}\upharpoonright }_{\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}\upharpoonright }_{\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}\upharpoonright }_{\left({{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\right)}\right)\leftrightarrow ⟨\left(x\in U⟼{\mathrm{Base}}_x\right),\left(x\in U,y\in U⟼{\mathrm{I}\upharpoonright }_{\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}\upharpoonright }_{\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	eqtrdi	$$⊢\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}\upharpoonright }_{\left({\mathrm{Base}}_R\times {\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}\upharpoonright }_{\left({{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\right)}\right)⟩{\upharpoonright }_f\mathrm{Hom}\left(R\right)\in \left(\left(\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\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}\upharpoonright }_{\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}\upharpoonright }_{\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\times {\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}\upharpoonright }_{\left({{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\right)}\right)⟩{\upharpoonright }_f\mathrm{Hom}\left(R\right)=⟨{\left(x\in U⟼{\mathrm{Base}}_x\right)\upharpoonright }_{{\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}\upharpoonright }_{\left({{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\right)}\right)b\right)\upharpoonright }_{\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)\upharpoonright }_{{\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)\upharpoonright }_{{\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}\upharpoonright }_{\left(x\mathrm{RingHom}y\right)}={\mathrm{I}\upharpoonright }_{\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}\upharpoonright }_{\left(a\mathrm{RingHom}y\right)}={\mathrm{I}\upharpoonright }_{\left(a\mathrm{RingHom}b\right)}$$
44	41 43	cbvmpov	$$⊢\left(x\in B,y\in B⟼{\mathrm{I}\upharpoonright }_{\left(x\mathrm{RingHom}y\right)}\right)=\left(a\in B,b\in B⟼{\mathrm{I}\upharpoonright }_{\left(a\mathrm{RingHom}b\right)}\right)$$
45	44	a1i	$$⊢\phi \to \left(x\in B,y\in B⟼{\mathrm{I}\upharpoonright }_{\left(x\mathrm{RingHom}y\right)}\right)=\left(a\in B,b\in B⟼{\mathrm{I}\upharpoonright }_{\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}\upharpoonright }_{\left({{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\right)}\right)=\left(x\in U,y\in U⟼{\mathrm{I}\upharpoonright }_{\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}\upharpoonright }_{\left({{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\right)}={\mathrm{I}\upharpoonright }_{\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}\upharpoonright }_{\left({{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\right)}={\mathrm{I}\upharpoonright }_{\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}\upharpoonright }_{\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}\upharpoonright }_{\left({{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\right)}\right)b={\mathrm{I}\upharpoonright }_{\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}\upharpoonright }_{\left({{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\right)}\right)b\right)\upharpoonright }_{\left(a\mathrm{Hom}\left(R\right)b\right)}={\left({\mathrm{I}\upharpoonright }_{\left({{\mathrm{Base}}_b}^{{\mathrm{Base}}_a}\right)}\right)\upharpoonright }_{\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}\upharpoonright }_{\left({{\mathrm{Base}}_b}^{{\mathrm{Base}}_a}\right)}\right)\upharpoonright }_{\left(a\mathrm{Hom}\left(R\right)b\right)}={\left({\mathrm{I}\upharpoonright }_{\left({{\mathrm{Base}}_b}^{{\mathrm{Base}}_a}\right)}\right)\upharpoonright }_{\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)\leftrightarrow 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)\leftrightarrow f:{\mathrm{Base}}_a⟶{\mathrm{Base}}_b\right)$$
79	72 78	imbitrrid	$$⊢\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}\upharpoonright }_{\left({{\mathrm{Base}}_b}^{{\mathrm{Base}}_a}\right)}\right)\upharpoonright }_{\left(a\mathrm{RingHom}b\right)}={\mathrm{I}\upharpoonright }_{\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}\upharpoonright }_{\left(a\mathrm{RingHom}b\right)}={\left(a\left(x\in U,y\in U⟼{\mathrm{I}\upharpoonright }_{\left({{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\right)}\right)b\right)\upharpoonright }_{\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}\upharpoonright }_{\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}\upharpoonright }_{\left({{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\right)}\right)b\right)\upharpoonright }_{\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}\upharpoonright }_{\left({{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\right)}\right)b\right)\upharpoonright }_{\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)\upharpoonright }_{{\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}\upharpoonright }_{\left({{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\right)}\right)b\right)\upharpoonright }_{\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}\upharpoonright }_{\left({{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\right)}\right)⟩{\upharpoonright }_f\mathrm{Hom}\left(R\right)$$
87	1 4 18 22	ringcval	$$⊢\phi \to R=\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\mathrm{Hom}\left(R\right)$$
88	87	oveq1d	$$⊢\phi \to R\mathrm{Func}S=\left(\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\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\leftrightarrow ⟨F,G⟩\in \left(R\mathrm{Func}S\right)$$
91	89 90	sylibr	$$⊢\phi \to F\left(R\mathrm{Func}S\right)G$$