Theorem oppfvalg

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

	Ref	Expression
Assertion	oppfvalg	Could not format assertion : No typesetting found for |- ( ( F e. _V /\ G e. _V ) -> ( F oppFunc G ) = if ( ( Rel G /\ Rel dom G ) , <. F , tpos G >. , (/) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		simpr	$$⊢\left(f=F\wedge g=G\right)\to g=G$$
2	1	releqd	$$⊢\left(f=F\wedge g=G\right)\to \left(\mathrm{Rel}g\leftrightarrow \mathrm{Rel}G\right)$$
3	1	dmeqd	$$⊢\left(f=F\wedge g=G\right)\to \mathrm{dom}g=\mathrm{dom}G$$
4	3	releqd	$$⊢\left(f=F\wedge g=G\right)\to \left(\mathrm{Rel}\mathrm{dom}g\leftrightarrow \mathrm{Rel}\mathrm{dom}G\right)$$
5	2 4	anbi12d	$$⊢\left(f=F\wedge g=G\right)\to \left(\left(\mathrm{Rel}g\wedge \mathrm{Rel}\mathrm{dom}g\right)\leftrightarrow \left(\mathrm{Rel}G\wedge \mathrm{Rel}\mathrm{dom}G\right)\right)$$
6		simpl	$$⊢\left(f=F\wedge g=G\right)\to f=F$$
7	1	tposeqd	$$⊢\left(f=F\wedge g=G\right)\to tposg=tposG$$
8	6 7	opeq12d	$$⊢\left(f=F\wedge g=G\right)\to ⟨f,tposg⟩=⟨F,tposG⟩$$
9	5 8	ifbieq1d	$$⊢\left(f=F\wedge g=G\right)\to if\left(\left(\mathrm{Rel}g\wedge \mathrm{Rel}\mathrm{dom}g\right),⟨f,tposg⟩,\varnothing \right)=if\left(\left(\mathrm{Rel}G\wedge \mathrm{Rel}\mathrm{dom}G\right),⟨F,tposG⟩,\varnothing \right)$$
10		df-oppf	Could not format oppFunc = ( f e. _V , g e. _V |-> if ( ( Rel g /\ Rel dom g ) , <. f , tpos g >. , (/) ) ) : No typesetting found for |- oppFunc = ( f e. _V , g e. _V |-> if ( ( Rel g /\ Rel dom g ) , <. f , tpos g >. , (/) ) ) with typecode |-
11		opex	$$⊢⟨F,tposG⟩\in \mathrm{V}$$
12		0ex	$$⊢\varnothing \in \mathrm{V}$$
13	11 12	ifex	$$⊢if\left(\left(\mathrm{Rel}G\wedge \mathrm{Rel}\mathrm{dom}G\right),⟨F,tposG⟩,\varnothing \right)\in \mathrm{V}$$
14	9 10 13	ovmpoa	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 |-