Metamath Proof Explorer

Theorem catcxpccl

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

Ref Expression
Hypotheses catcxpccl.c 
|- C = ( CatCat ` U )
catcxpccl.b 
|- B = ( Base ` C )
catcxpccl.o 
|- T = ( X Xc. Y )
catcxpccl.u 
|- ( ph -> U e. WUni )
catcxpccl.1 
|- ( ph -> _om e. U )
catcxpccl.x 
|- ( ph -> X e. B )
catcxpccl.y 
|- ( ph -> Y e. B )
Assertion catcxpccl 
|- ( ph -> T e. B )

Proof

Step Hyp Ref Expression
1 catcxpccl.c 
 |-  C = ( CatCat ` U )
2 catcxpccl.b 
 |-  B = ( Base ` C )
3 catcxpccl.o 
 |-  T = ( X Xc. Y )
4 catcxpccl.u 
 |-  ( ph -> U e. WUni )
5 catcxpccl.1 
 |-  ( ph -> _om e. U )
6 catcxpccl.x 
 |-  ( ph -> X e. B )
7 catcxpccl.y 
 |-  ( ph -> Y e. B )
8 eqid 
 |-  ( Base ` X ) = ( Base ` X )
9 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
10 eqid 
 |-  ( Hom ` X ) = ( Hom ` X )
11 eqid 
 |-  ( Hom ` Y ) = ( Hom ` Y )
12 eqid 
 |-  ( comp ` X ) = ( comp ` X )
13 eqid 
 |-  ( comp ` Y ) = ( comp ` Y )
14 eqidd 
 |-  ( ph -> ( ( Base ` X ) X. ( Base ` Y ) ) = ( ( Base ` X ) X. ( Base ` Y ) ) )
15 3 8 9 xpcbas 
 |-  ( ( Base ` X ) X. ( Base ` Y ) ) = ( Base ` T )
16 eqid 
 |-  ( Hom ` T ) = ( Hom ` T )
17 3 15 10 11 16 xpchomfval 
 |-  ( Hom ` T ) = ( u e. ( ( Base ` X ) X. ( Base ` Y ) ) , v e. ( ( Base ` X ) X. ( Base ` Y ) ) |-> ( ( ( 1st ` u ) ( Hom ` X ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` Y ) ( 2nd ` v ) ) ) )
18 17 a1i 
 |-  ( ph -> ( Hom ` T ) = ( u e. ( ( Base ` X ) X. ( Base ` Y ) ) , v e. ( ( Base ` X ) X. ( Base ` Y ) ) |-> ( ( ( 1st ` u ) ( Hom ` X ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` Y ) ( 2nd ` v ) ) ) ) )
19 eqidd 
 |-  ( ph -> ( x e. ( ( ( Base ` X ) X. ( Base ` Y ) ) X. ( ( Base ` X ) X. ( Base ` Y ) ) ) , y e. ( ( Base ` X ) X. ( Base ` Y ) ) |-> ( g e. ( ( 2nd ` x ) ( Hom ` T ) y ) , f e. ( ( Hom ` T ) ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` X ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` Y ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) ) = ( x e. ( ( ( Base ` X ) X. ( Base ` Y ) ) X. ( ( Base ` X ) X. ( Base ` Y ) ) ) , y e. ( ( Base ` X ) X. ( Base ` Y ) ) |-> ( g e. ( ( 2nd ` x ) ( Hom ` T ) y ) , f e. ( ( Hom ` T ) ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` X ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` Y ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) ) )
20 3 8 9 10 11 12 13 6 7 14 18 19 xpcval 
 |-  ( ph -> T = { <. ( Base ` ndx ) , ( ( Base ` X ) X. ( Base ` Y ) ) >. , <. ( Hom ` ndx ) , ( Hom ` T ) >. , <. ( comp ` ndx ) , ( x e. ( ( ( Base ` X ) X. ( Base ` Y ) ) X. ( ( Base ` X ) X. ( Base ` Y ) ) ) , y e. ( ( Base ` X ) X. ( Base ` Y ) ) |-> ( g e. ( ( 2nd ` x ) ( Hom ` T ) y ) , f e. ( ( Hom ` T ) ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` X ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` Y ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) ) >. } )
