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}=\mathrm{Vtx}\left({G}\right)$
Assertion wspn0 ${⊢}{V}=\varnothing \to {N}\mathrm{WSPathsN}{G}=\varnothing$

Proof

Step Hyp Ref Expression
1 wspn0.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 wspthsn ${⊢}{N}\mathrm{WSPathsN}{G}=\left\{{w}\in \left({N}\mathrm{WWalksN}{G}\right)|\exists {f}\phantom{\rule{.4em}{0ex}}{f}\mathrm{SPaths}\left({G}\right){w}\right\}$
3 wwlknbp1 ${⊢}{w}\in \left({N}\mathrm{WWalksN}{G}\right)\to \left({N}\in {ℕ}_{0}\wedge {w}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{w}\right|={N}+1\right)$
4 1 eqeq1i ${⊢}{V}=\varnothing ↔\mathrm{Vtx}\left({G}\right)=\varnothing$
5 wrdeq ${⊢}\mathrm{Vtx}\left({G}\right)=\varnothing \to \mathrm{Word}\mathrm{Vtx}\left({G}\right)=\mathrm{Word}\varnothing$
6 4 5 sylbi ${⊢}{V}=\varnothing \to \mathrm{Word}\mathrm{Vtx}\left({G}\right)=\mathrm{Word}\varnothing$
7 6 eleq2d ${⊢}{V}=\varnothing \to \left({w}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)↔{w}\in \mathrm{Word}\varnothing \right)$
8 0wrd0 ${⊢}{w}\in \mathrm{Word}\varnothing ↔{w}=\varnothing$
9 7 8 syl6bb ${⊢}{V}=\varnothing \to \left({w}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)↔{w}=\varnothing \right)$
10 fveq2 ${⊢}{w}=\varnothing \to \left|{w}\right|=\left|\varnothing \right|$
11 hash0 ${⊢}\left|\varnothing \right|=0$
12 10 11 syl6eq ${⊢}{w}=\varnothing \to \left|{w}\right|=0$
13 12 eqeq1d ${⊢}{w}=\varnothing \to \left(\left|{w}\right|={N}+1↔0={N}+1\right)$
14 13 adantl ${⊢}\left({N}\in {ℕ}_{0}\wedge {w}=\varnothing \right)\to \left(\left|{w}\right|={N}+1↔0={N}+1\right)$
15 nn0p1gt0 ${⊢}{N}\in {ℕ}_{0}\to 0<{N}+1$
16 15 gt0ne0d ${⊢}{N}\in {ℕ}_{0}\to {N}+1\ne 0$
17 eqneqall ${⊢}{N}+1=0\to \left({N}+1\ne 0\to ¬\exists {f}\phantom{\rule{.4em}{0ex}}{f}\mathrm{SPaths}\left({G}\right){w}\right)$
18 17 eqcoms ${⊢}0={N}+1\to \left({N}+1\ne 0\to ¬\exists {f}\phantom{\rule{.4em}{0ex}}{f}\mathrm{SPaths}\left({G}\right){w}\right)$
19 16 18 syl5com ${⊢}{N}\in {ℕ}_{0}\to \left(0={N}+1\to ¬\exists {f}\phantom{\rule{.4em}{0ex}}{f}\mathrm{SPaths}\left({G}\right){w}\right)$
20 19 adantr ${⊢}\left({N}\in {ℕ}_{0}\wedge {w}=\varnothing \right)\to \left(0={N}+1\to ¬\exists {f}\phantom{\rule{.4em}{0ex}}{f}\mathrm{SPaths}\left({G}\right){w}\right)$
21 14 20 sylbid ${⊢}\left({N}\in {ℕ}_{0}\wedge {w}=\varnothing \right)\to \left(\left|{w}\right|={N}+1\to ¬\exists {f}\phantom{\rule{.4em}{0ex}}{f}\mathrm{SPaths}\left({G}\right){w}\right)$
22 21 expcom ${⊢}{w}=\varnothing \to \left({N}\in {ℕ}_{0}\to \left(\left|{w}\right|={N}+1\to ¬\exists {f}\phantom{\rule{.4em}{0ex}}{f}\mathrm{SPaths}\left({G}\right){w}\right)\right)$
23 22 com23 ${⊢}{w}=\varnothing \to \left(\left|{w}\right|={N}+1\to \left({N}\in {ℕ}_{0}\to ¬\exists {f}\phantom{\rule{.4em}{0ex}}{f}\mathrm{SPaths}\left({G}\right){w}\right)\right)$
24 9 23 syl6bi ${⊢}{V}=\varnothing \to \left({w}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\to \left(\left|{w}\right|={N}+1\to \left({N}\in {ℕ}_{0}\to ¬\exists {f}\phantom{\rule{.4em}{0ex}}{f}\mathrm{SPaths}\left({G}\right){w}\right)\right)\right)$
25 24 com14 ${⊢}{N}\in {ℕ}_{0}\to \left({w}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\to \left(\left|{w}\right|={N}+1\to \left({V}=\varnothing \to ¬\exists {f}\phantom{\rule{.4em}{0ex}}{f}\mathrm{SPaths}\left({G}\right){w}\right)\right)\right)$
26 25 3imp ${⊢}\left({N}\in {ℕ}_{0}\wedge {w}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge \left|{w}\right|={N}+1\right)\to \left({V}=\varnothing \to ¬\exists {f}\phantom{\rule{.4em}{0ex}}{f}\mathrm{SPaths}\left({G}\right){w}\right)$
27 3 26 syl ${⊢}{w}\in \left({N}\mathrm{WWalksN}{G}\right)\to \left({V}=\varnothing \to ¬\exists {f}\phantom{\rule{.4em}{0ex}}{f}\mathrm{SPaths}\left({G}\right){w}\right)$
28 27 impcom ${⊢}\left({V}=\varnothing \wedge {w}\in \left({N}\mathrm{WWalksN}{G}\right)\right)\to ¬\exists {f}\phantom{\rule{.4em}{0ex}}{f}\mathrm{SPaths}\left({G}\right){w}$
29 28 ralrimiva ${⊢}{V}=\varnothing \to \forall {w}\in \left({N}\mathrm{WWalksN}{G}\right)\phantom{\rule{.4em}{0ex}}¬\exists {f}\phantom{\rule{.4em}{0ex}}{f}\mathrm{SPaths}\left({G}\right){w}$
30 rabeq0 ${⊢}\left\{{w}\in \left({N}\mathrm{WWalksN}{G}\right)|\exists {f}\phantom{\rule{.4em}{0ex}}{f}\mathrm{SPaths}\left({G}\right){w}\right\}=\varnothing ↔\forall {w}\in \left({N}\mathrm{WWalksN}{G}\right)\phantom{\rule{.4em}{0ex}}¬\exists {f}\phantom{\rule{.4em}{0ex}}{f}\mathrm{SPaths}\left({G}\right){w}$
31 29 30 sylibr ${⊢}{V}=\varnothing \to \left\{{w}\in \left({N}\mathrm{WWalksN}{G}\right)|\exists {f}\phantom{\rule{.4em}{0ex}}{f}\mathrm{SPaths}\left({G}\right){w}\right\}=\varnothing$
32 2 31 syl5eq ${⊢}{V}=\varnothing \to {N}\mathrm{WSPathsN}{G}=\varnothing$