Theorem reldmoppf

Description: The domain of oppFunc is a relation. (Contributed by Zhi Wang, 13-Nov-2025)

	Ref	Expression
Assertion	reldmoppf	⊢ Rel dom oppFunc

Proof

Step	Hyp	Ref	Expression
1		df-oppf	⊢ oppFunc = ( 𝑓 ∈ V , 𝑔 ∈ V ↦ if ( ( Rel 𝑔 ∧ Rel dom 𝑔 ) , ⟨ 𝑓 , tpos 𝑔 ⟩ , ∅ ) )
2	1	reldmmpo	⊢ Rel dom oppFunc