Metamath Proof Explorer

Theorem oppfvalg

Description: Value of the opposite functor. (Contributed by Zhi Wang, 13-Nov-2025)

Ref Expression
Assertion oppfvalg 
|- ( ( F e. _V /\ G e. _V ) -> ( F oppFunc G ) = if ( ( Rel G /\ Rel dom G ) , <. F , tpos G >. , (/) ) )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( f = F /\ g = G ) -> g = G )
2 1 releqd 
 |-  ( ( f = F /\ g = G ) -> ( Rel g <-> Rel G ) )
3 1 dmeqd 
 |-  ( ( f = F /\ g = G ) -> dom g = dom G )
4 3 releqd 
 |-  ( ( f = F /\ g = G ) -> ( Rel dom g <-> Rel dom G ) )
5 2 4 anbi12d 
 |-  ( ( f = F /\ g = G ) -> ( ( Rel g /\ Rel dom g ) <-> ( Rel G /\ Rel dom G ) ) )
6 simpl 
 |-  ( ( f = F /\ g = G ) -> f = F )
7 1 tposeqd 
 |-  ( ( f = F /\ g = G ) -> tpos g = tpos G )
8 6 7 opeq12d 
 |-  ( ( f = F /\ g = G ) -> <. f , tpos g >. = <. F , tpos G >. )
9 5 8 ifbieq1d 
 |-  ( ( f = F /\ g = G ) -> if ( ( Rel g /\ Rel dom g ) , <. f , tpos g >. , (/) ) = if ( ( Rel G /\ Rel dom G ) , <. F , tpos G >. , (/) ) )
10 df-oppf 
 |-  oppFunc = ( f e. _V , g e. _V |-> if ( ( Rel g /\ Rel dom g ) , <. f , tpos g >. , (/) ) )
11 opex 
 |-  <. F , tpos G >. e. _V
12 0ex 
 |-  (/) e. _V
13 11 12 ifex 
 |-  if ( ( Rel G /\ Rel dom G ) , <. F , tpos G >. , (/) ) e. _V
14 9 10 13 ovmpoa 
 |-  ( ( F e. _V /\ G e. _V ) -> ( F oppFunc G ) = if ( ( Rel G /\ Rel dom G ) , <. F , tpos G >. , (/) ) )