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	$$⊢\phi \to X\in \left(C\mathrm{Func}D\right)$$
Assertion	opf12	$$⊢\phi \to M{2}^{nd}\left(F\left(X\right)\right)N=N{2}^{nd}\left(X\right)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	$$⊢\phi \to X\in \left(C\mathrm{Func}D\right)$$
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	$$⊢\phi \to F\left(X\right)=⟨1^{st}\left(X\right),tpos{2}^{nd}\left(X\right)⟩$$
8		fvex	$$⊢1^{st}\left(X\right)\in \mathrm{V}$$
9		fvex	$$⊢2^{nd}\left(X\right)\in \mathrm{V}$$
10	9	tposex	$$⊢tpos{2}^{nd}\left(X\right)\in \mathrm{V}$$
11	8 10	op2ndd	$$⊢F\left(X\right)=⟨1^{st}\left(X\right),tpos{2}^{nd}\left(X\right)⟩\to 2^{nd}\left(F\left(X\right)\right)=tpos{2}^{nd}\left(X\right)$$
12	7 11	syl	$$⊢\phi \to 2^{nd}\left(F\left(X\right)\right)=tpos{2}^{nd}\left(X\right)$$
13	12	oveqd	$$⊢\phi \to M{2}^{nd}\left(F\left(X\right)\right)N=Mtpos{2}^{nd}\left(X\right)N$$
14		ovtpos	$$⊢Mtpos{2}^{nd}\left(X\right)N=N{2}^{nd}\left(X\right)M$$
15	13 14	eqtrdi	$$⊢\phi \to M{2}^{nd}\left(F\left(X\right)\right)N=N{2}^{nd}\left(X\right)M$$