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 
|- ( ph -> ( Vtx ` G ) = V )
1loopgruspgr.a 
|- ( ph -> A e. X )
1loopgruspgr.n 
|- ( ph -> N e. V )
1loopgruspgr.i 
|- ( ph -> ( iEdg ` G ) = { <. A , { N } >. } )
Assertion 1loopgrvd2 
|- ( ph -> ( ( VtxDeg ` G ) ` N ) = 2 )

Proof

Step Hyp Ref Expression
1 1loopgruspgr.v 
 |-  ( ph -> ( Vtx ` G ) = V )
2 1loopgruspgr.a 
 |-  ( ph -> A e. X )
3 1loopgruspgr.n 
 |-  ( ph -> N e. V )
4 1loopgruspgr.i 
 |-  ( ph -> ( iEdg ` G ) = { <. A , { N } >. } )
5 1 2 3 4 1loopgruspgr 
 |-  ( ph -> G e. USPGraph )
6 uspgrushgr 
 |-  ( G e. USPGraph -> G e. USHGraph )
7 5 6 syl 
 |-  ( ph -> G e. USHGraph )
8 3 1 eleqtrrd 
 |-  ( ph -> N e. ( 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 e. USHGraph /\ N e. ( Vtx ` G ) ) -> ( ( VtxDeg ` G ) ` N ) = ( ( # ` { e e. ( Edg ` G ) | N e. e } ) +e ( # ` { e e. ( Edg ` G ) | e = { N } } ) ) )
13 7 8 12 syl2anc 
 |-  ( ph -> ( ( VtxDeg ` G ) ` N ) = ( ( # ` { e e. ( Edg ` G ) | N e. e } ) +e ( # ` { e e. ( Edg ` G ) | e = { N } } ) ) )
14 snex 
 |-  { N } e. _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 
 |-  E. a { { N } } = { a }
19 18 a1i 
 |-  ( ph -> E. a { { N } } = { a } )
20 snidg 
 |-  ( N e. V -> N e. { N } )
21 3 20 syl 
 |-  ( ph -> N e. { N } )
22 21 iftrued 
 |-  ( ph -> if ( N e. { N } , { { N } } , (/) ) = { { N } } )
23 22 eqeq1d 
 |-  ( ph -> ( if ( N e. { N } , { { N } } , (/) ) = { a } <-> { { N } } = { a } ) )
24 23 exbidv 
 |-  ( ph -> ( E. a if ( N e. { N } , { { N } } , (/) ) = { a } <-> E. a { { N } } = { a } ) )
25 19 24 mpbird 
 |-  ( ph -> E. a if ( N e. { N } , { { N } } , (/) ) = { a } )
26 1 2 3 4 1loopgredg 
 |-  ( ph -> ( Edg ` G ) = { { N } } )
27 26 rabeqdv 
 |-  ( ph -> { e e. ( Edg ` G ) | N e. e } = { e e. { { N } } | N e. e } )
28 eleq2 
 |-  ( e = { N } -> ( N e. e <-> N e. { N } ) )
29 28 rabsnif 
 |-  { e e. { { N } } | N e. e } = if ( N e. { N } , { { N } } , (/) )
30 27 29 eqtrdi 
 |-  ( ph -> { e e. ( Edg ` G ) | N e. e } = if ( N e. { N } , { { N } } , (/) ) )
31 30 eqeq1d 
 |-  ( ph -> ( { e e. ( Edg ` G ) | N e. e } = { a } <-> if ( N e. { N } , { { N } } , (/) ) = { a } ) )
32 31 exbidv 
 |-  ( ph -> ( E. a { e e. ( Edg ` G ) | N e. e } = { a } <-> E. a if ( N e. { N } , { { N } } , (/) ) = { a } ) )
33 25 32 mpbird 
 |-  ( ph -> E. a { e e. ( Edg ` G ) | N e. e } = { a } )
34 fvex 
 |-  ( Edg ` G ) e. _V
35 34 rabex 
 |-  { e e. ( Edg ` G ) | N e. e } e. _V
36 hash1snb 
 |-  ( { e e. ( Edg ` G ) | N e. e } e. _V -> ( ( # ` { e e. ( Edg ` G ) | N e. e } ) = 1 <-> E. a { e e. ( Edg ` G ) | N e. e } = { a } ) )
37 35 36 ax-mp 
 |-  ( ( # ` { e e. ( Edg ` G ) | N e. e } ) = 1 <-> E. a { e e. ( Edg ` G ) | N e. e } = { a } )
38 33 37 sylibr 
 |-  ( ph -> ( # ` { e e. ( Edg ` G ) | N e. 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 
 |-  ( E. a if ( { N } = { N } , { { N } } , (/) ) = { a } <-> E. a { { N } } = { a } )
43 19 42 sylibr 
 |-  ( ph -> E. a if ( { N } = { N } , { { N } } , (/) ) = { a } )
44 26 rabeqdv 
 |-  ( ph -> { e e. ( Edg ` G ) | e = { N } } = { e e. { { N } } | e = { N } } )
45 eqeq1 
 |-  ( e = { N } -> ( e = { N } <-> { N } = { N } ) )
46 45 rabsnif 
 |-  { e e. { { N } } | e = { N } } = if ( { N } = { N } , { { N } } , (/) )
47 44 46 eqtrdi 
 |-  ( ph -> { e e. ( Edg ` G ) | e = { N } } = if ( { N } = { N } , { { N } } , (/) ) )
48 47 eqeq1d 
 |-  ( ph -> ( { e e. ( Edg ` G ) | e = { N } } = { a } <-> if ( { N } = { N } , { { N } } , (/) ) = { a } ) )
49 48 exbidv 
 |-  ( ph -> ( E. a { e e. ( Edg ` G ) | e = { N } } = { a } <-> E. a if ( { N } = { N } , { { N } } , (/) ) = { a } ) )
50 43 49 mpbird 
 |-  ( ph -> E. a { e e. ( Edg ` G ) | e = { N } } = { a } )
51 34 rabex 
 |-  { e e. ( Edg ` G ) | e = { N } } e. _V
52 hash1snb 
 |-  ( { e e. ( Edg ` G ) | e = { N } } e. _V -> ( ( # ` { e e. ( Edg ` G ) | e = { N } } ) = 1 <-> E. a { e e. ( Edg ` G ) | e = { N } } = { a } ) )
53 51 52 ax-mp 
 |-  ( ( # ` { e e. ( Edg ` G ) | e = { N } } ) = 1 <-> E. a { e e. ( Edg ` G ) | e = { N } } = { a } )
54 50 53 sylibr 
 |-  ( ph -> ( # ` { e e. ( Edg ` G ) | e = { N } } ) = 1 )
55 38 54 oveq12d 
 |-  ( ph -> ( ( # ` { e e. ( Edg ` G ) | N e. e } ) +e ( # ` { e e. ( Edg ` G ) | e = { N } } ) ) = ( 1 +e 1 ) )
56 1re 
 |-  1 e. RR
57 rexadd 
 |-  ( ( 1 e. RR /\ 1 e. RR ) -> ( 1 +e 1 ) = ( 1 + 1 ) )
58 56 56 57 mp2an 
 |-  ( 1 +e 1 ) = ( 1 + 1 )
59 1p1e2 
 |-  ( 1 + 1 ) = 2
60 58 59 eqtri 
 |-  ( 1 +e 1 ) = 2
61 60 a1i 
 |-  ( ph -> ( 1 +e 1 ) = 2 )
62 13 55 61 3eqtrd 
 |-  ( ph -> ( ( VtxDeg ` G ) ` N ) = 2 )