Theorem oppfval2

Description: Value of the opposite functor. (Contributed by Zhi Wang, 13-Nov-2025)

	Ref	Expression
Assertion	oppfval2	Could not format assertion : No typesetting found for |- ( F e. ( C Func D ) -> ( oppFunc ` F ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		relfunc	$$⊢\mathrm{Rel}\left(C\mathrm{Func}D\right)$$
2		1st2nd	$$⊢\left(\mathrm{Rel}\left(C\mathrm{Func}D\right)\wedge F\in \left(C\mathrm{Func}D\right)\right)\to F=⟨1^{st}\left(F\right),2^{nd}\left(F\right)⟩$$
3	1 2	mpan	$$⊢F\in \left(C\mathrm{Func}D\right)\to F=⟨1^{st}\left(F\right),2^{nd}\left(F\right)⟩$$
4	3	fveq2d	Could not format ( F e. ( C Func D ) -> ( oppFunc ` F ) = ( oppFunc ` <. ( 1st ` F ) , ( 2nd ` F ) >. ) ) : No typesetting found for |- ( F e. ( C Func D ) -> ( oppFunc ` F ) = ( oppFunc ` <. ( 1st ` F ) , ( 2nd ` F ) >. ) ) with typecode |-
5		df-ov	Could not format ( ( 1st ` F ) oppFunc ( 2nd ` F ) ) = ( oppFunc ` <. ( 1st ` F ) , ( 2nd ` F ) >. ) : No typesetting found for |- ( ( 1st ` F ) oppFunc ( 2nd ` F ) ) = ( oppFunc ` <. ( 1st ` F ) , ( 2nd ` F ) >. ) with typecode |-
6	4 5	eqtr4di	Could not format ( F e. ( C Func D ) -> ( oppFunc ` F ) = ( ( 1st ` F ) oppFunc ( 2nd ` F ) ) ) : No typesetting found for |- ( F e. ( C Func D ) -> ( oppFunc ` F ) = ( ( 1st ` F ) oppFunc ( 2nd ` F ) ) ) with typecode |-
7		1st2ndbr	$$⊢\left(\mathrm{Rel}\left(C\mathrm{Func}D\right)\wedge F\in \left(C\mathrm{Func}D\right)\right)\to 1^{st}\left(F\right)\left(C\mathrm{Func}D\right)2^{nd}\left(F\right)$$
8	1 7	mpan	$$⊢F\in \left(C\mathrm{Func}D\right)\to 1^{st}\left(F\right)\left(C\mathrm{Func}D\right)2^{nd}\left(F\right)$$
9		oppfval	Could not format ( ( 1st ` F ) ( C Func D ) ( 2nd ` F ) -> ( ( 1st ` F ) oppFunc ( 2nd ` F ) ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. ) : No typesetting found for |- ( ( 1st ` F ) ( C Func D ) ( 2nd ` F ) -> ( ( 1st ` F ) oppFunc ( 2nd ` F ) ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. ) with typecode |-
10	8 9	syl	Could not format ( F e. ( C Func D ) -> ( ( 1st ` F ) oppFunc ( 2nd ` F ) ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. ) : No typesetting found for |- ( F e. ( C Func D ) -> ( ( 1st ` F ) oppFunc ( 2nd ` F ) ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. ) with typecode |-
11	6 10	eqtrd	Could not format ( F e. ( C Func D ) -> ( oppFunc ` F ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. ) : No typesetting found for |- ( F e. ( C Func D ) -> ( oppFunc ` F ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. ) with typecode |-