Step | Hyp | Ref
| Expression |
1 | | wspthsn 41046 |
. . . . 5
⊢ (𝑁 WSPathsN 𝐺) = {𝑤 ∈ (𝑁 WWalkSN 𝐺) ∣ ∃𝑓 𝑓(SPathS‘𝐺)𝑤} |
2 | 1 | a1i 11 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐺 ∈ V) ∧
𝑉 = ∅) → (𝑁 WSPathsN 𝐺) = {𝑤 ∈ (𝑁 WWalkSN 𝐺) ∣ ∃𝑓 𝑓(SPathS‘𝐺)𝑤}) |
3 | | wwlknbp2 41063 |
. . . . . . . 8
⊢ (𝑤 ∈ (𝑁 WWalkSN 𝐺) → (𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = (𝑁 + 1))) |
4 | | wspn0.v |
. . . . . . . . . . . . . . . 16
⊢ 𝑉 = (Vtx‘𝐺) |
5 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑉 = ∅ → 𝑉 = ∅) |
6 | 4, 5 | syl5eqr 2658 |
. . . . . . . . . . . . . . 15
⊢ (𝑉 = ∅ →
(Vtx‘𝐺) =
∅) |
7 | | wrdeq 13182 |
. . . . . . . . . . . . . . 15
⊢
((Vtx‘𝐺) =
∅ → Word (Vtx‘𝐺) = Word ∅) |
8 | 6, 7 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑉 = ∅ → Word
(Vtx‘𝐺) = Word
∅) |
9 | 8 | eleq2d 2673 |
. . . . . . . . . . . . 13
⊢ (𝑉 = ∅ → (𝑤 ∈ Word (Vtx‘𝐺) ↔ 𝑤 ∈ Word ∅)) |
10 | | 0wrd0 13186 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ Word ∅ ↔
𝑤 =
∅) |
11 | 9, 10 | syl6bb 275 |
. . . . . . . . . . . 12
⊢ (𝑉 = ∅ → (𝑤 ∈ Word (Vtx‘𝐺) ↔ 𝑤 = ∅)) |
12 | 11 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ 𝐺 ∈ V) ∧
𝑉 = ∅) → (𝑤 ∈ Word (Vtx‘𝐺) ↔ 𝑤 = ∅)) |
13 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = ∅ → (#‘𝑤) =
(#‘∅)) |
14 | | hash0 13019 |
. . . . . . . . . . . . . . . . . 18
⊢
(#‘∅) = 0 |
15 | 13, 14 | syl6eq 2660 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = ∅ → (#‘𝑤) = 0) |
16 | 15 | eqeq1d 2612 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = ∅ →
((#‘𝑤) = (𝑁 + 1) ↔ 0 = (𝑁 + 1))) |
17 | 16 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ0
∧ 𝑤 = ∅) →
((#‘𝑤) = (𝑁 + 1) ↔ 0 = (𝑁 + 1))) |
18 | | nn0p1gt0 11199 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ0
→ 0 < (𝑁 +
1)) |
19 | 18 | gt0ne0d 10471 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ≠
0) |
20 | | eqneqall 2793 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 + 1) = 0 → ((𝑁 + 1) ≠ 0 → ¬
∃𝑓 𝑓(SPathS‘𝐺)𝑤)) |
21 | 20 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . 18
⊢ (0 =
(𝑁 + 1) → ((𝑁 + 1) ≠ 0 → ¬
∃𝑓 𝑓(SPathS‘𝐺)𝑤)) |
22 | 21 | com12 32 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 + 1) ≠ 0 → (0 = (𝑁 + 1) → ¬ ∃𝑓 𝑓(SPathS‘𝐺)𝑤)) |
23 | 19, 22 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ0
→ (0 = (𝑁 + 1) →
¬ ∃𝑓 𝑓(SPathS‘𝐺)𝑤)) |
24 | 23 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ0
∧ 𝑤 = ∅) →
(0 = (𝑁 + 1) → ¬
∃𝑓 𝑓(SPathS‘𝐺)𝑤)) |
25 | 17, 24 | sylbid 229 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ0
∧ 𝑤 = ∅) →
((#‘𝑤) = (𝑁 + 1) → ¬ ∃𝑓 𝑓(SPathS‘𝐺)𝑤)) |
26 | 25 | ex 449 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
→ (𝑤 = ∅ →
((#‘𝑤) = (𝑁 + 1) → ¬ ∃𝑓 𝑓(SPathS‘𝐺)𝑤))) |
27 | 26 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ 𝐺 ∈ V) →
(𝑤 = ∅ →
((#‘𝑤) = (𝑁 + 1) → ¬ ∃𝑓 𝑓(SPathS‘𝐺)𝑤))) |
28 | 27 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ 𝐺 ∈ V) ∧
𝑉 = ∅) → (𝑤 = ∅ →
((#‘𝑤) = (𝑁 + 1) → ¬ ∃𝑓 𝑓(SPathS‘𝐺)𝑤))) |
29 | 12, 28 | sylbid 229 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ 𝐺 ∈ V) ∧
𝑉 = ∅) → (𝑤 ∈ Word (Vtx‘𝐺) → ((#‘𝑤) = (𝑁 + 1) → ¬ ∃𝑓 𝑓(SPathS‘𝐺)𝑤))) |
30 | 29 | com3l 87 |
. . . . . . . . 9
⊢ (𝑤 ∈ Word (Vtx‘𝐺) → ((#‘𝑤) = (𝑁 + 1) → (((𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V) ∧ 𝑉 = ∅) → ¬
∃𝑓 𝑓(SPathS‘𝐺)𝑤))) |
31 | 30 | imp 444 |
. . . . . . . 8
⊢ ((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = (𝑁 + 1)) → (((𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V) ∧ 𝑉 = ∅) → ¬
∃𝑓 𝑓(SPathS‘𝐺)𝑤)) |
32 | 3, 31 | syl 17 |
. . . . . . 7
⊢ (𝑤 ∈ (𝑁 WWalkSN 𝐺) → (((𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V) ∧ 𝑉 = ∅) → ¬
∃𝑓 𝑓(SPathS‘𝐺)𝑤)) |
33 | 32 | impcom 445 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐺 ∈ V) ∧
𝑉 = ∅) ∧ 𝑤 ∈ (𝑁 WWalkSN 𝐺)) → ¬ ∃𝑓 𝑓(SPathS‘𝐺)𝑤) |
34 | 33 | ralrimiva 2949 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐺 ∈ V) ∧
𝑉 = ∅) →
∀𝑤 ∈ (𝑁 WWalkSN 𝐺) ¬ ∃𝑓 𝑓(SPathS‘𝐺)𝑤) |
35 | | rabeq0 3911 |
. . . . 5
⊢ ({𝑤 ∈ (𝑁 WWalkSN 𝐺) ∣ ∃𝑓 𝑓(SPathS‘𝐺)𝑤} = ∅ ↔ ∀𝑤 ∈ (𝑁 WWalkSN 𝐺) ¬ ∃𝑓 𝑓(SPathS‘𝐺)𝑤) |
36 | 34, 35 | sylibr 223 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐺 ∈ V) ∧
𝑉 = ∅) → {𝑤 ∈ (𝑁 WWalkSN 𝐺) ∣ ∃𝑓 𝑓(SPathS‘𝐺)𝑤} = ∅) |
37 | 2, 36 | eqtrd 2644 |
. . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝐺 ∈ V) ∧
𝑉 = ∅) → (𝑁 WSPathsN 𝐺) = ∅) |
38 | 37 | ex 449 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝐺 ∈ V) →
(𝑉 = ∅ → (𝑁 WSPathsN 𝐺) = ∅)) |
39 | | df-wspthsn 41036 |
. . . 4
⊢ WSPathsN
= (𝑛 ∈
ℕ0, 𝑔
∈ V ↦ {𝑤 ∈
(𝑛 WWalkSN 𝑔) ∣ ∃𝑓 𝑓(SPathS‘𝑔)𝑤}) |
40 | 39 | mpt2ndm0 6773 |
. . 3
⊢ (¬
(𝑁 ∈
ℕ0 ∧ 𝐺
∈ V) → (𝑁
WSPathsN 𝐺) =
∅) |
41 | 40 | a1d 25 |
. 2
⊢ (¬
(𝑁 ∈
ℕ0 ∧ 𝐺
∈ V) → (𝑉 =
∅ → (𝑁 WSPathsN
𝐺) =
∅)) |
42 | 38, 41 | pm2.61i 175 |
1
⊢ (𝑉 = ∅ → (𝑁 WSPathsN 𝐺) = ∅) |