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		oppfvalg	Could not format ( ( F e. _V /\ G e. _V ) -> ( F oppFunc G ) = if ( ( Rel G /\ Rel dom G ) , <. F , tpos G >. , (/) ) ) : No typesetting found for |- ( ( F e. _V /\ G e. _V ) -> ( F oppFunc G ) = if ( ( Rel G /\ Rel dom G ) , <. F , tpos G >. , (/) ) ) with typecode |-
4	2 3	syl	Could not format ( F ( C Func D ) G -> ( F oppFunc G ) = if ( ( Rel G /\ Rel dom G ) , <. F , tpos G >. , (/) ) ) : No typesetting found for |- ( F ( C Func D ) G -> ( F oppFunc G ) = if ( ( Rel G /\ Rel dom G ) , <. F , tpos G >. , (/) ) ) with typecode |-
5		oppfvallem	$$⊢F\left(C\mathrm{Func}D\right)G\to \left(\mathrm{Rel}G\wedge \mathrm{Rel}\mathrm{dom}G\right)$$
6	5	iftrued	$$⊢F\left(C\mathrm{Func}D\right)G\to if\left(\left(\mathrm{Rel}G\wedge \mathrm{Rel}\mathrm{dom}G\right),⟨F,tposG⟩,\varnothing \right)=⟨F,tposG⟩$$
7	4 6	eqtrd	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 |-