Description: The value of the vertex degree function. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Alexander van der Vekens, 20-Dec-2017) (Revised by AV, 9-Dec-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | vtxdgfval.v | |
|
vtxdgfval.i | |
||
vtxdgfval.a | |
||
Assertion | vtxdgfval | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vtxdgfval.v | |
|
2 | vtxdgfval.i | |
|
3 | vtxdgfval.a | |
|
4 | df-vtxdg | |
|
5 | fvex | |
|
6 | fvex | |
|
7 | simpl | |
|
8 | dmeq | |
|
9 | fveq1 | |
|
10 | 9 | eleq2d | |
11 | 8 10 | rabeqbidv | |
12 | 11 | fveq2d | |
13 | 9 | eqeq1d | |
14 | 8 13 | rabeqbidv | |
15 | 14 | fveq2d | |
16 | 12 15 | oveq12d | |
17 | 16 | adantl | |
18 | 7 17 | mpteq12dv | |
19 | 5 6 18 | csbie2 | |
20 | fveq2 | |
|
21 | 20 1 | eqtr4di | |
22 | fveq2 | |
|
23 | 22 | dmeqd | |
24 | 2 | dmeqi | |
25 | 3 24 | eqtri | |
26 | 23 25 | eqtr4di | |
27 | 22 2 | eqtr4di | |
28 | 27 | fveq1d | |
29 | 28 | eleq2d | |
30 | 26 29 | rabeqbidv | |
31 | 30 | fveq2d | |
32 | 28 | eqeq1d | |
33 | 26 32 | rabeqbidv | |
34 | 33 | fveq2d | |
35 | 31 34 | oveq12d | |
36 | 21 35 | mpteq12dv | |
37 | 36 | adantl | |
38 | 19 37 | eqtrid | |
39 | elex | |
|
40 | 1 | fvexi | |
41 | mptexg | |
|
42 | 40 41 | mp1i | |
43 | 4 38 39 42 | fvmptd2 | |