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

Metamath Proof Explorer

Theorem 2oppf

Description: The double opposite functor is the original functor. Remark 3.42 of Adamek p. 39. (Contributed by Zhi Wang, 14-Nov-2025)

Ref Expression
Hypotheses oppfrcl.1 
|- ( ph -> G e. R )
oppfrcl.2 
|- Rel R
oppfrcl.3 
|- G = ( oppFunc ` F )
Assertion 2oppf 
|- ( ph -> ( oppFunc ` G ) = F )

Proof

Step Hyp Ref Expression
1 oppfrcl.1 
 |-  ( ph -> G e. R )
2 oppfrcl.2 
 |-  Rel R
3 oppfrcl.3 
 |-  G = ( oppFunc ` F )
4 fvex 
 |-  ( 1st ` F ) e. _V
5 fvex 
 |-  ( 2nd ` F ) e. _V
6 5 tposex 
 |-  tpos ( 2nd ` F ) e. _V
7 oppfvalg 
 |-  ( ( ( 1st ` F ) e. _V /\ tpos ( 2nd ` F ) e. _V ) -> ( ( 1st ` F ) oppFunc tpos ( 2nd ` F ) ) = if ( ( Rel tpos ( 2nd ` F ) /\ Rel dom tpos ( 2nd ` F ) ) , <. ( 1st ` F ) , tpos tpos ( 2nd ` F ) >. , (/) ) )
8 4 6 7 mp2an 
 |-  ( ( 1st ` F ) oppFunc tpos ( 2nd ` F ) ) = if ( ( Rel tpos ( 2nd ` F ) /\ Rel dom tpos ( 2nd ` F ) ) , <. ( 1st ` F ) , tpos tpos ( 2nd ` F ) >. , (/) )
9 df-ov 
 |-  ( ( 1st ` F ) oppFunc tpos ( 2nd ` F ) ) = ( oppFunc ` <. ( 1st ` F ) , tpos ( 2nd ` F ) >. )
10 1 2 3 oppfrcl 
 |-  ( ph -> F e. ( _V X. _V ) )
11 1st2nd2 
 |-  ( F e. ( _V X. _V ) -> F = <. ( 1st ` F ) , ( 2nd ` F ) >. )
12 10 11 syl 
 |-  ( ph -> F = <. ( 1st ` F ) , ( 2nd ` F ) >. )
13 1 2 3 12 oppf1st2nd 
 |-  ( ph -> ( G e. ( _V X. _V ) /\ ( ( 1st ` G ) = ( 1st ` F ) /\ ( 2nd ` G ) = tpos ( 2nd ` F ) ) ) )
14 eqopi 
 |-  ( ( G e. ( _V X. _V ) /\ ( ( 1st ` G ) = ( 1st ` F ) /\ ( 2nd ` G ) = tpos ( 2nd ` F ) ) ) -> G = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. )
15 13 14 syl 
 |-  ( ph -> G = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. )
16 15 fveq2d 
 |-  ( ph -> ( oppFunc ` G ) = ( oppFunc ` <. ( 1st ` F ) , tpos ( 2nd ` F ) >. ) )
17 9 16 eqtr4id 
 |-  ( ph -> ( ( 1st ` F ) oppFunc tpos ( 2nd ` F ) ) = ( oppFunc ` G ) )
18 1 2 3 12 oppfrcl3 
 |-  ( ph -> ( Rel ( 2nd ` F ) /\ Rel dom ( 2nd ` F ) ) )
19 tpostpos2 
 |-  ( ( Rel ( 2nd ` F ) /\ Rel dom ( 2nd ` F ) ) -> tpos tpos ( 2nd ` F ) = ( 2nd ` F ) )
20 18 19 syl 
 |-  ( ph -> tpos tpos ( 2nd ` F ) = ( 2nd ` F ) )
21 20 opeq2d 
 |-  ( ph -> <. ( 1st ` F ) , tpos tpos ( 2nd ` F ) >. = <. ( 1st ` F ) , ( 2nd ` F ) >. )
22 0nelrel0 
 |-  ( Rel dom ( 2nd ` F ) -> -. (/) e. dom ( 2nd ` F ) )
23 18 22 simpl2im 
 |-  ( ph -> -. (/) e. dom ( 2nd ` F ) )
24 reldmtpos 
 |-  ( Rel dom tpos ( 2nd ` F ) <-> -. (/) e. dom ( 2nd ` F ) )
25 23 24 sylibr 
 |-  ( ph -> Rel dom tpos ( 2nd ` F ) )
26 reltpos 
 |-  Rel tpos ( 2nd ` F )
27 25 26 jctil 
 |-  ( ph -> ( Rel tpos ( 2nd ` F ) /\ Rel dom tpos ( 2nd ` F ) ) )
28 27 iftrued 
 |-  ( ph -> if ( ( Rel tpos ( 2nd ` F ) /\ Rel dom tpos ( 2nd ` F ) ) , <. ( 1st ` F ) , tpos tpos ( 2nd ` F ) >. , (/) ) = <. ( 1st ` F ) , tpos tpos ( 2nd ` F ) >. )
29 21 28 12 3eqtr4d 
 |-  ( ph -> if ( ( Rel tpos ( 2nd ` F ) /\ Rel dom tpos ( 2nd ` F ) ) , <. ( 1st ` F ) , tpos tpos ( 2nd ` F ) >. , (/) ) = F )
30 8 17 29 3eqtr3a 
 |-  ( ph -> ( oppFunc ` G ) = F )