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 ⊢ V = Vtx ⁡ G
Assertion wspthsnwspthsnon ⊢ W ∈ N WSPathsN G ↔ ∃ a ∈ V ∃ b ∈ V W ∈ a N WSPathsNOn G b

Proof

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