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	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	opf11	$$⊢\phi \to 1^{st}\left(F\left(X\right)\right)=1^{st}\left(X\right)$$

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	op1std	$$⊢F\left(X\right)=⟨1^{st}\left(X\right),tpos{2}^{nd}\left(X\right)⟩\to 1^{st}\left(F\left(X\right)\right)=1^{st}\left(X\right)$$
12	7 11	syl	$$⊢\phi \to 1^{st}\left(F\left(X\right)\right)=1^{st}\left(X\right)$$