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 𝐾 ⟩ )