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) (Proof shortened by AV, 14-Oct-2024)

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 baseid 
 |-  Base = Slot ( Base ` ndx )
22 4 5 wunndx 
 |-  ( ph -> ndx e. U )
23 21 4 22 wunstr 
 |-  ( ph -> ( Base ` ndx ) e. U )
24 1 2 4 6 catcbaselcl 
 |-  ( ph -> ( Base ` X ) e. U )
25 1 2 4 7 catcbaselcl 
 |-  ( ph -> ( Base ` Y ) e. U )
26 4 24 25 wunxp 
 |-  ( ph -> ( ( Base ` X ) X. ( Base ` Y ) ) e. U )
27 4 23 26 wunop 
 |-  ( ph -> <. ( Base ` ndx ) , ( ( Base ` X ) X. ( Base ` Y ) ) >. e. U )
28 homid 
 |-  Hom = Slot ( Hom ` ndx )
29 28 4 22 wunstr 
 |-  ( ph -> ( Hom ` ndx ) e. U )
30 4 26 26 wunxp 
 |-  ( ph -> ( ( ( Base ` X ) X. ( Base ` Y ) ) X. ( ( Base ` X ) X. ( Base ` Y ) ) ) e. U )
31 1 2 4 6 catchomcl 
 |-  ( ph -> ( Hom ` X ) e. U )
32 4 31 wunrn 
 |-  ( ph -> ran ( Hom ` X ) e. U )
33 4 32 wununi 
 |-  ( ph -> U. ran ( Hom ` X ) e. U )
34 1 2 4 7 catchomcl 
 |-  ( ph -> ( Hom ` Y ) e. U )
35 4 34 wunrn 
 |-  ( ph -> ran ( Hom ` Y ) e. U )
36 4 35 wununi 
 |-  ( ph -> U. ran ( Hom ` Y ) e. U )
37 4 33 36 wunxp 
 |-  ( ph -> ( U. ran ( Hom ` X ) X. U. ran ( Hom ` Y ) ) e. U )
38 4 37 wunpw 
 |-  ( ph -> ~P ( U. ran ( Hom ` X ) X. U. ran ( Hom ` Y ) ) e. U )
39 ovssunirn 
 |-  ( ( 1st ` u ) ( Hom ` X ) ( 1st ` v ) ) C_ U. ran ( Hom ` X )
40 ovssunirn 
 |-  ( ( 2nd ` u ) ( Hom ` Y ) ( 2nd ` v ) ) C_ U. ran ( Hom ` Y )
41 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 ) ) )
42 39 40 41 mp2an 
 |-  ( ( ( 1st ` u ) ( Hom ` X ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` Y ) ( 2nd ` v ) ) ) C_ ( U. ran ( Hom ` X ) X. U. ran ( Hom ` Y ) )
43 ovex 
 |-  ( ( 1st ` u ) ( Hom ` X ) ( 1st ` v ) ) e. _V
44 ovex 
 |-  ( ( 2nd ` u ) ( Hom ` Y ) ( 2nd ` v ) ) e. _V
45 43 44 xpex 
 |-  ( ( ( 1st ` u ) ( Hom ` X ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` Y ) ( 2nd ` v ) ) ) e. _V
46 45 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 ) ) )
47 42 46 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 ) )
48 47 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 ) )
49 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 ) ) ) )
50 49 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 ) ) )
51 48 50 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 ) )
52 51 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 ) ) )
53 4 30 38 52 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 )
54 17 53 eqeltrid 
 |-  ( ph -> ( Hom ` T ) e. U )
55 4 29 54 wunop 
 |-  ( ph -> <. ( Hom ` ndx ) , ( Hom ` T ) >. e. U )
56 ccoid 
 |-  comp = Slot ( comp ` ndx )
57 56 4 22 wunstr 
 |-  ( ph -> ( comp ` ndx ) e. U )
58 4 30 26 wunxp 
 |-  ( ph -> ( ( ( ( Base ` X ) X. ( Base ` Y ) ) X. ( ( Base ` X ) X. ( Base ` Y ) ) ) X. ( ( Base ` X ) X. ( Base ` Y ) ) ) e. U )
59 1 2 4 6 catcccocl 
 |-  ( ph -> ( comp ` X ) e. U )
60 4 59 wunrn 
 |-  ( ph -> ran ( comp ` X ) e. U )
61 4 60 wununi 
 |-  ( ph -> U. ran ( comp ` X ) e. U )
62 4 61 wunrn 
 |-  ( ph -> ran U. ran ( comp ` X ) e. U )
63 4 62 wununi 
 |-  ( ph -> U. ran U. ran ( comp ` X ) e. U )
64 4 63 wunpw 
 |-  ( ph -> ~P U. ran U. ran ( comp ` X ) e. U )
65 1 2 4 7 catcccocl 
 |-  ( ph -> ( comp ` Y ) e. U )
66 4 65 wunrn 
 |-  ( ph -> ran ( comp ` Y ) e. U )
67 4 66 wununi 
 |-  ( ph -> U. ran ( comp ` Y ) e. U )
68 4 67 wunrn 
 |-  ( ph -> ran U. ran ( comp ` Y ) e. U )
69 4 68 wununi 
 |-  ( ph -> U. ran U. ran ( comp ` Y ) e. U )
70 4 69 wunpw 
 |-  ( ph -> ~P U. ran U. ran ( comp ` Y ) e. U )
