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

Metamath Proof Explorer

Theorem oppfval3

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

Ref Expression
Hypotheses oppfval3.g ⊢ ( 𝜑 → 𝐹 = ⟨ 𝐺 , 𝐾 ⟩ )
oppfval3.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
Assertion oppfval3 ( 𝜑 → ( oppFunc ‘ 𝐹 ) = ⟨ 𝐺 , tpos 𝐾 ⟩ )

Proof

Step Hyp Ref Expression
1 oppfval3.g ⊢ ( 𝜑 → 𝐹 = ⟨ 𝐺 , 𝐾 ⟩ )
2 oppfval3.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
3 1 fveq2d ⊢ ( 𝜑 → ( oppFunc ‘ 𝐹 ) = ( oppFunc ‘ ⟨ 𝐺 , 𝐾 ⟩ ) )
4 df-ov ⊢ ( 𝐺 oppFunc 𝐾 ) = ( oppFunc ‘ ⟨ 𝐺 , 𝐾 ⟩ )
5 3 4 eqtr4di ⊢ ( 𝜑 → ( oppFunc ‘ 𝐹 ) = ( 𝐺 oppFunc 𝐾 ) )
6 1 2 eqeltrrd ⊢ ( 𝜑 → ⟨ 𝐺 , 𝐾 ⟩ ∈ ( 𝐶 Func 𝐷 ) )
7 df-br ⊢ ( 𝐺 ( 𝐶 Func 𝐷 ) 𝐾 ↔ ⟨ 𝐺 , 𝐾 ⟩ ∈ ( 𝐶 Func 𝐷 ) )
8 6 7 sylibr ⊢ ( 𝜑 → 𝐺 ( 𝐶 Func 𝐷 ) 𝐾 )
9 oppfval ⊢ ( 𝐺 ( 𝐶 Func 𝐷 ) 𝐾 → ( 𝐺 oppFunc 𝐾 ) = ⟨ 𝐺 , tpos 𝐾 ⟩ )
10 8 9 syl ⊢ ( 𝜑 → ( 𝐺 oppFunc 𝐾 ) = ⟨ 𝐺 , tpos 𝐾 ⟩ )
11 5 10 eqtrd ⊢ ( 𝜑 → ( oppFunc ‘ 𝐹 ) = ⟨ 𝐺 , tpos 𝐾 ⟩ )