This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )