Metamath Proof Explorer

Theorem wwlksnfiOLD

Description: Obsolete version of wwlksnfi as of 4-May-2023. (Contributed by Alexander van der Vekens, 30-Jul-2018) (Revised by AV, 19-Apr-2021) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion wwlksnfiOLD ⊢ Vtx ⁡ G ∈ Fin → N WWalksN G ∈ Fin

Proof

Step Hyp Ref Expression
1 wwlksn ⊢ N ∈ ℕ 0 → N WWalksN G = w ∈ WWalks ⁡ G | w = N + 1
2 df-rab ⊢ w ∈ WWalks ⁡ G | w = N + 1 = w | w ∈ WWalks ⁡ G ∧ w = N + 1
3 1 2 syl6eq ⊢ N ∈ ℕ 0 → N WWalksN G = w | w ∈ WWalks ⁡ G ∧ w = N + 1
4 3 adantl ⊢ G ∈ V ∧ N ∈ ℕ 0 → N WWalksN G = w | w ∈ WWalks ⁡ G ∧ w = N + 1
5 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
6 eqid ⊢ Edg ⁡ G = Edg ⁡ G
7 5 6 iswwlks ⊢ w ∈ WWalks ⁡ G ↔ w ≠ ∅ ∧ w ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ G
8 7 a1i ⊢ G ∈ V ∧ N ∈ ℕ 0 → w ∈ WWalks ⁡ G ↔ w ≠ ∅ ∧ w ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ G
9 8 anbi1d ⊢ G ∈ V ∧ N ∈ ℕ 0 → w ∈ WWalks ⁡ G ∧ w = N + 1 ↔ w ≠ ∅ ∧ w ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ G ∧ w = N + 1
10 9 abbidv ⊢ G ∈ V ∧ N ∈ ℕ 0 → w | w ∈ WWalks ⁡ G ∧ w = N + 1 = w | w ≠ ∅ ∧ w ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ G ∧ w = N + 1
11 3anan12 ⊢ w ≠ ∅ ∧ w ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ G ↔ w ∈ Word Vtx ⁡ G ∧ w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ G
12 11 anbi1i ⊢ w ≠ ∅ ∧ w ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ G ∧ w = N + 1 ↔ w ∈ Word Vtx ⁡ G ∧ w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ G ∧ w = N + 1
13 anass ⊢ w ∈ Word Vtx ⁡ G ∧ w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ G ∧ w = N + 1 ↔ w ∈ Word Vtx ⁡ G ∧ w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ G ∧ w = N + 1
14 12 13 bitri ⊢ w ≠ ∅ ∧ w ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ G ∧ w = N + 1 ↔ w ∈ Word Vtx ⁡ G ∧ w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ G ∧ w = N + 1
15 14 abbii ⊢ w | w ≠ ∅ ∧ w ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ G ∧ w = N + 1 = w | w ∈ Word Vtx ⁡ G ∧ w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ G ∧ w = N + 1
16 df-rab ⊢ w ∈ Word Vtx ⁡ G | w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ G ∧ w = N + 1 = w | w ∈ Word Vtx ⁡ G ∧ w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ G ∧ w = N + 1
17 15 16 eqtr4i ⊢ w | w ≠ ∅ ∧ w ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ G ∧ w = N + 1 = w ∈ Word Vtx ⁡ G | w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ G ∧ w = N + 1
18 10 17 syl6eq ⊢ G ∈ V ∧ N ∈ ℕ 0 → w | w ∈ WWalks ⁡ G ∧ w = N + 1 = w ∈ Word Vtx ⁡ G | w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ G ∧ w = N + 1
19 4 18 eqtrd ⊢ G ∈ V ∧ N ∈ ℕ 0 → N WWalksN G = w ∈ Word Vtx ⁡ G | w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ G ∧ w = N + 1
20 19 adantr ⊢ G ∈ V ∧ N ∈ ℕ 0 ∧ Vtx ⁡ G ∈ Fin → N WWalksN G = w ∈ Word Vtx ⁡ G | w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ G ∧ w = N + 1
21 peano2nn0 ⊢ N ∈ ℕ 0 → N + 1 ∈ ℕ 0
22 21 adantl ⊢ G ∈ V ∧ N ∈ ℕ 0 → N + 1 ∈ ℕ 0
23 22 anim2i ⊢ Vtx ⁡ G ∈ Fin ∧ G ∈ V ∧ N ∈ ℕ 0 → Vtx ⁡ G ∈ Fin ∧ N + 1 ∈ ℕ 0
24 23 ancoms ⊢ G ∈ V ∧ N ∈ ℕ 0 ∧ Vtx ⁡ G ∈ Fin → Vtx ⁡ G ∈ Fin ∧ N + 1 ∈ ℕ 0
25 wrdnfiOLD ⊢ Vtx ⁡ G ∈ Fin ∧ N + 1 ∈ ℕ 0 → w ∈ Word Vtx ⁡ G | w = N + 1 ∈ Fin
26 24 25 syl ⊢ G ∈ V ∧ N ∈ ℕ 0 ∧ Vtx ⁡ G ∈ Fin → w ∈ Word Vtx ⁡ G | w = N + 1 ∈ Fin
27 simpr ⊢ w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ G ∧ w = N + 1 → w = N + 1
28 27 rgenw ⊢ ∀ w ∈ Word Vtx ⁡ G w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ G ∧ w = N + 1 → w = N + 1
29 ss2rab ⊢ w ∈ Word Vtx ⁡ G | w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ G ∧ w = N + 1 ⊆ w ∈ Word Vtx ⁡ G | w = N + 1 ↔ ∀ w ∈ Word Vtx ⁡ G w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ G ∧ w = N + 1 → w = N + 1
30 28 29 mpbir ⊢ w ∈ Word Vtx ⁡ G | w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ G ∧ w = N + 1 ⊆ w ∈ Word Vtx ⁡ G | w = N + 1
31 ssfi ⊢ w ∈ Word Vtx ⁡ G | w = N + 1 ∈ Fin ∧ w ∈ Word Vtx ⁡ G | w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ G ∧ w = N + 1 ⊆ w ∈ Word Vtx ⁡ G | w = N + 1 → w ∈ Word Vtx ⁡ G | w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ G ∧ w = N + 1 ∈ Fin
32 26 30 31 sylancl ⊢ G ∈ V ∧ N ∈ ℕ 0 ∧ Vtx ⁡ G ∈ Fin → w ∈ Word Vtx ⁡ G | w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ G ∧ w = N + 1 ∈ Fin
33 20 32 eqeltrd ⊢ G ∈ V ∧ N ∈ ℕ 0 ∧ Vtx ⁡ G ∈ Fin → N WWalksN G ∈ Fin
34 33 ex ⊢ G ∈ V ∧ N ∈ ℕ 0 → Vtx ⁡ G ∈ Fin → N WWalksN G ∈ Fin
35 wwlksnndef ⊢ G ∉ V ∨ N ∉ ℕ 0 → N WWalksN G = ∅
36 ioran ⊢ ¬ G ∉ V ∨ N ∉ ℕ 0 ↔ ¬ G ∉ V ∧ ¬ N ∉ ℕ 0
37 nnel ⊢ ¬ G ∉ V ↔ G ∈ V
38 nnel ⊢ ¬ N ∉ ℕ 0 ↔ N ∈ ℕ 0
39 37 38 anbi12i ⊢ ¬ G ∉ V ∧ ¬ N ∉ ℕ 0 ↔ G ∈ V ∧ N ∈ ℕ 0
40 36 39 sylbb ⊢ ¬ G ∉ V ∨ N ∉ ℕ 0 → G ∈ V ∧ N ∈ ℕ 0
41 35 40 nsyl4 ⊢ ¬ G ∈ V ∧ N ∈ ℕ 0 → N WWalksN G = ∅
42 0fin ⊢ ∅ ∈ Fin
43 42 a1i ⊢ ¬ G ∈ V ∧ N ∈ ℕ 0 → ∅ ∈ Fin
44 41 43 eqeltrd ⊢ ¬ G ∈ V ∧ N ∈ ℕ 0 → N WWalksN G ∈ Fin
45 44 a1d ⊢ ¬ G ∈ V ∧ N ∈ ℕ 0 → Vtx ⁡ G ∈ Fin → N WWalksN G ∈ Fin
46 34 45 pm2.61i ⊢ Vtx ⁡ G ∈ Fin → N WWalksN G ∈ Fin