21 df-base 
 |-  Base = Slot 1
22 4 5 wunndx 
 |-  ( ph -> ndx e. U )
23 21 4 22 wunstr 
 |-  ( ph -> ( Base ` ndx ) e. U )
24 1 2 4 catcbas 
 |-  ( ph -> B = ( U i^i Cat ) )
25 6 24 eleqtrd 
 |-  ( ph -> X e. ( U i^i Cat ) )
26 25 elin1d 
 |-  ( ph -> X e. U )
27 21 4 26 wunstr 
 |-  ( ph -> ( Base ` X ) e. U )
28 7 24 eleqtrd 
 |-  ( ph -> Y e. ( U i^i Cat ) )
29 28 elin1d 
 |-  ( ph -> Y e. U )
30 21 4 29 wunstr 
 |-  ( ph -> ( Base ` Y ) e. U )
31 4 27 30 wunxp 
 |-  ( ph -> ( ( Base ` X ) X. ( Base ` Y ) ) e. U )
32 4 23 31 wunop 
 |-  ( ph -> <. ( Base ` ndx ) , ( ( Base ` X ) X. ( Base ` Y ) ) >. e. U )
33 df-hom 
 |-  Hom = Slot ; 1 4
34 33 4 22 wunstr 
 |-  ( ph -> ( Hom ` ndx ) e. U )
35 4 31 31 wunxp 
 |-  ( ph -> ( ( ( Base ` X ) X. ( Base ` Y ) ) X. ( ( Base ` X ) X. ( Base ` Y ) ) ) e. U )
36 33 4 26 wunstr 
 |-  ( ph -> ( Hom ` X ) e. U )
37 4 36 wunrn 
 |-  ( ph -> ran ( Hom ` X ) e. U )
38 4 37 wununi 
 |-  ( ph -> U. ran ( Hom ` X ) e. U )
39 33 4 29 wunstr 
 |-  ( ph -> ( Hom ` Y ) e. U )
40 4 39 wunrn 
 |-  ( ph -> ran ( Hom ` Y ) e. U )
41 4 40 wununi 
 |-  ( ph -> U. ran ( Hom ` Y ) e. U )
42 4 38 41 wunxp 
 |-  ( ph -> ( U. ran ( Hom ` X ) X. U. ran ( Hom ` Y ) ) e. U )
43 4 42 wunpw 
 |-  ( ph -> ~P ( U. ran ( Hom ` X ) X. U. ran ( Hom ` Y ) ) e. U )
44 ovssunirn 
 |-  ( ( 1st ` u ) ( Hom ` X ) ( 1st ` v ) ) C_ U. ran ( Hom ` X )
45 ovssunirn 
 |-  ( ( 2nd ` u ) ( Hom ` Y ) ( 2nd ` v ) ) C_ U. ran ( Hom ` Y )
46 xpss12 
 |-  ( ( ( ( 1st ` u ) ( Hom ` X ) ( 1st ` v ) ) C_ U. ran ( Hom ` X ) /\ ( ( 2nd ` u ) ( Hom ` Y ) ( 2nd ` v ) ) C_ U. ran ( Hom ` Y ) ) -> ( ( ( 1st ` u ) ( Hom ` X ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` Y ) ( 2nd ` v ) ) ) C_ ( U. ran ( Hom ` X ) X. U. ran ( Hom ` Y ) ) )
47 44 45 46 mp2an 
 |-  ( ( ( 1st ` u ) ( Hom ` X ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` Y ) ( 2nd ` v ) ) ) C_ ( U. ran ( Hom ` X ) X. U. ran ( Hom ` Y ) )
48 ovex 
 |-  ( ( 1st ` u ) ( Hom ` X ) ( 1st ` v ) ) e. _V
