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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	wspn0	⊢ ( 𝑉 = ∅ → ( 𝑁 WSPathsN 𝐺 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		wspn0.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		wspthsn	⊢ ( 𝑁 WSPathsN 𝐺 ) = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑤 }
3		wwlknbp1	⊢ ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑁 ∈ ℕ0 ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ) )
4	1	eqeq1i	⊢ ( 𝑉 = ∅ ↔ ( Vtx ‘ 𝐺 ) = ∅ )
5		wrdeq	⊢ ( ( Vtx ‘ 𝐺 ) = ∅ → Word ( Vtx ‘ 𝐺 ) = Word ∅ )
6	4 5	sylbi	⊢ ( 𝑉 = ∅ → Word ( Vtx ‘ 𝐺 ) = Word ∅ )
7	6	eleq2d	⊢ ( 𝑉 = ∅ → ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ↔ 𝑤 ∈ Word ∅ ) )
8		0wrd0	⊢ ( 𝑤 ∈ Word ∅ ↔ 𝑤 = ∅ )
9	7 8	bitrdi	⊢ ( 𝑉 = ∅ → ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ↔ 𝑤 = ∅ ) )
10		fveq2	⊢ ( 𝑤 = ∅ → ( ♯ ‘ 𝑤 ) = ( ♯ ‘ ∅ ) )
11		hash0	⊢ ( ♯ ‘ ∅ ) = 0
12	10 11	eqtrdi	⊢ ( 𝑤 = ∅ → ( ♯ ‘ 𝑤 ) = 0 )
13	12	eqeq1d	⊢ ( 𝑤 = ∅ → ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ↔ 0 = ( 𝑁 + 1 ) ) )
14	13	adantl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑤 = ∅ ) → ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ↔ 0 = ( 𝑁 + 1 ) ) )
15		nn0p1gt0	⊢ ( 𝑁 ∈ ℕ0 → 0 < ( 𝑁 + 1 ) )
16	15	gt0ne0d	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ≠ 0 )
17		eqneqall	⊢ ( ( 𝑁 + 1 ) = 0 → ( ( 𝑁 + 1 ) ≠ 0 → ¬ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑤 ) )
18	17	eqcoms	⊢ ( 0 = ( 𝑁 + 1 ) → ( ( 𝑁 + 1 ) ≠ 0 → ¬ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑤 ) )
19	16 18	syl5com	⊢ ( 𝑁 ∈ ℕ0 → ( 0 = ( 𝑁 + 1 ) → ¬ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑤 ) )
20	19	adantr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑤 = ∅ ) → ( 0 = ( 𝑁 + 1 ) → ¬ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑤 ) )
21	14 20	sylbid	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑤 = ∅ ) → ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) → ¬ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑤 ) )
22	21	expcom	⊢ ( 𝑤 = ∅ → ( 𝑁 ∈ ℕ0 → ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) → ¬ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑤 ) ) )
23	22	com23	⊢ ( 𝑤 = ∅ → ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) → ( 𝑁 ∈ ℕ0 → ¬ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑤 ) ) )
24	9 23	syl6bi	⊢ ( 𝑉 = ∅ → ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) → ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) → ( 𝑁 ∈ ℕ0 → ¬ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑤 ) ) ) )
25	24	com14	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) → ( ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) → ( 𝑉 = ∅ → ¬ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑤 ) ) ) )
26	25	3imp	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑤 ) = ( 𝑁 + 1 ) ) → ( 𝑉 = ∅ → ¬ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑤 ) )
27	3 26	syl	⊢ ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑉 = ∅ → ¬ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑤 ) )
28	27	impcom	⊢ ( ( 𝑉 = ∅ ∧ 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ) → ¬ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑤 )
29	28	ralrimiva	⊢ ( 𝑉 = ∅ → ∀ 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ¬ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑤 )
30		rabeq0	⊢ ( { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑤 } = ∅ ↔ ∀ 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ¬ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑤 )
31	29 30	sylibr	⊢ ( 𝑉 = ∅ → { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑤 } = ∅ )
32	2 31	syl5eq	⊢ ( 𝑉 = ∅ → ( 𝑁 WSPathsN 𝐺 ) = ∅ )