MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-homf Structured version   Visualization version   GIF version

Definition df-homf 17369
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.)
Assertion
Ref Expression
df-homf Homf = (𝑐 ∈ V ↦ (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ (𝑥(Hom ‘𝑐)𝑦)))
Distinct variable group:   𝑥,𝑐,𝑦

Detailed syntax breakdown of Definition df-homf
StepHypRef Expression
1 chomf 17365 . 2 class Homf
2 vc . . 3 setvar 𝑐
3 cvv 3431 . . 3 class V
4 vx . . . 4 setvar 𝑥
5 vy . . . 4 setvar 𝑦
62cv 1541 . . . . 5 class 𝑐
7 cbs 16902 . . . . 5 class Base
86, 7cfv 6431 . . . 4 class (Base‘𝑐)
94cv 1541 . . . . 5 class 𝑥
105cv 1541 . . . . 5 class 𝑦
11 chom 16963 . . . . . 6 class Hom
126, 11cfv 6431 . . . . 5 class (Hom ‘𝑐)
139, 10, 12co 7269 . . . 4 class (𝑥(Hom ‘𝑐)𝑦)
144, 5, 8, 8, 13cmpo 7271 . . 3 class (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ (𝑥(Hom ‘𝑐)𝑦))
152, 3, 14cmpt 5162 . 2 class (𝑐 ∈ V ↦ (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ (𝑥(Hom ‘𝑐)𝑦)))
161, 15wceq 1542 1 wff Homf = (𝑐 ∈ V ↦ (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ (𝑥(Hom ‘𝑐)𝑦)))
Colors of variables: wff setvar class
This definition is referenced by:  homffval  17389
  Copyright terms: Public domain W3C validator