This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem oppchomfval

Description: Hom-sets of the opposite category. (Contributed by Mario Carneiro, 2-Jan-2017) (Proof shortened by AV, 14-Oct-2024)

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 slotsbhcdif 
 |-  ( ( Base ` ndx ) =/= ( Hom ` ndx ) /\ ( Base ` ndx ) =/= ( comp ` ndx ) /\ ( Hom ` ndx ) =/= ( comp ` ndx ) )
5 4 simp3i 
 |-  ( Hom ` ndx ) =/= ( comp ` ndx )
6 3 5 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 ) ) ) >. ) )
7 1 fvexi 
 |-  H e. _V
8 7 tposex 
 |-  tpos H e. _V
9 3 setsid 
 |-  ( ( C e. _V /\ tpos H e. _V ) -> tpos H = ( Hom ` ( C sSet <. ( Hom ` ndx ) , tpos H >. ) ) )
10 8 9 mpan2 
 |-  ( C e. _V -> tpos H = ( Hom ` ( C sSet <. ( Hom ` ndx ) , tpos H >. ) ) )
11 eqid 
 |-  ( Base ` C ) = ( Base ` C )
12 eqid 
 |-  ( comp ` C ) = ( comp ` C )
13 11 1 12 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 ) ) ) >. ) )
14 13 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 ) ) ) >. ) ) )
15 6 10 14 3eqtr4a 
 |-  ( C e. _V -> tpos H = ( Hom ` O ) )
16 tpos0 
 |-  tpos (/) = (/)
17 fvprc 
 |-  ( -. C e. _V -> ( Hom ` C ) = (/) )
18 1 17 eqtrid 
 |-  ( -. C e. _V -> H = (/) )
19 18 tposeqd 
 |-  ( -. C e. _V -> tpos H = tpos (/) )
20 fvprc 
 |-  ( -. C e. _V -> ( oppCat ` C ) = (/) )
21 2 20 eqtrid 
 |-  ( -. C e. _V -> O = (/) )
22 21 fveq2d 
 |-  ( -. C e. _V -> ( Hom ` O ) = ( Hom ` (/) ) )
23 3 str0 
 |-  (/) = ( Hom ` (/) )
24 22 23 eqtr4di 
 |-  ( -. C e. _V -> ( Hom ` O ) = (/) )
25 16 19 24 3eqtr4a 
 |-  ( -. C e. _V -> tpos H = ( Hom ` O ) )
26 15 25 pm2.61i 
 |-  tpos H = ( Hom ` O )