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

Metamath Proof Explorer

Definition df-homf

Description: Define the functionalized Hom-set operator, which is exactly like Hom but is guaranteed to be a function on the base. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Assertion df-homf ⊢ Hom 𝑓 = c ∈ V ⟼ x ∈ Base c , y ∈ Base c ⟼ x Hom ⁡ c y

Detailed syntax breakdown

Step Hyp Ref Expression
0 chomf class Hom 𝑓
1 vc setvar c
2 cvv class V
3 vx setvar x
4 cbs class Base
5 1 cv setvar c
6 5 4 cfv class Base c
7 vy setvar y
8 3 cv setvar x
9 chom class Hom
10 5 9 cfv class Hom ⁡ c
11 7 cv setvar y
12 8 11 10 co class x Hom ⁡ c y
13 3 7 6 6 12 cmpo class x ∈ Base c , y ∈ Base c ⟼ x Hom ⁡ c y
14 1 2 13 cmpt class c ∈ V ⟼ x ∈ Base c , y ∈ Base c ⟼ x Hom ⁡ c y
15 0 14 wceq wff Hom 𝑓 = c ∈ V ⟼ x ∈ Base c , y ∈ Base c ⟼ x Hom ⁡ c y