49 ovex 
 |-  ( ( 2nd ` u ) ( Hom ` Y ) ( 2nd ` v ) ) e. _V
50 48 49 xpex 
 |-  ( ( ( 1st ` u ) ( Hom ` X ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` Y ) ( 2nd ` v ) ) ) e. _V
51 50 elpw 
 |-  ( ( ( ( 1st ` u ) ( Hom ` X ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` Y ) ( 2nd ` v ) ) ) e. ~P ( U. ran ( Hom ` X ) X. U. ran ( Hom ` Y ) ) <-> ( ( ( 1st ` u ) ( Hom ` X ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` Y ) ( 2nd ` v ) ) ) C_ ( U. ran ( Hom ` X ) X. U. ran ( Hom ` Y ) ) )
52 47 51 mpbir 
 |-  ( ( ( 1st ` u ) ( Hom ` X ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` Y ) ( 2nd ` v ) ) ) e. ~P ( U. ran ( Hom ` X ) X. U. ran ( Hom ` Y ) )
53 52 rgen2w 
 |-  A. u e. ( ( Base ` X ) X. ( Base ` Y ) ) A. v e. ( ( Base ` X ) X. ( Base ` Y ) ) ( ( ( 1st ` u ) ( Hom ` X ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` Y ) ( 2nd ` v ) ) ) e. ~P ( U. ran ( Hom ` X ) X. U. ran ( Hom ` Y ) )
54 eqid 
 |-  ( u e. ( ( Base ` X ) X. ( Base ` Y ) ) , v e. ( ( Base ` X ) X. ( Base ` Y ) ) |-> ( ( ( 1st ` u ) ( Hom ` X ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` Y ) ( 2nd ` v ) ) ) ) = ( u e. ( ( Base ` X ) X. ( Base ` Y ) ) , v e. ( ( Base ` X ) X. ( Base ` Y ) ) |-> ( ( ( 1st ` u ) ( Hom ` X ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` Y ) ( 2nd ` v ) ) ) )
55 54 fmpo 
 |-  ( A. u e. ( ( Base ` X ) X. ( Base ` Y ) ) A. v e. ( ( Base ` X ) X. ( Base ` Y ) ) ( ( ( 1st ` u ) ( Hom ` X ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` Y ) ( 2nd ` v ) ) ) e. ~P ( U. ran ( Hom ` X ) X. U. ran ( Hom ` Y ) ) <-> ( u e. ( ( Base ` X ) X. ( Base ` Y ) ) , v e. ( ( Base ` X ) X. ( Base ` Y ) ) |-> ( ( ( 1st ` u ) ( Hom ` X ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` Y ) ( 2nd ` v ) ) ) ) : ( ( ( Base ` X ) X. ( Base ` Y ) ) X. ( ( Base ` X ) X. ( Base ` Y ) ) ) --> ~P ( U. ran ( Hom ` X ) X. U. ran ( Hom ` Y ) ) )
56 53 55 mpbi 
 |-  ( u e. ( ( Base ` X ) X. ( Base ` Y ) ) , v e. ( ( Base ` X ) X. ( Base ` Y ) ) |-> ( ( ( 1st ` u ) ( Hom ` X ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` Y ) ( 2nd ` v ) ) ) ) : ( ( ( Base ` X ) X. ( Base ` Y ) ) X. ( ( Base ` X ) X. ( Base ` Y ) ) ) --> ~P ( U. ran ( Hom ` X ) X. U. ran ( Hom ` Y ) )
57 56 a1i 
 |-  ( ph -> ( u e. ( ( Base ` X ) X. ( Base ` Y ) ) , v e. ( ( Base ` X ) X. ( Base ` Y ) ) |-> ( ( ( 1st ` u ) ( Hom ` X ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` Y ) ( 2nd ` v ) ) ) ) : ( ( ( Base ` X ) X. ( Base ` Y ) ) X. ( ( Base ` X ) X. ( Base ` Y ) ) ) --> ~P ( U. ran ( Hom ` X ) X. U. ran ( Hom ` Y ) ) )
58 4 35 43 57 wunf 
 |-  ( ph -> ( u e. ( ( Base ` X ) X. ( Base ` Y ) ) , v e. ( ( Base ` X ) X. ( Base ` Y ) ) |-> ( ( ( 1st ` u ) ( Hom ` X ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` Y ) ( 2nd ` v ) ) ) ) e. U )
59 17 58 eqeltrid 
 |-  ( ph -> ( Hom ` T ) e. U )
