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 16263
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 16259 . 2 class Homf
2 vc . . 3 setvar 𝑐
3 cvv 3189 . . 3 class V
4 vx . . . 4 setvar 𝑥
5 vy . . . 4 setvar 𝑦
62cv 1479 . . . . 5 class 𝑐
7 cbs 15792 . . . . 5 class Base
86, 7cfv 5852 . . . 4 class (Base‘𝑐)
94cv 1479 . . . . 5 class 𝑥
105cv 1479 . . . . 5 class 𝑦
11 chom 15884 . . . . . 6 class Hom
126, 11cfv 5852 . . . . 5 class (Hom ‘𝑐)
139, 10, 12co 6610 . . . 4 class (𝑥(Hom ‘𝑐)𝑦)
144, 5, 8, 8, 13cmpt2 6612 . . 3 class (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ (𝑥(Hom ‘𝑐)𝑦))
152, 3, 14cmpt 4678 . 2 class (𝑐 ∈ V ↦ (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ (𝑥(Hom ‘𝑐)𝑦)))
161, 15wceq 1480 1 wff Homf = (𝑐 ∈ V ↦ (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ (𝑥(Hom ‘𝑐)𝑦)))
Colors of variables: wff setvar class
This definition is referenced by:  homffval  16282
  Copyright terms: Public domain W3C validator