Theorem wunnat

Description: A weak universe is closed under the natural transformation operation. (Contributed by Mario Carneiro, 12-Jan-2017)

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

Proof

Step	Hyp	Ref	Expression
1		wunnat.1	$$⊢\phi \to U\in \mathrm{WUni}$$
2		wunnat.2	$$⊢\phi \to C\in U$$
3		wunnat.3	$$⊢\phi \to D\in U$$
4	1 2 3	wunfunc	$$⊢\phi \to C\mathrm{Func}D\in U$$
5	1 4 4	wunxp	$$⊢\phi \to \left(C\mathrm{Func}D\right)\times \left(C\mathrm{Func}D\right)\in U$$
6		df-hom	$$⊢\mathrm{Hom}=\mathrm{Slot}14$$
7	6 1 3	wunstr	$$⊢\phi \to \mathrm{Hom}\left(D\right)\in U$$
8	1 7	wunrn	$$⊢\phi \to \mathrm{ran}\mathrm{Hom}\left(D\right)\in U$$
9	1 8	wununi	$$⊢\phi \to \bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)\in U$$
10		df-base	$$⊢\mathrm{Base}=\mathrm{Slot}1$$
11	10 1 2	wunstr	$$⊢\phi \to {\mathrm{Base}}_C\in U$$
12	1 9 11	wunmap	$$⊢\phi \to {\bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)}^{{\mathrm{Base}}_C}\in U$$
13	1 12	wunpw	$$⊢\phi \to 𝒫\left({\bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)}^{{\mathrm{Base}}_C}\right)\in U$$
14		fvex	$$⊢1^{st}\left(f\right)\in \mathrm{V}$$
15		fvex	$$⊢1^{st}\left(g\right)\in \mathrm{V}$$
16		ovex	$$⊢{\bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)}^{{\mathrm{Base}}_C}\in \mathrm{V}$$
17		ssrab2	$$⊢\left\{a\in \underset{x\in {\mathrm{Base}}_C}{⨉}\left(r\left(x\right)\mathrm{Hom}\left(D\right)s\left(x\right)\right)|\forall x\in {\mathrm{Base}}_C\forall y\in {\mathrm{Base}}_C\forall z\in \left(x\mathrm{Hom}\left(C\right)y\right)a\left(y\right)\left(⟨r\left(x\right),r\left(y\right)⟩\mathrm{comp}\left(D\right)s\left(y\right)\right)\left(x{2}^{nd}\left(f\right)y\right)\left(z\right)=\left(x{2}^{nd}\left(g\right)y\right)\left(z\right)\left(⟨r\left(x\right),s\left(x\right)⟩\mathrm{comp}\left(D\right)s\left(y\right)\right)a\left(x\right)\right\}\subseteq \underset{x\in {\mathrm{Base}}_C}{⨉}\left(r\left(x\right)\mathrm{Hom}\left(D\right)s\left(x\right)\right)$$
18		ovssunirn	$$⊢r\left(x\right)\mathrm{Hom}\left(D\right)s\left(x\right)\subseteq \bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)$$
19	18	rgenw	$$⊢\forall x\in {\mathrm{Base}}_{C}r\left(x\right)\mathrm{Hom}\left(D\right)s\left(x\right)\subseteq \bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)$$
20		ss2ixp	$$⊢\forall x\in {\mathrm{Base}}_{C}r\left(x\right)\mathrm{Hom}\left(D\right)s\left(x\right)\subseteq \bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)\to \underset{x\in {\mathrm{Base}}_C}{⨉}\left(r\left(x\right)\mathrm{Hom}\left(D\right)s\left(x\right)\right)\subseteq \underset{x\in {\mathrm{Base}}_C}{⨉}\bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)$$
21	19 20	ax-mp	$$⊢\underset{x\in {\mathrm{Base}}_C}{⨉}\left(r\left(x\right)\mathrm{Hom}\left(D\right)s\left(x\right)\right)\subseteq \underset{x\in {\mathrm{Base}}_C}{⨉}\bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)$$
22		fvex	$$⊢{\mathrm{Base}}_C\in \mathrm{V}$$
23		fvex	$$⊢\mathrm{Hom}\left(D\right)\in \mathrm{V}$$
24	23	rnex	$$⊢\mathrm{ran}\mathrm{Hom}\left(D\right)\in \mathrm{V}$$
25	24	uniex	$$⊢\bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)\in \mathrm{V}$$
26	22 25	ixpconst	$$⊢\underset{x\in {\mathrm{Base}}_C}{⨉}\bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)={\bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)}^{{\mathrm{Base}}_C}$$
27	21 26	sseqtri	$$⊢\underset{x\in {\mathrm{Base}}_C}{⨉}\left(r\left(x\right)\mathrm{Hom}\left(D\right)s\left(x\right)\right)\subseteq {\bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)}^{{\mathrm{Base}}_C}$$
28	17 27	sstri	$$⊢\left\{a\in \underset{x\in {\mathrm{Base}}_C}{⨉}\left(r\left(x\right)\mathrm{Hom}\left(D\right)s\left(x\right)\right)|\forall x\in {\mathrm{Base}}_C\forall y\in {\mathrm{Base}}_C\forall z\in \left(x\mathrm{Hom}\left(C\right)y\right)a\left(y\right)\left(⟨r\left(x\right),r\left(y\right)⟩\mathrm{comp}\left(D\right)s\left(y\right)\right)\left(x{2}^{nd}\left(f\right)y\right)\left(z\right)=\left(x{2}^{nd}\left(g\right)y\right)\left(z\right)\left(⟨r\left(x\right),s\left(x\right)⟩\mathrm{comp}\left(D\right)s\left(y\right)\right)a\left(x\right)\right\}\subseteq {\bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)}^{{\mathrm{Base}}_C}$$
29	16 28	elpwi2	$$⊢\left\{a\in \underset{x\in {\mathrm{Base}}_C}{⨉}\left(r\left(x\right)\mathrm{Hom}\left(D\right)s\left(x\right)\right)|\forall x\in {\mathrm{Base}}_C\forall y\in {\mathrm{Base}}_C\forall z\in \left(x\mathrm{Hom}\left(C\right)y\right)a\left(y\right)\left(⟨r\left(x\right),r\left(y\right)⟩\mathrm{comp}\left(D\right)s\left(y\right)\right)\left(x{2}^{nd}\left(f\right)y\right)\left(z\right)=\left(x{2}^{nd}\left(g\right)y\right)\left(z\right)\left(⟨r\left(x\right),s\left(x\right)⟩\mathrm{comp}\left(D\right)s\left(y\right)\right)a\left(x\right)\right\}\in 𝒫\left({\bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)}^{{\mathrm{Base}}_C}\right)$$
30	29	sbcth	$$⊢1^{st}\left(g\right)\in \mathrm{V}\to \underset{\dot{}}{[}{1}^{st}\left(g\right)/s\underset{\dot{}}{]}\left\{a\in \underset{x\in {\mathrm{Base}}_C}{⨉}\left(r\left(x\right)\mathrm{Hom}\left(D\right)s\left(x\right)\right)|\forall x\in {\mathrm{Base}}_C\forall y\in {\mathrm{Base}}_C\forall z\in \left(x\mathrm{Hom}\left(C\right)y\right)a\left(y\right)\left(⟨r\left(x\right),r\left(y\right)⟩\mathrm{comp}\left(D\right)s\left(y\right)\right)\left(x{2}^{nd}\left(f\right)y\right)\left(z\right)=\left(x{2}^{nd}\left(g\right)y\right)\left(z\right)\left(⟨r\left(x\right),s\left(x\right)⟩\mathrm{comp}\left(D\right)s\left(y\right)\right)a\left(x\right)\right\}\in 𝒫\left({\bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)}^{{\mathrm{Base}}_C}\right)$$
31		sbcel1g	$$⊢1^{st}\left(g\right)\in \mathrm{V}\to \left(\underset{\dot{}}{[}{1}^{st}\left(g\right)/s\underset{\dot{}}{]}\left\{a\in \underset{x\in {\mathrm{Base}}_C}{⨉}\left(r\left(x\right)\mathrm{Hom}\left(D\right)s\left(x\right)\right)|\forall x\in {\mathrm{Base}}_C\forall y\in {\mathrm{Base}}_C\forall z\in \left(x\mathrm{Hom}\left(C\right)y\right)a\left(y\right)\left(⟨r\left(x\right),r\left(y\right)⟩\mathrm{comp}\left(D\right)s\left(y\right)\right)\left(x{2}^{nd}\left(f\right)y\right)\left(z\right)=\left(x{2}^{nd}\left(g\right)y\right)\left(z\right)\left(⟨r\left(x\right),s\left(x\right)⟩\mathrm{comp}\left(D\right)s\left(y\right)\right)a\left(x\right)\right\}\in 𝒫\left({\bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)}^{{\mathrm{Base}}_C}\right)\leftrightarrow ⦋1^{st}\left(g\right)/s⦌\left\{a\in \underset{x\in {\mathrm{Base}}_C}{⨉}\left(r\left(x\right)\mathrm{Hom}\left(D\right)s\left(x\right)\right)|\forall x\in {\mathrm{Base}}_C\forall y\in {\mathrm{Base}}_C\forall z\in \left(x\mathrm{Hom}\left(C\right)y\right)a\left(y\right)\left(⟨r\left(x\right),r\left(y\right)⟩\mathrm{comp}\left(D\right)s\left(y\right)\right)\left(x{2}^{nd}\left(f\right)y\right)\left(z\right)=\left(x{2}^{nd}\left(g\right)y\right)\left(z\right)\left(⟨r\left(x\right),s\left(x\right)⟩\mathrm{comp}\left(D\right)s\left(y\right)\right)a\left(x\right)\right\}\in 𝒫\left({\bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)}^{{\mathrm{Base}}_C}\right)\right)$$
32	30 31	mpbid	$$⊢1^{st}\left(g\right)\in \mathrm{V}\to ⦋1^{st}\left(g\right)/s⦌\left\{a\in \underset{x\in {\mathrm{Base}}_C}{⨉}\left(r\left(x\right)\mathrm{Hom}\left(D\right)s\left(x\right)\right)|\forall x\in {\mathrm{Base}}_C\forall y\in {\mathrm{Base}}_C\forall z\in \left(x\mathrm{Hom}\left(C\right)y\right)a\left(y\right)\left(⟨r\left(x\right),r\left(y\right)⟩\mathrm{comp}\left(D\right)s\left(y\right)\right)\left(x{2}^{nd}\left(f\right)y\right)\left(z\right)=\left(x{2}^{nd}\left(g\right)y\right)\left(z\right)\left(⟨r\left(x\right),s\left(x\right)⟩\mathrm{comp}\left(D\right)s\left(y\right)\right)a\left(x\right)\right\}\in 𝒫\left({\bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)}^{{\mathrm{Base}}_C}\right)$$
33	15 32	ax-mp	$$⊢⦋1^{st}\left(g\right)/s⦌\left\{a\in \underset{x\in {\mathrm{Base}}_C}{⨉}\left(r\left(x\right)\mathrm{Hom}\left(D\right)s\left(x\right)\right)|\forall x\in {\mathrm{Base}}_C\forall y\in {\mathrm{Base}}_C\forall z\in \left(x\mathrm{Hom}\left(C\right)y\right)a\left(y\right)\left(⟨r\left(x\right),r\left(y\right)⟩\mathrm{comp}\left(D\right)s\left(y\right)\right)\left(x{2}^{nd}\left(f\right)y\right)\left(z\right)=\left(x{2}^{nd}\left(g\right)y\right)\left(z\right)\left(⟨r\left(x\right),s\left(x\right)⟩\mathrm{comp}\left(D\right)s\left(y\right)\right)a\left(x\right)\right\}\in 𝒫\left({\bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)}^{{\mathrm{Base}}_C}\right)$$
34	33	sbcth	$$⊢1^{st}\left(f\right)\in \mathrm{V}\to \underset{\dot{}}{[}{1}^{st}\left(f\right)/r\underset{\dot{}}{]}⦋1^{st}\left(g\right)/s⦌\left\{a\in \underset{x\in {\mathrm{Base}}_C}{⨉}\left(r\left(x\right)\mathrm{Hom}\left(D\right)s\left(x\right)\right)|\forall x\in {\mathrm{Base}}_C\forall y\in {\mathrm{Base}}_C\forall z\in \left(x\mathrm{Hom}\left(C\right)y\right)a\left(y\right)\left(⟨r\left(x\right),r\left(y\right)⟩\mathrm{comp}\left(D\right)s\left(y\right)\right)\left(x{2}^{nd}\left(f\right)y\right)\left(z\right)=\left(x{2}^{nd}\left(g\right)y\right)\left(z\right)\left(⟨r\left(x\right),s\left(x\right)⟩\mathrm{comp}\left(D\right)s\left(y\right)\right)a\left(x\right)\right\}\in 𝒫\left({\bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)}^{{\mathrm{Base}}_C}\right)$$
35		sbcel1g	$$⊢1^{st}\left(f\right)\in \mathrm{V}\to \left(\underset{\dot{}}{[}{1}^{st}\left(f\right)/r\underset{\dot{}}{]}⦋1^{st}\left(g\right)/s⦌\left\{a\in \underset{x\in {\mathrm{Base}}_C}{⨉}\left(r\left(x\right)\mathrm{Hom}\left(D\right)s\left(x\right)\right)|\forall x\in {\mathrm{Base}}_C\forall y\in {\mathrm{Base}}_C\forall z\in \left(x\mathrm{Hom}\left(C\right)y\right)a\left(y\right)\left(⟨r\left(x\right),r\left(y\right)⟩\mathrm{comp}\left(D\right)s\left(y\right)\right)\left(x{2}^{nd}\left(f\right)y\right)\left(z\right)=\left(x{2}^{nd}\left(g\right)y\right)\left(z\right)\left(⟨r\left(x\right),s\left(x\right)⟩\mathrm{comp}\left(D\right)s\left(y\right)\right)a\left(x\right)\right\}\in 𝒫\left({\bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)}^{{\mathrm{Base}}_C}\right)\leftrightarrow ⦋1^{st}\left(f\right)/r⦌⦋1^{st}\left(g\right)/s⦌\left\{a\in \underset{x\in {\mathrm{Base}}_C}{⨉}\left(r\left(x\right)\mathrm{Hom}\left(D\right)s\left(x\right)\right)|\forall x\in {\mathrm{Base}}_C\forall y\in {\mathrm{Base}}_C\forall z\in \left(x\mathrm{Hom}\left(C\right)y\right)a\left(y\right)\left(⟨r\left(x\right),r\left(y\right)⟩\mathrm{comp}\left(D\right)s\left(y\right)\right)\left(x{2}^{nd}\left(f\right)y\right)\left(z\right)=\left(x{2}^{nd}\left(g\right)y\right)\left(z\right)\left(⟨r\left(x\right),s\left(x\right)⟩\mathrm{comp}\left(D\right)s\left(y\right)\right)a\left(x\right)\right\}\in 𝒫\left({\bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)}^{{\mathrm{Base}}_C}\right)\right)$$
36	34 35	mpbid	$$⊢1^{st}\left(f\right)\in \mathrm{V}\to ⦋1^{st}\left(f\right)/r⦌⦋1^{st}\left(g\right)/s⦌\left\{a\in \underset{x\in {\mathrm{Base}}_C}{⨉}\left(r\left(x\right)\mathrm{Hom}\left(D\right)s\left(x\right)\right)|\forall x\in {\mathrm{Base}}_C\forall y\in {\mathrm{Base}}_C\forall z\in \left(x\mathrm{Hom}\left(C\right)y\right)a\left(y\right)\left(⟨r\left(x\right),r\left(y\right)⟩\mathrm{comp}\left(D\right)s\left(y\right)\right)\left(x{2}^{nd}\left(f\right)y\right)\left(z\right)=\left(x{2}^{nd}\left(g\right)y\right)\left(z\right)\left(⟨r\left(x\right),s\left(x\right)⟩\mathrm{comp}\left(D\right)s\left(y\right)\right)a\left(x\right)\right\}\in 𝒫\left({\bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)}^{{\mathrm{Base}}_C}\right)$$
37	14 36	ax-mp	$$⊢⦋1^{st}\left(f\right)/r⦌⦋1^{st}\left(g\right)/s⦌\left\{a\in \underset{x\in {\mathrm{Base}}_C}{⨉}\left(r\left(x\right)\mathrm{Hom}\left(D\right)s\left(x\right)\right)|\forall x\in {\mathrm{Base}}_C\forall y\in {\mathrm{Base}}_C\forall z\in \left(x\mathrm{Hom}\left(C\right)y\right)a\left(y\right)\left(⟨r\left(x\right),r\left(y\right)⟩\mathrm{comp}\left(D\right)s\left(y\right)\right)\left(x{2}^{nd}\left(f\right)y\right)\left(z\right)=\left(x{2}^{nd}\left(g\right)y\right)\left(z\right)\left(⟨r\left(x\right),s\left(x\right)⟩\mathrm{comp}\left(D\right)s\left(y\right)\right)a\left(x\right)\right\}\in 𝒫\left({\bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)}^{{\mathrm{Base}}_C}\right)$$
38	37	rgen2w	$$⊢\forall f\in \left(C\mathrm{Func}D\right)\forall g\in \left(C\mathrm{Func}D\right)⦋1^{st}\left(f\right)/r⦌⦋1^{st}\left(g\right)/s⦌\left\{a\in \underset{x\in {\mathrm{Base}}_C}{⨉}\left(r\left(x\right)\mathrm{Hom}\left(D\right)s\left(x\right)\right)|\forall x\in {\mathrm{Base}}_C\forall y\in {\mathrm{Base}}_C\forall z\in \left(x\mathrm{Hom}\left(C\right)y\right)a\left(y\right)\left(⟨r\left(x\right),r\left(y\right)⟩\mathrm{comp}\left(D\right)s\left(y\right)\right)\left(x{2}^{nd}\left(f\right)y\right)\left(z\right)=\left(x{2}^{nd}\left(g\right)y\right)\left(z\right)\left(⟨r\left(x\right),s\left(x\right)⟩\mathrm{comp}\left(D\right)s\left(y\right)\right)a\left(x\right)\right\}\in 𝒫\left({\bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)}^{{\mathrm{Base}}_C}\right)$$
39		eqid	$$⊢C\mathrm{Nat}D=C\mathrm{Nat}D$$
40		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
41		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
42		eqid	$$⊢\mathrm{Hom}\left(D\right)=\mathrm{Hom}\left(D\right)$$
43		eqid	$$⊢\mathrm{comp}\left(D\right)=\mathrm{comp}\left(D\right)$$
44	39 40 41 42 43	natfval	$$⊢C\mathrm{Nat}D=\left(f\in \left(C\mathrm{Func}D\right),g\in \left(C\mathrm{Func}D\right)⟼⦋1^{st}\left(f\right)/r⦌⦋1^{st}\left(g\right)/s⦌\left\{a\in \underset{x\in {\mathrm{Base}}_C}{⨉}\left(r\left(x\right)\mathrm{Hom}\left(D\right)s\left(x\right)\right)|\forall x\in {\mathrm{Base}}_C\forall y\in {\mathrm{Base}}_C\forall z\in \left(x\mathrm{Hom}\left(C\right)y\right)a\left(y\right)\left(⟨r\left(x\right),r\left(y\right)⟩\mathrm{comp}\left(D\right)s\left(y\right)\right)\left(x{2}^{nd}\left(f\right)y\right)\left(z\right)=\left(x{2}^{nd}\left(g\right)y\right)\left(z\right)\left(⟨r\left(x\right),s\left(x\right)⟩\mathrm{comp}\left(D\right)s\left(y\right)\right)a\left(x\right)\right\}\right)$$
45	44	fmpo	$$⊢\forall f\in \left(C\mathrm{Func}D\right)\forall g\in \left(C\mathrm{Func}D\right)⦋1^{st}\left(f\right)/r⦌⦋1^{st}\left(g\right)/s⦌\left\{a\in \underset{x\in {\mathrm{Base}}_C}{⨉}\left(r\left(x\right)\mathrm{Hom}\left(D\right)s\left(x\right)\right)|\forall x\in {\mathrm{Base}}_C\forall y\in {\mathrm{Base}}_C\forall z\in \left(x\mathrm{Hom}\left(C\right)y\right)a\left(y\right)\left(⟨r\left(x\right),r\left(y\right)⟩\mathrm{comp}\left(D\right)s\left(y\right)\right)\left(x{2}^{nd}\left(f\right)y\right)\left(z\right)=\left(x{2}^{nd}\left(g\right)y\right)\left(z\right)\left(⟨r\left(x\right),s\left(x\right)⟩\mathrm{comp}\left(D\right)s\left(y\right)\right)a\left(x\right)\right\}\in 𝒫\left({\bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)}^{{\mathrm{Base}}_C}\right)\leftrightarrow \left(C\mathrm{Nat}D\right):\left(C\mathrm{Func}D\right)\times \left(C\mathrm{Func}D\right)⟶𝒫\left({\bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)}^{{\mathrm{Base}}_C}\right)$$
46	38 45	mpbi	$$⊢\left(C\mathrm{Nat}D\right):\left(C\mathrm{Func}D\right)\times \left(C\mathrm{Func}D\right)⟶𝒫\left({\bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)}^{{\mathrm{Base}}_C}\right)$$
47	46	a1i	$$⊢\phi \to \left(C\mathrm{Nat}D\right):\left(C\mathrm{Func}D\right)\times \left(C\mathrm{Func}D\right)⟶𝒫\left({\bigcup \mathrm{ran}\mathrm{Hom}\left(D\right)}^{{\mathrm{Base}}_C}\right)$$
48	1 5 13 47	wunf	$$⊢\phi \to C\mathrm{Nat}D\in U$$