60 4 34 59 wunop 
 |-  ( ph -> <. ( Hom ` ndx ) , ( Hom ` T ) >. e. U )
61 df-cco 
 |-  comp = Slot ; 1 5
62 61 4 22 wunstr 
 |-  ( ph -> ( comp ` ndx ) e. U )
63 4 35 31 wunxp 
 |-  ( ph -> ( ( ( ( Base ` X ) X. ( Base ` Y ) ) X. ( ( Base ` X ) X. ( Base ` Y ) ) ) X. ( ( Base ` X ) X. ( Base ` Y ) ) ) e. U )
64 61 4 26 wunstr 
 |-  ( ph -> ( comp ` X ) e. U )
65 4 64 wunrn 
 |-  ( ph -> ran ( comp ` X ) e. U )
66 4 65 wununi 
 |-  ( ph -> U. ran ( comp ` X ) e. U )
67 4 66 wunrn 
 |-  ( ph -> ran U. ran ( comp ` X ) e. U )
68 4 67 wununi 
 |-  ( ph -> U. ran U. ran ( comp ` X ) e. U )
69 4 68 wunpw 
 |-  ( ph -> ~P U. ran U. ran ( comp ` X ) e. U )
70 61 4 29 wunstr 
 |-  ( ph -> ( comp ` Y ) e. U )
71 4 70 wunrn 
 |-  ( ph -> ran ( comp ` Y ) e. U )
72 4 71 wununi 
 |-  ( ph -> U. ran ( comp ` Y ) e. U )
73 4 72 wunrn 
 |-  ( ph -> ran U. ran ( comp ` Y ) e. U )
74 4 73 wununi 
 |-  ( ph -> U. ran U. ran ( comp ` Y ) e. U )
75 4 74 wunpw 
 |-  ( ph -> ~P U. ran U. ran ( comp ` Y ) e. U )
76 4 69 75 wunxp 
 |-  ( ph -> ( ~P U. ran U. ran ( comp ` X ) X. ~P U. ran U. ran ( comp ` Y ) ) e. U )
77 4 59 wunrn 
 |-  ( ph -> ran ( Hom ` T ) e. U )
78 4 77 wununi 
 |-  ( ph -> U. ran ( Hom ` T ) e. U )
79 4 78 78 wunxp 
 |-  ( ph -> ( U. ran ( Hom ` T ) X. U. ran ( Hom ` T ) ) e. U )
80 4 76 79 wunpm 
 |-  ( ph -> ( ( ~P U. ran U. ran ( comp ` X ) X. ~P U. ran U. ran ( comp ` Y ) ) ^pm ( U. ran ( Hom ` T ) X. U. ran ( Hom ` T ) ) ) e. U )
81 fvex 
 |-  ( comp ` X ) e. _V
82 81 rnex 
 |-  ran ( comp ` X ) e. _V
83 82 uniex 
 |-  U. ran ( comp ` X ) e. _V
84 83 rnex 
 |-  ran U. ran ( comp ` X ) e. _V
85 84 uniex 
 |-  U. ran U. ran ( comp ` X ) e. _V
86 85 pwex 
 |-  ~P U. ran U. ran ( comp ` X ) e. _V
87 fvex 
 |-  ( comp ` Y ) e. _V
88 87 rnex 
 |-  ran ( comp ` Y ) e. _V
89 88 uniex 
 |-  U. ran ( comp ` Y ) e. _V
90 89 rnex 
 |-  ran U. ran ( comp ` Y ) e. _V
91 90 uniex 
 |-  U. ran U. ran ( comp ` Y ) e. _V
92 91 pwex 
 |-  ~P U. ran U. ran ( comp ` Y ) e. _V
93 86 92 xpex 
 |-  ( ~P U. ran U. ran ( comp ` X ) X. ~P U. ran U. ran ( comp ` Y ) ) e. _V
94 fvex 
 |-  ( Hom ` T ) e. _V
95 94 rnex 
 |-  ran ( Hom ` T ) e. _V
96 95 uniex 
 |-  U. ran ( Hom ` T ) e. _V
97 96 96 xpex 
 |-  ( U. ran ( Hom ` T ) X. U. ran ( Hom ` T ) ) e. _V
98 ovssunirn 
 |-  ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` X ) ( 1st ` y ) ) ( 1st ` f ) ) C_ U. ran ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` X ) ( 1st ` y ) )
99 ovssunirn 
 |-  ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` X ) ( 1st ` y ) ) C_ U. ran ( comp ` X )
