Step | Hyp | Ref
| Expression |
1 | | nnnn0 11176 |
. . . 4
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
2 | | wwlksn 41040 |
. . . 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 2610 |
. . . . . . . 8
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
6 | | eqid 2610 |
. . . . . . . 8
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
7 | 5, 6 | iswwlks 41039 |
. . . . . . 7
⊢ (𝑤 ∈ (WWalkS‘𝐺) ↔ (𝑤 ≠ ∅ ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
8 | | nncn 10905 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
9 | | pncan1 10333 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℂ → ((𝑁 + 1) − 1) = 𝑁) |
10 | 8, 9 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) − 1) = 𝑁) |
11 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ) |
12 | 10, 11 | eqeltrd 2688 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) − 1) ∈
ℕ) |
13 | 12 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢
(((Edg‘𝐺) =
∅ ∧ 𝑁 ∈
ℕ) → ((𝑁 + 1)
− 1) ∈ ℕ) |
14 | 13 | adantl 481 |
. . . . . . . . . . . . . 14
⊢
(((#‘𝑤) =
(𝑁 + 1) ∧
((Edg‘𝐺) = ∅
∧ 𝑁 ∈ ℕ))
→ ((𝑁 + 1) − 1)
∈ ℕ) |
15 | | oveq1 6556 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝑤) =
(𝑁 + 1) →
((#‘𝑤) − 1) =
((𝑁 + 1) −
1)) |
16 | 15 | eleq1d 2672 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑤) =
(𝑁 + 1) →
(((#‘𝑤) − 1)
∈ ℕ ↔ ((𝑁 +
1) − 1) ∈ ℕ)) |
17 | 16 | adantr 480 |
. . . . . . . . . . . . . 14
⊢
(((#‘𝑤) =
(𝑁 + 1) ∧
((Edg‘𝐺) = ∅
∧ 𝑁 ∈ ℕ))
→ (((#‘𝑤)
− 1) ∈ ℕ ↔ ((𝑁 + 1) − 1) ∈
ℕ)) |
18 | 14, 17 | mpbird 246 |
. . . . . . . . . . . . 13
⊢
(((#‘𝑤) =
(𝑁 + 1) ∧
((Edg‘𝐺) = ∅
∧ 𝑁 ∈ ℕ))
→ ((#‘𝑤) −
1) ∈ ℕ) |
19 | | lbfzo0 12375 |
. . . . . . . . . . . . 13
⊢ (0 ∈
(0..^((#‘𝑤) −
1)) ↔ ((#‘𝑤)
− 1) ∈ ℕ) |
20 | 18, 19 | sylibr 223 |
. . . . . . . . . . . 12
⊢
(((#‘𝑤) =
(𝑁 + 1) ∧
((Edg‘𝐺) = ∅
∧ 𝑁 ∈ ℕ))
→ 0 ∈ (0..^((#‘𝑤) − 1))) |
21 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = 0 → (𝑤‘𝑖) = (𝑤‘0)) |
22 | | oveq1 6556 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 = 0 → (𝑖 + 1) = (0 + 1)) |
23 | | 0p1e1 11009 |
. . . . . . . . . . . . . . . . 17
⊢ (0 + 1) =
1 |
24 | 22, 23 | syl6eq 2660 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = 0 → (𝑖 + 1) = 1) |
25 | 24 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = 0 → (𝑤‘(𝑖 + 1)) = (𝑤‘1)) |
26 | 21, 25 | preq12d 4220 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 0 → {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} = {(𝑤‘0), (𝑤‘1)}) |
27 | 26 | eleq1d 2672 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 0 → ({(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺))) |
28 | 27 | adantl 481 |
. . . . . . . . . . . 12
⊢
((((#‘𝑤) =
(𝑁 + 1) ∧
((Edg‘𝐺) = ∅
∧ 𝑁 ∈ ℕ))
∧ 𝑖 = 0) →
({(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺))) |
29 | 20, 28 | rspcdv 3285 |
. . . . . . . . . . 11
⊢
(((#‘𝑤) =
(𝑁 + 1) ∧
((Edg‘𝐺) = ∅
∧ 𝑁 ∈ ℕ))
→ (∀𝑖 ∈
(0..^((#‘𝑤) −
1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) → {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺))) |
30 | | eleq2 2677 |
. . . . . . . . . . . . . 14
⊢
((Edg‘𝐺) =
∅ → ({(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺) ↔ {(𝑤‘0), (𝑤‘1)} ∈ ∅)) |
31 | | noel 3878 |
. . . . . . . . . . . . . . 15
⊢ ¬
{(𝑤‘0), (𝑤‘1)} ∈
∅ |
32 | 31 | pm2.21i 115 |
. . . . . . . . . . . . . 14
⊢ ({(𝑤‘0), (𝑤‘1)} ∈ ∅ → ¬
(#‘𝑤) = (𝑁 + 1)) |
33 | 30, 32 | syl6bi 242 |
. . . . . . . . . . . . 13
⊢
((Edg‘𝐺) =
∅ → ({(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺) → ¬ (#‘𝑤) = (𝑁 + 1))) |
34 | 33 | adantr 480 |
. . . . . . . . . . . 12
⊢
(((Edg‘𝐺) =
∅ ∧ 𝑁 ∈
ℕ) → ({(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺) → ¬ (#‘𝑤) = (𝑁 + 1))) |
35 | 34 | adantl 481 |
. . . . . . . . . . 11
⊢
(((#‘𝑤) =
(𝑁 + 1) ∧
((Edg‘𝐺) = ∅
∧ 𝑁 ∈ ℕ))
→ ({(𝑤‘0),
(𝑤‘1)} ∈
(Edg‘𝐺) → ¬
(#‘𝑤) = (𝑁 + 1))) |
36 | 29, 35 | syld 46 |
. . . . . . . . . 10
⊢
(((#‘𝑤) =
(𝑁 + 1) ∧
((Edg‘𝐺) = ∅
∧ 𝑁 ∈ ℕ))
→ (∀𝑖 ∈
(0..^((#‘𝑤) −
1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ¬ (#‘𝑤) = (𝑁 + 1))) |
37 | 36 | com12 32 |
. . . . . . . . 9
⊢
(∀𝑖 ∈
(0..^((#‘𝑤) −
1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) → (((#‘𝑤) = (𝑁 + 1) ∧ ((Edg‘𝐺) = ∅ ∧ 𝑁 ∈ ℕ)) → ¬
(#‘𝑤) = (𝑁 + 1))) |
38 | 37 | 3ad2ant3 1077 |
. . . . . . . 8
⊢ ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → (((#‘𝑤) = (𝑁 + 1) ∧ ((Edg‘𝐺) = ∅ ∧ 𝑁 ∈ ℕ)) → ¬
(#‘𝑤) = (𝑁 + 1))) |
39 | 38 | com12 32 |
. . . . . . 7
⊢
(((#‘𝑤) =
(𝑁 + 1) ∧
((Edg‘𝐺) = ∅
∧ 𝑁 ∈ ℕ))
→ ((𝑤 ≠ ∅
∧ 𝑤 ∈ Word
(Vtx‘𝐺) ∧
∀𝑖 ∈
(0..^((#‘𝑤) −
1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ¬ (#‘𝑤) = (𝑁 + 1))) |
40 | 7, 39 | syl5bi 231 |
. . . . . 6
⊢
(((#‘𝑤) =
(𝑁 + 1) ∧
((Edg‘𝐺) = ∅
∧ 𝑁 ∈ ℕ))
→ (𝑤 ∈
(WWalkS‘𝐺) →
¬ (#‘𝑤) = (𝑁 + 1))) |
41 | 40 | expimpd 627 |
. . . . 5
⊢
((#‘𝑤) =
(𝑁 + 1) →
((((Edg‘𝐺) = ∅
∧ 𝑁 ∈ ℕ)
∧ 𝑤 ∈
(WWalkS‘𝐺)) →
¬ (#‘𝑤) = (𝑁 + 1))) |
42 | | ax-1 6 |
. . . . 5
⊢ (¬
(#‘𝑤) = (𝑁 + 1) → ((((Edg‘𝐺) = ∅ ∧ 𝑁 ∈ ℕ) ∧ 𝑤 ∈ (WWalkS‘𝐺)) → ¬ (#‘𝑤) = (𝑁 + 1))) |
43 | 41, 42 | pm2.61i 175 |
. . . 4
⊢
((((Edg‘𝐺) =
∅ ∧ 𝑁 ∈
ℕ) ∧ 𝑤 ∈
(WWalkS‘𝐺)) →
¬ (#‘𝑤) = (𝑁 + 1)) |
44 | 43 | ralrimiva 2949 |
. . 3
⊢
(((Edg‘𝐺) =
∅ ∧ 𝑁 ∈
ℕ) → ∀𝑤
∈ (WWalkS‘𝐺)
¬ (#‘𝑤) = (𝑁 + 1)) |
45 | | rabeq0 3911 |
. . 3
⊢ ({𝑤 ∈ (WWalkS‘𝐺) ∣ (#‘𝑤) = (𝑁 + 1)} = ∅ ↔ ∀𝑤 ∈ (WWalkS‘𝐺) ¬ (#‘𝑤) = (𝑁 + 1)) |
46 | 44, 45 | sylibr 223 |
. 2
⊢
(((Edg‘𝐺) =
∅ ∧ 𝑁 ∈
ℕ) → {𝑤 ∈
(WWalkS‘𝐺) ∣
(#‘𝑤) = (𝑁 + 1)} =
∅) |
47 | 4, 46 | eqtrd 2644 |
1
⊢
(((Edg‘𝐺) =
∅ ∧ 𝑁 ∈
ℕ) → (𝑁 WWalkSN
𝐺) =
∅) |