| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | nnnn0 12533 | . . . 4
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) | 
| 2 |  | wwlksn 29857 | . . . 4
⊢ (𝑁 ∈ ℕ0
→ (𝑁 WWalksN 𝐺) = {𝑤 ∈ (WWalks‘𝐺) ∣ (♯‘𝑤) = (𝑁 + 1)}) | 
| 3 | 1, 2 | syl 17 | . . 3
⊢ (𝑁 ∈ ℕ → (𝑁 WWalksN 𝐺) = {𝑤 ∈ (WWalks‘𝐺) ∣ (♯‘𝑤) = (𝑁 + 1)}) | 
| 4 | 3 | adantl 481 | . 2
⊢
(((Edg‘𝐺) =
∅ ∧ 𝑁 ∈
ℕ) → (𝑁 WWalksN
𝐺) = {𝑤 ∈ (WWalks‘𝐺) ∣ (♯‘𝑤) = (𝑁 + 1)}) | 
| 5 |  | eqid 2737 | . . . . . . . 8
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) | 
| 6 |  | eqid 2737 | . . . . . . . 8
⊢
(Edg‘𝐺) =
(Edg‘𝐺) | 
| 7 | 5, 6 | iswwlks 29856 | . . . . . . 7
⊢ (𝑤 ∈ (WWalks‘𝐺) ↔ (𝑤 ≠ ∅ ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺))) | 
| 8 |  | nncn 12274 | . . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) | 
| 9 |  | pncan1 11687 | . . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℂ → ((𝑁 + 1) − 1) = 𝑁) | 
| 10 | 8, 9 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) − 1) = 𝑁) | 
| 11 |  | id 22 | . . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ) | 
| 12 | 10, 11 | eqeltrd 2841 | . . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) − 1) ∈
ℕ) | 
| 13 | 12 | adantl 481 | . . . . . . . . . . . . . 14
⊢
(((Edg‘𝐺) =
∅ ∧ 𝑁 ∈
ℕ) → ((𝑁 + 1)
− 1) ∈ ℕ) | 
| 14 | 13 | adantl 481 | . . . . . . . . . . . . 13
⊢
(((♯‘𝑤)
= (𝑁 + 1) ∧
((Edg‘𝐺) = ∅
∧ 𝑁 ∈ ℕ))
→ ((𝑁 + 1) − 1)
∈ ℕ) | 
| 15 |  | oveq1 7438 | . . . . . . . . . . . . . . 15
⊢
((♯‘𝑤) =
(𝑁 + 1) →
((♯‘𝑤) −
1) = ((𝑁 + 1) −
1)) | 
| 16 | 15 | eleq1d 2826 | . . . . . . . . . . . . . 14
⊢
((♯‘𝑤) =
(𝑁 + 1) →
(((♯‘𝑤) −
1) ∈ ℕ ↔ ((𝑁 + 1) − 1) ∈
ℕ)) | 
| 17 | 16 | adantr 480 | . . . . . . . . . . . . 13
⊢
(((♯‘𝑤)
= (𝑁 + 1) ∧
((Edg‘𝐺) = ∅
∧ 𝑁 ∈ ℕ))
→ (((♯‘𝑤)
− 1) ∈ ℕ ↔ ((𝑁 + 1) − 1) ∈
ℕ)) | 
| 18 | 14, 17 | mpbird 257 | . . . . . . . . . . . 12
⊢
(((♯‘𝑤)
= (𝑁 + 1) ∧
((Edg‘𝐺) = ∅
∧ 𝑁 ∈ ℕ))
→ ((♯‘𝑤)
− 1) ∈ ℕ) | 
| 19 |  | lbfzo0 13739 | . . . . . . . . . . . 12
⊢ (0 ∈
(0..^((♯‘𝑤)
− 1)) ↔ ((♯‘𝑤) − 1) ∈ ℕ) | 
| 20 | 18, 19 | sylibr 234 | . . . . . . . . . . 11
⊢
(((♯‘𝑤)
= (𝑁 + 1) ∧
((Edg‘𝐺) = ∅
∧ 𝑁 ∈ ℕ))
→ 0 ∈ (0..^((♯‘𝑤) − 1))) | 
| 21 |  | fveq2 6906 | . . . . . . . . . . . . . 14
⊢ (𝑖 = 0 → (𝑤‘𝑖) = (𝑤‘0)) | 
| 22 |  | fv0p1e1 12389 | . . . . . . . . . . . . . 14
⊢ (𝑖 = 0 → (𝑤‘(𝑖 + 1)) = (𝑤‘1)) | 
| 23 | 21, 22 | preq12d 4741 | . . . . . . . . . . . . 13
⊢ (𝑖 = 0 → {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} = {(𝑤‘0), (𝑤‘1)}) | 
| 24 | 23 | eleq1d 2826 | . . . . . . . . . . . 12
⊢ (𝑖 = 0 → ({(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺))) | 
| 25 | 24 | adantl 481 | . . . . . . . . . . 11
⊢
((((♯‘𝑤)
= (𝑁 + 1) ∧
((Edg‘𝐺) = ∅
∧ 𝑁 ∈ ℕ))
∧ 𝑖 = 0) →
({(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺))) | 
| 26 | 20, 25 | rspcdv 3614 | . . . . . . . . . 10
⊢
(((♯‘𝑤)
= (𝑁 + 1) ∧
((Edg‘𝐺) = ∅
∧ 𝑁 ∈ ℕ))
→ (∀𝑖 ∈
(0..^((♯‘𝑤)
− 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) → {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺))) | 
| 27 |  | eleq2 2830 | . . . . . . . . . . . . 13
⊢
((Edg‘𝐺) =
∅ → ({(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺) ↔ {(𝑤‘0), (𝑤‘1)} ∈ ∅)) | 
| 28 |  | noel 4338 | . . . . . . . . . . . . . 14
⊢  ¬
{(𝑤‘0), (𝑤‘1)} ∈
∅ | 
| 29 | 28 | pm2.21i 119 | . . . . . . . . . . . . 13
⊢ ({(𝑤‘0), (𝑤‘1)} ∈ ∅ → ¬
(♯‘𝑤) = (𝑁 + 1)) | 
| 30 | 27, 29 | biimtrdi 253 | . . . . . . . . . . . 12
⊢
((Edg‘𝐺) =
∅ → ({(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺) → ¬
(♯‘𝑤) = (𝑁 + 1))) | 
| 31 | 30 | adantr 480 | . . . . . . . . . . 11
⊢
(((Edg‘𝐺) =
∅ ∧ 𝑁 ∈
ℕ) → ({(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺) → ¬
(♯‘𝑤) = (𝑁 + 1))) | 
| 32 | 31 | adantl 481 | . . . . . . . . . 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 | biimtrid 242 | . . . . . 6
⊢
(((♯‘𝑤)
= (𝑁 + 1) ∧
((Edg‘𝐺) = ∅
∧ 𝑁 ∈ ℕ))
→ (𝑤 ∈
(WWalks‘𝐺) →
¬ (♯‘𝑤) =
(𝑁 + 1))) | 
| 37 | 36 | expimpd 453 | . . . . 5
⊢
((♯‘𝑤) =
(𝑁 + 1) →
((((Edg‘𝐺) = ∅
∧ 𝑁 ∈ ℕ)
∧ 𝑤 ∈
(WWalks‘𝐺)) →
¬ (♯‘𝑤) =
(𝑁 + 1))) | 
| 38 |  | ax-1 6 | . . . . 5
⊢ (¬
(♯‘𝑤) = (𝑁 + 1) → ((((Edg‘𝐺) = ∅ ∧ 𝑁 ∈ ℕ) ∧ 𝑤 ∈ (WWalks‘𝐺)) → ¬
(♯‘𝑤) = (𝑁 + 1))) | 
| 39 | 37, 38 | pm2.61i 182 | . . . 4
⊢
((((Edg‘𝐺) =
∅ ∧ 𝑁 ∈
ℕ) ∧ 𝑤 ∈
(WWalks‘𝐺)) →
¬ (♯‘𝑤) =
(𝑁 + 1)) | 
| 40 | 39 | ralrimiva 3146 | . . 3
⊢
(((Edg‘𝐺) =
∅ ∧ 𝑁 ∈
ℕ) → ∀𝑤
∈ (WWalks‘𝐺)
¬ (♯‘𝑤) =
(𝑁 + 1)) | 
| 41 |  | rabeq0 4388 | . . 3
⊢ ({𝑤 ∈ (WWalks‘𝐺) ∣ (♯‘𝑤) = (𝑁 + 1)} = ∅ ↔ ∀𝑤 ∈ (WWalks‘𝐺) ¬ (♯‘𝑤) = (𝑁 + 1)) | 
| 42 | 40, 41 | sylibr 234 | . 2
⊢
(((Edg‘𝐺) =
∅ ∧ 𝑁 ∈
ℕ) → {𝑤 ∈
(WWalks‘𝐺) ∣
(♯‘𝑤) = (𝑁 + 1)} =
∅) | 
| 43 | 4, 42 | eqtrd 2777 | 1
⊢
(((Edg‘𝐺) =
∅ ∧ 𝑁 ∈
ℕ) → (𝑁 WWalksN
𝐺) =
∅) |