Metamath Proof Explorer

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 = ( f e. _V , g e. _V |-> if ( ( Rel g /\ Rel dom g ) , <. f , tpos g >. , (/) ) )
2 1 reldmmpo 
 |-  Rel dom oppFunc