Metamath Proof Explorer

Theorem oppchomfval

Description: Hom-sets of the opposite category. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses oppchom.h 
|- H = ( Hom ` C )
oppchom.o 
|- O = ( oppCat ` C )
Assertion oppchomfval 
|- tpos H = ( Hom ` O )

Proof

Step Hyp Ref Expression
1 oppchom.h 
 |-  H = ( Hom ` C )
2 oppchom.o 
 |-  O = ( oppCat ` C )
3 homid 
 |-  Hom = Slot ( Hom ` ndx )
4 1nn0 
 |-  1 e. NN0
5 4nn 
 |-  4 e. NN
6 4 5 decnncl 
 |-  ; 1 4 e. NN
7 6 nnrei 
 |-  ; 1 4 e. RR
8 4nn0 
 |-  4 e. NN0
9 5nn 
 |-  5 e. NN
10 4lt5 
 |-  4 < 5
11 4 8 9 10 declt 
 |-  ; 1 4 < ; 1 5
12 7 11 ltneii 
 |-  ; 1 4 =/= ; 1 5
13 homndx 
 |-  ( Hom ` ndx ) = ; 1 4
14 ccondx 
 |-  ( comp ` ndx ) = ; 1 5
15 13 14 neeq12i 
 |-  ( ( Hom ` ndx ) =/= ( comp ` ndx ) <-> ; 1 4 =/= ; 1 5 )
16 12 15 mpbir 
 |-  ( Hom ` ndx ) =/= ( comp ` ndx )
17 3 16 setsnid 
 |-  ( Hom ` ( C sSet <. ( Hom ` ndx ) , tpos H >. ) ) = ( Hom ` ( ( C sSet <. ( Hom ` ndx ) , tpos H >. ) sSet <. ( comp ` ndx ) , ( u e. ( ( Base ` C ) X. ( Base ` C ) ) , z e. ( Base ` C ) |-> tpos ( <. z , ( 2nd ` u ) >. ( comp ` C ) ( 1st ` u ) ) ) >. ) )
18 1 fvexi 
 |-  H e. _V
19 18 tposex 
 |-  tpos H e. _V
20 3 setsid 
 |-  ( ( C e. _V /\ tpos H e. _V ) -> tpos H = ( Hom ` ( C sSet <. ( Hom ` ndx ) , tpos H >. ) ) )
21 19 20 mpan2 
 |-  ( C e. _V -> tpos H = ( Hom ` ( C sSet <. ( Hom ` ndx ) , tpos H >. ) ) )
22 eqid 
 |-  ( Base ` C ) = ( Base ` C )
23 eqid 
 |-  ( comp ` C ) = ( comp ` C )
24 22 1 23 2 oppcval 
 |-  ( C e. _V -> O = ( ( C sSet <. ( Hom ` ndx ) , tpos H >. ) sSet <. ( comp ` ndx ) , ( u e. ( ( Base ` C ) X. ( Base ` C ) ) , z e. ( Base ` C ) |-> tpos ( <. z , ( 2nd ` u ) >. ( comp ` C ) ( 1st ` u ) ) ) >. ) )
25 24 fveq2d 
 |-  ( C e. _V -> ( Hom ` O ) = ( Hom ` ( ( C sSet <. ( Hom ` ndx ) , tpos H >. ) sSet <. ( comp ` ndx ) , ( u e. ( ( Base ` C ) X. ( Base ` C ) ) , z e. ( Base ` C ) |-> tpos ( <. z , ( 2nd ` u ) >. ( comp ` C ) ( 1st ` u ) ) ) >. ) ) )
26 17 21 25 3eqtr4a 
 |-  ( C e. _V -> tpos H = ( Hom ` O ) )
27 tpos0 
 |-  tpos (/) = (/)
28 fvprc 
 |-  ( -. C e. _V -> ( Hom ` C ) = (/) )
29 1 28 syl5eq 
 |-  ( -. C e. _V -> H = (/) )
30 29 tposeqd 
 |-  ( -. C e. _V -> tpos H = tpos (/) )
31 fvprc 
 |-  ( -. C e. _V -> ( oppCat ` C ) = (/) )
32 2 31 syl5eq 
 |-  ( -. C e. _V -> O = (/) )
33 32 fveq2d 
 |-  ( -. C e. _V -> ( Hom ` O ) = ( Hom ` (/) ) )
34 df-hom 
 |-  Hom = Slot ; 1 4
35 34 str0 
 |-  (/) = ( Hom ` (/) )
36 33 35 eqtr4di 
 |-  ( -. C e. _V -> ( Hom ` O ) = (/) )
37 27 30 36 3eqtr4a 
 |-  ( -. C e. _V -> tpos H = ( Hom ` O ) )
38 26 37 pm2.61i 
 |-  tpos H = ( Hom ` O )