100 rnss 
 |-  ( ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` X ) ( 1st ` y ) ) C_ U. ran ( comp ` X ) -> ran ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` X ) ( 1st ` y ) ) C_ ran U. ran ( comp ` X ) )
101 uniss 
 |-  ( ran ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` X ) ( 1st ` y ) ) C_ ran U. ran ( comp ` X ) -> U. ran ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` X ) ( 1st ` y ) ) C_ U. ran U. ran ( comp ` X ) )
102 99 100 101 mp2b 
 |-  U. ran ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` X ) ( 1st ` y ) ) C_ U. ran U. ran ( comp ` X )
103 98 102 sstri 
 |-  ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` X ) ( 1st ` y ) ) ( 1st ` f ) ) C_ U. ran U. ran ( comp ` X )
104 ovex 
 |-  ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` X ) ( 1st ` y ) ) ( 1st ` f ) ) e. _V
105 104 elpw 
 |-  ( ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` X ) ( 1st ` y ) ) ( 1st ` f ) ) e. ~P U. ran U. ran ( comp ` X ) <-> ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` X ) ( 1st ` y ) ) ( 1st ` f ) ) C_ U. ran U. ran ( comp ` X ) )
106 103 105 mpbir 
 |-  ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` X ) ( 1st ` y ) ) ( 1st ` f ) ) e. ~P U. ran U. ran ( comp ` X )
107 ovssunirn 
 |-  ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` Y ) ( 2nd ` y ) ) ( 2nd ` f ) ) C_ U. ran ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` Y ) ( 2nd ` y ) )
108 ovssunirn 
 |-  ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` Y ) ( 2nd ` y ) ) C_ U. ran ( comp ` Y )
109 rnss 
 |-  ( ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` Y ) ( 2nd ` y ) ) C_ U. ran ( comp ` Y ) -> ran ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` Y ) ( 2nd ` y ) ) C_ ran U. ran ( comp ` Y ) )
110 uniss 
 |-  ( ran ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` Y ) ( 2nd ` y ) ) C_ ran U. ran ( comp ` Y ) -> U. ran ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` Y ) ( 2nd ` y ) ) C_ U. ran U. ran ( comp ` Y ) )
111 108 109 110 mp2b 
 |-  U. ran ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` Y ) ( 2nd ` y ) ) C_ U. ran U. ran ( comp ` Y )
112 107 111 sstri 
 |-  ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` Y ) ( 2nd ` y ) ) ( 2nd ` f ) ) C_ U. ran U. ran ( comp ` Y )
113 ovex 
 |-  ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` Y ) ( 2nd ` y ) ) ( 2nd ` f ) ) e. _V
114 113 elpw 
 |-  ( ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` Y ) ( 2nd ` y ) ) ( 2nd ` f ) ) e. ~P U. ran U. ran ( comp ` Y ) <-> ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` Y ) ( 2nd ` y ) ) ( 2nd ` f ) ) C_ U. ran U. ran ( comp ` Y ) )
115 112 114 mpbir 
 |-  ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` Y ) ( 2nd ` y ) ) ( 2nd ` f ) ) e. ~P U. ran U. ran ( comp ` Y )
