This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eloppf2

Description: Both components of a pre-image of a non-empty opposite functor exist; and the second component is a relation on triples. (Contributed by Zhi Wang, 18-Nov-2025)

Ref Expression
Hypotheses eloppf2.k 
|- ( F oppFunc G ) = K
eloppf2.x 
|- ( ph -> X e. K )
Assertion eloppf2 
|- ( ph -> ( ( F e. _V /\ G e. _V ) /\ ( Rel G /\ Rel dom G ) ) )

Proof

Step Hyp Ref Expression
1 eloppf2.k 
 |-  ( F oppFunc G ) = K
2 eloppf2.x 
 |-  ( ph -> X e. K )
3 2 1 eleqtrrdi 
 |-  ( ph -> X e. ( F oppFunc G ) )
4 df-oppf 
 |-  oppFunc = ( f e. _V , g e. _V |-> if ( ( Rel g /\ Rel dom g ) , <. f , tpos g >. , (/) ) )
5 4 elmpocl 
 |-  ( X e. ( F oppFunc G ) -> ( F e. _V /\ G e. _V ) )
6 3 5 syl 
 |-  ( ph -> ( F e. _V /\ G e. _V ) )
7 oppfvalg 
 |-  ( ( F e. _V /\ G e. _V ) -> ( F oppFunc G ) = if ( ( Rel G /\ Rel dom G ) , <. F , tpos G >. , (/) ) )
8 6 7 syl 
 |-  ( ph -> ( F oppFunc G ) = if ( ( Rel G /\ Rel dom G ) , <. F , tpos G >. , (/) ) )
9 3 8 eleqtrd 
 |-  ( ph -> X e. if ( ( Rel G /\ Rel dom G ) , <. F , tpos G >. , (/) ) )
10 9 ne0d 
 |-  ( ph -> if ( ( Rel G /\ Rel dom G ) , <. F , tpos G >. , (/) ) =/= (/) )
11 iffalse 
 |-  ( -. ( Rel G /\ Rel dom G ) -> if ( ( Rel G /\ Rel dom G ) , <. F , tpos G >. , (/) ) = (/) )
12 11 necon1ai 
 |-  ( if ( ( Rel G /\ Rel dom G ) , <. F , tpos G >. , (/) ) =/= (/) -> ( Rel G /\ Rel dom G ) )
13 10 12 syl 
 |-  ( ph -> ( Rel G /\ Rel dom G ) )
14 6 13 jca 
 |-  ( ph -> ( ( F e. _V /\ G e. _V ) /\ ( Rel G /\ Rel dom G ) ) )