Theorem oppffn

Description: oppFunc is a function on (V X. V ) . (Contributed by Zhi Wang, 17-Nov-2025)

	Ref	Expression
Assertion	oppffn	Could not format assertion : No typesetting found for |- oppFunc Fn ( _V X. _V ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		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 |-
2		opex	$$⊢⟨f,tposg⟩\in \mathrm{V}$$
3		0ex	$$⊢\varnothing \in \mathrm{V}$$
4	2 3	ifex	$$⊢if\left(\left(\mathrm{Rel}g\wedge \mathrm{Rel}\mathrm{dom}g\right),⟨f,tposg⟩,\varnothing \right)\in \mathrm{V}$$
5	1 4	fnmpoi	Could not format oppFunc Fn ( _V X. _V ) : No typesetting found for |- oppFunc Fn ( _V X. _V ) with typecode |-