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

Metamath Proof Explorer

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

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 opf2.c ⊢ φ → C = D
5 opf2.d ⊢ φ → D ∈ Y N X
6 1 2 3 opf2fval ⊢ φ → X F Y = I ↾ Y N X
7 6 4 fveq12d ⊢ φ → X F Y ⁡ C = I ↾ Y N X ⁡ D
8 fvresi ⊢ D ∈ Y N X → I ↾ Y N X ⁡ D = D
9 5 8 syl ⊢ φ → I ↾ Y N X ⁡ D = D
10 7 9 eqtrd ⊢ φ → X F Y ⁡ C = D