Theorem oppfval

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

	Ref	Expression
Assertion	oppfval	⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 → ( 𝐹 oppFunc 𝐺 ) = ⟨ 𝐹 , tpos 𝐺 ⟩ )

Proof

Step	Hyp	Ref	Expression
1		relfunc	⊢ Rel ( 𝐶 Func 𝐷 )
2	1	brrelex12i	⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 → ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) )
3		simpl	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → 𝑓 = 𝐹 )
4		simpr	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → 𝑔 = 𝐺 )
5	4	tposeqd	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → tpos 𝑔 = tpos 𝐺 )
6	3 5	opeq12d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ⟨ 𝑓 , tpos 𝑔 ⟩ = ⟨ 𝐹 , tpos 𝐺 ⟩ )
7		df-oppf	⊢ oppFunc = ( 𝑓 ∈ V , 𝑔 ∈ V ↦ ⟨ 𝑓 , tpos 𝑔 ⟩ )
8		opex	⊢ ⟨ 𝐹 , tpos 𝐺 ⟩ ∈ V
9	6 7 8	ovmpoa	⊢ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) → ( 𝐹 oppFunc 𝐺 ) = ⟨ 𝐹 , tpos 𝐺 ⟩ )
10	2 9	syl	⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 → ( 𝐹 oppFunc 𝐺 ) = ⟨ 𝐹 , tpos 𝐺 ⟩ )