# Metamath Proof Explorer

## 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)×\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}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\forall {z}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\phantom{\rule{.4em}{0ex}}{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}}\phantom{\rule{.4em}{0ex}}{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}}\phantom{\rule{.4em}{0ex}}{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}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\forall {z}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\phantom{\rule{.4em}{0ex}}{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}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\forall {z}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\phantom{\rule{.4em}{0ex}}{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
31 sbcel1g
32 30 31 mpbid
33 15 32 ax-mp
34 33 sbcth
35 sbcel1g
36 34 35 mpbid
37 14 36 ax-mp
38 37 rgen2w
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
45 44 fmpo
46 38 45 mpbi ${⊢}\left({C}\mathrm{Nat}{D}\right):\left({C}\mathrm{Func}{D}\right)×\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)×\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}$