Step |
Hyp |
Ref |
Expression |
1 |
|
oyoncl.o |
|- O = ( oppCat ` C ) |
2 |
|
oyoncl.y |
|- Y = ( Yon ` O ) |
3 |
|
oyoncl.c |
|- ( ph -> C e. Cat ) |
4 |
|
oyoncl.s |
|- S = ( SetCat ` U ) |
5 |
|
oyoncl.u |
|- ( ph -> U e. V ) |
6 |
|
oyoncl.h |
|- ( ph -> ran ( Homf ` C ) C_ U ) |
7 |
|
oyoncl.q |
|- Q = ( C FuncCat S ) |
8 |
1
|
oppccat |
|- ( C e. Cat -> O e. Cat ) |
9 |
3 8
|
syl |
|- ( ph -> O e. Cat ) |
10 |
|
eqid |
|- ( oppCat ` O ) = ( oppCat ` O ) |
11 |
|
eqid |
|- ( ( oppCat ` O ) FuncCat S ) = ( ( oppCat ` O ) FuncCat S ) |
12 |
|
eqid |
|- ( Homf ` C ) = ( Homf ` C ) |
13 |
1 12
|
oppchomf |
|- tpos ( Homf ` C ) = ( Homf ` O ) |
14 |
13
|
rneqi |
|- ran tpos ( Homf ` C ) = ran ( Homf ` O ) |
15 |
|
relxp |
|- Rel ( ( Base ` C ) X. ( Base ` C ) ) |
16 |
|
eqid |
|- ( Base ` C ) = ( Base ` C ) |
17 |
12 16
|
homffn |
|- ( Homf ` C ) Fn ( ( Base ` C ) X. ( Base ` C ) ) |
18 |
17
|
fndmi |
|- dom ( Homf ` C ) = ( ( Base ` C ) X. ( Base ` C ) ) |
19 |
18
|
releqi |
|- ( Rel dom ( Homf ` C ) <-> Rel ( ( Base ` C ) X. ( Base ` C ) ) ) |
20 |
15 19
|
mpbir |
|- Rel dom ( Homf ` C ) |
21 |
|
rntpos |
|- ( Rel dom ( Homf ` C ) -> ran tpos ( Homf ` C ) = ran ( Homf ` C ) ) |
22 |
20 21
|
ax-mp |
|- ran tpos ( Homf ` C ) = ran ( Homf ` C ) |
23 |
14 22
|
eqtr3i |
|- ran ( Homf ` O ) = ran ( Homf ` C ) |
24 |
23 6
|
eqsstrid |
|- ( ph -> ran ( Homf ` O ) C_ U ) |
25 |
2 9 10 4 11 5 24
|
yoncl |
|- ( ph -> Y e. ( O Func ( ( oppCat ` O ) FuncCat S ) ) ) |
26 |
1
|
2oppchomf |
|- ( Homf ` C ) = ( Homf ` ( oppCat ` O ) ) |
27 |
26
|
a1i |
|- ( ph -> ( Homf ` C ) = ( Homf ` ( oppCat ` O ) ) ) |
28 |
1
|
2oppccomf |
|- ( comf ` C ) = ( comf ` ( oppCat ` O ) ) |
29 |
28
|
a1i |
|- ( ph -> ( comf ` C ) = ( comf ` ( oppCat ` O ) ) ) |
30 |
|
eqidd |
|- ( ph -> ( Homf ` S ) = ( Homf ` S ) ) |
31 |
|
eqidd |
|- ( ph -> ( comf ` S ) = ( comf ` S ) ) |
32 |
10
|
oppccat |
|- ( O e. Cat -> ( oppCat ` O ) e. Cat ) |
33 |
9 32
|
syl |
|- ( ph -> ( oppCat ` O ) e. Cat ) |
34 |
4
|
setccat |
|- ( U e. V -> S e. Cat ) |
35 |
5 34
|
syl |
|- ( ph -> S e. Cat ) |
36 |
27 29 30 31 3 33 35 35
|
fucpropd |
|- ( ph -> ( C FuncCat S ) = ( ( oppCat ` O ) FuncCat S ) ) |
37 |
7 36
|
eqtrid |
|- ( ph -> Q = ( ( oppCat ` O ) FuncCat S ) ) |
38 |
37
|
oveq2d |
|- ( ph -> ( O Func Q ) = ( O Func ( ( oppCat ` O ) FuncCat S ) ) ) |
39 |
25 38
|
eleqtrrd |
|- ( ph -> Y e. ( O Func Q ) ) |