71 4 64 70 wunxp 
 |-  ( ph -> ( ~P U. ran U. ran ( comp ` X ) X. ~P U. ran U. ran ( comp ` Y ) ) e. U )
72 4 54 wunrn 
 |-  ( ph -> ran ( Hom ` T ) e. U )
73 4 72 wununi 
 |-  ( ph -> U. ran ( Hom ` T ) e. U )
74 4 73 73 wunxp 
 |-  ( ph -> ( U. ran ( Hom ` T ) X. U. ran ( Hom ` T ) ) e. U )
75 4 71 74 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 )
76 fvex 
 |-  ( comp ` X ) e. _V
77 76 rnex 
 |-  ran ( comp ` X ) e. _V
78 77 uniex 
 |-  U. ran ( comp ` X ) e. _V
79 78 rnex 
 |-  ran U. ran ( comp ` X ) e. _V
80 79 uniex 
 |-  U. ran U. ran ( comp ` X ) e. _V
81 80 pwex 
 |-  ~P U. ran U. ran ( comp ` X ) e. _V
82 fvex 
 |-  ( comp ` Y ) e. _V
83 82 rnex 
 |-  ran ( comp ` Y ) e. _V
84 83 uniex 
 |-  U. ran ( comp ` Y ) e. _V
85 84 rnex 
 |-  ran U. ran ( comp ` Y ) e. _V
86 85 uniex 
 |-  U. ran U. ran ( comp ` Y ) e. _V
87 86 pwex 
 |-  ~P U. ran U. ran ( comp ` Y ) e. _V
88 81 87 xpex 
 |-  ( ~P U. ran U. ran ( comp ` X ) X. ~P U. ran U. ran ( comp ` Y ) ) e. _V
89 fvex 
 |-  ( Hom ` T ) e. _V
90 89 rnex 
 |-  ran ( Hom ` T ) e. _V
91 90 uniex 
 |-  U. ran ( Hom ` T ) e. _V
92 91 91 xpex 
 |-  ( U. ran ( Hom ` T ) X. U. ran ( Hom ` T ) ) e. _V
93 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 ) )
94 ovssunirn 
 |-  ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` X ) ( 1st ` y ) ) C_ U. ran ( comp ` X )
95 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 ) )
96 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 ) )
97 94 95 96 mp2b 
 |-  U. ran ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` X ) ( 1st ` y ) ) C_ U. ran U. ran ( comp ` X )
98 93 97 sstri 
 |-  ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` X ) ( 1st ` y ) ) ( 1st ` f ) ) C_ U. ran U. ran ( comp ` X )
99 ovex 
 |-  ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` X ) ( 1st ` y ) ) ( 1st ` f ) ) e. _V
100 99 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 ) )
101 98 100 mpbir 
 |-  ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` X ) ( 1st ` y ) ) ( 1st ` f ) ) e. ~P U. ran U. ran ( comp ` X )
102 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 ) )
103 ovssunirn 
 |-  ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` Y ) ( 2nd ` y ) ) C_ U. ran ( comp ` Y )
104 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 ) )
105 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 ) )
106 103 104 105 mp2b 
 |-  U. ran ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` Y ) ( 2nd ` y ) ) C_ U. ran U. ran ( comp ` Y )
107 102 106 sstri 
 |-  ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` Y ) ( 2nd ` y ) ) ( 2nd ` f ) ) C_ U. ran U. ran ( comp ` Y )
108 ovex 
 |-  ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` Y ) ( 2nd ` y ) ) ( 2nd ` f ) ) e. _V
109 108 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 ) )
110 107 109 mpbir 
 |-  ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` Y ) ( 2nd ` y ) ) ( 2nd ` f ) ) e. ~P U. ran U. ran ( comp ` Y )
111 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 ) ) )
112 101 110 111 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 ) )
113 112 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 ) )
114 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 ) ) >. )
115 114 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 ) ) )
116 113 115 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 ) )
117 ovssunirn 
 |-  ( ( 2nd ` x ) ( Hom ` T ) y ) C_ U. ran ( Hom ` T )
118 fvssunirn 
 |-  ( ( Hom ` T ) ` x ) C_ U. ran ( Hom ` T )
119 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 ) ) )
120 117 118 119 mp2an 
 |-  ( ( ( 2nd ` x ) ( Hom ` T ) y ) X. ( ( Hom ` T ) ` x ) ) C_ ( U. ran ( Hom ` T ) X. U. ran ( Hom ` T ) )
121 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 ) ) ) )
122 88 92 116 120 121 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 ) ) )
123 122 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 ) ) )
124 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 ) ) >. ) )
125 124 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 ) ) ) )
126 123 125 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 ) ) )
127 126 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 ) ) ) )
128 4 58 75 127 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 )
129 4 57 128 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 )
130 4 27 55 129 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 )
131 20 130 eqeltrd 
 |-  ( ph -> T e. U )
132 1 2 4 catcbas 
 |-  ( ph -> B = ( U i^i Cat ) )
133 6 132 eleqtrd 
 |-  ( ph -> X e. ( U i^i Cat ) )
134 133 elin2d 
 |-  ( ph -> X e. Cat )
135 7 132 eleqtrd 
 |-  ( ph -> Y e. ( U i^i Cat ) )
136 135 elin2d 
 |-  ( ph -> Y e. Cat )
137 3 134 136 xpccat 
 |-  ( ph -> T e. Cat )
138 131 137 elind 
 |-  ( ph -> T e. ( U i^i Cat ) )
139 138 132 eleqtrrd 
 |-  ( ph -> T e. B )