Theorem wunfunc

Description: A weak universe is closed under the functor set operation. (Contributed by Mario Carneiro, 12-Jan-2017) (Proof shortened by AV, 13-Oct-2024)

	Ref	Expression
Hypotheses	wunfunc.1	$$⊢\phi \to U\in \mathrm{WUni}$$
	wunfunc.2	$$⊢\phi \to C\in U$$
	wunfunc.3	$$⊢\phi \to D\in U$$
Assertion	wunfunc	$$⊢\phi \to C\mathrm{Func}D\in U$$

Proof

Step	Hyp	Ref	Expression
1		wunfunc.1	$$⊢\phi \to U\in \mathrm{WUni}$$
2		wunfunc.2	$$⊢\phi \to C\in U$$
3		wunfunc.3	$$⊢\phi \to D\in U$$
4		baseid	$$⊢\mathrm{Base}=\mathrm{Slot}{\mathrm{Base}}_{\mathrm{ndx}}$$
5	4 1 3	wunstr	$$⊢\phi \to {\mathrm{Base}}_D\in U$$
6	4 1 2	wunstr	$$⊢\phi \to {\mathrm{Base}}_C\in U$$
7	1 5 6	wunmap	$$⊢\phi \to {{\mathrm{Base}}_D}^{{\mathrm{Base}}_C}\in U$$
8		homid	$$⊢\mathrm{Hom}=\mathrm{Slot}\mathrm{Hom}\left(\mathrm{ndx}\right)$$
9	8 1 2	wunstr	$$⊢\phi \to \mathrm{Hom}\left(C\right)\in U$$
10	1 9	wunrn	$$⊢\phi \to \mathrm{ran}\mathrm{Hom}\left(C\right)\in U$$
11	1 10	wununi	$$⊢\phi \to \bigcup \mathrm{ran}\mathrm{Hom}\left(C\right)\in U$$
12	8 1 3	wunstr	$$⊢\phi \to \mathrm{Hom}\left(D\right)\in U$$
13	1 12	wunrn	$$⊢\phi \to \mathrm{ran}\mathrm{Hom}\left(D\right)\in U$$
14	1 13	wununi	$$⊢\phi \to \bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)\in U$$
15	1 11 14	wunxp	$$⊢\phi \to \bigcup \mathrm{ran}\mathrm{Hom}\left(C\right)\times \bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)\in U$$
16	1 15	wunpw	$$⊢\phi \to 𝒫\left(\bigcup \mathrm{ran}\mathrm{Hom}\left(C\right)\times \bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)\right)\in U$$
17	1 6 6	wunxp	$$⊢\phi \to {\mathrm{Base}}_C\times {\mathrm{Base}}_C\in U$$
18	1 16 17	wunmap	$$⊢\phi \to {𝒫\left(\bigcup \mathrm{ran}\mathrm{Hom}\left(C\right)\times \bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)\right)}^{\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)}\in U$$
19	1 7 18	wunxp	$$⊢\phi \to \left({{\mathrm{Base}}_D}^{{\mathrm{Base}}_C}\right)\times \left({𝒫\left(\bigcup \mathrm{ran}\mathrm{Hom}\left(C\right)\times \bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)\right)}^{\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)}\right)\in U$$
20		relfunc	$$⊢\mathrm{Rel}\left(C\mathrm{Func}D\right)$$
21	20	a1i	$$⊢\phi \to \mathrm{Rel}\left(C\mathrm{Func}D\right)$$
22		df-br	$$⊢f\left(C\mathrm{Func}D\right)g\leftrightarrow ⟨f,g⟩\in \left(C\mathrm{Func}D\right)$$
23		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
24		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
25		simpr	$$⊢\left(\phi \wedge f\left(C\mathrm{Func}D\right)g\right)\to f\left(C\mathrm{Func}D\right)g$$
26	23 24 25	funcf1	$$⊢\left(\phi \wedge f\left(C\mathrm{Func}D\right)g\right)\to f:{\mathrm{Base}}_C⟶{\mathrm{Base}}_D$$
27		fvex	$$⊢{\mathrm{Base}}_D\in \mathrm{V}$$
28		fvex	$$⊢{\mathrm{Base}}_C\in \mathrm{V}$$
29	27 28	elmap	$$⊢f\in \left({{\mathrm{Base}}_D}^{{\mathrm{Base}}_C}\right)\leftrightarrow f:{\mathrm{Base}}_C⟶{\mathrm{Base}}_D$$
30	26 29	sylibr	$$⊢\left(\phi \wedge f\left(C\mathrm{Func}D\right)g\right)\to f\in \left({{\mathrm{Base}}_D}^{{\mathrm{Base}}_C}\right)$$
31		mapsspw	$$⊢{\left(f\left(1^{st}\left(z\right)\right)\mathrm{Hom}\left(D\right)f\left(2^{nd}\left(z\right)\right)\right)}^{\mathrm{Hom}\left(C\right)\left(z\right)}\subseteq 𝒫\left(\mathrm{Hom}\left(C\right)\left(z\right)\times \left(f\left(1^{st}\left(z\right)\right)\mathrm{Hom}\left(D\right)f\left(2^{nd}\left(z\right)\right)\right)\right)$$
32		fvssunirn	$$⊢\mathrm{Hom}\left(C\right)\left(z\right)\subseteq \bigcup \mathrm{ran}\mathrm{Hom}\left(C\right)$$
33		ovssunirn	$$⊢f\left(1^{st}\left(z\right)\right)\mathrm{Hom}\left(D\right)f\left(2^{nd}\left(z\right)\right)\subseteq \bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)$$
34		xpss12	$$⊢\left(\mathrm{Hom}\left(C\right)\left(z\right)\subseteq \bigcup \mathrm{ran}\mathrm{Hom}\left(C\right)\wedge f\left(1^{st}\left(z\right)\right)\mathrm{Hom}\left(D\right)f\left(2^{nd}\left(z\right)\right)\subseteq \bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)\right)\to \mathrm{Hom}\left(C\right)\left(z\right)\times \left(f\left(1^{st}\left(z\right)\right)\mathrm{Hom}\left(D\right)f\left(2^{nd}\left(z\right)\right)\right)\subseteq \bigcup \mathrm{ran}\mathrm{Hom}\left(C\right)\times \bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)$$
35	32 33 34	mp2an	$$⊢\mathrm{Hom}\left(C\right)\left(z\right)\times \left(f\left(1^{st}\left(z\right)\right)\mathrm{Hom}\left(D\right)f\left(2^{nd}\left(z\right)\right)\right)\subseteq \bigcup \mathrm{ran}\mathrm{Hom}\left(C\right)\times \bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)$$
36	35	sspwi	$$⊢𝒫\left(\mathrm{Hom}\left(C\right)\left(z\right)\times \left(f\left(1^{st}\left(z\right)\right)\mathrm{Hom}\left(D\right)f\left(2^{nd}\left(z\right)\right)\right)\right)\subseteq 𝒫\left(\bigcup \mathrm{ran}\mathrm{Hom}\left(C\right)\times \bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)\right)$$
37	31 36	sstri	$$⊢{\left(f\left(1^{st}\left(z\right)\right)\mathrm{Hom}\left(D\right)f\left(2^{nd}\left(z\right)\right)\right)}^{\mathrm{Hom}\left(C\right)\left(z\right)}\subseteq 𝒫\left(\bigcup \mathrm{ran}\mathrm{Hom}\left(C\right)\times \bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)\right)$$
38	37	rgenw	$$⊢\forall z\in \left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right){\left(f\left(1^{st}\left(z\right)\right)\mathrm{Hom}\left(D\right)f\left(2^{nd}\left(z\right)\right)\right)}^{\mathrm{Hom}\left(C\right)\left(z\right)}\subseteq 𝒫\left(\bigcup \mathrm{ran}\mathrm{Hom}\left(C\right)\times \bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)\right)$$
39		ss2ixp	$$⊢\forall z\in \left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right){\left(f\left(1^{st}\left(z\right)\right)\mathrm{Hom}\left(D\right)f\left(2^{nd}\left(z\right)\right)\right)}^{\mathrm{Hom}\left(C\right)\left(z\right)}\subseteq 𝒫\left(\bigcup \mathrm{ran}\mathrm{Hom}\left(C\right)\times \bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)\right)\to \underset{z\in {\mathrm{Base}}_C\times {\mathrm{Base}}_C}{⨉}\left({\left(f\left(1^{st}\left(z\right)\right)\mathrm{Hom}\left(D\right)f\left(2^{nd}\left(z\right)\right)\right)}^{\mathrm{Hom}\left(C\right)\left(z\right)}\right)\subseteq \underset{z\in {\mathrm{Base}}_C\times {\mathrm{Base}}_C}{⨉}𝒫\left(\bigcup \mathrm{ran}\mathrm{Hom}\left(C\right)\times \bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)\right)$$
40	38 39	ax-mp	$$⊢\underset{z\in {\mathrm{Base}}_C\times {\mathrm{Base}}_C}{⨉}\left({\left(f\left(1^{st}\left(z\right)\right)\mathrm{Hom}\left(D\right)f\left(2^{nd}\left(z\right)\right)\right)}^{\mathrm{Hom}\left(C\right)\left(z\right)}\right)\subseteq \underset{z\in {\mathrm{Base}}_C\times {\mathrm{Base}}_C}{⨉}𝒫\left(\bigcup \mathrm{ran}\mathrm{Hom}\left(C\right)\times \bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)\right)$$
41	28 28	xpex	$$⊢{\mathrm{Base}}_C\times {\mathrm{Base}}_C\in \mathrm{V}$$
42		fvex	$$⊢\mathrm{Hom}\left(C\right)\in \mathrm{V}$$
43	42	rnex	$$⊢\mathrm{ran}\mathrm{Hom}\left(C\right)\in \mathrm{V}$$
44	43	uniex	$$⊢\bigcup \mathrm{ran}\mathrm{Hom}\left(C\right)\in \mathrm{V}$$
45		fvex	$$⊢\mathrm{Hom}\left(D\right)\in \mathrm{V}$$
46	45	rnex	$$⊢\mathrm{ran}\mathrm{Hom}\left(D\right)\in \mathrm{V}$$
47	46	uniex	$$⊢\bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)\in \mathrm{V}$$
48	44 47	xpex	$$⊢\bigcup \mathrm{ran}\mathrm{Hom}\left(C\right)\times \bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)\in \mathrm{V}$$
49	48	pwex	$$⊢𝒫\left(\bigcup \mathrm{ran}\mathrm{Hom}\left(C\right)\times \bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)\right)\in \mathrm{V}$$
50	41 49	ixpconst	$$⊢\underset{z\in {\mathrm{Base}}_C\times {\mathrm{Base}}_C}{⨉}𝒫\left(\bigcup \mathrm{ran}\mathrm{Hom}\left(C\right)\times \bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)\right)={𝒫\left(\bigcup \mathrm{ran}\mathrm{Hom}\left(C\right)\times \bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)\right)}^{\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)}$$
51	40 50	sseqtri	$$⊢\underset{z\in {\mathrm{Base}}_C\times {\mathrm{Base}}_C}{⨉}\left({\left(f\left(1^{st}\left(z\right)\right)\mathrm{Hom}\left(D\right)f\left(2^{nd}\left(z\right)\right)\right)}^{\mathrm{Hom}\left(C\right)\left(z\right)}\right)\subseteq {𝒫\left(\bigcup \mathrm{ran}\mathrm{Hom}\left(C\right)\times \bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)\right)}^{\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)}$$
52		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
53		eqid	$$⊢\mathrm{Hom}\left(D\right)=\mathrm{Hom}\left(D\right)$$
54	23 52 53 25	funcixp	$$⊢\left(\phi \wedge f\left(C\mathrm{Func}D\right)g\right)\to g\in \underset{z\in {\mathrm{Base}}_C\times {\mathrm{Base}}_C}{⨉}\left({\left(f\left(1^{st}\left(z\right)\right)\mathrm{Hom}\left(D\right)f\left(2^{nd}\left(z\right)\right)\right)}^{\mathrm{Hom}\left(C\right)\left(z\right)}\right)$$
55	51 54	sselid	$$⊢\left(\phi \wedge f\left(C\mathrm{Func}D\right)g\right)\to g\in \left({𝒫\left(\bigcup \mathrm{ran}\mathrm{Hom}\left(C\right)\times \bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)\right)}^{\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)}\right)$$
56	30 55	opelxpd	$$⊢\left(\phi \wedge f\left(C\mathrm{Func}D\right)g\right)\to ⟨f,g⟩\in \left(\left({{\mathrm{Base}}_D}^{{\mathrm{Base}}_C}\right)\times \left({𝒫\left(\bigcup \mathrm{ran}\mathrm{Hom}\left(C\right)\times \bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)\right)}^{\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)}\right)\right)$$
57	56	ex	$$⊢\phi \to \left(f\left(C\mathrm{Func}D\right)g\to ⟨f,g⟩\in \left(\left({{\mathrm{Base}}_D}^{{\mathrm{Base}}_C}\right)\times \left({𝒫\left(\bigcup \mathrm{ran}\mathrm{Hom}\left(C\right)\times \bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)\right)}^{\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)}\right)\right)\right)$$
58	22 57	biimtrrid	$$⊢\phi \to \left(⟨f,g⟩\in \left(C\mathrm{Func}D\right)\to ⟨f,g⟩\in \left(\left({{\mathrm{Base}}_D}^{{\mathrm{Base}}_C}\right)\times \left({𝒫\left(\bigcup \mathrm{ran}\mathrm{Hom}\left(C\right)\times \bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)\right)}^{\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)}\right)\right)\right)$$
59	21 58	relssdv	$$⊢\phi \to C\mathrm{Func}D\subseteq \left({{\mathrm{Base}}_D}^{{\mathrm{Base}}_C}\right)\times \left({𝒫\left(\bigcup \mathrm{ran}\mathrm{Hom}\left(C\right)\times \bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)\right)}^{\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)}\right)$$
60	1 19 59	wunss	$$⊢\phi \to C\mathrm{Func}D\in U$$