oppf2

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

		Ref	Expression
	Hypothesis	oppf1.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
	Assertion	oppf2	⊢ ( 𝜑 → ( 𝑀 ( 2^nd ‘ ( oppFunc ‘ 𝐹 ) ) 𝑁 ) = ( 𝑁 ( 2^nd ‘ 𝐹 ) 𝑀 ) )

Step	Hyp	Ref	Expression
1		oppf1.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
2		oppfval2	⊢ ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) → ( oppFunc ‘ 𝐹 ) = ⟨ ( 1^st ‘ 𝐹 ) , tpos ( 2^nd ‘ 𝐹 ) ⟩ )
3		fvex	⊢ ( 1^st ‘ 𝐹 ) ∈ V
4		fvex	⊢ ( 2^nd ‘ 𝐹 ) ∈ V
5	4	tposex	⊢ tpos ( 2^nd ‘ 𝐹 ) ∈ V
6	3 5	op2ndd	⊢ ( ( oppFunc ‘ 𝐹 ) = ⟨ ( 1^st ‘ 𝐹 ) , tpos ( 2^nd ‘ 𝐹 ) ⟩ → ( 2^nd ‘ ( oppFunc ‘ 𝐹 ) ) = tpos ( 2^nd ‘ 𝐹 ) )
7	1 2 6	3syl	⊢ ( 𝜑 → ( 2^nd ‘ ( oppFunc ‘ 𝐹 ) ) = tpos ( 2^nd ‘ 𝐹 ) )
8	7	oveqd	⊢ ( 𝜑 → ( 𝑀 ( 2^nd ‘ ( oppFunc ‘ 𝐹 ) ) 𝑁 ) = ( 𝑀 tpos ( 2^nd ‘ 𝐹 ) 𝑁 ) )
9		ovtpos	⊢ ( 𝑀 tpos ( 2^nd ‘ 𝐹 ) 𝑁 ) = ( 𝑁 ( 2^nd ‘ 𝐹 ) 𝑀 )
10	8 9	eqtrdi	⊢ ( 𝜑 → ( 𝑀 ( 2^nd ‘ ( oppFunc ‘ 𝐹 ) ) 𝑁 ) = ( 𝑁 ( 2^nd ‘ 𝐹 ) 𝑀 ) )

Metamath Proof Explorer