116 opelxpi 
 |-  ( ( ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` X ) ( 1st ` y ) ) ( 1st ` f ) ) e. ~P U. ran U. ran ( comp ` X ) /\ ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` Y ) ( 2nd ` y ) ) ( 2nd ` f ) ) e. ~P U. ran U. ran ( comp ` Y ) ) -> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` X ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` Y ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. e. ( ~P U. ran U. ran ( comp ` X ) X. ~P U. ran U. ran ( comp ` Y ) ) )
117 106 115 116 mp2an 
 |-  <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` X ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` Y ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. e. ( ~P U. ran U. ran ( comp ` X ) X. ~P U. ran U. ran ( comp ` Y ) )
118 117 rgen2w 
 |-  A. g e. ( ( 2nd ` x ) ( Hom ` T ) y ) A. f e. ( ( Hom ` T ) ` x ) <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` X ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` Y ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. e. ( ~P U. ran U. ran ( comp ` X ) X. ~P U. ran U. ran ( comp ` Y ) )
119 eqid 
 |-  ( g e. ( ( 2nd ` x ) ( Hom ` T ) y ) , f e. ( ( Hom ` T ) ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` X ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` Y ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) = ( g e. ( ( 2nd ` x ) ( Hom ` T ) y ) , f e. ( ( Hom ` T ) ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` X ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` Y ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. )
120 119 fmpo 
 |-  ( A. g e. ( ( 2nd ` x ) ( Hom ` T ) y ) A. f e. ( ( Hom ` T ) ` x ) <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` X ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` Y ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. e. ( ~P U. ran U. ran ( comp ` X ) X. ~P U. ran U. ran ( comp ` Y ) ) <-> ( g e. ( ( 2nd ` x ) ( Hom ` T ) y ) , f e. ( ( Hom ` T ) ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` X ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` Y ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) : ( ( ( 2nd ` x ) ( Hom ` T ) y ) X. ( ( Hom ` T ) ` x ) ) --> ( ~P U. ran U. ran ( comp ` X ) X. ~P U. ran U. ran ( comp ` Y ) ) )
121 118 120 mpbi 
 |-  ( g e. ( ( 2nd ` x ) ( Hom ` T ) y ) , f e. ( ( Hom ` T ) ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` X ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` Y ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) : ( ( ( 2nd ` x ) ( Hom ` T ) y ) X. ( ( Hom ` T ) ` x ) ) --> ( ~P U. ran U. ran ( comp ` X ) X. ~P U. ran U. ran ( comp ` Y ) )
122 ovssunirn 
 |-  ( ( 2nd ` x ) ( Hom ` T ) y ) C_ U. ran ( Hom ` T )
123 fvssunirn 
 |-  ( ( Hom ` T ) ` x ) C_ U. ran ( Hom ` T )
124 xpss12 
 |-  ( ( ( ( 2nd ` x ) ( Hom ` T ) y ) C_ U. ran ( Hom ` T ) /\ ( ( Hom ` T ) ` x ) C_ U. ran ( Hom ` T ) ) -> ( ( ( 2nd ` x ) ( Hom ` T ) y ) X. ( ( Hom ` T ) ` x ) ) C_ ( U. ran ( Hom ` T ) X. U. ran ( Hom ` T ) ) )
125 122 123 124 mp2an 
 |-  ( ( ( 2nd ` x ) ( Hom ` T ) y ) X. ( ( Hom ` T ) ` x ) ) C_ ( U. ran ( Hom ` T ) X. U. ran ( Hom ` T ) )
126 elpm2r 
 |-  ( ( ( ( ~P U. ran U. ran ( comp ` X ) X. ~P U. ran U. ran ( comp ` Y ) ) e. _V /\ ( U. ran ( Hom ` T ) X. U. ran ( Hom ` T ) ) e. _V ) /\ ( ( g e. ( ( 2nd ` x ) ( Hom ` T ) y ) , f e. ( ( Hom ` T ) ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` X ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` Y ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) : ( ( ( 2nd ` x ) ( Hom ` T ) y ) X. ( ( Hom ` T ) ` x ) ) --> ( ~P U. ran U. ran ( comp ` X ) X. ~P U. ran U. ran ( comp ` Y ) ) /\ ( ( ( 2nd ` x ) ( Hom ` T ) y ) X. ( ( Hom ` T ) ` x ) ) C_ ( U. ran ( Hom ` T ) X. U. ran ( Hom ` T ) ) ) ) -> ( g e. ( ( 2nd ` x ) ( Hom ` T ) y ) , f e. ( ( Hom ` T ) ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` X ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` Y ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) e. ( ( ~P U. ran U. ran ( comp ` X ) X. ~P U. ran U. ran ( comp ` Y ) ) ^pm ( U. ran ( Hom ` T ) X. U. ran ( Hom ` T ) ) ) )
127 93 97 121 125 126 mp4an 
 |-  ( g e. ( ( 2nd ` x ) ( Hom ` T ) y ) , f e. ( ( Hom ` T ) ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` X ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` Y ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) e. ( ( ~P U. ran U. ran ( comp ` X ) X. ~P U. ran U. ran ( comp ` Y ) ) ^pm ( U. ran ( Hom ` T ) X. U. ran ( Hom ` T ) ) )
128 127 rgen2w 
 |-  A. x e. ( ( ( Base ` X ) X. ( Base ` Y ) ) X. ( ( Base ` X ) X. ( Base ` Y ) ) ) A. y e. ( ( Base ` X ) X. ( Base ` Y ) ) ( g e. ( ( 2nd ` x ) ( Hom ` T ) y ) , f e. ( ( Hom ` T ) ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` X ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` Y ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) e. ( ( ~P U. ran U. ran ( comp ` X ) X. ~P U. ran U. ran ( comp ` Y ) ) ^pm ( U. ran ( Hom ` T ) X. U. ran ( Hom ` T ) ) )
129 eqid 
 |-  ( x e. ( ( ( Base ` X ) X. ( Base ` Y ) ) X. ( ( Base ` X ) X. ( Base ` Y ) ) ) , y e. ( ( Base ` X ) X. ( Base ` Y ) ) |-> ( g e. ( ( 2nd ` x ) ( Hom ` T ) y ) , f e. ( ( Hom ` T ) ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` X ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` Y ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) ) = ( x e. ( ( ( Base ` X ) X. ( Base ` Y ) ) X. ( ( Base ` X ) X. ( Base ` Y ) ) ) , y e. ( ( Base ` X ) X. ( Base ` Y ) ) |-> ( g e. ( ( 2nd ` x ) ( Hom ` T ) y ) , f e. ( ( Hom ` T ) ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` X ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` Y ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) )
130 129 fmpo 
 |-  ( A. x e. ( ( ( Base ` X ) X. ( Base ` Y ) ) X. ( ( Base ` X ) X. ( Base ` Y ) ) ) A. y e. ( ( Base ` X ) X. ( Base ` Y ) ) ( g e. ( ( 2nd ` x ) ( Hom ` T ) y ) , f e. ( ( Hom ` T ) ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` X ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` Y ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) e. ( ( ~P U. ran U. ran ( comp ` X ) X. ~P U. ran U. ran ( comp ` Y ) ) ^pm ( U. ran ( Hom ` T ) X. U. ran ( Hom ` T ) ) ) <-> ( x e. ( ( ( Base ` X ) X. ( Base ` Y ) ) X. ( ( Base ` X ) X. ( Base ` Y ) ) ) , y e. ( ( Base ` X ) X. ( Base ` Y ) ) |-> ( g e. ( ( 2nd ` x ) ( Hom ` T ) y ) , f e. ( ( Hom ` T ) ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` X ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` Y ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) ) : ( ( ( ( Base ` X ) X. ( Base ` Y ) ) X. ( ( Base ` X ) X. ( Base ` Y ) ) ) X. ( ( Base ` X ) X. ( Base ` Y ) ) ) --> ( ( ~P U. ran U. ran ( comp ` X ) X. ~P U. ran U. ran ( comp ` Y ) ) ^pm ( U. ran ( Hom ` T ) X. U. ran ( Hom ` T ) ) ) )
131 128 130 mpbi 
 |-  ( x e. ( ( ( Base ` X ) X. ( Base ` Y ) ) X. ( ( Base ` X ) X. ( Base ` Y ) ) ) , y e. ( ( Base ` X ) X. ( Base ` Y ) ) |-> ( g e. ( ( 2nd ` x ) ( Hom ` T ) y ) , f e. ( ( Hom ` T ) ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` X ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` Y ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) ) : ( ( ( ( Base ` X ) X. ( Base ` Y ) ) X. ( ( Base ` X ) X. ( Base ` Y ) ) ) X. ( ( Base ` X ) X. ( Base ` Y ) ) ) --> ( ( ~P U. ran U. ran ( comp ` X ) X. ~P U. ran U. ran ( comp ` Y ) ) ^pm ( U. ran ( Hom ` T ) X. U. ran ( Hom ` T ) ) )
132 131 a1i 
 |-  ( ph -> ( x e. ( ( ( Base ` X ) X. ( Base ` Y ) ) X. ( ( Base ` X ) X. ( Base ` Y ) ) ) , y e. ( ( Base ` X ) X. ( Base ` Y ) ) |-> ( g e. ( ( 2nd ` x ) ( Hom ` T ) y ) , f e. ( ( Hom ` T ) ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` X ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` Y ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) ) : ( ( ( ( Base ` X ) X. ( Base ` Y ) ) X. ( ( Base ` X ) X. ( Base ` Y ) ) ) X. ( ( Base ` X ) X. ( Base ` Y ) ) ) --> ( ( ~P U. ran U. ran ( comp ` X ) X. ~P U. ran U. ran ( comp ` Y ) ) ^pm ( U. ran ( Hom ` T ) X. U. ran ( Hom ` T ) ) ) )
133 4 63 80 132 wunf 
 |-  ( ph -> ( x e. ( ( ( Base ` X ) X. ( Base ` Y ) ) X. ( ( Base ` X ) X. ( Base ` Y ) ) ) , y e. ( ( Base ` X ) X. ( Base ` Y ) ) |-> ( g e. ( ( 2nd ` x ) ( Hom ` T ) y ) , f e. ( ( Hom ` T ) ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` X ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` Y ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) ) e. U )
134 4 62 133 wunop 
 |-  ( ph -> <. ( comp ` ndx ) , ( x e. ( ( ( Base ` X ) X. ( Base ` Y ) ) X. ( ( Base ` X ) X. ( Base ` Y ) ) ) , y e. ( ( Base ` X ) X. ( Base ` Y ) ) |-> ( g e. ( ( 2nd ` x ) ( Hom ` T ) y ) , f e. ( ( Hom ` T ) ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` X ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` Y ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) ) >. e. U )
135 4 32 60 134 wuntp 
 |-  ( ph -> { <. ( Base ` ndx ) , ( ( Base ` X ) X. ( Base ` Y ) ) >. , <. ( Hom ` ndx ) , ( Hom ` T ) >. , <. ( comp ` ndx ) , ( x e. ( ( ( Base ` X ) X. ( Base ` Y ) ) X. ( ( Base ` X ) X. ( Base ` Y ) ) ) , y e. ( ( Base ` X ) X. ( Base ` Y ) ) |-> ( g e. ( ( 2nd ` x ) ( Hom ` T ) y ) , f e. ( ( Hom ` T ) ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` X ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` Y ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) ) >. } e. U )
136 20 135 eqeltrd 
 |-  ( ph -> T e. U )
137 25 elin2d 
 |-  ( ph -> X e. Cat )
138 28 elin2d 
 |-  ( ph -> Y e. Cat )
139 3 137 138 xpccat 
 |-  ( ph -> T e. Cat )
140 136 139 elind 
 |-  ( ph -> T e. ( U i^i Cat ) )
141 140 24 eleqtrrd 
 |-  ( ph -> T e. B )