Metamath Proof Explorer

Theorem vdn0conngrumgrv2

Description: A vertex in a connected multigraph with more than one vertex cannot have degree 0. (Contributed by Alexander van der Vekens, 9-Dec-2017) (Revised by AV, 4-Apr-2021)

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

Proof

Step Hyp Ref Expression
1 vdn0conngrv2.v 
 |-  V = ( Vtx ` G )
2 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
3 eqid 
 |-  dom ( iEdg ` G ) = dom ( iEdg ` G )
4 eqid 
 |-  ( VtxDeg ` G ) = ( VtxDeg ` G )
5 1 2 3 4 vtxdumgrval 
 |-  ( ( G e. UMGraph /\ N e. V ) -> ( ( VtxDeg ` G ) ` N ) = ( # ` { x e. dom ( iEdg ` G ) | N e. ( ( iEdg ` G ) ` x ) } ) )
6 5 ad2ant2lr 
 |-  ( ( ( G e. ConnGraph /\ G e. UMGraph ) /\ ( N e. V /\ 1 < ( # ` V ) ) ) -> ( ( VtxDeg ` G ) ` N ) = ( # ` { x e. dom ( iEdg ` G ) | N e. ( ( iEdg ` G ) ` x ) } ) )
7 umgruhgr 
 |-  ( G e. UMGraph -> G e. UHGraph )
8 2 uhgrfun 
 |-  ( G e. UHGraph -> Fun ( iEdg ` G ) )
9 funfn 
 |-  ( Fun ( iEdg ` G ) <-> ( iEdg ` G ) Fn dom ( iEdg ` G ) )
10 9 biimpi 
 |-  ( Fun ( iEdg ` G ) -> ( iEdg ` G ) Fn dom ( iEdg ` G ) )
11 7 8 10 3syl 
 |-  ( G e. UMGraph -> ( iEdg ` G ) Fn dom ( iEdg ` G ) )
12 11 adantl 
 |-  ( ( G e. ConnGraph /\ G e. UMGraph ) -> ( iEdg ` G ) Fn dom ( iEdg ` G ) )
13 12 adantr 
 |-  ( ( ( G e. ConnGraph /\ G e. UMGraph ) /\ ( N e. V /\ 1 < ( # ` V ) ) ) -> ( iEdg ` G ) Fn dom ( iEdg ` G ) )
14 simpl 
 |-  ( ( G e. ConnGraph /\ G e. UMGraph ) -> G e. ConnGraph )
