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 )