# Metamath Proof Explorer

## Theorem catcfuccl

Description: The category of categories for a weak universe is closed under the functor category operation. (Contributed by Mario Carneiro, 12-Jan-2017)

Ref Expression
Hypotheses catcfuccl.c ${⊢}{C}=\mathrm{CatCat}\left({U}\right)$
catcfuccl.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
catcfuccl.o ${⊢}{Q}={X}\mathrm{FuncCat}{Y}$
catcfuccl.u ${⊢}{\phi }\to {U}\in \mathrm{WUni}$
catcfuccl.1 ${⊢}{\phi }\to \mathrm{\omega }\in {U}$
catcfuccl.x ${⊢}{\phi }\to {X}\in {B}$
catcfuccl.y ${⊢}{\phi }\to {Y}\in {B}$
Assertion catcfuccl ${⊢}{\phi }\to {Q}\in {B}$

### Proof

Step Hyp Ref Expression
1 catcfuccl.c ${⊢}{C}=\mathrm{CatCat}\left({U}\right)$
2 catcfuccl.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
3 catcfuccl.o ${⊢}{Q}={X}\mathrm{FuncCat}{Y}$
4 catcfuccl.u ${⊢}{\phi }\to {U}\in \mathrm{WUni}$
5 catcfuccl.1 ${⊢}{\phi }\to \mathrm{\omega }\in {U}$
6 catcfuccl.x ${⊢}{\phi }\to {X}\in {B}$
7 catcfuccl.y ${⊢}{\phi }\to {Y}\in {B}$
8 eqid ${⊢}{X}\mathrm{Func}{Y}={X}\mathrm{Func}{Y}$
9 eqid ${⊢}{X}\mathrm{Nat}{Y}={X}\mathrm{Nat}{Y}$
10 eqid ${⊢}{\mathrm{Base}}_{{X}}={\mathrm{Base}}_{{X}}$
11 eqid ${⊢}\mathrm{comp}\left({Y}\right)=\mathrm{comp}\left({Y}\right)$
12 1 2 4 catcbas ${⊢}{\phi }\to {B}={U}\cap \mathrm{Cat}$
13 6 12 eleqtrd ${⊢}{\phi }\to {X}\in \left({U}\cap \mathrm{Cat}\right)$
14 13 elin2d ${⊢}{\phi }\to {X}\in \mathrm{Cat}$
15 7 12 eleqtrd ${⊢}{\phi }\to {Y}\in \left({U}\cap \mathrm{Cat}\right)$
16 15 elin2d ${⊢}{\phi }\to {Y}\in \mathrm{Cat}$
17 eqidd
18 3 8 9 10 11 14 16 17 fucval
19 df-base ${⊢}\mathrm{Base}=\mathrm{Slot}1$
20 4 5 wunndx ${⊢}{\phi }\to \mathrm{ndx}\in {U}$
21 19 4 20 wunstr ${⊢}{\phi }\to {\mathrm{Base}}_{\mathrm{ndx}}\in {U}$
22 13 elin1d ${⊢}{\phi }\to {X}\in {U}$
23 15 elin1d ${⊢}{\phi }\to {Y}\in {U}$
24 4 22 23 wunfunc ${⊢}{\phi }\to {X}\mathrm{Func}{Y}\in {U}$
25 4 21 24 wunop ${⊢}{\phi }\to ⟨{\mathrm{Base}}_{\mathrm{ndx}},{X}\mathrm{Func}{Y}⟩\in {U}$
26 df-hom ${⊢}\mathrm{Hom}=\mathrm{Slot}14$
27 26 4 20 wunstr ${⊢}{\phi }\to \mathrm{Hom}\left(\mathrm{ndx}\right)\in {U}$
28 4 22 23 wunnat ${⊢}{\phi }\to {X}\mathrm{Nat}{Y}\in {U}$
29 4 27 28 wunop ${⊢}{\phi }\to ⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{X}\mathrm{Nat}{Y}⟩\in {U}$
30 df-cco ${⊢}\mathrm{comp}=\mathrm{Slot}15$
31 30 4 20 wunstr ${⊢}{\phi }\to \mathrm{comp}\left(\mathrm{ndx}\right)\in {U}$
32 4 24 24 wunxp ${⊢}{\phi }\to \left({X}\mathrm{Func}{Y}\right)×\left({X}\mathrm{Func}{Y}\right)\in {U}$
33 4 32 24 wunxp ${⊢}{\phi }\to \left(\left({X}\mathrm{Func}{Y}\right)×\left({X}\mathrm{Func}{Y}\right)\right)×\left({X}\mathrm{Func}{Y}\right)\in {U}$
34 30 4 23 wunstr ${⊢}{\phi }\to \mathrm{comp}\left({Y}\right)\in {U}$
35 4 34 wunrn ${⊢}{\phi }\to \mathrm{ran}\mathrm{comp}\left({Y}\right)\in {U}$
36 4 35 wununi ${⊢}{\phi }\to \bigcup \mathrm{ran}\mathrm{comp}\left({Y}\right)\in {U}$
37 4 36 wunrn ${⊢}{\phi }\to \mathrm{ran}\bigcup \mathrm{ran}\mathrm{comp}\left({Y}\right)\in {U}$
38 4 37 wununi ${⊢}{\phi }\to \bigcup \mathrm{ran}\bigcup \mathrm{ran}\mathrm{comp}\left({Y}\right)\in {U}$
39 4 38 wunpw ${⊢}{\phi }\to 𝒫\bigcup \mathrm{ran}\bigcup \mathrm{ran}\mathrm{comp}\left({Y}\right)\in {U}$
40 19 4 22 wunstr ${⊢}{\phi }\to {\mathrm{Base}}_{{X}}\in {U}$
41 4 39 40 wunmap ${⊢}{\phi }\to {𝒫\bigcup \mathrm{ran}\bigcup \mathrm{ran}\mathrm{comp}\left({Y}\right)}^{{\mathrm{Base}}_{{X}}}\in {U}$
42 4 28 wunrn ${⊢}{\phi }\to \mathrm{ran}\left({X}\mathrm{Nat}{Y}\right)\in {U}$
43 4 42 wununi ${⊢}{\phi }\to \bigcup \mathrm{ran}\left({X}\mathrm{Nat}{Y}\right)\in {U}$
44 4 43 43 wunxp ${⊢}{\phi }\to \bigcup \mathrm{ran}\left({X}\mathrm{Nat}{Y}\right)×\bigcup \mathrm{ran}\left({X}\mathrm{Nat}{Y}\right)\in {U}$
45 4 41 44 wunpm ${⊢}{\phi }\to \left({𝒫\bigcup \mathrm{ran}\bigcup \mathrm{ran}\mathrm{comp}\left({Y}\right)}^{{\mathrm{Base}}_{{X}}}\right){↑}_{𝑝𝑚}\left(\bigcup \mathrm{ran}\left({X}\mathrm{Nat}{Y}\right)×\bigcup \mathrm{ran}\left({X}\mathrm{Nat}{Y}\right)\right)\in {U}$
46 fvex ${⊢}{1}^{st}\left({v}\right)\in \mathrm{V}$
47 fvex ${⊢}{2}^{nd}\left({v}\right)\in \mathrm{V}$
48 ovex ${⊢}{𝒫\bigcup \mathrm{ran}\bigcup \mathrm{ran}\mathrm{comp}\left({Y}\right)}^{{\mathrm{Base}}_{{X}}}\in \mathrm{V}$
49 ovex ${⊢}{X}\mathrm{Nat}{Y}\in \mathrm{V}$
50 49 rnex ${⊢}\mathrm{ran}\left({X}\mathrm{Nat}{Y}\right)\in \mathrm{V}$
51 50 uniex ${⊢}\bigcup \mathrm{ran}\left({X}\mathrm{Nat}{Y}\right)\in \mathrm{V}$
52 51 51 xpex ${⊢}\bigcup \mathrm{ran}\left({X}\mathrm{Nat}{Y}\right)×\bigcup \mathrm{ran}\left({X}\mathrm{Nat}{Y}\right)\in \mathrm{V}$
53 eqid ${⊢}\left({x}\in {\mathrm{Base}}_{{X}}⟼{b}\left({x}\right)\left(⟨{1}^{st}\left({f}\right)\left({x}\right),{1}^{st}\left({g}\right)\left({x}\right)⟩\mathrm{comp}\left({Y}\right){1}^{st}\left({h}\right)\left({x}\right)\right){a}\left({x}\right)\right)=\left({x}\in {\mathrm{Base}}_{{X}}⟼{b}\left({x}\right)\left(⟨{1}^{st}\left({f}\right)\left({x}\right),{1}^{st}\left({g}\right)\left({x}\right)⟩\mathrm{comp}\left({Y}\right){1}^{st}\left({h}\right)\left({x}\right)\right){a}\left({x}\right)\right)$
54 ovssunirn ${⊢}{b}\left({x}\right)\left(⟨{1}^{st}\left({f}\right)\left({x}\right),{1}^{st}\left({g}\right)\left({x}\right)⟩\mathrm{comp}\left({Y}\right){1}^{st}\left({h}\right)\left({x}\right)\right){a}\left({x}\right)\subseteq \bigcup \mathrm{ran}\left(⟨{1}^{st}\left({f}\right)\left({x}\right),{1}^{st}\left({g}\right)\left({x}\right)⟩\mathrm{comp}\left({Y}\right){1}^{st}\left({h}\right)\left({x}\right)\right)$
55 ovssunirn ${⊢}⟨{1}^{st}\left({f}\right)\left({x}\right),{1}^{st}\left({g}\right)\left({x}\right)⟩\mathrm{comp}\left({Y}\right){1}^{st}\left({h}\right)\left({x}\right)\subseteq \bigcup \mathrm{ran}\mathrm{comp}\left({Y}\right)$
56 rnss ${⊢}⟨{1}^{st}\left({f}\right)\left({x}\right),{1}^{st}\left({g}\right)\left({x}\right)⟩\mathrm{comp}\left({Y}\right){1}^{st}\left({h}\right)\left({x}\right)\subseteq \bigcup \mathrm{ran}\mathrm{comp}\left({Y}\right)\to \mathrm{ran}\left(⟨{1}^{st}\left({f}\right)\left({x}\right),{1}^{st}\left({g}\right)\left({x}\right)⟩\mathrm{comp}\left({Y}\right){1}^{st}\left({h}\right)\left({x}\right)\right)\subseteq \mathrm{ran}\bigcup \mathrm{ran}\mathrm{comp}\left({Y}\right)$
57 uniss ${⊢}\mathrm{ran}\left(⟨{1}^{st}\left({f}\right)\left({x}\right),{1}^{st}\left({g}\right)\left({x}\right)⟩\mathrm{comp}\left({Y}\right){1}^{st}\left({h}\right)\left({x}\right)\right)\subseteq \mathrm{ran}\bigcup \mathrm{ran}\mathrm{comp}\left({Y}\right)\to \bigcup \mathrm{ran}\left(⟨{1}^{st}\left({f}\right)\left({x}\right),{1}^{st}\left({g}\right)\left({x}\right)⟩\mathrm{comp}\left({Y}\right){1}^{st}\left({h}\right)\left({x}\right)\right)\subseteq \bigcup \mathrm{ran}\bigcup \mathrm{ran}\mathrm{comp}\left({Y}\right)$
58 55 56 57 mp2b ${⊢}\bigcup \mathrm{ran}\left(⟨{1}^{st}\left({f}\right)\left({x}\right),{1}^{st}\left({g}\right)\left({x}\right)⟩\mathrm{comp}\left({Y}\right){1}^{st}\left({h}\right)\left({x}\right)\right)\subseteq \bigcup \mathrm{ran}\bigcup \mathrm{ran}\mathrm{comp}\left({Y}\right)$
59 54 58 sstri ${⊢}{b}\left({x}\right)\left(⟨{1}^{st}\left({f}\right)\left({x}\right),{1}^{st}\left({g}\right)\left({x}\right)⟩\mathrm{comp}\left({Y}\right){1}^{st}\left({h}\right)\left({x}\right)\right){a}\left({x}\right)\subseteq \bigcup \mathrm{ran}\bigcup \mathrm{ran}\mathrm{comp}\left({Y}\right)$
60 ovex ${⊢}{b}\left({x}\right)\left(⟨{1}^{st}\left({f}\right)\left({x}\right),{1}^{st}\left({g}\right)\left({x}\right)⟩\mathrm{comp}\left({Y}\right){1}^{st}\left({h}\right)\left({x}\right)\right){a}\left({x}\right)\in \mathrm{V}$
61 60 elpw ${⊢}{b}\left({x}\right)\left(⟨{1}^{st}\left({f}\right)\left({x}\right),{1}^{st}\left({g}\right)\left({x}\right)⟩\mathrm{comp}\left({Y}\right){1}^{st}\left({h}\right)\left({x}\right)\right){a}\left({x}\right)\in 𝒫\bigcup \mathrm{ran}\bigcup \mathrm{ran}\mathrm{comp}\left({Y}\right)↔{b}\left({x}\right)\left(⟨{1}^{st}\left({f}\right)\left({x}\right),{1}^{st}\left({g}\right)\left({x}\right)⟩\mathrm{comp}\left({Y}\right){1}^{st}\left({h}\right)\left({x}\right)\right){a}\left({x}\right)\subseteq \bigcup \mathrm{ran}\bigcup \mathrm{ran}\mathrm{comp}\left({Y}\right)$
62 59 61 mpbir ${⊢}{b}\left({x}\right)\left(⟨{1}^{st}\left({f}\right)\left({x}\right),{1}^{st}\left({g}\right)\left({x}\right)⟩\mathrm{comp}\left({Y}\right){1}^{st}\left({h}\right)\left({x}\right)\right){a}\left({x}\right)\in 𝒫\bigcup \mathrm{ran}\bigcup \mathrm{ran}\mathrm{comp}\left({Y}\right)$
63 62 a1i ${⊢}{x}\in {\mathrm{Base}}_{{X}}\to {b}\left({x}\right)\left(⟨{1}^{st}\left({f}\right)\left({x}\right),{1}^{st}\left({g}\right)\left({x}\right)⟩\mathrm{comp}\left({Y}\right){1}^{st}\left({h}\right)\left({x}\right)\right){a}\left({x}\right)\in 𝒫\bigcup \mathrm{ran}\bigcup \mathrm{ran}\mathrm{comp}\left({Y}\right)$
64 53 63 fmpti ${⊢}\left({x}\in {\mathrm{Base}}_{{X}}⟼{b}\left({x}\right)\left(⟨{1}^{st}\left({f}\right)\left({x}\right),{1}^{st}\left({g}\right)\left({x}\right)⟩\mathrm{comp}\left({Y}\right){1}^{st}\left({h}\right)\left({x}\right)\right){a}\left({x}\right)\right):{\mathrm{Base}}_{{X}}⟶𝒫\bigcup \mathrm{ran}\bigcup \mathrm{ran}\mathrm{comp}\left({Y}\right)$
65 fvex ${⊢}\mathrm{comp}\left({Y}\right)\in \mathrm{V}$
66 65 rnex ${⊢}\mathrm{ran}\mathrm{comp}\left({Y}\right)\in \mathrm{V}$
67 66 uniex ${⊢}\bigcup \mathrm{ran}\mathrm{comp}\left({Y}\right)\in \mathrm{V}$
68 67 rnex ${⊢}\mathrm{ran}\bigcup \mathrm{ran}\mathrm{comp}\left({Y}\right)\in \mathrm{V}$
69 68 uniex ${⊢}\bigcup \mathrm{ran}\bigcup \mathrm{ran}\mathrm{comp}\left({Y}\right)\in \mathrm{V}$
70 69 pwex ${⊢}𝒫\bigcup \mathrm{ran}\bigcup \mathrm{ran}\mathrm{comp}\left({Y}\right)\in \mathrm{V}$
71 fvex ${⊢}{\mathrm{Base}}_{{X}}\in \mathrm{V}$
72 70 71 elmap ${⊢}\left({x}\in {\mathrm{Base}}_{{X}}⟼{b}\left({x}\right)\left(⟨{1}^{st}\left({f}\right)\left({x}\right),{1}^{st}\left({g}\right)\left({x}\right)⟩\mathrm{comp}\left({Y}\right){1}^{st}\left({h}\right)\left({x}\right)\right){a}\left({x}\right)\right)\in \left({𝒫\bigcup \mathrm{ran}\bigcup \mathrm{ran}\mathrm{comp}\left({Y}\right)}^{{\mathrm{Base}}_{{X}}}\right)↔\left({x}\in {\mathrm{Base}}_{{X}}⟼{b}\left({x}\right)\left(⟨{1}^{st}\left({f}\right)\left({x}\right),{1}^{st}\left({g}\right)\left({x}\right)⟩\mathrm{comp}\left({Y}\right){1}^{st}\left({h}\right)\left({x}\right)\right){a}\left({x}\right)\right):{\mathrm{Base}}_{{X}}⟶𝒫\bigcup \mathrm{ran}\bigcup \mathrm{ran}\mathrm{comp}\left({Y}\right)$
73 64 72 mpbir ${⊢}\left({x}\in {\mathrm{Base}}_{{X}}⟼{b}\left({x}\right)\left(⟨{1}^{st}\left({f}\right)\left({x}\right),{1}^{st}\left({g}\right)\left({x}\right)⟩\mathrm{comp}\left({Y}\right){1}^{st}\left({h}\right)\left({x}\right)\right){a}\left({x}\right)\right)\in \left({𝒫\bigcup \mathrm{ran}\bigcup \mathrm{ran}\mathrm{comp}\left({Y}\right)}^{{\mathrm{Base}}_{{X}}}\right)$
74 73 rgen2w ${⊢}\forall {b}\in \left({g}\left({X}\mathrm{Nat}{Y}\right){h}\right)\phantom{\rule{.4em}{0ex}}\forall {a}\in \left({f}\left({X}\mathrm{Nat}{Y}\right){g}\right)\phantom{\rule{.4em}{0ex}}\left({x}\in {\mathrm{Base}}_{{X}}⟼{b}\left({x}\right)\left(⟨{1}^{st}\left({f}\right)\left({x}\right),{1}^{st}\left({g}\right)\left({x}\right)⟩\mathrm{comp}\left({Y}\right){1}^{st}\left({h}\right)\left({x}\right)\right){a}\left({x}\right)\right)\in \left({𝒫\bigcup \mathrm{ran}\bigcup \mathrm{ran}\mathrm{comp}\left({Y}\right)}^{{\mathrm{Base}}_{{X}}}\right)$
75 eqid ${⊢}\left({b}\in \left({g}\left({X}\mathrm{Nat}{Y}\right){h}\right),{a}\in \left({f}\left({X}\mathrm{Nat}{Y}\right){g}\right)⟼\left({x}\in {\mathrm{Base}}_{{X}}⟼{b}\left({x}\right)\left(⟨{1}^{st}\left({f}\right)\left({x}\right),{1}^{st}\left({g}\right)\left({x}\right)⟩\mathrm{comp}\left({Y}\right){1}^{st}\left({h}\right)\left({x}\right)\right){a}\left({x}\right)\right)\right)=\left({b}\in \left({g}\left({X}\mathrm{Nat}{Y}\right){h}\right),{a}\in \left({f}\left({X}\mathrm{Nat}{Y}\right){g}\right)⟼\left({x}\in {\mathrm{Base}}_{{X}}⟼{b}\left({x}\right)\left(⟨{1}^{st}\left({f}\right)\left({x}\right),{1}^{st}\left({g}\right)\left({x}\right)⟩\mathrm{comp}\left({Y}\right){1}^{st}\left({h}\right)\left({x}\right)\right){a}\left({x}\right)\right)\right)$
76 75 fmpo ${⊢}\forall {b}\in \left({g}\left({X}\mathrm{Nat}{Y}\right){h}\right)\phantom{\rule{.4em}{0ex}}\forall {a}\in \left({f}\left({X}\mathrm{Nat}{Y}\right){g}\right)\phantom{\rule{.4em}{0ex}}\left({x}\in {\mathrm{Base}}_{{X}}⟼{b}\left({x}\right)\left(⟨{1}^{st}\left({f}\right)\left({x}\right),{1}^{st}\left({g}\right)\left({x}\right)⟩\mathrm{comp}\left({Y}\right){1}^{st}\left({h}\right)\left({x}\right)\right){a}\left({x}\right)\right)\in \left({𝒫\bigcup \mathrm{ran}\bigcup \mathrm{ran}\mathrm{comp}\left({Y}\right)}^{{\mathrm{Base}}_{{X}}}\right)↔\left({b}\in \left({g}\left({X}\mathrm{Nat}{Y}\right){h}\right),{a}\in \left({f}\left({X}\mathrm{Nat}{Y}\right){g}\right)⟼\left({x}\in {\mathrm{Base}}_{{X}}⟼{b}\left({x}\right)\left(⟨{1}^{st}\left({f}\right)\left({x}\right),{1}^{st}\left({g}\right)\left({x}\right)⟩\mathrm{comp}\left({Y}\right){1}^{st}\left({h}\right)\left({x}\right)\right){a}\left({x}\right)\right)\right):\left({g}\left({X}\mathrm{Nat}{Y}\right){h}\right)×\left({f}\left({X}\mathrm{Nat}{Y}\right){g}\right)⟶{𝒫\bigcup \mathrm{ran}\bigcup \mathrm{ran}\mathrm{comp}\left({Y}\right)}^{{\mathrm{Base}}_{{X}}}$
77 74 76 mpbi ${⊢}\left({b}\in \left({g}\left({X}\mathrm{Nat}{Y}\right){h}\right),{a}\in \left({f}\left({X}\mathrm{Nat}{Y}\right){g}\right)⟼\left({x}\in {\mathrm{Base}}_{{X}}⟼{b}\left({x}\right)\left(⟨{1}^{st}\left({f}\right)\left({x}\right),{1}^{st}\left({g}\right)\left({x}\right)⟩\mathrm{comp}\left({Y}\right){1}^{st}\left({h}\right)\left({x}\right)\right){a}\left({x}\right)\right)\right):\left({g}\left({X}\mathrm{Nat}{Y}\right){h}\right)×\left({f}\left({X}\mathrm{Nat}{Y}\right){g}\right)⟶{𝒫\bigcup \mathrm{ran}\bigcup \mathrm{ran}\mathrm{comp}\left({Y}\right)}^{{\mathrm{Base}}_{{X}}}$
78 ovssunirn ${⊢}{g}\left({X}\mathrm{Nat}{Y}\right){h}\subseteq \bigcup \mathrm{ran}\left({X}\mathrm{Nat}{Y}\right)$
79 ovssunirn ${⊢}{f}\left({X}\mathrm{Nat}{Y}\right){g}\subseteq \bigcup \mathrm{ran}\left({X}\mathrm{Nat}{Y}\right)$
80 xpss12 ${⊢}\left({g}\left({X}\mathrm{Nat}{Y}\right){h}\subseteq \bigcup \mathrm{ran}\left({X}\mathrm{Nat}{Y}\right)\wedge {f}\left({X}\mathrm{Nat}{Y}\right){g}\subseteq \bigcup \mathrm{ran}\left({X}\mathrm{Nat}{Y}\right)\right)\to \left({g}\left({X}\mathrm{Nat}{Y}\right){h}\right)×\left({f}\left({X}\mathrm{Nat}{Y}\right){g}\right)\subseteq \bigcup \mathrm{ran}\left({X}\mathrm{Nat}{Y}\right)×\bigcup \mathrm{ran}\left({X}\mathrm{Nat}{Y}\right)$
81 78 79 80 mp2an ${⊢}\left({g}\left({X}\mathrm{Nat}{Y}\right){h}\right)×\left({f}\left({X}\mathrm{Nat}{Y}\right){g}\right)\subseteq \bigcup \mathrm{ran}\left({X}\mathrm{Nat}{Y}\right)×\bigcup \mathrm{ran}\left({X}\mathrm{Nat}{Y}\right)$
82 elpm2r ${⊢}\left(\left({𝒫\bigcup \mathrm{ran}\bigcup \mathrm{ran}\mathrm{comp}\left({Y}\right)}^{{\mathrm{Base}}_{{X}}}\in \mathrm{V}\wedge \bigcup \mathrm{ran}\left({X}\mathrm{Nat}{Y}\right)×\bigcup \mathrm{ran}\left({X}\mathrm{Nat}{Y}\right)\in \mathrm{V}\right)\wedge \left(\left({b}\in \left({g}\left({X}\mathrm{Nat}{Y}\right){h}\right),{a}\in \left({f}\left({X}\mathrm{Nat}{Y}\right){g}\right)⟼\left({x}\in {\mathrm{Base}}_{{X}}⟼{b}\left({x}\right)\left(⟨{1}^{st}\left({f}\right)\left({x}\right),{1}^{st}\left({g}\right)\left({x}\right)⟩\mathrm{comp}\left({Y}\right){1}^{st}\left({h}\right)\left({x}\right)\right){a}\left({x}\right)\right)\right):\left({g}\left({X}\mathrm{Nat}{Y}\right){h}\right)×\left({f}\left({X}\mathrm{Nat}{Y}\right){g}\right)⟶{𝒫\bigcup \mathrm{ran}\bigcup \mathrm{ran}\mathrm{comp}\left({Y}\right)}^{{\mathrm{Base}}_{{X}}}\wedge \left({g}\left({X}\mathrm{Nat}{Y}\right){h}\right)×\left({f}\left({X}\mathrm{Nat}{Y}\right){g}\right)\subseteq \bigcup \mathrm{ran}\left({X}\mathrm{Nat}{Y}\right)×\bigcup \mathrm{ran}\left({X}\mathrm{Nat}{Y}\right)\right)\right)\to \left({b}\in \left({g}\left({X}\mathrm{Nat}{Y}\right){h}\right),{a}\in \left({f}\left({X}\mathrm{Nat}{Y}\right){g}\right)⟼\left({x}\in {\mathrm{Base}}_{{X}}⟼{b}\left({x}\right)\left(⟨{1}^{st}\left({f}\right)\left({x}\right),{1}^{st}\left({g}\right)\left({x}\right)⟩\mathrm{comp}\left({Y}\right){1}^{st}\left({h}\right)\left({x}\right)\right){a}\left({x}\right)\right)\right)\in \left(\left({𝒫\bigcup \mathrm{ran}\bigcup \mathrm{ran}\mathrm{comp}\left({Y}\right)}^{{\mathrm{Base}}_{{X}}}\right){↑}_{𝑝𝑚}\left(\bigcup \mathrm{ran}\left({X}\mathrm{Nat}{Y}\right)×\bigcup \mathrm{ran}\left({X}\mathrm{Nat}{Y}\right)\right)\right)$
83 48 52 77 81 82 mp4an ${⊢}\left({b}\in \left({g}\left({X}\mathrm{Nat}{Y}\right){h}\right),{a}\in \left({f}\left({X}\mathrm{Nat}{Y}\right){g}\right)⟼\left({x}\in {\mathrm{Base}}_{{X}}⟼{b}\left({x}\right)\left(⟨{1}^{st}\left({f}\right)\left({x}\right),{1}^{st}\left({g}\right)\left({x}\right)⟩\mathrm{comp}\left({Y}\right){1}^{st}\left({h}\right)\left({x}\right)\right){a}\left({x}\right)\right)\right)\in \left(\left({𝒫\bigcup \mathrm{ran}\bigcup \mathrm{ran}\mathrm{comp}\left({Y}\right)}^{{\mathrm{Base}}_{{X}}}\right){↑}_{𝑝𝑚}\left(\bigcup \mathrm{ran}\left({X}\mathrm{Nat}{Y}\right)×\bigcup \mathrm{ran}\left({X}\mathrm{Nat}{Y}\right)\right)\right)$
84 83 sbcth
85 sbcel1g
86 84 85 mpbid
87 47 86 ax-mp
88 87 sbcth
89 sbcel1g
90 88 89 mpbid
91 46 90 ax-mp
92 91 rgen2w
93 eqid
94 93 fmpo
95 92 94 mpbi
96 95 a1i
97 4 33 45 96 wunf
98 4 31 97 wunop
99 4 25 29 98 wuntp
100 18 99 eqeltrd ${⊢}{\phi }\to {Q}\in {U}$
101 3 14 16 fuccat ${⊢}{\phi }\to {Q}\in \mathrm{Cat}$
102 100 101 elind ${⊢}{\phi }\to {Q}\in \left({U}\cap \mathrm{Cat}\right)$
103 102 12 eleqtrrd ${⊢}{\phi }\to {Q}\in {B}$