oppfval2

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

		Ref	Expression
	Assertion	oppfval2	⊢ ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) → ( oppFunc ‘ 𝐹 ) = ⟨ ( 1^st ‘ 𝐹 ) , tpos ( 2^nd ‘ 𝐹 ) ⟩ )

Step	Hyp	Ref	Expression
1		relfunc	⊢ Rel ( 𝐶 Func 𝐷 )
2		1st2nd	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐹 ∈ ( 𝐶 Func 𝐷 ) ) → 𝐹 = ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ )
3	1 2	mpan	⊢ ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) → 𝐹 = ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ )
4	3	fveq2d	⊢ ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) → ( oppFunc ‘ 𝐹 ) = ( oppFunc ‘ ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ ) )
5		df-ov	⊢ ( ( 1^st ‘ 𝐹 ) oppFunc ( 2^nd ‘ 𝐹 ) ) = ( oppFunc ‘ ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ )
6	4 5	eqtr4di	⊢ ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) → ( oppFunc ‘ 𝐹 ) = ( ( 1^st ‘ 𝐹 ) oppFunc ( 2^nd ‘ 𝐹 ) ) )
7		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐹 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
8	1 7	mpan	⊢ ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
9		oppfval	⊢ ( ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) → ( ( 1^st ‘ 𝐹 ) oppFunc ( 2^nd ‘ 𝐹 ) ) = ⟨ ( 1^st ‘ 𝐹 ) , tpos ( 2^nd ‘ 𝐹 ) ⟩ )
10	8 9	syl	⊢ ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) → ( ( 1^st ‘ 𝐹 ) oppFunc ( 2^nd ‘ 𝐹 ) ) = ⟨ ( 1^st ‘ 𝐹 ) , tpos ( 2^nd ‘ 𝐹 ) ⟩ )
11	6 10	eqtrd	⊢ ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) → ( oppFunc ‘ 𝐹 ) = ⟨ ( 1^st ‘ 𝐹 ) , tpos ( 2^nd ‘ 𝐹 ) ⟩ )

Metamath Proof Explorer