This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem opf2fval

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 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion opf2fval ( 𝜑 → ( 𝑋 𝐹 𝑌 ) = ( I ↾ ( 𝑌 𝑁 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 opf2fval.f ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ( I ↾ ( 𝑦 𝑁 𝑥 ) ) ) )
2 opf2fval.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
3 opf2fval.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
4 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → 𝑦 = 𝑌 )
5 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → 𝑥 = 𝑋 )
6 4 5 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( 𝑦 𝑁 𝑥 ) = ( 𝑌 𝑁 𝑋 ) )
7 6 reseq2d ⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( I ↾ ( 𝑦 𝑁 𝑥 ) ) = ( I ↾ ( 𝑌 𝑁 𝑋 ) ) )
8 ovexd ⊢ ( 𝜑 → ( 𝑌 𝑁 𝑋 ) ∈ V )
9 resiexg ⊢ ( ( 𝑌 𝑁 𝑋 ) ∈ V → ( I ↾ ( 𝑌 𝑁 𝑋 ) ) ∈ V )
10 8 9 syl ⊢ ( 𝜑 → ( I ↾ ( 𝑌 𝑁 𝑋 ) ) ∈ V )
11 1 7 2 3 10 ovmpod ⊢ ( 𝜑 → ( 𝑋 𝐹 𝑌 ) = ( I ↾ ( 𝑌 𝑁 𝑋 ) ) )