Metamath Proof Explorer

Theorem 1loopgrvd0

Description: The vertex degree of a one-edge graph, case 1 (for a loop): a loop at a vertex other than the given vertex contributes nothing to the vertex degree. (Contributed by Mario Carneiro, 12-Mar-2015) (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 } >. } )
1loopgrvd0.k 
|- ( ph -> K e. ( V \ { N } ) )
Assertion 1loopgrvd0 
|- ( ph -> ( ( VtxDeg ` G ) ` K ) = 0 )

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 1loopgrvd0.k 
 |-  ( ph -> K e. ( V \ { N } ) )
6 5 eldifbd 
 |-  ( ph -> -. K e. { N } )
7 snex 
 |-  { N } e. _V
8 fvsng 
 |-  ( ( A e. X /\ { N } e. _V ) -> ( { <. A , { N } >. } ` A ) = { N } )
9 2 7 8 sylancl 
 |-  ( ph -> ( { <. A , { N } >. } ` A ) = { N } )
10 9 eleq2d 
 |-  ( ph -> ( K e. ( { <. A , { N } >. } ` A ) <-> K e. { N } ) )
11 6 10 mtbird 
 |-  ( ph -> -. K e. ( { <. A , { N } >. } ` A ) )
12 4 dmeqd 
 |-  ( ph -> dom ( iEdg ` G ) = dom { <. A , { N } >. } )
13 dmsnopg 
 |-  ( { N } e. _V -> dom { <. A , { N } >. } = { A } )
14 7 13 mp1i 
 |-  ( ph -> dom { <. A , { N } >. } = { A } )
15 12 14 eqtrd 
 |-  ( ph -> dom ( iEdg ` G ) = { A } )
16 4 fveq1d 
 |-  ( ph -> ( ( iEdg ` G ) ` i ) = ( { <. A , { N } >. } ` i ) )
17 16 eleq2d 
 |-  ( ph -> ( K e. ( ( iEdg ` G ) ` i ) <-> K e. ( { <. A , { N } >. } ` i ) ) )
18 15 17 rexeqbidv 
 |-  ( ph -> ( E. i e. dom ( iEdg ` G ) K e. ( ( iEdg ` G ) ` i ) <-> E. i e. { A } K e. ( { <. A , { N } >. } ` i ) ) )
19 fveq2 
 |-  ( i = A -> ( { <. A , { N } >. } ` i ) = ( { <. A , { N } >. } ` A ) )
20 19 eleq2d 
 |-  ( i = A -> ( K e. ( { <. A , { N } >. } ` i ) <-> K e. ( { <. A , { N } >. } ` A ) ) )
21 20 rexsng 
 |-  ( A e. X -> ( E. i e. { A } K e. ( { <. A , { N } >. } ` i ) <-> K e. ( { <. A , { N } >. } ` A ) ) )
22 2 21 syl 
 |-  ( ph -> ( E. i e. { A } K e. ( { <. A , { N } >. } ` i ) <-> K e. ( { <. A , { N } >. } ` A ) ) )
23 18 22 bitrd 
 |-  ( ph -> ( E. i e. dom ( iEdg ` G ) K e. ( ( iEdg ` G ) ` i ) <-> K e. ( { <. A , { N } >. } ` A ) ) )
24 11 23 mtbird 
 |-  ( ph -> -. E. i e. dom ( iEdg ` G ) K e. ( ( iEdg ` G ) ` i ) )
25 5 eldifad 
 |-  ( ph -> K e. V )
26 1 eleq2d 
 |-  ( ph -> ( K e. ( Vtx ` G ) <-> K e. V ) )
27 25 26 mpbird 
 |-  ( ph -> K e. ( Vtx ` G ) )
28 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
29 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
30 eqid 
 |-  ( VtxDeg ` G ) = ( VtxDeg ` G )
31 28 29 30 vtxd0nedgb 
 |-  ( K e. ( Vtx ` G ) -> ( ( ( VtxDeg ` G ) ` K ) = 0 <-> -. E. i e. dom ( iEdg ` G ) K e. ( ( iEdg ` G ) ` i ) ) )
32 27 31 syl 
 |-  ( ph -> ( ( ( VtxDeg ` G ) ` K ) = 0 <-> -. E. i e. dom ( iEdg ` G ) K e. ( ( iEdg ` G ) ` i ) ) )
33 24 32 mpbird 
 |-  ( ph -> ( ( VtxDeg ` G ) ` K ) = 0 )