Theorem oppfval

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

	Ref	Expression
Assertion	oppfval	Could not format assertion : No typesetting found for |- ( F ( C Func D ) G -> ( F oppFunc G ) = <. F , tpos G >. ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		relfunc	$$⊢\mathrm{Rel}\left(C\mathrm{Func}D\right)$$
2	1	brrelex12i	$$⊢F\left(C\mathrm{Func}D\right)G\to \left(F\in \mathrm{V}\wedge G\in \mathrm{V}\right)$$
3		simpl	$$⊢\left(f=F\wedge g=G\right)\to f=F$$
4		simpr	$$⊢\left(f=F\wedge g=G\right)\to g=G$$
5	4	tposeqd	$$⊢\left(f=F\wedge g=G\right)\to tposg=tposG$$
6	3 5	opeq12d	$$⊢\left(f=F\wedge g=G\right)\to ⟨f,tposg⟩=⟨F,tposG⟩$$
7		df-oppf	Could not format oppFunc = ( f e. _V , g e. _V |-> <. f , tpos g >. ) : No typesetting found for |- oppFunc = ( f e. _V , g e. _V |-> <. f , tpos g >. ) with typecode |-
8		opex	$$⊢⟨F,tposG⟩\in \mathrm{V}$$
9	6 7 8	ovmpoa	Could not format ( ( F e. _V /\ G e. _V ) -> ( F oppFunc G ) = <. F , tpos G >. ) : No typesetting found for |- ( ( F e. _V /\ G e. _V ) -> ( F oppFunc G ) = <. F , tpos G >. ) with typecode |-
10	2 9	syl	Could not format ( F ( C Func D ) G -> ( F oppFunc G ) = <. F , tpos G >. ) : No typesetting found for |- ( F ( C Func D ) G -> ( F oppFunc G ) = <. F , tpos G >. ) with typecode |-