Metamath Proof Explorer


Theorem catcxpcclOLD

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

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