Metamath Proof Explorer


Theorem catcfucclOLD

Description: Obsolete proof of catcfuccl as of 14-Oct-2024. (Contributed by Mario Carneiro, 12-Jan-2017) (Proof modification is discouraged.) (New usage is discouraged.)

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 catcfucclOLD
|- ( 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 )