Metamath Proof Explorer

Theorem wspthsnwspthsnon

Description: A simple path of fixed length is a simple path of fixed length between two vertices. (Contributed by Alexander van der Vekens, 1-Mar-2018) (Revised by AV, 16-May-2021) (Revised by AV, 13-Mar-2022)

Ref Expression
Hypothesis wwlksnwwlksnon.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion wspthsnwspthsnon ( 𝑊 ∈ ( 𝑁 WSPathsN 𝐺 ) ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑊 ∈ ( 𝑎 ( 𝑁 WSPathsNOn 𝐺 ) 𝑏 ) )

Proof

Step Hyp Ref Expression
1 wwlksnwwlksnon.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 iswspthn ⊢ ( 𝑊 ∈ ( 𝑁 WSPathsN 𝐺 ) ↔ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑊 ) )
3 1 wwlksnwwlksnon ⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑊 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) )
4 3 anbi1i ⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑊 ) ↔ ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑊 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) ∧ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑊 ) )
5 r19.41vv ⊢ ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑊 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) ∧ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑊 ) ↔ ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑊 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) ∧ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑊 ) )
6 4 5 bitr4i ⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑊 ) ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑊 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) ∧ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑊 ) )
7 3anass ⊢ ( ( 𝑓 ( SPaths ‘ 𝐺 ) 𝑊 ∧ ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) ↔ ( 𝑓 ( SPaths ‘ 𝐺 ) 𝑊 ∧ ( ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) ) )
8 7 a1i ⊢ ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑊 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) ) → ( ( 𝑓 ( SPaths ‘ 𝐺 ) 𝑊 ∧ ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) ↔ ( 𝑓 ( SPaths ‘ 𝐺 ) 𝑊 ∧ ( ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) ) ) )
9 vex ⊢ 𝑓 ∈ V
10 1 isspthonpth ⊢ ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑓 ∈ V ∧ 𝑊 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) ) ) → ( 𝑓 ( 𝑎 ( SPathsOn ‘ 𝐺 ) 𝑏 ) 𝑊 ↔ ( 𝑓 ( SPaths ‘ 𝐺 ) 𝑊 ∧ ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) ) )
11 9 10 mpanr1 ⊢ ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑊 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) ) → ( 𝑓 ( 𝑎 ( SPathsOn ‘ 𝐺 ) 𝑏 ) 𝑊 ↔ ( 𝑓 ( SPaths ‘ 𝐺 ) 𝑊 ∧ ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) ) )
12 spthiswlk ⊢ ( 𝑓 ( SPaths ‘ 𝐺 ) 𝑊 → 𝑓 ( Walks ‘ 𝐺 ) 𝑊 )
13 wlklenvm1 ⊢ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑊 → ( ♯ ‘ 𝑓 ) = ( ( ♯ ‘ 𝑊 ) − 1 ) )
14 wwlknon ⊢ ( 𝑊 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) ↔ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ 𝑁 ) = 𝑏 ) )
15 simpl2 ⊢ ( ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ 𝑁 ) = 𝑏 ) ∧ ( ♯ ‘ 𝑓 ) = ( ( ♯ ‘ 𝑊 ) − 1 ) ) → ( 𝑊 ‘ 0 ) = 𝑎 )
16 simpr ⊢ ( ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ 𝑁 ) = 𝑏 ) ∧ ( ♯ ‘ 𝑓 ) = ( ( ♯ ‘ 𝑊 ) − 1 ) ) → ( ♯ ‘ 𝑓 ) = ( ( ♯ ‘ 𝑊 ) − 1 ) )
17 wwlknbp1 ⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) )
18 oveq1 ⊢ ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) → ( ( ♯ ‘ 𝑊 ) − 1 ) = ( ( 𝑁 + 1 ) − 1 ) )
19 18 3ad2ant3 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( ( ♯ ‘ 𝑊 ) − 1 ) = ( ( 𝑁 + 1 ) − 1 ) )
20 nn0cn ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ )
21 pncan1 ⊢ ( 𝑁 ∈ ℂ → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
22 20 21 syl ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
23 22 3ad2ant1 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
24 19 23 eqtrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ) → ( ( ♯ ‘ 𝑊 ) − 1 ) = 𝑁 )
25 17 24 syl ⊢ ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) → ( ( ♯ ‘ 𝑊 ) − 1 ) = 𝑁 )
26 25 3ad2ant1 ⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ 𝑁 ) = 𝑏 ) → ( ( ♯ ‘ 𝑊 ) − 1 ) = 𝑁 )
27 26 adantr ⊢ ( ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ 𝑁 ) = 𝑏 ) ∧ ( ♯ ‘ 𝑓 ) = ( ( ♯ ‘ 𝑊 ) − 1 ) ) → ( ( ♯ ‘ 𝑊 ) − 1 ) = 𝑁 )
28 16 27 eqtrd ⊢ ( ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ 𝑁 ) = 𝑏 ) ∧ ( ♯ ‘ 𝑓 ) = ( ( ♯ ‘ 𝑊 ) − 1 ) ) → ( ♯ ‘ 𝑓 ) = 𝑁 )
29 28 fveq2d ⊢ ( ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ 𝑁 ) = 𝑏 ) ∧ ( ♯ ‘ 𝑓 ) = ( ( ♯ ‘ 𝑊 ) − 1 ) ) → ( 𝑊 ‘ ( ♯ ‘ 𝑓 ) ) = ( 𝑊 ‘ 𝑁 ) )
30 simpl3 ⊢ ( ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ 𝑁 ) = 𝑏 ) ∧ ( ♯ ‘ 𝑓 ) = ( ( ♯ ‘ 𝑊 ) − 1 ) ) → ( 𝑊 ‘ 𝑁 ) = 𝑏 )
31 29 30 eqtrd ⊢ ( ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ 𝑁 ) = 𝑏 ) ∧ ( ♯ ‘ 𝑓 ) = ( ( ♯ ‘ 𝑊 ) − 1 ) ) → ( 𝑊 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 )
32 15 31 jca ⊢ ( ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ 𝑁 ) = 𝑏 ) ∧ ( ♯ ‘ 𝑓 ) = ( ( ♯ ‘ 𝑊 ) − 1 ) ) → ( ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) )
33 32 ex ⊢ ( ( 𝑊 ∈ ( 𝑁 WWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ 𝑁 ) = 𝑏 ) → ( ( ♯ ‘ 𝑓 ) = ( ( ♯ ‘ 𝑊 ) − 1 ) → ( ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) ) )
34 14 33 sylbi ⊢ ( 𝑊 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) → ( ( ♯ ‘ 𝑓 ) = ( ( ♯ ‘ 𝑊 ) − 1 ) → ( ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) ) )
35 34 adantl ⊢ ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑊 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) ) → ( ( ♯ ‘ 𝑓 ) = ( ( ♯ ‘ 𝑊 ) − 1 ) → ( ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) ) )
36 35 com12 ⊢ ( ( ♯ ‘ 𝑓 ) = ( ( ♯ ‘ 𝑊 ) − 1 ) → ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑊 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) ) → ( ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) ) )
37 12 13 36 3syl ⊢ ( 𝑓 ( SPaths ‘ 𝐺 ) 𝑊 → ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑊 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) ) → ( ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) ) )
38 37 com12 ⊢ ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑊 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) ) → ( 𝑓 ( SPaths ‘ 𝐺 ) 𝑊 → ( ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) ) )
39 38 pm4.71d ⊢ ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑊 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) ) → ( 𝑓 ( SPaths ‘ 𝐺 ) 𝑊 ↔ ( 𝑓 ( SPaths ‘ 𝐺 ) 𝑊 ∧ ( ( 𝑊 ‘ 0 ) = 𝑎 ∧ ( 𝑊 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) ) ) )
40 8 11 39 3bitr4rd ⊢ ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑊 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) ) → ( 𝑓 ( SPaths ‘ 𝐺 ) 𝑊 ↔ 𝑓 ( 𝑎 ( SPathsOn ‘ 𝐺 ) 𝑏 ) 𝑊 ) )
41 40 exbidv ⊢ ( ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ 𝑊 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) ) → ( ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑊 ↔ ∃ 𝑓 𝑓 ( 𝑎 ( SPathsOn ‘ 𝐺 ) 𝑏 ) 𝑊 ) )
42 41 pm5.32da ⊢ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( ( 𝑊 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) ∧ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑊 ) ↔ ( 𝑊 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) ∧ ∃ 𝑓 𝑓 ( 𝑎 ( SPathsOn ‘ 𝐺 ) 𝑏 ) 𝑊 ) ) )
43 wspthnon ⊢ ( 𝑊 ∈ ( 𝑎 ( 𝑁 WSPathsNOn 𝐺 ) 𝑏 ) ↔ ( 𝑊 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) ∧ ∃ 𝑓 𝑓 ( 𝑎 ( SPathsOn ‘ 𝐺 ) 𝑏 ) 𝑊 ) )
44 42 43 bitr4di ⊢ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( ( 𝑊 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) ∧ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑊 ) ↔ 𝑊 ∈ ( 𝑎 ( 𝑁 WSPathsNOn 𝐺 ) 𝑏 ) ) )
45 44 2rexbiia ⊢ ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑊 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) ∧ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑊 ) ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑊 ∈ ( 𝑎 ( 𝑁 WSPathsNOn 𝐺 ) 𝑏 ) )
46 2 6 45 3bitri ⊢ ( 𝑊 ∈ ( 𝑁 WSPathsN 𝐺 ) ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑊 ∈ ( 𝑎 ( 𝑁 WSPathsNOn 𝐺 ) 𝑏 ) )