Step | Hyp | Ref
| Expression |
1 | | nnnn0 11983 |
. . . 4
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
2 | | wwlksn 27775 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (𝑁 WWalksN 𝐺) = {𝑤 ∈ (WWalks‘𝐺) ∣ (♯‘𝑤) = (𝑁 + 1)}) |
3 | 1, 2 | syl 17 |
. . 3
⊢ (𝑁 ∈ ℕ → (𝑁 WWalksN 𝐺) = {𝑤 ∈ (WWalks‘𝐺) ∣ (♯‘𝑤) = (𝑁 + 1)}) |
4 | 3 | adantl 485 |
. 2
⊢
(((Edg‘𝐺) =
∅ ∧ 𝑁 ∈
ℕ) → (𝑁 WWalksN
𝐺) = {𝑤 ∈ (WWalks‘𝐺) ∣ (♯‘𝑤) = (𝑁 + 1)}) |
5 | | eqid 2738 |
. . . . . . . 8
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
6 | | eqid 2738 |
. . . . . . . 8
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
7 | 5, 6 | iswwlks 27774 |
. . . . . . 7
⊢ (𝑤 ∈ (WWalks‘𝐺) ↔ (𝑤 ≠ ∅ ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
8 | | nncn 11724 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
9 | | pncan1 11142 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℂ → ((𝑁 + 1) − 1) = 𝑁) |
10 | 8, 9 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) − 1) = 𝑁) |
11 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ) |
12 | 10, 11 | eqeltrd 2833 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) − 1) ∈
ℕ) |
13 | 12 | adantl 485 |
. . . . . . . . . . . . . 14
⊢
(((Edg‘𝐺) =
∅ ∧ 𝑁 ∈
ℕ) → ((𝑁 + 1)
− 1) ∈ ℕ) |
14 | 13 | adantl 485 |
. . . . . . . . . . . . 13
⊢
(((♯‘𝑤)
= (𝑁 + 1) ∧
((Edg‘𝐺) = ∅
∧ 𝑁 ∈ ℕ))
→ ((𝑁 + 1) − 1)
∈ ℕ) |
15 | | oveq1 7177 |
. . . . . . . . . . . . . . 15
⊢
((♯‘𝑤) =
(𝑁 + 1) →
((♯‘𝑤) −
1) = ((𝑁 + 1) −
1)) |
16 | 15 | eleq1d 2817 |
. . . . . . . . . . . . . 14
⊢
((♯‘𝑤) =
(𝑁 + 1) →
(((♯‘𝑤) −
1) ∈ ℕ ↔ ((𝑁 + 1) − 1) ∈
ℕ)) |
17 | 16 | adantr 484 |
. . . . . . . . . . . . 13
⊢
(((♯‘𝑤)
= (𝑁 + 1) ∧
((Edg‘𝐺) = ∅
∧ 𝑁 ∈ ℕ))
→ (((♯‘𝑤)
− 1) ∈ ℕ ↔ ((𝑁 + 1) − 1) ∈
ℕ)) |
18 | 14, 17 | mpbird 260 |
. . . . . . . . . . . 12
⊢
(((♯‘𝑤)
= (𝑁 + 1) ∧
((Edg‘𝐺) = ∅
∧ 𝑁 ∈ ℕ))
→ ((♯‘𝑤)
− 1) ∈ ℕ) |
19 | | lbfzo0 13168 |
. . . . . . . . . . . 12
⊢ (0 ∈
(0..^((♯‘𝑤)
− 1)) ↔ ((♯‘𝑤) − 1) ∈ ℕ) |
20 | 18, 19 | sylibr 237 |
. . . . . . . . . . 11
⊢
(((♯‘𝑤)
= (𝑁 + 1) ∧
((Edg‘𝐺) = ∅
∧ 𝑁 ∈ ℕ))
→ 0 ∈ (0..^((♯‘𝑤) − 1))) |
21 | | fveq2 6674 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 0 → (𝑤‘𝑖) = (𝑤‘0)) |
22 | | fv0p1e1 11839 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 0 → (𝑤‘(𝑖 + 1)) = (𝑤‘1)) |
23 | 21, 22 | preq12d 4632 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 0 → {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} = {(𝑤‘0), (𝑤‘1)}) |
24 | 23 | eleq1d 2817 |
. . . . . . . . . . . 12
⊢ (𝑖 = 0 → ({(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺))) |
25 | 24 | adantl 485 |
. . . . . . . . . . 11
⊢
((((♯‘𝑤)
= (𝑁 + 1) ∧
((Edg‘𝐺) = ∅
∧ 𝑁 ∈ ℕ))
∧ 𝑖 = 0) →
({(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺))) |
26 | 20, 25 | rspcdv 3518 |
. . . . . . . . . 10
⊢
(((♯‘𝑤)
= (𝑁 + 1) ∧
((Edg‘𝐺) = ∅
∧ 𝑁 ∈ ℕ))
→ (∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) → {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺))) |
27 | | eleq2 2821 |
. . . . . . . . . . . . 13
⊢
((Edg‘𝐺) =
∅ → ({(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺) ↔ {(𝑤‘0), (𝑤‘1)} ∈ ∅)) |
28 | | noel 4219 |
. . . . . . . . . . . . . 14
⊢ ¬
{(𝑤‘0), (𝑤‘1)} ∈
∅ |
29 | 28 | pm2.21i 119 |
. . . . . . . . . . . . 13
⊢ ({(𝑤‘0), (𝑤‘1)} ∈ ∅ → ¬
(♯‘𝑤) = (𝑁 + 1)) |
30 | 27, 29 | syl6bi 256 |
. . . . . . . . . . . 12
⊢
((Edg‘𝐺) =
∅ → ({(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺) → ¬
(♯‘𝑤) = (𝑁 + 1))) |
31 | 30 | adantr 484 |
. . . . . . . . . . 11
⊢
(((Edg‘𝐺) =
∅ ∧ 𝑁 ∈
ℕ) → ({(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺) → ¬
(♯‘𝑤) = (𝑁 + 1))) |
32 | 31 | adantl 485 |
. . . . . . . . . 10
⊢
(((♯‘𝑤)
= (𝑁 + 1) ∧
((Edg‘𝐺) = ∅
∧ 𝑁 ∈ ℕ))
→ ({(𝑤‘0),
(𝑤‘1)} ∈
(Edg‘𝐺) → ¬
(♯‘𝑤) = (𝑁 + 1))) |
33 | 26, 32 | syldc 48 |
. . . . . . . . 9
⊢
(∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) → (((♯‘𝑤) = (𝑁 + 1) ∧ ((Edg‘𝐺) = ∅ ∧ 𝑁 ∈ ℕ)) → ¬
(♯‘𝑤) = (𝑁 + 1))) |
34 | 33 | 3ad2ant3 1136 |
. . . . . . . 8
⊢ ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → (((♯‘𝑤) = (𝑁 + 1) ∧ ((Edg‘𝐺) = ∅ ∧ 𝑁 ∈ ℕ)) → ¬
(♯‘𝑤) = (𝑁 + 1))) |
35 | 34 | com12 32 |
. . . . . . 7
⊢
(((♯‘𝑤)
= (𝑁 + 1) ∧
((Edg‘𝐺) = ∅
∧ 𝑁 ∈ ℕ))
→ ((𝑤 ≠ ∅
∧ 𝑤 ∈ Word
(Vtx‘𝐺) ∧
∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ¬ (♯‘𝑤) = (𝑁 + 1))) |
36 | 7, 35 | syl5bi 245 |
. . . . . 6
⊢
(((♯‘𝑤)
= (𝑁 + 1) ∧
((Edg‘𝐺) = ∅
∧ 𝑁 ∈ ℕ))
→ (𝑤 ∈
(WWalks‘𝐺) →
¬ (♯‘𝑤) =
(𝑁 + 1))) |
37 | 36 | expimpd 457 |
. . . . 5
⊢
((♯‘𝑤) =
(𝑁 + 1) →
((((Edg‘𝐺) = ∅
∧ 𝑁 ∈ ℕ)
∧ 𝑤 ∈
(WWalks‘𝐺)) →
¬ (♯‘𝑤) =
(𝑁 + 1))) |
38 | | ax-1 6 |
. . . . 5
⊢ (¬
(♯‘𝑤) = (𝑁 + 1) → ((((Edg‘𝐺) = ∅ ∧ 𝑁 ∈ ℕ) ∧ 𝑤 ∈ (WWalks‘𝐺)) → ¬
(♯‘𝑤) = (𝑁 + 1))) |
39 | 37, 38 | pm2.61i 185 |
. . . 4
⊢
((((Edg‘𝐺) =
∅ ∧ 𝑁 ∈
ℕ) ∧ 𝑤 ∈
(WWalks‘𝐺)) →
¬ (♯‘𝑤) =
(𝑁 + 1)) |
40 | 39 | ralrimiva 3096 |
. . 3
⊢
(((Edg‘𝐺) =
∅ ∧ 𝑁 ∈
ℕ) → ∀𝑤
∈ (WWalks‘𝐺)
¬ (♯‘𝑤) =
(𝑁 + 1)) |
41 | | rabeq0 4273 |
. . 3
⊢ ({𝑤 ∈ (WWalks‘𝐺) ∣ (♯‘𝑤) = (𝑁 + 1)} = ∅ ↔ ∀𝑤 ∈ (WWalks‘𝐺) ¬ (♯‘𝑤) = (𝑁 + 1)) |
42 | 40, 41 | sylibr 237 |
. 2
⊢
(((Edg‘𝐺) =
∅ ∧ 𝑁 ∈
ℕ) → {𝑤 ∈
(WWalks‘𝐺) ∣
(♯‘𝑤) = (𝑁 + 1)} =
∅) |
43 | 4, 42 | eqtrd 2773 |
1
⊢
(((Edg‘𝐺) =
∅ ∧ 𝑁 ∈
ℕ) → (𝑁 WWalksN
𝐺) =
∅) |