Metamath Proof Explorer

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 X. _V )

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 opex 
 |-  <. f , tpos g >. e. _V
3 0ex 
 |-  (/) e. _V
4 2 3 ifex 
 |-  if ( ( Rel g /\ Rel dom g ) , <. f , tpos g >. , (/) ) e. _V
5 1 4 fnmpoi 
 |-  oppFunc Fn ( _V X. _V )