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

Definition df-comf 16264
Description: Define the functionalized composition operator, which is exactly like comp but is guaranteed to be a function of the proper type. (Contributed by Mario Carneiro, 4-Jan-2017.)
Assertion
Ref Expression
df-comf compf = (𝑐 ∈ V ↦ (𝑥 ∈ ((Base‘𝑐) × (Base‘𝑐)), 𝑦 ∈ (Base‘𝑐) ↦ (𝑔 ∈ ((2nd𝑥)(Hom ‘𝑐)𝑦), 𝑓 ∈ ((Hom ‘𝑐)‘𝑥) ↦ (𝑔(𝑥(comp‘𝑐)𝑦)𝑓))))
Distinct variable group:   𝑓,𝑐,𝑔,𝑥,𝑦

Detailed syntax breakdown of Definition df-comf
StepHypRef Expression
1 ccomf 16260 . 2 class compf
2 vc . . 3 setvar 𝑐
3 cvv 3189 . . 3 class V
4 vx . . . 4 setvar 𝑥
5 vy . . . 4 setvar 𝑦
62cv 1479 . . . . . 6 class 𝑐
7 cbs 15792 . . . . . 6 class Base
86, 7cfv 5852 . . . . 5 class (Base‘𝑐)
98, 8cxp 5077 . . . 4 class ((Base‘𝑐) × (Base‘𝑐))
10 vg . . . . 5 setvar 𝑔
11 vf . . . . 5 setvar 𝑓
124cv 1479 . . . . . . 7 class 𝑥
13 c2nd 7119 . . . . . . 7 class 2nd
1412, 13cfv 5852 . . . . . 6 class (2nd𝑥)
155cv 1479 . . . . . 6 class 𝑦
16 chom 15884 . . . . . . 7 class Hom
176, 16cfv 5852 . . . . . 6 class (Hom ‘𝑐)
1814, 15, 17co 6610 . . . . 5 class ((2nd𝑥)(Hom ‘𝑐)𝑦)
1912, 17cfv 5852 . . . . 5 class ((Hom ‘𝑐)‘𝑥)
2010cv 1479 . . . . . 6 class 𝑔
2111cv 1479 . . . . . 6 class 𝑓
22 cco 15885 . . . . . . . 8 class comp
236, 22cfv 5852 . . . . . . 7 class (comp‘𝑐)
2412, 15, 23co 6610 . . . . . 6 class (𝑥(comp‘𝑐)𝑦)
2520, 21, 24co 6610 . . . . 5 class (𝑔(𝑥(comp‘𝑐)𝑦)𝑓)
2610, 11, 18, 19, 25cmpt2 6612 . . . 4 class (𝑔 ∈ ((2nd𝑥)(Hom ‘𝑐)𝑦), 𝑓 ∈ ((Hom ‘𝑐)‘𝑥) ↦ (𝑔(𝑥(comp‘𝑐)𝑦)𝑓))
274, 5, 9, 8, 26cmpt2 6612 . . 3 class (𝑥 ∈ ((Base‘𝑐) × (Base‘𝑐)), 𝑦 ∈ (Base‘𝑐) ↦ (𝑔 ∈ ((2nd𝑥)(Hom ‘𝑐)𝑦), 𝑓 ∈ ((Hom ‘𝑐)‘𝑥) ↦ (𝑔(𝑥(comp‘𝑐)𝑦)𝑓)))
282, 3, 27cmpt 4678 . 2 class (𝑐 ∈ V ↦ (𝑥 ∈ ((Base‘𝑐) × (Base‘𝑐)), 𝑦 ∈ (Base‘𝑐) ↦ (𝑔 ∈ ((2nd𝑥)(Hom ‘𝑐)𝑦), 𝑓 ∈ ((Hom ‘𝑐)‘𝑥) ↦ (𝑔(𝑥(comp‘𝑐)𝑦)𝑓))))
291, 28wceq 1480 1 wff compf = (𝑐 ∈ V ↦ (𝑥 ∈ ((Base‘𝑐) × (Base‘𝑐)), 𝑦 ∈ (Base‘𝑐) ↦ (𝑔 ∈ ((2nd𝑥)(Hom ‘𝑐)𝑦), 𝑓 ∈ ((Hom ‘𝑐)‘𝑥) ↦ (𝑔(𝑥(comp‘𝑐)𝑦)𝑓))))
Colors of variables: wff setvar class
This definition is referenced by:  comfffval  16290
  Copyright terms: Public domain W3C validator