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=AN
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=AN
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 ⊢∃aN=a
19 18 a1i ⊢φ→∃aN=a
20 snidg ⊢N∈V→N∈N
21 3 20 syl ⊢φ→N∈N
22 21 iftrued ⊢φ→ifN∈NN∅=N
23 22 eqeq1d ⊢φ→ifN∈NN∅=a↔N=a
24 23 exbidv ⊢φ→∃aifN∈NN∅=a↔∃aN=a
25 19 24 mpbird ⊢φ→∃aifN∈NN∅=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=ifN∈NN∅
30 27 29 eqtrdi ⊢φ→e∈Edg⁡G|N∈e=ifN∈NN∅
31 30 eqeq1d ⊢φ→e∈Edg⁡G|N∈e=a↔ifN∈NN∅=a
32 31 exbidv ⊢φ→∃ae∈Edg⁡G|N∈e=a↔∃aifN∈NN∅=a
33 25 32 mpbird ⊢φ→∃ae∈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↔∃ae∈Edg⁡G|N∈e=a
37 35 36 ax-mp ⊢e∈Edg⁡G|N∈e=1↔∃ae∈Edg⁡G|N∈e=a
38 33 37 sylibr ⊢φ→e∈Edg⁡G|N∈e=1
39 eqid ⊢N=N
40 39 iftruei ⊢ifN=NN∅=N
41 40 eqeq1i ⊢ifN=NN∅=a↔N=a
42 41 exbii ⊢∃aifN=NN∅=a↔∃aN=a
43 19 42 sylibr ⊢φ→∃aifN=NN∅=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=ifN=NN∅
47 44 46 eqtrdi ⊢φ→e∈Edg⁡G|e=N=ifN=NN∅
48 47 eqeq1d ⊢φ→e∈Edg⁡G|e=N=a↔ifN=NN∅=a
49 48 exbidv ⊢φ→∃ae∈Edg⁡G|e=N=a↔∃aifN=NN∅=a
50 43 49 mpbird ⊢φ→∃ae∈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↔∃ae∈Edg⁡G|e=N=a
53 51 52 ax-mp ⊢e∈Edg⁡G|e=N=1↔∃ae∈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