Theorem opf12

Description: The object part of the op functor on functor categories. Lemma for oppfdiag . (Contributed by Zhi Wang, 19-Nov-2025)

	Ref	Expression
Hypotheses	opf11.f	⊢ ( 𝜑 → 𝐹 = ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) )
	opf11.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐶 Func 𝐷 ) )
Assertion	opf12	⊢ ( 𝜑 → ( 𝑀 ( 2nd ‘ ( 𝐹 ‘ 𝑋 ) ) 𝑁 ) = ( 𝑁 ( 2nd ‘ 𝑋 ) 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		opf11.f	⊢ ( 𝜑 → 𝐹 = ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) )
2		opf11.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐶 Func 𝐷 ) )
3	1	fveq1d	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) = ( ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) ‘ 𝑋 ) )
4	2	fvresd	⊢ ( 𝜑 → ( ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) ‘ 𝑋 ) = ( oppFunc ‘ 𝑋 ) )
5		oppfval2	⊢ ( 𝑋 ∈ ( 𝐶 Func 𝐷 ) → ( oppFunc ‘ 𝑋 ) = ⟨ ( 1st ‘ 𝑋 ) , tpos ( 2nd ‘ 𝑋 ) ⟩ )
6	2 5	syl	⊢ ( 𝜑 → ( oppFunc ‘ 𝑋 ) = ⟨ ( 1st ‘ 𝑋 ) , tpos ( 2nd ‘ 𝑋 ) ⟩ )
7	3 4 6	3eqtrd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) = ⟨ ( 1st ‘ 𝑋 ) , tpos ( 2nd ‘ 𝑋 ) ⟩ )
8		fvex	⊢ ( 1st ‘ 𝑋 ) ∈ V
9		fvex	⊢ ( 2nd ‘ 𝑋 ) ∈ V
10	9	tposex	⊢ tpos ( 2nd ‘ 𝑋 ) ∈ V
11	8 10	op2ndd	⊢ ( ( 𝐹 ‘ 𝑋 ) = ⟨ ( 1st ‘ 𝑋 ) , tpos ( 2nd ‘ 𝑋 ) ⟩ → ( 2nd ‘ ( 𝐹 ‘ 𝑋 ) ) = tpos ( 2nd ‘ 𝑋 ) )
12	7 11	syl	⊢ ( 𝜑 → ( 2nd ‘ ( 𝐹 ‘ 𝑋 ) ) = tpos ( 2nd ‘ 𝑋 ) )
13	12	oveqd	⊢ ( 𝜑 → ( 𝑀 ( 2nd ‘ ( 𝐹 ‘ 𝑋 ) ) 𝑁 ) = ( 𝑀 tpos ( 2nd ‘ 𝑋 ) 𝑁 ) )
14		ovtpos	⊢ ( 𝑀 tpos ( 2nd ‘ 𝑋 ) 𝑁 ) = ( 𝑁 ( 2nd ‘ 𝑋 ) 𝑀 )
15	13 14	eqtrdi	⊢ ( 𝜑 → ( 𝑀 ( 2nd ‘ ( 𝐹 ‘ 𝑋 ) ) 𝑁 ) = ( 𝑁 ( 2nd ‘ 𝑋 ) 𝑀 ) )