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

Metamath Proof Explorer

Theorem vdumgr0

Description: A vertex in a multigraph has degree 0 if the graph consists of only one vertex. (Contributed by Alexander van der Vekens, 6-Dec-2017) (Revised by AV, 2-Apr-2021)

Ref Expression
Hypothesis vdumgr0.v 
|- V = ( Vtx ` G )
Assertion vdumgr0 
|- ( ( G e. UMGraph /\ N e. V /\ ( # ` V ) = 1 ) -> ( ( VtxDeg ` G ) ` N ) = 0 )

Proof

Step Hyp Ref Expression
1 vdumgr0.v 
 |-  V = ( Vtx ` G )
2 umgruhgr 
 |-  ( G e. UMGraph -> G e. UHGraph )
3 2 3ad2ant1 
 |-  ( ( G e. UMGraph /\ N e. V /\ ( # ` V ) = 1 ) -> G e. UHGraph )
4 simp3 
 |-  ( ( G e. UMGraph /\ N e. V /\ ( # ` V ) = 1 ) -> ( # ` V ) = 1 )
5 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
6 1 5 umgrislfupgr 
 |-  ( G e. UMGraph <-> ( G e. UPGraph /\ ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ~P V | 2 <_ ( # ` x ) } ) )
7 6 simprbi 
 |-  ( G e. UMGraph -> ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ~P V | 2 <_ ( # ` x ) } )
8 7 3ad2ant1 
 |-  ( ( G e. UMGraph /\ N e. V /\ ( # ` V ) = 1 ) -> ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ~P V | 2 <_ ( # ` x ) } )
9 3 4 8 3jca 
 |-  ( ( G e. UMGraph /\ N e. V /\ ( # ` V ) = 1 ) -> ( G e. UHGraph /\ ( # ` V ) = 1 /\ ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ~P V | 2 <_ ( # ` x ) } ) )
10 simp2 
 |-  ( ( G e. UMGraph /\ N e. V /\ ( # ` V ) = 1 ) -> N e. V )
11 eqid 
 |-  { x e. ~P V | 2 <_ ( # ` x ) } = { x e. ~P V | 2 <_ ( # ` x ) }
12 1 5 11 vtxdlfuhgr1v 
 |-  ( ( G e. UHGraph /\ ( # ` V ) = 1 /\ ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ~P V | 2 <_ ( # ` x ) } ) -> ( N e. V -> ( ( VtxDeg ` G ) ` N ) = 0 ) )
13 9 10 12 sylc 
 |-  ( ( G e. UMGraph /\ N e. V /\ ( # ` V ) = 1 ) -> ( ( VtxDeg ` G ) ` N ) = 0 )