Metamath Proof Explorer

Theorem eloppf

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

Ref Expression
Hypotheses eloppf.g 
|- G = ( oppFunc ` F )
eloppf.x 
|- ( ph -> X e. G )
Assertion eloppf 
|- ( ph -> ( F =/= (/) /\ ( Rel ( 2nd ` F ) /\ Rel dom ( 2nd ` F ) ) ) )

Proof

Step Hyp Ref Expression
1 eloppf.g 
 |-  G = ( oppFunc ` F )
2 eloppf.x 
 |-  ( ph -> X e. G )
3 2 1 eleqtrdi 
 |-  ( ph -> X e. ( oppFunc ` F ) )
4 elfvdm 
 |-  ( X e. ( oppFunc ` F ) -> F e. dom oppFunc )
5 oppffn 
 |-  oppFunc Fn ( _V X. _V )
6 5 fndmi 
 |-  dom oppFunc = ( _V X. _V )
7 4 6 eleqtrdi 
 |-  ( X e. ( oppFunc ` F ) -> F e. ( _V X. _V ) )
8 3 7 syl 
 |-  ( ph -> F e. ( _V X. _V ) )
9 0nelxp 
 |-  -. (/) e. ( _V X. _V )
10 nelne2 
 |-  ( ( F e. ( _V X. _V ) /\ -. (/) e. ( _V X. _V ) ) -> F =/= (/) )
11 8 9 10 sylancl 
 |-  ( ph -> F =/= (/) )
12 1st2nd2 
 |-  ( F e. ( _V X. _V ) -> F = <. ( 1st ` F ) , ( 2nd ` F ) >. )
13 3 7 12 3syl 
 |-  ( ph -> F = <. ( 1st ` F ) , ( 2nd ` F ) >. )
14 13 fveq2d 
 |-  ( ph -> ( oppFunc ` F ) = ( oppFunc ` <. ( 1st ` F ) , ( 2nd ` F ) >. ) )
15 df-ov 
 |-  ( ( 1st ` F ) oppFunc ( 2nd ` F ) ) = ( oppFunc ` <. ( 1st ` F ) , ( 2nd ` F ) >. )
16 fvex 
 |-  ( 1st ` F ) e. _V
17 fvex 
 |-  ( 2nd ` F ) e. _V
18 oppfvalg 
 |-  ( ( ( 1st ` F ) e. _V /\ ( 2nd ` F ) e. _V ) -> ( ( 1st ` F ) oppFunc ( 2nd ` F ) ) = if ( ( Rel ( 2nd ` F ) /\ Rel dom ( 2nd ` F ) ) , <. ( 1st ` F ) , tpos ( 2nd ` F ) >. , (/) ) )
19 16 17 18 mp2an 
 |-  ( ( 1st ` F ) oppFunc ( 2nd ` F ) ) = if ( ( Rel ( 2nd ` F ) /\ Rel dom ( 2nd ` F ) ) , <. ( 1st ` F ) , tpos ( 2nd ` F ) >. , (/) )
20 15 19 eqtr3i 
 |-  ( oppFunc ` <. ( 1st ` F ) , ( 2nd ` F ) >. ) = if ( ( Rel ( 2nd ` F ) /\ Rel dom ( 2nd ` F ) ) , <. ( 1st ` F ) , tpos ( 2nd ` F ) >. , (/) )
21 14 20 eqtrdi 
 |-  ( ph -> ( oppFunc ` F ) = if ( ( Rel ( 2nd ` F ) /\ Rel dom ( 2nd ` F ) ) , <. ( 1st ` F ) , tpos ( 2nd ` F ) >. , (/) ) )
22 3 21 eleqtrd 
 |-  ( ph -> X e. if ( ( Rel ( 2nd ` F ) /\ Rel dom ( 2nd ` F ) ) , <. ( 1st ` F ) , tpos ( 2nd ` F ) >. , (/) ) )
23 22 ne0d 
 |-  ( ph -> if ( ( Rel ( 2nd ` F ) /\ Rel dom ( 2nd ` F ) ) , <. ( 1st ` F ) , tpos ( 2nd ` F ) >. , (/) ) =/= (/) )
24 iffalse 
 |-  ( -. ( Rel ( 2nd ` F ) /\ Rel dom ( 2nd ` F ) ) -> if ( ( Rel ( 2nd ` F ) /\ Rel dom ( 2nd ` F ) ) , <. ( 1st ` F ) , tpos ( 2nd ` F ) >. , (/) ) = (/) )
25 24 necon1ai 
 |-  ( if ( ( Rel ( 2nd ` F ) /\ Rel dom ( 2nd ` F ) ) , <. ( 1st ` F ) , tpos ( 2nd ` F ) >. , (/) ) =/= (/) -> ( Rel ( 2nd ` F ) /\ Rel dom ( 2nd ` F ) ) )
26 23 25 syl 
 |-  ( ph -> ( Rel ( 2nd ` F ) /\ Rel dom ( 2nd ` F ) ) )
27 11 26 jca 
 |-  ( ph -> ( F =/= (/) /\ ( Rel ( 2nd ` F ) /\ Rel dom ( 2nd ` F ) ) ) )