Metamath Proof Explorer

Theorem oppchofcl

Description: Closure of the opposite Hom functor. (Contributed by Mario Carneiro, 17-Jan-2017)

Ref Expression
Hypotheses oppchofcl.o 
|- O = ( oppCat ` C )
oppchofcl.m 
|- M = ( HomF ` O )
oppchofcl.d 
|- D = ( SetCat ` U )
oppchofcl.c 
|- ( ph -> C e. Cat )
oppchofcl.u 
|- ( ph -> U e. V )
oppchofcl.h 
|- ( ph -> ran ( Homf ` C ) C_ U )
Assertion oppchofcl 
|- ( ph -> M e. ( ( C Xc. O ) Func D ) )

Proof

Step Hyp Ref Expression
1 oppchofcl.o 
 |-  O = ( oppCat ` C )
2 oppchofcl.m 
 |-  M = ( HomF ` O )
3 oppchofcl.d 
 |-  D = ( SetCat ` U )
4 oppchofcl.c 
 |-  ( ph -> C e. Cat )
5 oppchofcl.u 
 |-  ( ph -> U e. V )
6 oppchofcl.h 
 |-  ( ph -> ran ( Homf ` C ) C_ U )
7 eqid 
 |-  ( oppCat ` O ) = ( oppCat ` O )
8 1 oppccat 
 |-  ( C e. Cat -> O e. Cat )
9 4 8 syl 
 |-  ( ph -> O e. Cat )
10 eqid 
 |-  ( Homf ` C ) = ( Homf ` C )
11 1 10 oppchomf 
 |-  tpos ( Homf ` C ) = ( Homf ` O )
12 11 rneqi 
 |-  ran tpos ( Homf ` C ) = ran ( Homf ` O )
13 relxp 
 |-  Rel ( ( Base ` C ) X. ( Base ` C ) )
14 eqid 
 |-  ( Base ` C ) = ( Base ` C )
15 10 14 homffn 
 |-  ( Homf ` C ) Fn ( ( Base ` C ) X. ( Base ` C ) )
16 15 fndmi 
 |-  dom ( Homf ` C ) = ( ( Base ` C ) X. ( Base ` C ) )
17 16 releqi 
 |-  ( Rel dom ( Homf ` C ) <-> Rel ( ( Base ` C ) X. ( Base ` C ) ) )
18 13 17 mpbir 
 |-  Rel dom ( Homf ` C )
19 rntpos 
 |-  ( Rel dom ( Homf ` C ) -> ran tpos ( Homf ` C ) = ran ( Homf ` C ) )
20 18 19 ax-mp 
 |-  ran tpos ( Homf ` C ) = ran ( Homf ` C )
21 12 20 eqtr3i 
 |-  ran ( Homf ` O ) = ran ( Homf ` C )
22 21 6 eqsstrid 
 |-  ( ph -> ran ( Homf ` O ) C_ U )
23 2 7 3 9 5 22 hofcl 
 |-  ( ph -> M e. ( ( ( oppCat ` O ) Xc. O ) Func D ) )
24 1 2oppchomf 
 |-  ( Homf ` C ) = ( Homf ` ( oppCat ` O ) )
25 24 a1i 
 |-  ( ph -> ( Homf ` C ) = ( Homf ` ( oppCat ` O ) ) )
26 1 2oppccomf 
 |-  ( comf ` C ) = ( comf ` ( oppCat ` O ) )
27 26 a1i 
 |-  ( ph -> ( comf ` C ) = ( comf ` ( oppCat ` O ) ) )
28 eqidd 
 |-  ( ph -> ( Homf ` O ) = ( Homf ` O ) )
29 eqidd 
 |-  ( ph -> ( comf ` O ) = ( comf ` O ) )
30 7 oppccat 
 |-  ( O e. Cat -> ( oppCat ` O ) e. Cat )
31 9 30 syl 
 |-  ( ph -> ( oppCat ` O ) e. Cat )
32 25 27 28 29 4 31 9 9 xpcpropd 
 |-  ( ph -> ( C Xc. O ) = ( ( oppCat ` O ) Xc. O ) )
33 32 oveq1d 
 |-  ( ph -> ( ( C Xc. O ) Func D ) = ( ( ( oppCat ` O ) Xc. O ) Func D ) )
34 23 33 eleqtrrd 
 |-  ( ph -> M e. ( ( C Xc. O ) Func D ) )