15 14 adantr 
 |-  ( ( ( G e. ConnGraph /\ G e. UMGraph ) /\ ( N e. V /\ 1 < ( # ` V ) ) ) -> G e. ConnGraph )
16 simpl 
 |-  ( ( N e. V /\ 1 < ( # ` V ) ) -> N e. V )
17 16 adantl 
 |-  ( ( ( G e. ConnGraph /\ G e. UMGraph ) /\ ( N e. V /\ 1 < ( # ` V ) ) ) -> N e. V )
18 simprr 
 |-  ( ( ( G e. ConnGraph /\ G e. UMGraph ) /\ ( N e. V /\ 1 < ( # ` V ) ) ) -> 1 < ( # ` V ) )
19 1 2 conngrv2edg 
 |-  ( ( G e. ConnGraph /\ N e. V /\ 1 < ( # ` V ) ) -> E. e e. ran ( iEdg ` G ) N e. e )
20 15 17 18 19 syl3anc 
 |-  ( ( ( G e. ConnGraph /\ G e. UMGraph ) /\ ( N e. V /\ 1 < ( # ` V ) ) ) -> E. e e. ran ( iEdg ` G ) N e. e )
21 eleq2 
 |-  ( e = ( ( iEdg ` G ) ` x ) -> ( N e. e <-> N e. ( ( iEdg ` G ) ` x ) ) )
22 21 rexrn 
 |-  ( ( iEdg ` G ) Fn dom ( iEdg ` G ) -> ( E. e e. ran ( iEdg ` G ) N e. e <-> E. x e. dom ( iEdg ` G ) N e. ( ( iEdg ` G ) ` x ) ) )
23 22 biimpd 
 |-  ( ( iEdg ` G ) Fn dom ( iEdg ` G ) -> ( E. e e. ran ( iEdg ` G ) N e. e -> E. x e. dom ( iEdg ` G ) N e. ( ( iEdg ` G ) ` x ) ) )
24 13 20 23 sylc 
 |-  ( ( ( G e. ConnGraph /\ G e. UMGraph ) /\ ( N e. V /\ 1 < ( # ` V ) ) ) -> E. x e. dom ( iEdg ` G ) N e. ( ( iEdg ` G ) ` x ) )
25 dfrex2 
 |-  ( E. x e. dom ( iEdg ` G ) N e. ( ( iEdg ` G ) ` x ) <-> -. A. x e. dom ( iEdg ` G ) -. N e. ( ( iEdg ` G ) ` x ) )
26 24 25 sylib 
 |-  ( ( ( G e. ConnGraph /\ G e. UMGraph ) /\ ( N e. V /\ 1 < ( # ` V ) ) ) -> -. A. x e. dom ( iEdg ` G ) -. N e. ( ( iEdg ` G ) ` x ) )
27 fvex 
 |-  ( iEdg ` G ) e. _V
28 27 dmex 
 |-  dom ( iEdg ` G ) e. _V
29 28 a1i 
 |-  ( ( ( G e. ConnGraph /\ G e. UMGraph ) /\ ( N e. V /\ 1 < ( # ` V ) ) ) -> dom ( iEdg ` G ) e. _V )
30 rabexg 
 |-  ( dom ( iEdg ` G ) e. _V -> { x e. dom ( iEdg ` G ) | N e. ( ( iEdg ` G ) ` x ) } e. _V )
31 hasheq0 
 |-  ( { x e. dom ( iEdg ` G ) | N e. ( ( iEdg ` G ) ` x ) } e. _V -> ( ( # ` { x e. dom ( iEdg ` G ) | N e. ( ( iEdg ` G ) ` x ) } ) = 0 <-> { x e. dom ( iEdg ` G ) | N e. ( ( iEdg ` G ) ` x ) } = (/) ) )
32 29 30 31 3syl 
 |-  ( ( ( G e. ConnGraph /\ G e. UMGraph ) /\ ( N e. V /\ 1 < ( # ` V ) ) ) -> ( ( # ` { x e. dom ( iEdg ` G ) | N e. ( ( iEdg ` G ) ` x ) } ) = 0 <-> { x e. dom ( iEdg ` G ) | N e. ( ( iEdg ` G ) ` x ) } = (/) ) )
33 rabeq0 
 |-  ( { x e. dom ( iEdg ` G ) | N e. ( ( iEdg ` G ) ` x ) } = (/) <-> A. x e. dom ( iEdg ` G ) -. N e. ( ( iEdg ` G ) ` x ) )
34 32 33 bitrdi 
 |-  ( ( ( G e. ConnGraph /\ G e. UMGraph ) /\ ( N e. V /\ 1 < ( # ` V ) ) ) -> ( ( # ` { x e. dom ( iEdg ` G ) | N e. ( ( iEdg ` G ) ` x ) } ) = 0 <-> A. x e. dom ( iEdg ` G ) -. N e. ( ( iEdg ` G ) ` x ) ) )
35 34 necon3abid 
 |-  ( ( ( G e. ConnGraph /\ G e. UMGraph ) /\ ( N e. V /\ 1 < ( # ` V ) ) ) -> ( ( # ` { x e. dom ( iEdg ` G ) | N e. ( ( iEdg ` G ) ` x ) } ) =/= 0 <-> -. A. x e. dom ( iEdg ` G ) -. N e. ( ( iEdg ` G ) ` x ) ) )
36 26 35 mpbird 
 |-  ( ( ( G e. ConnGraph /\ G e. UMGraph ) /\ ( N e. V /\ 1 < ( # ` V ) ) ) -> ( # ` { x e. dom ( iEdg ` G ) | N e. ( ( iEdg ` G ) ` x ) } ) =/= 0 )
37 6 36 eqnetrd 
 |-  ( ( ( G e. ConnGraph /\ G e. UMGraph ) /\ ( N e. V /\ 1 < ( # ` V ) ) ) -> ( ( VtxDeg ` G ) ` N ) =/= 0 )