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 = ( CatCat ` U )
catcfuccl.b 
|- B = ( Base ` C )
catcfuccl.o 
|- Q = ( X FuncCat Y )
catcfuccl.u 
|- ( ph -> U e. WUni )
catcfuccl.1 
|- ( ph -> _om e. U )
catcfuccl.x 
|- ( ph -> X e. B )
catcfuccl.y 
|- ( ph -> Y e. B )
Assertion catcfuccl 
|- ( ph -> Q e. B )

Proof

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