Metamath Proof Explorer

Theorem wwlksn0s

Description: The set of all walks as words of length 0 is the set of all words of length 1 over the vertices. (Contributed by Alexander van der Vekens, 22-Jul-2018) (Revised by AV, 12-Apr-2021)

Ref Expression
Assertion wwlksn0s ⊢ 0 WWalksN G = w ∈ Word Vtx ⁡ G | w = 1

Proof

Step Hyp Ref Expression
1 0nn0 ⊢ 0 ∈ ℕ 0
2 wwlksn ⊢ 0 ∈ ℕ 0 → 0 WWalksN G = w ∈ WWalks ⁡ G | w = 0 + 1
3 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
4 eqid ⊢ Edg ⁡ G = Edg ⁡ G
5 3 4 iswwlks ⊢ w ∈ WWalks ⁡ G ↔ w ≠ ∅ ∧ w ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ G
6 0p1e1 ⊢ 0 + 1 = 1
7 6 eqeq2i ⊢ w = 0 + 1 ↔ w = 1
8 5 7 anbi12i ⊢ w ∈ WWalks ⁡ G ∧ w = 0 + 1 ↔ w ≠ ∅ ∧ w ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ G ∧ w = 1
9 simp2 ⊢ w ≠ ∅ ∧ w ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ G → w ∈ Word Vtx ⁡ G
10 vex ⊢ w ∈ V
11 0lt1 ⊢ 0 < 1
12 breq2 ⊢ w = 1 → 0 < w ↔ 0 < 1
13 11 12 mpbiri ⊢ w = 1 → 0 < w
14 hashgt0n0 ⊢ w ∈ V ∧ 0 < w → w ≠ ∅
15 10 13 14 sylancr ⊢ w = 1 → w ≠ ∅
16 15 adantr ⊢ w = 1 ∧ w ∈ Word Vtx ⁡ G → w ≠ ∅
17 simpr ⊢ w = 1 ∧ w ∈ Word Vtx ⁡ G → w ∈ Word Vtx ⁡ G
18 ral0 ⊢ ∀ i ∈ ∅ w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ G
19 oveq1 ⊢ w = 1 → w − 1 = 1 − 1
20 1m1e0 ⊢ 1 − 1 = 0
21 19 20 eqtrdi ⊢ w = 1 → w − 1 = 0
22 21 oveq2d ⊢ w = 1 → 0 ..^ w − 1 = 0 ..^ 0
23 fzo0 ⊢ 0 ..^ 0 = ∅
24 22 23 eqtrdi ⊢ w = 1 → 0 ..^ w − 1 = ∅
25 24 raleqdv ⊢ w = 1 → ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ G ↔ ∀ i ∈ ∅ w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ G
26 18 25 mpbiri ⊢ w = 1 → ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ G
27 26 adantr ⊢ w = 1 ∧ w ∈ Word Vtx ⁡ G → ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ G
28 16 17 27 3jca ⊢ w = 1 ∧ w ∈ Word Vtx ⁡ G → w ≠ ∅ ∧ w ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ G
29 28 ex ⊢ w = 1 → w ∈ Word Vtx ⁡ G → w ≠ ∅ ∧ w ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ G
30 9 29 impbid2 ⊢ w = 1 → w ≠ ∅ ∧ w ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ G ↔ w ∈ Word Vtx ⁡ G
31 30 pm5.32ri ⊢ w ≠ ∅ ∧ w ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ G ∧ w = 1 ↔ w ∈ Word Vtx ⁡ G ∧ w = 1
32 8 31 bitri ⊢ w ∈ WWalks ⁡ G ∧ w = 0 + 1 ↔ w ∈ Word Vtx ⁡ G ∧ w = 1
33 32 a1i ⊢ 0 ∈ ℕ 0 → w ∈ WWalks ⁡ G ∧ w = 0 + 1 ↔ w ∈ Word Vtx ⁡ G ∧ w = 1
34 33 rabbidva2 ⊢ 0 ∈ ℕ 0 → w ∈ WWalks ⁡ G | w = 0 + 1 = w ∈ Word Vtx ⁡ G | w = 1
35 2 34 eqtrd ⊢ 0 ∈ ℕ 0 → 0 WWalksN G = w ∈ Word Vtx ⁡ G | w = 1
36 1 35 ax-mp ⊢ 0 WWalksN G = w ∈ Word Vtx ⁡ G | w = 1