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

Metamath Proof Explorer

Theorem catchom

Description: Set of arrows of the category of categories (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses catcbas.c ⊢ C = CatCat ⁡ U
catcbas.b ⊢ B = Base C
catcbas.u ⊢ φ → U ∈ V
catchomfval.h ⊢ H = Hom ⁡ C
catchom.x ⊢ φ → X ∈ B
catchom.y ⊢ φ → Y ∈ B
Assertion catchom ⊢ φ → X H Y = X Func Y

Proof

Step Hyp Ref Expression
1 catcbas.c ⊢ C = CatCat ⁡ U
2 catcbas.b ⊢ B = Base C
3 catcbas.u ⊢ φ → U ∈ V
4 catchomfval.h ⊢ H = Hom ⁡ C
5 catchom.x ⊢ φ → X ∈ B
6 catchom.y ⊢ φ → Y ∈ B
7 1 2 3 4 catchomfval ⊢ φ → H = x ∈ B , y ∈ B ⟼ x Func y
8 oveq12 ⊢ x = X ∧ y = Y → x Func y = X Func Y
9 8 adantl ⊢ φ ∧ x = X ∧ y = Y → x Func y = X Func Y
10 ovexd ⊢ φ → X Func Y ∈ V
11 7 9 5 6 10 ovmpod ⊢ φ → X H Y = X Func Y