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

Metamath Proof Explorer

Theorem homfval

Description: Value of the functionalized Hom-set operation. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypotheses homffval.f ⊢ F = Hom 𝑓 ⁡ C
homffval.b ⊢ B = Base C
homffval.h ⊢ H = Hom ⁡ C
homfval.x ⊢ φ → X ∈ B
homfval.y ⊢ φ → Y ∈ B
Assertion homfval ⊢ φ → X F Y = X H Y

Proof

Step Hyp Ref Expression
1 homffval.f ⊢ F = Hom 𝑓 ⁡ C
2 homffval.b ⊢ B = Base C
3 homffval.h ⊢ H = Hom ⁡ C
4 homfval.x ⊢ φ → X ∈ B
5 homfval.y ⊢ φ → Y ∈ B
6 1 2 3 homffval ⊢ F = x ∈ B , y ∈ B ⟼ x H y
7 6 a1i ⊢ φ → F = x ∈ B , y ∈ B ⟼ x H y
8 oveq12 ⊢ x = X ∧ y = Y → x H y = X H Y
9 8 adantl ⊢ φ ∧ x = X ∧ y = Y → x H y = X H Y
10 ovexd ⊢ φ → X H Y ∈ V
11 7 9 4 5 10 ovmpod ⊢ φ → X F Y = X H Y