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 ‘ 𝐺 ) = 𝑉 )
1loopgruspgr.a ( 𝜑𝐴𝑋 )
1loopgruspgr.n ( 𝜑𝑁𝑉 )
1loopgruspgr.i ( 𝜑 → ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝑁 } ⟩ } )
Assertion 1loopgrvd2 ( 𝜑 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) = 2 )

Proof

Step Hyp Ref Expression
1 1loopgruspgr.v ( 𝜑 → ( Vtx ‘ 𝐺 ) = 𝑉 )
2 1loopgruspgr.a ( 𝜑𝐴𝑋 )
3 1loopgruspgr.n ( 𝜑𝑁𝑉 )
4 1loopgruspgr.i ( 𝜑 → ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝑁 } ⟩ } )
5 1 2 3 4 1loopgruspgr ( 𝜑𝐺 ∈ USPGraph )
6 uspgrushgr ( 𝐺 ∈ USPGraph → 𝐺 ∈ USHGraph )
7 5 6 syl ( 𝜑𝐺 ∈ USHGraph )
8 3 1 eleqtrrd ( 𝜑𝑁 ∈ ( Vtx ‘ 𝐺 ) )
9 eqid ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
10 eqid ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
11 eqid ( VtxDeg ‘ 𝐺 ) = ( VtxDeg ‘ 𝐺 )
12 9 10 11 vtxdushgrfvedg ( ( 𝐺 ∈ USHGraph ∧ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) = ( ( ♯ ‘ { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑁𝑒 } ) +𝑒 ( ♯ ‘ { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑒 = { 𝑁 } } ) ) )
13 7 8 12 syl2anc ( 𝜑 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) = ( ( ♯ ‘ { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑁𝑒 } ) +𝑒 ( ♯ ‘ { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑒 = { 𝑁 } } ) ) )
14 snex { 𝑁 } ∈ V
15 sneq ( 𝑎 = { 𝑁 } → { 𝑎 } = { { 𝑁 } } )
16 15 eqeq2d ( 𝑎 = { 𝑁 } → ( { { 𝑁 } } = { 𝑎 } ↔ { { 𝑁 } } = { { 𝑁 } } ) )
17 eqid { { 𝑁 } } = { { 𝑁 } }
18 14 16 17 ceqsexv2d 𝑎 { { 𝑁 } } = { 𝑎 }
19 18 a1i ( 𝜑 → ∃ 𝑎 { { 𝑁 } } = { 𝑎 } )
20 snidg ( 𝑁𝑉𝑁 ∈ { 𝑁 } )
21 3 20 syl ( 𝜑𝑁 ∈ { 𝑁 } )
22 21 iftrued ( 𝜑 → if ( 𝑁 ∈ { 𝑁 } , { { 𝑁 } } , ∅ ) = { { 𝑁 } } )
23 22 eqeq1d ( 𝜑 → ( if ( 𝑁 ∈ { 𝑁 } , { { 𝑁 } } , ∅ ) = { 𝑎 } ↔ { { 𝑁 } } = { 𝑎 } ) )
24 23 exbidv ( 𝜑 → ( ∃ 𝑎 if ( 𝑁 ∈ { 𝑁 } , { { 𝑁 } } , ∅ ) = { 𝑎 } ↔ ∃ 𝑎 { { 𝑁 } } = { 𝑎 } ) )
25 19 24 mpbird ( 𝜑 → ∃ 𝑎 if ( 𝑁 ∈ { 𝑁 } , { { 𝑁 } } , ∅ ) = { 𝑎 } )
26 1 2 3 4 1loopgredg ( 𝜑 → ( Edg ‘ 𝐺 ) = { { 𝑁 } } )
27 26 rabeqdv ( 𝜑 → { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑁𝑒 } = { 𝑒 ∈ { { 𝑁 } } ∣ 𝑁𝑒 } )
28 eleq2 ( 𝑒 = { 𝑁 } → ( 𝑁𝑒𝑁 ∈ { 𝑁 } ) )
29 28 rabsnif { 𝑒 ∈ { { 𝑁 } } ∣ 𝑁𝑒 } = if ( 𝑁 ∈ { 𝑁 } , { { 𝑁 } } , ∅ )
30 27 29 eqtrdi ( 𝜑 → { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑁𝑒 } = if ( 𝑁 ∈ { 𝑁 } , { { 𝑁 } } , ∅ ) )
31 30 eqeq1d ( 𝜑 → ( { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑁𝑒 } = { 𝑎 } ↔ if ( 𝑁 ∈ { 𝑁 } , { { 𝑁 } } , ∅ ) = { 𝑎 } ) )
32 31 exbidv ( 𝜑 → ( ∃ 𝑎 { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑁𝑒 } = { 𝑎 } ↔ ∃ 𝑎 if ( 𝑁 ∈ { 𝑁 } , { { 𝑁 } } , ∅ ) = { 𝑎 } ) )
33 25 32 mpbird ( 𝜑 → ∃ 𝑎 { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑁𝑒 } = { 𝑎 } )
34 fvex ( Edg ‘ 𝐺 ) ∈ V
35 34 rabex { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑁𝑒 } ∈ V
36 hash1snb ( { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑁𝑒 } ∈ V → ( ( ♯ ‘ { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑁𝑒 } ) = 1 ↔ ∃ 𝑎 { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑁𝑒 } = { 𝑎 } ) )
37 35 36 ax-mp ( ( ♯ ‘ { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑁𝑒 } ) = 1 ↔ ∃ 𝑎 { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑁𝑒 } = { 𝑎 } )
38 33 37 sylibr ( 𝜑 → ( ♯ ‘ { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑁𝑒 } ) = 1 )
39 eqid { 𝑁 } = { 𝑁 }
40 39 iftruei if ( { 𝑁 } = { 𝑁 } , { { 𝑁 } } , ∅ ) = { { 𝑁 } }
41 40 eqeq1i ( if ( { 𝑁 } = { 𝑁 } , { { 𝑁 } } , ∅ ) = { 𝑎 } ↔ { { 𝑁 } } = { 𝑎 } )
42 41 exbii ( ∃ 𝑎 if ( { 𝑁 } = { 𝑁 } , { { 𝑁 } } , ∅ ) = { 𝑎 } ↔ ∃ 𝑎 { { 𝑁 } } = { 𝑎 } )
43 19 42 sylibr ( 𝜑 → ∃ 𝑎 if ( { 𝑁 } = { 𝑁 } , { { 𝑁 } } , ∅ ) = { 𝑎 } )
44 26 rabeqdv ( 𝜑 → { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑒 = { 𝑁 } } = { 𝑒 ∈ { { 𝑁 } } ∣ 𝑒 = { 𝑁 } } )
45 eqeq1 ( 𝑒 = { 𝑁 } → ( 𝑒 = { 𝑁 } ↔ { 𝑁 } = { 𝑁 } ) )
46 45 rabsnif { 𝑒 ∈ { { 𝑁 } } ∣ 𝑒 = { 𝑁 } } = if ( { 𝑁 } = { 𝑁 } , { { 𝑁 } } , ∅ )
47 44 46 eqtrdi ( 𝜑 → { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑒 = { 𝑁 } } = if ( { 𝑁 } = { 𝑁 } , { { 𝑁 } } , ∅ ) )
48 47 eqeq1d ( 𝜑 → ( { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑒 = { 𝑁 } } = { 𝑎 } ↔ if ( { 𝑁 } = { 𝑁 } , { { 𝑁 } } , ∅ ) = { 𝑎 } ) )
49 48 exbidv ( 𝜑 → ( ∃ 𝑎 { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑒 = { 𝑁 } } = { 𝑎 } ↔ ∃ 𝑎 if ( { 𝑁 } = { 𝑁 } , { { 𝑁 } } , ∅ ) = { 𝑎 } ) )
50 43 49 mpbird ( 𝜑 → ∃ 𝑎 { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑒 = { 𝑁 } } = { 𝑎 } )
51 34 rabex { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑒 = { 𝑁 } } ∈ V
52 hash1snb ( { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑒 = { 𝑁 } } ∈ V → ( ( ♯ ‘ { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑒 = { 𝑁 } } ) = 1 ↔ ∃ 𝑎 { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑒 = { 𝑁 } } = { 𝑎 } ) )
53 51 52 ax-mp ( ( ♯ ‘ { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑒 = { 𝑁 } } ) = 1 ↔ ∃ 𝑎 { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑒 = { 𝑁 } } = { 𝑎 } )
54 50 53 sylibr ( 𝜑 → ( ♯ ‘ { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑒 = { 𝑁 } } ) = 1 )
55 38 54 oveq12d ( 𝜑 → ( ( ♯ ‘ { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑁𝑒 } ) +𝑒 ( ♯ ‘ { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑒 = { 𝑁 } } ) ) = ( 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 ‘ 𝐺 ) ‘ 𝑁 ) = 2 )