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

Metamath Proof Explorer

Theorem wspn0

Description: If there are no vertices, then there are no simple paths (of any length), too. (Contributed by Alexander van der Vekens, 11-Mar-2018) (Revised by AV, 16-May-2021) (Proof shortened by AV, 13-Mar-2022)

Ref Expression
Hypothesis wspn0.v 
|- V = ( Vtx ` G )
Assertion wspn0 
|- ( V = (/) -> ( N WSPathsN G ) = (/) )

Proof

Step Hyp Ref Expression
1 wspn0.v 
 |-  V = ( Vtx ` G )
2 wspthsn 
 |-  ( N WSPathsN G ) = { w e. ( N WWalksN G ) | E. f f ( SPaths ` G ) w }
3 wwlknbp1 
 |-  ( w e. ( N WWalksN G ) -> ( N e. NN0 /\ w e. Word ( Vtx ` G ) /\ ( # ` w ) = ( N + 1 ) ) )
4 1 eqeq1i 
 |-  ( V = (/) <-> ( Vtx ` G ) = (/) )
5 wrdeq 
 |-  ( ( Vtx ` G ) = (/) -> Word ( Vtx ` G ) = Word (/) )
6 4 5 sylbi 
 |-  ( V = (/) -> Word ( Vtx ` G ) = Word (/) )
7 6 eleq2d 
 |-  ( V = (/) -> ( w e. Word ( Vtx ` G ) <-> w e. Word (/) ) )
8 0wrd0 
 |-  ( w e. Word (/) <-> w = (/) )
9 7 8 bitrdi 
 |-  ( V = (/) -> ( w e. Word ( Vtx ` G ) <-> w = (/) ) )
10 fveq2 
 |-  ( w = (/) -> ( # ` w ) = ( # ` (/) ) )
11 hash0 
 |-  ( # ` (/) ) = 0
12 10 11 eqtrdi 
 |-  ( w = (/) -> ( # ` w ) = 0 )
13 12 eqeq1d 
 |-  ( w = (/) -> ( ( # ` w ) = ( N + 1 ) <-> 0 = ( N + 1 ) ) )
14 13 adantl 
 |-  ( ( N e. NN0 /\ w = (/) ) -> ( ( # ` w ) = ( N + 1 ) <-> 0 = ( N + 1 ) ) )
15 nn0p1gt0 
 |-  ( N e. NN0 -> 0 < ( N + 1 ) )
16 15 gt0ne0d 
 |-  ( N e. NN0 -> ( N + 1 ) =/= 0 )
17 eqneqall 
 |-  ( ( N + 1 ) = 0 -> ( ( N + 1 ) =/= 0 -> -. E. f f ( SPaths ` G ) w ) )
18 17 eqcoms 
 |-  ( 0 = ( N + 1 ) -> ( ( N + 1 ) =/= 0 -> -. E. f f ( SPaths ` G ) w ) )
19 16 18 syl5com 
 |-  ( N e. NN0 -> ( 0 = ( N + 1 ) -> -. E. f f ( SPaths ` G ) w ) )
20 19 adantr 
 |-  ( ( N e. NN0 /\ w = (/) ) -> ( 0 = ( N + 1 ) -> -. E. f f ( SPaths ` G ) w ) )
21 14 20 sylbid 
 |-  ( ( N e. NN0 /\ w = (/) ) -> ( ( # ` w ) = ( N + 1 ) -> -. E. f f ( SPaths ` G ) w ) )
22 21 expcom 
 |-  ( w = (/) -> ( N e. NN0 -> ( ( # ` w ) = ( N + 1 ) -> -. E. f f ( SPaths ` G ) w ) ) )
23 22 com23 
 |-  ( w = (/) -> ( ( # ` w ) = ( N + 1 ) -> ( N e. NN0 -> -. E. f f ( SPaths ` G ) w ) ) )
24 9 23 biimtrdi 
 |-  ( V = (/) -> ( w e. Word ( Vtx ` G ) -> ( ( # ` w ) = ( N + 1 ) -> ( N e. NN0 -> -. E. f f ( SPaths ` G ) w ) ) ) )
25 24 com14 
 |-  ( N e. NN0 -> ( w e. Word ( Vtx ` G ) -> ( ( # ` w ) = ( N + 1 ) -> ( V = (/) -> -. E. f f ( SPaths ` G ) w ) ) ) )
26 25 3imp 
 |-  ( ( N e. NN0 /\ w e. Word ( Vtx ` G ) /\ ( # ` w ) = ( N + 1 ) ) -> ( V = (/) -> -. E. f f ( SPaths ` G ) w ) )
27 3 26 syl 
 |-  ( w e. ( N WWalksN G ) -> ( V = (/) -> -. E. f f ( SPaths ` G ) w ) )
28 27 impcom 
 |-  ( ( V = (/) /\ w e. ( N WWalksN G ) ) -> -. E. f f ( SPaths ` G ) w )
29 28 ralrimiva 
 |-  ( V = (/) -> A. w e. ( N WWalksN G ) -. E. f f ( SPaths ` G ) w )
30 rabeq0 
 |-  ( { w e. ( N WWalksN G ) | E. f f ( SPaths ` G ) w } = (/) <-> A. w e. ( N WWalksN G ) -. E. f f ( SPaths ` G ) w )
31 29 30 sylibr 
 |-  ( V = (/) -> { w e. ( N WWalksN G ) | E. f f ( SPaths ` G ) w } = (/) )
32 2 31 eqtrid 
 |-  ( V = (/) -> ( N WSPathsN G ) = (/) )