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 × c Y
catcxpccl.u φ U WUni
catcxpccl.1 φ ω U
catcxpccl.x φ X B
catcxpccl.y φ Y B
Assertion catcxpcclOLD φ T B

Proof

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