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

Definition df-comf 14919
 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 comp
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-comf
StepHypRef Expression
1 ccomf 14915 . 2 compf
2 vc . . 3
3 cvv 3113 . . 3
4 vx . . . 4
5 vy . . . 4
62cv 1378 . . . . . 6
7 cbs 14483 . . . . . 6
86, 7cfv 5586 . . . . 5
98, 8cxp 4997 . . . 4
10 vg . . . . 5
11 vf . . . . 5
124cv 1378 . . . . . . 7
13 c2nd 6780 . . . . . . 7
1412, 13cfv 5586 . . . . . 6
155cv 1378 . . . . . 6
16 chom 14559 . . . . . . 7
176, 16cfv 5586 . . . . . 6
1814, 15, 17co 6282 . . . . 5
1912, 17cfv 5586 . . . . 5
2010cv 1378 . . . . . 6
2111cv 1378 . . . . . 6
22 cco 14560 . . . . . . . 8 comp
236, 22cfv 5586 . . . . . . 7 comp
2412, 15, 23co 6282 . . . . . 6 comp
2520, 21, 24co 6282 . . . . 5 comp
2610, 11, 18, 19, 25cmpt2 6284 . . . 4 comp
274, 5, 9, 8, 26cmpt2 6284 . . 3 comp
282, 3, 27cmpt 4505 . 2 comp
291, 28wceq 1379 1 compf comp
 Colors of variables: wff setvar class This definition is referenced by:  comfffval  14947
 Copyright terms: Public domain W3C validator