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 ⊢ φ → F = x ∈ A , y ∈ B ⟼ I ↾ y N x
opf2fval.x ⊢ φ → X ∈ A
opf2fval.y ⊢ φ → Y ∈ B
Assertion opf2fval ⊢ φ → X F Y = I ↾ Y N X

Proof

Step Hyp Ref Expression
1 opf2fval.f ⊢ φ → F = x ∈ A , y ∈ B ⟼ I ↾ y N x
2 opf2fval.x ⊢ φ → X ∈ A
3 opf2fval.y ⊢ φ → Y ∈ B
4 simprr ⊢ φ ∧ x = X ∧ y = Y → y = Y
5 simprl ⊢ φ ∧ x = X ∧ y = Y → x = X
6 4 5 oveq12d ⊢ φ ∧ x = X ∧ y = Y → y N x = Y N X
7 6 reseq2d ⊢ φ ∧ x = X ∧ y = Y → I ↾ y N x = I ↾ Y N X
8 ovexd ⊢ φ → Y N X ∈ V
9 resiexg ⊢ Y N X ∈ V → I ↾ Y N X ∈ V
10 8 9 syl ⊢ φ → I ↾ Y N X ∈ V
11 1 7 2 3 10 ovmpod ⊢ φ → X F Y = I ↾ Y N X