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 ⊢ φ → G ∈ R
oppfrcl.2 ⊢ Rel ⁡ R
oppfrcl.3 No typesetting found for |- G = ( oppFunc ` F ) with typecode |-
Assertion 2oppf Could not format assertion : No typesetting found for |- ( ph -> ( oppFunc ` G ) = F ) with typecode |-

Proof

Step Hyp Ref Expression
1 oppfrcl.1 ⊢ φ → G ∈ R
2 oppfrcl.2 ⊢ Rel ⁡ R
3 oppfrcl.3 Could not format G = ( oppFunc ` F ) : No typesetting found for |- G = ( oppFunc ` F ) with typecode |-
4 fvex ⊢ 1 st ⁡ F ∈ V
5 fvex ⊢ 2 nd ⁡ F ∈ V
6 5 tposex ⊢ tpos 2 nd ⁡ F ∈ V
7 oppfvalg Could not format ( ( ( 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 ) >. , (/) ) ) : No typesetting found for |- ( ( ( 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 ) >. , (/) ) ) with typecode |-
8 4 6 7 mp2an Could not format ( ( 1st ` F ) oppFunc tpos ( 2nd ` F ) ) = if ( ( Rel tpos ( 2nd ` F ) /\ Rel dom tpos ( 2nd ` F ) ) , <. ( 1st ` F ) , tpos tpos ( 2nd ` F ) >. , (/) ) : No typesetting found for |- ( ( 1st ` F ) oppFunc tpos ( 2nd ` F ) ) = if ( ( Rel tpos ( 2nd ` F ) /\ Rel dom tpos ( 2nd ` F ) ) , <. ( 1st ` F ) , tpos tpos ( 2nd ` F ) >. , (/) ) with typecode |-
9 df-ov Could not format ( ( 1st ` F ) oppFunc tpos ( 2nd ` F ) ) = ( oppFunc ` <. ( 1st ` F ) , tpos ( 2nd ` F ) >. ) : No typesetting found for |- ( ( 1st ` F ) oppFunc tpos ( 2nd ` F ) ) = ( oppFunc ` <. ( 1st ` F ) , tpos ( 2nd ` F ) >. ) with typecode |-
10 1 2 3 oppfrcl ⊢ φ → F ∈ V × V
11 1st2nd2 ⊢ F ∈ V × V → F = 1 st ⁡ F 2 nd ⁡ F
12 10 11 syl ⊢ φ → F = 1 st ⁡ F 2 nd ⁡ F
13 1 2 3 12 oppf1st2nd ⊢ φ → G ∈ V × V ∧ 1 st ⁡ G = 1 st ⁡ F ∧ 2 nd ⁡ G = tpos 2 nd ⁡ F
14 eqopi ⊢ G ∈ V × V ∧ 1 st ⁡ G = 1 st ⁡ F ∧ 2 nd ⁡ G = tpos 2 nd ⁡ F → G = 1 st ⁡ F tpos 2 nd ⁡ F
15 13 14 syl ⊢ φ → G = 1 st ⁡ F tpos 2 nd ⁡ F
16 15 fveq2d Could not format ( ph -> ( oppFunc ` G ) = ( oppFunc ` <. ( 1st ` F ) , tpos ( 2nd ` F ) >. ) ) : No typesetting found for |- ( ph -> ( oppFunc ` G ) = ( oppFunc ` <. ( 1st ` F ) , tpos ( 2nd ` F ) >. ) ) with typecode |-
17 9 16 eqtr4id Could not format ( ph -> ( ( 1st ` F ) oppFunc tpos ( 2nd ` F ) ) = ( oppFunc ` G ) ) : No typesetting found for |- ( ph -> ( ( 1st ` F ) oppFunc tpos ( 2nd ` F ) ) = ( oppFunc ` G ) ) with typecode |-
18 1 2 3 12 oppfrcl3 ⊢ φ → Rel ⁡ 2 nd ⁡ F ∧ Rel ⁡ dom ⁡ 2 nd ⁡ F
19 tpostpos2 ⊢ Rel ⁡ 2 nd ⁡ F ∧ Rel ⁡ dom ⁡ 2 nd ⁡ F → tpos tpos 2 nd ⁡ F = 2 nd ⁡ F
20 18 19 syl ⊢ φ → tpos tpos 2 nd ⁡ F = 2 nd ⁡ F
21 20 opeq2d ⊢ φ → 1 st ⁡ F tpos tpos 2 nd ⁡ F = 1 st ⁡ F 2 nd ⁡ F
22 0nelrel0 ⊢ Rel ⁡ dom ⁡ 2 nd ⁡ F → ¬ ∅ ∈ dom ⁡ 2 nd ⁡ F
23 18 22 simpl2im ⊢ φ → ¬ ∅ ∈ dom ⁡ 2 nd ⁡ F
24 reldmtpos ⊢ Rel ⁡ dom ⁡ tpos 2 nd ⁡ F ↔ ¬ ∅ ∈ dom ⁡ 2 nd ⁡ F
25 23 24 sylibr ⊢ φ → Rel ⁡ dom ⁡ tpos 2 nd ⁡ F
26 reltpos ⊢ Rel ⁡ tpos 2 nd ⁡ F
27 25 26 jctil ⊢ φ → Rel ⁡ tpos 2 nd ⁡ F ∧ Rel ⁡ dom ⁡ tpos 2 nd ⁡ F
28 27 iftrued ⊢ φ → if Rel ⁡ tpos 2 nd ⁡ F ∧ Rel ⁡ dom ⁡ tpos 2 nd ⁡ F 1 st ⁡ F tpos tpos 2 nd ⁡ F ∅ = 1 st ⁡ F tpos tpos 2 nd ⁡ F
29 21 28 12 3eqtr4d ⊢ φ → if Rel ⁡ tpos 2 nd ⁡ F ∧ Rel ⁡ dom ⁡ tpos 2 nd ⁡ F 1 st ⁡ F tpos tpos 2 nd ⁡ F ∅ = F
30 8 17 29 3eqtr3a Could not format ( ph -> ( oppFunc ` G ) = F ) : No typesetting found for |- ( ph -> ( oppFunc ` G ) = F ) with typecode |-