Theorem opf2

Description: The morphism part of the op functor on functor categories. Lemma for fucoppc . (Contributed by Zhi Wang, 18-Nov-2025)

	Ref	Expression
Hypotheses	opf2fval.f	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ( I ↾ ( 𝑦 𝑁 𝑥 ) ) ) )
	opf2fval.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
	opf2fval.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	opf2.c	⊢ ( 𝜑 → 𝐶 = 𝐷 )
	opf2.d	⊢ ( 𝜑 → 𝐷 ∈ ( 𝑌 𝑁 𝑋 ) )
Assertion	opf2	⊢ ( 𝜑 → ( ( 𝑋 𝐹 𝑌 ) ‘ 𝐶 ) = 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		opf2fval.f	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ( I ↾ ( 𝑦 𝑁 𝑥 ) ) ) )
2		opf2fval.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
3		opf2fval.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
4		opf2.c	⊢ ( 𝜑 → 𝐶 = 𝐷 )
5		opf2.d	⊢ ( 𝜑 → 𝐷 ∈ ( 𝑌 𝑁 𝑋 ) )
6	1 2 3	opf2fval	⊢ ( 𝜑 → ( 𝑋 𝐹 𝑌 ) = ( I ↾ ( 𝑌 𝑁 𝑋 ) ) )
7	6 4	fveq12d	⊢ ( 𝜑 → ( ( 𝑋 𝐹 𝑌 ) ‘ 𝐶 ) = ( ( I ↾ ( 𝑌 𝑁 𝑋 ) ) ‘ 𝐷 ) )
8		fvresi	⊢ ( 𝐷 ∈ ( 𝑌 𝑁 𝑋 ) → ( ( I ↾ ( 𝑌 𝑁 𝑋 ) ) ‘ 𝐷 ) = 𝐷 )
9	5 8	syl	⊢ ( 𝜑 → ( ( I ↾ ( 𝑌 𝑁 𝑋 ) ) ‘ 𝐷 ) = 𝐷 )
10	7 9	eqtrd	⊢ ( 𝜑 → ( ( 𝑋 𝐹 𝑌 ) ‘ 𝐶 ) = 𝐷 )