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

Metamath Proof Explorer

Theorem opf12

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

Ref Expression
Hypotheses opf11.f No typesetting found for |- ( ph -> F = ( oppFunc |` ( C Func D ) ) ) with typecode |-
opf11.x ⊢ φ → X ∈ C Func D
Assertion opf12 ⊢ φ → M 2 nd ⁡ F ⁡ X N = N 2 nd ⁡ X M

Proof

Step Hyp Ref Expression
1 opf11.f Could not format ( ph -> F = ( oppFunc |` ( C Func D ) ) ) : No typesetting found for |- ( ph -> F = ( oppFunc |` ( C Func D ) ) ) with typecode |-
2 opf11.x ⊢ φ → X ∈ C Func D
3 1 fveq1d Could not format ( ph -> ( F ` X ) = ( ( oppFunc |` ( C Func D ) ) ` X ) ) : No typesetting found for |- ( ph -> ( F ` X ) = ( ( oppFunc |` ( C Func D ) ) ` X ) ) with typecode |-
4 2 fvresd Could not format ( ph -> ( ( oppFunc |` ( C Func D ) ) ` X ) = ( oppFunc ` X ) ) : No typesetting found for |- ( ph -> ( ( oppFunc |` ( C Func D ) ) ` X ) = ( oppFunc ` X ) ) with typecode |-
5 oppfval2 Could not format ( X e. ( C Func D ) -> ( oppFunc ` X ) = <. ( 1st ` X ) , tpos ( 2nd ` X ) >. ) : No typesetting found for |- ( X e. ( C Func D ) -> ( oppFunc ` X ) = <. ( 1st ` X ) , tpos ( 2nd ` X ) >. ) with typecode |-
6 2 5 syl Could not format ( ph -> ( oppFunc ` X ) = <. ( 1st ` X ) , tpos ( 2nd ` X ) >. ) : No typesetting found for |- ( ph -> ( oppFunc ` X ) = <. ( 1st ` X ) , tpos ( 2nd ` X ) >. ) with typecode |-
7 3 4 6 3eqtrd ⊢ φ → F ⁡ X = 1 st ⁡ X tpos 2 nd ⁡ X
8 fvex ⊢ 1 st ⁡ X ∈ V
9 fvex ⊢ 2 nd ⁡ X ∈ V
10 9 tposex ⊢ tpos 2 nd ⁡ X ∈ V
11 8 10 op2ndd ⊢ F ⁡ X = 1 st ⁡ X tpos 2 nd ⁡ X → 2 nd ⁡ F ⁡ X = tpos 2 nd ⁡ X
12 7 11 syl ⊢ φ → 2 nd ⁡ F ⁡ X = tpos 2 nd ⁡ X
13 12 oveqd ⊢ φ → M 2 nd ⁡ F ⁡ X N = M tpos 2 nd ⁡ X N
14 ovtpos ⊢ M tpos 2 nd ⁡ X N = N 2 nd ⁡ X M
15 13 14 eqtrdi ⊢ φ → M 2 nd ⁡ F ⁡ X N = N 2 nd ⁡ X M