Theorem oppffn

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

	Ref	Expression
Assertion	oppffn	⊢ oppFunc Fn ( V × V )

Proof

Step	Hyp	Ref	Expression
1		df-oppf	⊢ oppFunc = ( 𝑓 ∈ V , 𝑔 ∈ V ↦ if ( ( Rel 𝑔 ∧ Rel dom 𝑔 ) , ⟨ 𝑓 , tpos 𝑔 ⟩ , ∅ ) )
2		opex	⊢ ⟨ 𝑓 , tpos 𝑔 ⟩ ∈ V
3		0ex	⊢ ∅ ∈ V
4	2 3	ifex	⊢ if ( ( Rel 𝑔 ∧ Rel dom 𝑔 ) , ⟨ 𝑓 , tpos 𝑔 ⟩ , ∅ ) ∈ V
5	1 4	fnmpoi	⊢ oppFunc Fn ( V × V )