| Step | Hyp | Ref
| Expression |
| 1 | | 0nn0 12541 |
. 2
⊢ 0 ∈
ℕ0 |
| 2 | | wwlksn 29857 |
. . 3
⊢ (0 ∈
ℕ0 → (0 WWalksN 𝐺) = {𝑤 ∈ (WWalks‘𝐺) ∣ (♯‘𝑤) = (0 + 1)}) |
| 3 | | eqid 2737 |
. . . . . . . 8
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
| 4 | | eqid 2737 |
. . . . . . . 8
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
| 5 | 3, 4 | iswwlks 29856 |
. . . . . . 7
⊢ (𝑤 ∈ (WWalks‘𝐺) ↔ (𝑤 ≠ ∅ ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
| 6 | | 0p1e1 12388 |
. . . . . . . 8
⊢ (0 + 1) =
1 |
| 7 | 6 | eqeq2i 2750 |
. . . . . . 7
⊢
((♯‘𝑤) =
(0 + 1) ↔ (♯‘𝑤) = 1) |
| 8 | 5, 7 | anbi12i 628 |
. . . . . 6
⊢ ((𝑤 ∈ (WWalks‘𝐺) ∧ (♯‘𝑤) = (0 + 1)) ↔ ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑤) = 1)) |
| 9 | | simp2 1138 |
. . . . . . . 8
⊢ ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → 𝑤 ∈ Word (Vtx‘𝐺)) |
| 10 | | vex 3484 |
. . . . . . . . . . . 12
⊢ 𝑤 ∈ V |
| 11 | | 0lt1 11785 |
. . . . . . . . . . . . 13
⊢ 0 <
1 |
| 12 | | breq2 5147 |
. . . . . . . . . . . . 13
⊢
((♯‘𝑤) =
1 → (0 < (♯‘𝑤) ↔ 0 < 1)) |
| 13 | 11, 12 | mpbiri 258 |
. . . . . . . . . . . 12
⊢
((♯‘𝑤) =
1 → 0 < (♯‘𝑤)) |
| 14 | | hashgt0n0 14404 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ V ∧ 0 <
(♯‘𝑤)) →
𝑤 ≠
∅) |
| 15 | 10, 13, 14 | sylancr 587 |
. . . . . . . . . . 11
⊢
((♯‘𝑤) =
1 → 𝑤 ≠
∅) |
| 16 | 15 | adantr 480 |
. . . . . . . . . 10
⊢
(((♯‘𝑤)
= 1 ∧ 𝑤 ∈ Word
(Vtx‘𝐺)) → 𝑤 ≠ ∅) |
| 17 | | simpr 484 |
. . . . . . . . . 10
⊢
(((♯‘𝑤)
= 1 ∧ 𝑤 ∈ Word
(Vtx‘𝐺)) → 𝑤 ∈ Word (Vtx‘𝐺)) |
| 18 | | ral0 4513 |
. . . . . . . . . . . 12
⊢
∀𝑖 ∈
∅ {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) |
| 19 | | oveq1 7438 |
. . . . . . . . . . . . . . . 16
⊢
((♯‘𝑤) =
1 → ((♯‘𝑤)
− 1) = (1 − 1)) |
| 20 | | 1m1e0 12338 |
. . . . . . . . . . . . . . . 16
⊢ (1
− 1) = 0 |
| 21 | 19, 20 | eqtrdi 2793 |
. . . . . . . . . . . . . . 15
⊢
((♯‘𝑤) =
1 → ((♯‘𝑤)
− 1) = 0) |
| 22 | 21 | oveq2d 7447 |
. . . . . . . . . . . . . 14
⊢
((♯‘𝑤) =
1 → (0..^((♯‘𝑤) − 1)) = (0..^0)) |
| 23 | | fzo0 13723 |
. . . . . . . . . . . . . 14
⊢ (0..^0) =
∅ |
| 24 | 22, 23 | eqtrdi 2793 |
. . . . . . . . . . . . 13
⊢
((♯‘𝑤) =
1 → (0..^((♯‘𝑤) − 1)) = ∅) |
| 25 | 24 | raleqdv 3326 |
. . . . . . . . . . . 12
⊢
((♯‘𝑤) =
1 → (∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ ∅ {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
| 26 | 18, 25 | mpbiri 258 |
. . . . . . . . . . 11
⊢
((♯‘𝑤) =
1 → ∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) |
| 27 | 26 | adantr 480 |
. . . . . . . . . 10
⊢
(((♯‘𝑤)
= 1 ∧ 𝑤 ∈ Word
(Vtx‘𝐺)) →
∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) |
| 28 | 16, 17, 27 | 3jca 1129 |
. . . . . . . . 9
⊢
(((♯‘𝑤)
= 1 ∧ 𝑤 ∈ Word
(Vtx‘𝐺)) →
(𝑤 ≠ ∅ ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
| 29 | 28 | ex 412 |
. . . . . . . 8
⊢
((♯‘𝑤) =
1 → (𝑤 ∈ Word
(Vtx‘𝐺) → (𝑤 ≠ ∅ ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)))) |
| 30 | 9, 29 | impbid2 226 |
. . . . . . 7
⊢
((♯‘𝑤) =
1 → ((𝑤 ≠ ∅
∧ 𝑤 ∈ Word
(Vtx‘𝐺) ∧
∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ↔ 𝑤 ∈ Word (Vtx‘𝐺))) |
| 31 | 30 | pm5.32ri 575 |
. . . . . 6
⊢ (((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑤) = 1) ↔ (𝑤 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑤) = 1)) |
| 32 | 8, 31 | bitri 275 |
. . . . 5
⊢ ((𝑤 ∈ (WWalks‘𝐺) ∧ (♯‘𝑤) = (0 + 1)) ↔ (𝑤 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑤) = 1)) |
| 33 | 32 | a1i 11 |
. . . 4
⊢ (0 ∈
ℕ0 → ((𝑤 ∈ (WWalks‘𝐺) ∧ (♯‘𝑤) = (0 + 1)) ↔ (𝑤 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑤) = 1))) |
| 34 | 33 | rabbidva2 3438 |
. . 3
⊢ (0 ∈
ℕ0 → {𝑤 ∈ (WWalks‘𝐺) ∣ (♯‘𝑤) = (0 + 1)} = {𝑤 ∈ Word (Vtx‘𝐺) ∣ (♯‘𝑤) = 1}) |
| 35 | 2, 34 | eqtrd 2777 |
. 2
⊢ (0 ∈
ℕ0 → (0 WWalksN 𝐺) = {𝑤 ∈ Word (Vtx‘𝐺) ∣ (♯‘𝑤) = 1}) |
| 36 | 1, 35 | ax-mp 5 |
1
⊢ (0
WWalksN 𝐺) = {𝑤 ∈ Word (Vtx‘𝐺) ∣ (♯‘𝑤) = 1} |