Metamath Proof Explorer

Theorem wlklnwwlkln2lem

Description: Lemma for wlklnwwlkln2 and wlklnwwlklnupgr2 . Formerly part of proof for wlklnwwlkln2 . (Contributed by Alexander van der Vekens, 21-Jul-2018) (Revised by AV, 12-Apr-2021)

Ref Expression
Hypothesis wlklnwwlkln2lem.1 ⊢ φ → P ∈ WWalks ⁡ G → ∃ f f Walks ⁡ G P
Assertion wlklnwwlkln2lem ⊢ φ → P ∈ N WWalksN G → ∃ f f Walks ⁡ G P ∧ f = N

Proof

Step Hyp Ref Expression
1 wlklnwwlkln2lem.1 ⊢ φ → P ∈ WWalks ⁡ G → ∃ f f Walks ⁡ G P
2 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
3 2 wwlknbp ⊢ P ∈ N WWalksN G → G ∈ V ∧ N ∈ ℕ 0 ∧ P ∈ Word Vtx ⁡ G
4 iswwlksn ⊢ N ∈ ℕ 0 → P ∈ N WWalksN G ↔ P ∈ WWalks ⁡ G ∧ P = N + 1
5 4 adantr ⊢ N ∈ ℕ 0 ∧ P ∈ Word Vtx ⁡ G → P ∈ N WWalksN G ↔ P ∈ WWalks ⁡ G ∧ P = N + 1
6 lencl ⊢ P ∈ Word Vtx ⁡ G → P ∈ ℕ 0
7 6 nn0cnd ⊢ P ∈ Word Vtx ⁡ G → P ∈ ℂ
8 7 adantl ⊢ N ∈ ℕ 0 ∧ P ∈ Word Vtx ⁡ G → P ∈ ℂ
9 1cnd ⊢ N ∈ ℕ 0 ∧ P ∈ Word Vtx ⁡ G → 1 ∈ ℂ
10 nn0cn ⊢ N ∈ ℕ 0 → N ∈ ℂ
11 10 adantr ⊢ N ∈ ℕ 0 ∧ P ∈ Word Vtx ⁡ G → N ∈ ℂ
12 8 9 11 subadd2d ⊢ N ∈ ℕ 0 ∧ P ∈ Word Vtx ⁡ G → P − 1 = N ↔ N + 1 = P
13 eqcom ⊢ N + 1 = P ↔ P = N + 1
14 12 13 bitr2di ⊢ N ∈ ℕ 0 ∧ P ∈ Word Vtx ⁡ G → P = N + 1 ↔ P − 1 = N
15 14 biimpcd ⊢ P = N + 1 → N ∈ ℕ 0 ∧ P ∈ Word Vtx ⁡ G → P − 1 = N
16 15 adantl ⊢ P ∈ WWalks ⁡ G ∧ P = N + 1 → N ∈ ℕ 0 ∧ P ∈ Word Vtx ⁡ G → P − 1 = N
17 16 impcom ⊢ N ∈ ℕ 0 ∧ P ∈ Word Vtx ⁡ G ∧ P ∈ WWalks ⁡ G ∧ P = N + 1 → P − 1 = N
18 1 com12 ⊢ P ∈ WWalks ⁡ G → φ → ∃ f f Walks ⁡ G P
19 18 adantr ⊢ P ∈ WWalks ⁡ G ∧ P = N + 1 → φ → ∃ f f Walks ⁡ G P
20 19 adantl ⊢ N ∈ ℕ 0 ∧ P ∈ Word Vtx ⁡ G ∧ P ∈ WWalks ⁡ G ∧ P = N + 1 → φ → ∃ f f Walks ⁡ G P
21 20 imp ⊢ N ∈ ℕ 0 ∧ P ∈ Word Vtx ⁡ G ∧ P ∈ WWalks ⁡ G ∧ P = N + 1 ∧ φ → ∃ f f Walks ⁡ G P
22 simpr ⊢ N ∈ ℕ 0 ∧ P ∈ Word Vtx ⁡ G ∧ P ∈ WWalks ⁡ G ∧ P = N + 1 ∧ φ ∧ f Walks ⁡ G P → f Walks ⁡ G P
23 wlklenvm1 ⊢ f Walks ⁡ G P → f = P − 1
24 22 23 jccir ⊢ N ∈ ℕ 0 ∧ P ∈ Word Vtx ⁡ G ∧ P ∈ WWalks ⁡ G ∧ P = N + 1 ∧ φ ∧ f Walks ⁡ G P → f Walks ⁡ G P ∧ f = P − 1
25 24 ex ⊢ N ∈ ℕ 0 ∧ P ∈ Word Vtx ⁡ G ∧ P ∈ WWalks ⁡ G ∧ P = N + 1 ∧ φ → f Walks ⁡ G P → f Walks ⁡ G P ∧ f = P − 1
26 25 eximdv ⊢ N ∈ ℕ 0 ∧ P ∈ Word Vtx ⁡ G ∧ P ∈ WWalks ⁡ G ∧ P = N + 1 ∧ φ → ∃ f f Walks ⁡ G P → ∃ f f Walks ⁡ G P ∧ f = P − 1
27 21 26 mpd ⊢ N ∈ ℕ 0 ∧ P ∈ Word Vtx ⁡ G ∧ P ∈ WWalks ⁡ G ∧ P = N + 1 ∧ φ → ∃ f f Walks ⁡ G P ∧ f = P − 1
28 eqeq2 ⊢ P − 1 = N → f = P − 1 ↔ f = N
29 28 anbi2d ⊢ P − 1 = N → f Walks ⁡ G P ∧ f = P − 1 ↔ f Walks ⁡ G P ∧ f = N
30 29 exbidv ⊢ P − 1 = N → ∃ f f Walks ⁡ G P ∧ f = P − 1 ↔ ∃ f f Walks ⁡ G P ∧ f = N
31 27 30 imbitrid ⊢ P − 1 = N → N ∈ ℕ 0 ∧ P ∈ Word Vtx ⁡ G ∧ P ∈ WWalks ⁡ G ∧ P = N + 1 ∧ φ → ∃ f f Walks ⁡ G P ∧ f = N
32 31 expd ⊢ P − 1 = N → N ∈ ℕ 0 ∧ P ∈ Word Vtx ⁡ G ∧ P ∈ WWalks ⁡ G ∧ P = N + 1 → φ → ∃ f f Walks ⁡ G P ∧ f = N
33 17 32 mpcom ⊢ N ∈ ℕ 0 ∧ P ∈ Word Vtx ⁡ G ∧ P ∈ WWalks ⁡ G ∧ P = N + 1 → φ → ∃ f f Walks ⁡ G P ∧ f = N
34 33 ex ⊢ N ∈ ℕ 0 ∧ P ∈ Word Vtx ⁡ G → P ∈ WWalks ⁡ G ∧ P = N + 1 → φ → ∃ f f Walks ⁡ G P ∧ f = N
35 5 34 sylbid ⊢ N ∈ ℕ 0 ∧ P ∈ Word Vtx ⁡ G → P ∈ N WWalksN G → φ → ∃ f f Walks ⁡ G P ∧ f = N
36 35 3adant1 ⊢ G ∈ V ∧ N ∈ ℕ 0 ∧ P ∈ Word Vtx ⁡ G → P ∈ N WWalksN G → φ → ∃ f f Walks ⁡ G P ∧ f = N
37 3 36 mpcom ⊢ P ∈ N WWalksN G → φ → ∃ f f Walks ⁡ G P ∧ f = N
38 37 com12 ⊢ φ → P ∈ N WWalksN G → ∃ f f Walks ⁡ G P ∧ f = N