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