Metamath Proof Explorer

Theorem opf11

Description: The object part of the op functor on functor categories. Lemma for fucoppc . (Contributed by Zhi Wang, 18-Nov-2025)

Ref Expression
Hypotheses opf11.f 
|- ( ph -> F = ( oppFunc |` ( C Func D ) ) )
opf11.x 
|- ( ph -> X e. ( C Func D ) )
Assertion opf11 
|- ( ph -> ( 1st ` ( F ` X ) ) = ( 1st ` X ) )

Proof

Step Hyp Ref Expression
1 opf11.f 
 |-  ( ph -> F = ( oppFunc |` ( C Func D ) ) )
2 opf11.x 
 |-  ( ph -> X e. ( C Func D ) )
3 1 fveq1d 
 |-  ( ph -> ( F ` X ) = ( ( oppFunc |` ( C Func D ) ) ` X ) )
4 2 fvresd 
 |-  ( ph -> ( ( oppFunc |` ( C Func D ) ) ` X ) = ( oppFunc ` X ) )
5 oppfval2 
 |-  ( X e. ( C Func D ) -> ( oppFunc ` X ) = <. ( 1st ` X ) , tpos ( 2nd ` X ) >. )
6 2 5 syl 
 |-  ( ph -> ( oppFunc ` X ) = <. ( 1st ` X ) , tpos ( 2nd ` X ) >. )
7 3 4 6 3eqtrd 
 |-  ( ph -> ( F ` X ) = <. ( 1st ` X ) , tpos ( 2nd ` X ) >. )
8 fvex 
 |-  ( 1st ` X ) e. _V
9 fvex 
 |-  ( 2nd ` X ) e. _V
10 9 tposex 
 |-  tpos ( 2nd ` X ) e. _V
11 8 10 op1std 
 |-  ( ( F ` X ) = <. ( 1st ` X ) , tpos ( 2nd ` X ) >. -> ( 1st ` ( F ` X ) ) = ( 1st ` X ) )
12 7 11 syl 
 |-  ( ph -> ( 1st ` ( F ` X ) ) = ( 1st ` X ) )