Description: In a multigraph with two edges connecting the same two vertices, each of the vertices has degree 2. (Contributed by AV, 18-Dec-2020)
Ref | Expression | ||
---|---|---|---|
Hypothesis | umgr2v2evtx.g | |
|
Assertion | umgr2v2evd2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | umgr2v2evtx.g | |
|
2 | 1 | umgr2v2e | |
3 | 1 | umgr2v2evtxel | |
4 | 3 | 3adant3 | |
5 | 4 | adantr | |
6 | eqid | |
|
7 | eqid | |
|
8 | eqid | |
|
9 | eqid | |
|
10 | 6 7 8 9 | vtxdumgrval | |
11 | 2 5 10 | syl2anc | |
12 | 1 | umgr2v2eiedg | |
13 | 12 | dmeqd | |
14 | prex | |
|
15 | 14 14 | dmprop | |
16 | 13 15 | eqtrdi | |
17 | 12 | fveq1d | |
18 | 17 | eleq2d | |
19 | 16 18 | rabeqbidv | |
20 | 19 | fveq2d | |
21 | prid1g | |
|
22 | 0ne1 | |
|
23 | c0ex | |
|
24 | 23 14 | fvpr1 | |
25 | 22 24 | ax-mp | |
26 | 21 25 | eleqtrrdi | |
27 | 1ex | |
|
28 | 27 14 | fvpr2 | |
29 | 22 28 | ax-mp | |
30 | 21 29 | eleqtrrdi | |
31 | fveq2 | |
|
32 | 31 | eleq2d | |
33 | fveq2 | |
|
34 | 33 | eleq2d | |
35 | 23 27 32 34 | ralpr | |
36 | 26 30 35 | sylanbrc | |
37 | rabid2 | |
|
38 | 36 37 | sylibr | |
39 | 38 | eqcomd | |
40 | 39 | fveq2d | |
41 | prhash2ex | |
|
42 | 40 41 | eqtrdi | |
43 | 42 | 3ad2ant2 | |
44 | 20 43 | eqtrd | |
45 | 44 | adantr | |
46 | 11 45 | eqtrd | |