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=∅→NWSPathsNG=∅

Proof

Step Hyp Ref Expression
1 wspn0.v ⊢V=Vtx⁡G
2 wspthsn ⊢NWSPathsNG=w∈NWWalksNG|∃ffSPaths⁡Gw
3 wwlknbp1 ⊢w∈NWWalksNG→N∈ℕ0∧w∈WordVtx⁡G∧w=N+1
4 1 eqeq1i ⊢V=∅↔Vtx⁡G=∅
5 wrdeq ⊢Vtx⁡G=∅→WordVtx⁡G=Word∅
6 4 5 sylbi ⊢V=∅→WordVtx⁡G=Word∅
7 6 eleq2d ⊢V=∅→w∈WordVtx⁡G↔w∈Word∅
8 0wrd0 ⊢w∈Word∅↔w=∅
9 7 8 bitrdi ⊢V=∅→w∈WordVtx⁡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∈ℕ0∧w=∅→w=N+1↔0=N+1
15 nn0p1gt0 ⊢N∈ℕ0→0<N+1
16 15 gt0ne0d ⊢N∈ℕ0→N+1≠0
17 eqneqall ⊢N+1=0→N+1≠0→¬∃ffSPaths⁡Gw
18 17 eqcoms ⊢0=N+1→N+1≠0→¬∃ffSPaths⁡Gw
19 16 18 syl5com ⊢N∈ℕ0→0=N+1→¬∃ffSPaths⁡Gw
20 19 adantr ⊢N∈ℕ0∧w=∅→0=N+1→¬∃ffSPaths⁡Gw
21 14 20 sylbid ⊢N∈ℕ0∧w=∅→w=N+1→¬∃ffSPaths⁡Gw
22 21 expcom ⊢w=∅→N∈ℕ0→w=N+1→¬∃ffSPaths⁡Gw
23 22 com23 ⊢w=∅→w=N+1→N∈ℕ0→¬∃ffSPaths⁡Gw
24 9 23 biimtrdi ⊢V=∅→w∈WordVtx⁡G→w=N+1→N∈ℕ0→¬∃ffSPaths⁡Gw
25 24 com14 ⊢N∈ℕ0→w∈WordVtx⁡G→w=N+1→V=∅→¬∃ffSPaths⁡Gw
26 25 3imp ⊢N∈ℕ0∧w∈WordVtx⁡G∧w=N+1→V=∅→¬∃ffSPaths⁡Gw
27 3 26 syl ⊢w∈NWWalksNG→V=∅→¬∃ffSPaths⁡Gw
28 27 impcom ⊢V=∅∧w∈NWWalksNG→¬∃ffSPaths⁡Gw
29 28 ralrimiva ⊢V=∅→∀w∈NWWalksNG¬∃ffSPaths⁡Gw
30 rabeq0 ⊢w∈NWWalksNG|∃ffSPaths⁡Gw=∅↔∀w∈NWWalksNG¬∃ffSPaths⁡Gw
31 29 30 sylibr ⊢V=∅→w∈NWWalksNG|∃ffSPaths⁡Gw=∅
32 2 31 eqtrid ⊢V=∅→NWSPathsNG=∅