Metamath Proof Explorer

Theorem oppchomf

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

Ref Expression
Hypotheses oppcbas.1 
|- O = ( oppCat ` C )
oppchomf.h 
|- H = ( Homf ` C )
Assertion oppchomf 
|- tpos H = ( Homf ` O )

Proof

Step Hyp Ref Expression
1 oppcbas.1 
 |-  O = ( oppCat ` C )
2 oppchomf.h 
 |-  H = ( Homf ` C )
3 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
4 3 1 oppchom 
 |-  ( y ( Hom ` O ) x ) = ( x ( Hom ` C ) y )
5 4 a1i 
 |-  ( ( y e. ( Base ` C ) /\ x e. ( Base ` C ) ) -> ( y ( Hom ` O ) x ) = ( x ( Hom ` C ) y ) )
6 5 mpoeq3ia 
 |-  ( y e. ( Base ` C ) , x e. ( Base ` C ) |-> ( y ( Hom ` O ) x ) ) = ( y e. ( Base ` C ) , x e. ( Base ` C ) |-> ( x ( Hom ` C ) y ) )
7 eqid 
 |-  ( Homf ` O ) = ( Homf ` O )
8 eqid 
 |-  ( Base ` C ) = ( Base ` C )
9 1 8 oppcbas 
 |-  ( Base ` C ) = ( Base ` O )
10 eqid 
 |-  ( Hom ` O ) = ( Hom ` O )
11 7 9 10 homffval 
 |-  ( Homf ` O ) = ( y e. ( Base ` C ) , x e. ( Base ` C ) |-> ( y ( Hom ` O ) x ) )
12 2 8 3 homffval 
 |-  H = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( x ( Hom ` C ) y ) )
13 12 tposmpo 
 |-  tpos H = ( y e. ( Base ` C ) , x e. ( Base ` C ) |-> ( x ( Hom ` C ) y ) )
14 6 11 13 3eqtr4ri 
 |-  tpos H = ( Homf ` O )