Metamath Proof Explorer


Theorem 1loopgrvd2

Description: The vertex degree of a one-edge graph, case 4: an edge from a vertex to itself contributes two to the vertex's degree. I. e. in a graph (simple pseudograph) with one edge which is a loop, the vertex connected with itself by the loop has degree 2. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Alexander van der Vekens, 22-Dec-2017) (Revised by AV, 21-Feb-2021)

Ref Expression
Hypotheses 1loopgruspgr.v φ Vtx G = V
1loopgruspgr.a φ A X
1loopgruspgr.n φ N V
1loopgruspgr.i φ iEdg G = A N
Assertion 1loopgrvd2 φ VtxDeg G N = 2

Proof

Step Hyp Ref Expression
1 1loopgruspgr.v φ Vtx G = V
2 1loopgruspgr.a φ A X
3 1loopgruspgr.n φ N V
4 1loopgruspgr.i φ iEdg G = A N
5 1 2 3 4 1loopgruspgr φ G USHGraph
6 uspgrushgr G USHGraph G USHGraph
7 5 6 syl φ G USHGraph
8 3 1 eleqtrrd φ N Vtx G
9 eqid Vtx G = Vtx G
10 eqid Edg G = Edg G
11 eqid VtxDeg G = VtxDeg G
12 9 10 11 vtxdushgrfvedg G USHGraph N Vtx G VtxDeg G N = e Edg G | N e + 𝑒 e Edg G | e = N
13 7 8 12 syl2anc φ VtxDeg G N = e Edg G | N e + 𝑒 e Edg G | e = N
14 snex N V
15 sneq a = N a = N
16 15 eqeq2d a = N N = a N = N
17 eqid N = N
18 14 16 17 ceqsexv2d a N = a
19 18 a1i φ a N = a
20 snidg N V N N
21 3 20 syl φ N N
22 21 iftrued φ if N N N = N
23 22 eqeq1d φ if N N N = a N = a
24 23 exbidv φ a if N N N = a a N = a
25 19 24 mpbird φ a if N N N = a
26 1 2 3 4 1loopgredg φ Edg G = N
27 26 rabeqdv φ e Edg G | N e = e N | N e
28 eleq2 e = N N e N N
29 28 rabsnif e N | N e = if N N N
30 27 29 eqtrdi φ e Edg G | N e = if N N N
31 30 eqeq1d φ e Edg G | N e = a if N N N = a
32 31 exbidv φ a e Edg G | N e = a a if N N N = a
33 25 32 mpbird φ a e Edg G | N e = a
34 fvex Edg G V
35 34 rabex e Edg G | N e V
36 hash1snb e Edg G | N e V e Edg G | N e = 1 a e Edg G | N e = a
37 35 36 ax-mp e Edg G | N e = 1 a e Edg G | N e = a
38 33 37 sylibr φ e Edg G | N e = 1
39 eqid N = N
40 39 iftruei if N = N N = N
41 40 eqeq1i if N = N N = a N = a
42 41 exbii a if N = N N = a a N = a
43 19 42 sylibr φ a if N = N N = a
44 26 rabeqdv φ e Edg G | e = N = e N | e = N
45 eqeq1 e = N e = N N = N
46 45 rabsnif e N | e = N = if N = N N
47 44 46 eqtrdi φ e Edg G | e = N = if N = N N
48 47 eqeq1d φ e Edg G | e = N = a if N = N N = a
49 48 exbidv φ a e Edg G | e = N = a a if N = N N = a
50 43 49 mpbird φ a e Edg G | e = N = a
51 34 rabex e Edg G | e = N V
52 hash1snb e Edg G | e = N V e Edg G | e = N = 1 a e Edg G | e = N = a
53 51 52 ax-mp e Edg G | e = N = 1 a e Edg G | e = N = a
54 50 53 sylibr φ e Edg G | e = N = 1
55 38 54 oveq12d φ e Edg G | N e + 𝑒 e Edg G | e = N = 1 + 𝑒 1
56 1re 1
57 rexadd 1 1 1 + 𝑒 1 = 1 + 1
58 56 56 57 mp2an 1 + 𝑒 1 = 1 + 1
59 1p1e2 1 + 1 = 2
60 58 59 eqtri 1 + 𝑒 1 = 2
61 60 a1i φ 1 + 𝑒 1 = 2
62 13 55 61 3eqtrd φ VtxDeg G N = 2