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 syl6bi
 |-  ( 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 syl5eq
 |-  ( V = (/) -> ( N WSPathsN G ) = (/) )