Step | Hyp | Ref
| Expression |
1 | | ne0i 3880 |
. . 3
⊢ (𝑃 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ((𝑉 ClWWalksN 𝐸)‘𝑁) ≠ ∅) |
2 | | ndmfv 6128 |
. . . 4
⊢ (¬
𝑁 ∈ dom (𝑉 ClWWalksN 𝐸) → ((𝑉 ClWWalksN 𝐸)‘𝑁) = ∅) |
3 | 2 | necon1ai 2809 |
. . 3
⊢ (((𝑉 ClWWalksN 𝐸)‘𝑁) ≠ ∅ → 𝑁 ∈ dom (𝑉 ClWWalksN 𝐸)) |
4 | | oveq12 6558 |
. . . . . . . . . . 11
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝑣 ClWWalks 𝑒) = (𝑉 ClWWalks 𝐸)) |
5 | 4 | rabeqdv 3167 |
. . . . . . . . . 10
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → {𝑤 ∈ (𝑣 ClWWalks 𝑒) ∣ (#‘𝑤) = 𝑛} = {𝑤 ∈ (𝑉 ClWWalks 𝐸) ∣ (#‘𝑤) = 𝑛}) |
6 | 5 | mpteq2dv 4673 |
. . . . . . . . 9
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝑣 ClWWalks 𝑒) ∣ (#‘𝑤) = 𝑛}) = (𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝑉 ClWWalks 𝐸) ∣ (#‘𝑤) = 𝑛})) |
7 | | df-clwwlkn 26280 |
. . . . . . . . 9
⊢
ClWWalksN = (𝑣 ∈ V,
𝑒 ∈ V ↦ (𝑛 ∈ ℕ0
↦ {𝑤 ∈ (𝑣 ClWWalks 𝑒) ∣ (#‘𝑤) = 𝑛})) |
8 | | nn0ex 11175 |
. . . . . . . . . 10
⊢
ℕ0 ∈ V |
9 | 8 | mptex 6390 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ0
↦ {𝑤 ∈ (𝑉 ClWWalks 𝐸) ∣ (#‘𝑤) = 𝑛}) ∈ V |
10 | 6, 7, 9 | ovmpt2a 6689 |
. . . . . . . 8
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑉 ClWWalksN 𝐸) = (𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝑉 ClWWalks 𝐸) ∣ (#‘𝑤) = 𝑛})) |
11 | 10 | 3adant3 1074 |
. . . . . . 7
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V)) → (𝑉 ClWWalksN 𝐸) = (𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝑉 ClWWalks 𝐸) ∣ (#‘𝑤) = 𝑛})) |
12 | 11 | dmeqd 5248 |
. . . . . 6
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V)) → dom (𝑉 ClWWalksN 𝐸) = dom (𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝑉 ClWWalks 𝐸) ∣ (#‘𝑤) = 𝑛})) |
13 | 12 | eleq2d 2673 |
. . . . 5
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V)) → (𝑁 ∈ dom (𝑉 ClWWalksN 𝐸) ↔ 𝑁 ∈ dom (𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝑉 ClWWalks 𝐸) ∣ (#‘𝑤) = 𝑛}))) |
14 | | dmopabss 5258 |
. . . . . . . 8
⊢ dom
{〈𝑛, 𝑡〉 ∣ (𝑛 ∈ ℕ0
∧ 𝑡 = {𝑤 ∈ (𝑉 ClWWalks 𝐸) ∣ (#‘𝑤) = 𝑛})} ⊆
ℕ0 |
15 | 14 | sseli 3564 |
. . . . . . 7
⊢ (𝑁 ∈ dom {〈𝑛, 𝑡〉 ∣ (𝑛 ∈ ℕ0 ∧ 𝑡 = {𝑤 ∈ (𝑉 ClWWalks 𝐸) ∣ (#‘𝑤) = 𝑛})} → 𝑁 ∈
ℕ0) |
16 | | clwwlkn 26295 |
. . . . . . . . . . . . . . 15
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
→ ((𝑉 ClWWalksN 𝐸)‘𝑁) = {𝑝 ∈ (𝑉 ClWWalks 𝐸) ∣ (#‘𝑝) = 𝑁}) |
17 | 16 | 3expa 1257 |
. . . . . . . . . . . . . 14
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑁 ∈ ℕ0)
→ ((𝑉 ClWWalksN 𝐸)‘𝑁) = {𝑝 ∈ (𝑉 ClWWalks 𝐸) ∣ (#‘𝑝) = 𝑁}) |
18 | 17 | eleq2d 2673 |
. . . . . . . . . . . . 13
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑁 ∈ ℕ0)
→ (𝑃 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ↔ 𝑃 ∈ {𝑝 ∈ (𝑉 ClWWalks 𝐸) ∣ (#‘𝑝) = 𝑁})) |
19 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑝 = 𝑃 → (#‘𝑝) = (#‘𝑃)) |
20 | 19 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑝 = 𝑃 → ((#‘𝑝) = 𝑁 ↔ (#‘𝑃) = 𝑁)) |
21 | 20 | elrab 3331 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑃 ∈ {𝑝 ∈ (𝑉 ClWWalks 𝐸) ∣ (#‘𝑝) = 𝑁} ↔ (𝑃 ∈ (𝑉 ClWWalks 𝐸) ∧ (#‘𝑃) = 𝑁)) |
22 | | clwwlkprop 26298 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ (𝑉 ClWWalks 𝐸) → (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑃 ∈ Word 𝑉)) |
23 | | simpl3 1059 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑃 ∈ Word 𝑉) ∧ (#‘𝑃) = 𝑁) → 𝑃 ∈ Word 𝑉) |
24 | | lencl 13179 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑃 ∈ Word 𝑉 → (#‘𝑃) ∈
ℕ0) |
25 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((#‘𝑃) = 𝑁 → ((#‘𝑃) ∈ ℕ0
↔ 𝑁 ∈
ℕ0)) |
26 | 24, 25 | syl5ibcom 234 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃 ∈ Word 𝑉 → ((#‘𝑃) = 𝑁 → 𝑁 ∈
ℕ0)) |
27 | 26 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑃 ∈ Word 𝑉) → ((#‘𝑃) = 𝑁 → 𝑁 ∈
ℕ0)) |
28 | 27 | impac 649 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑃 ∈ Word 𝑉) ∧ (#‘𝑃) = 𝑁) → (𝑁 ∈ ℕ0 ∧
(#‘𝑃) = 𝑁)) |
29 | 23, 28 | jca 553 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑃 ∈ Word 𝑉) ∧ (#‘𝑃) = 𝑁) → (𝑃 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑃) = 𝑁))) |
30 | 22, 29 | sylan 487 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑃 ∈ (𝑉 ClWWalks 𝐸) ∧ (#‘𝑃) = 𝑁) → (𝑃 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑃) = 𝑁))) |
31 | 21, 30 | sylbi 206 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈ {𝑝 ∈ (𝑉 ClWWalks 𝐸) ∣ (#‘𝑝) = 𝑁} → (𝑃 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑃) = 𝑁))) |
32 | 31 | anim2i 591 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑃 ∈ {𝑝 ∈ (𝑉 ClWWalks 𝐸) ∣ (#‘𝑝) = 𝑁}) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑃 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑃) = 𝑁)))) |
33 | | 3anass 1035 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑃 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑃) = 𝑁)) ↔ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑃 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑃) = 𝑁)))) |
34 | 32, 33 | sylibr 223 |
. . . . . . . . . . . . . . 15
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑃 ∈ {𝑝 ∈ (𝑉 ClWWalks 𝐸) ∣ (#‘𝑝) = 𝑁}) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑃 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑃) = 𝑁))) |
35 | 34 | ex 449 |
. . . . . . . . . . . . . 14
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑃 ∈ {𝑝 ∈ (𝑉 ClWWalks 𝐸) ∣ (#‘𝑝) = 𝑁} → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑃 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑃) = 𝑁)))) |
36 | 35 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑁 ∈ ℕ0)
→ (𝑃 ∈ {𝑝 ∈ (𝑉 ClWWalks 𝐸) ∣ (#‘𝑝) = 𝑁} → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑃 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑃) = 𝑁)))) |
37 | 18, 36 | sylbid 229 |
. . . . . . . . . . . 12
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑁 ∈ ℕ0)
→ (𝑃 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑃 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑃) = 𝑁)))) |
38 | 37 | ex 449 |
. . . . . . . . . . 11
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑁 ∈ ℕ0
→ (𝑃 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑃 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑃) = 𝑁))))) |
39 | 38 | com23 84 |
. . . . . . . . . 10
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑃 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → (𝑁 ∈ ℕ0 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑃 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑃) = 𝑁))))) |
40 | 39 | a1d 25 |
. . . . . . . . 9
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (((𝑉 ClWWalksN 𝐸)‘𝑁) ≠ ∅ → (𝑃 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → (𝑁 ∈ ℕ0 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑃 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑃) = 𝑁)))))) |
41 | 7 | mpt2ndm0 6773 |
. . . . . . . . . 10
⊢ (¬
(𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑉 ClWWalksN 𝐸) = ∅) |
42 | | fveq1 6102 |
. . . . . . . . . . 11
⊢ ((𝑉 ClWWalksN 𝐸) = ∅ → ((𝑉 ClWWalksN 𝐸)‘𝑁) = (∅‘𝑁)) |
43 | | 0fv 6137 |
. . . . . . . . . . 11
⊢
(∅‘𝑁) =
∅ |
44 | 42, 43 | syl6eq 2660 |
. . . . . . . . . 10
⊢ ((𝑉 ClWWalksN 𝐸) = ∅ → ((𝑉 ClWWalksN 𝐸)‘𝑁) = ∅) |
45 | | eqneqall 2793 |
. . . . . . . . . 10
⊢ (((𝑉 ClWWalksN 𝐸)‘𝑁) = ∅ → (((𝑉 ClWWalksN 𝐸)‘𝑁) ≠ ∅ → (𝑃 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → (𝑁 ∈ ℕ0 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑃 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑃) = 𝑁)))))) |
46 | 41, 44, 45 | 3syl 18 |
. . . . . . . . 9
⊢ (¬
(𝑉 ∈ V ∧ 𝐸 ∈ V) → (((𝑉 ClWWalksN 𝐸)‘𝑁) ≠ ∅ → (𝑃 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → (𝑁 ∈ ℕ0 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑃 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑃) = 𝑁)))))) |
47 | 40, 46 | pm2.61i 175 |
. . . . . . . 8
⊢ (((𝑉 ClWWalksN 𝐸)‘𝑁) ≠ ∅ → (𝑃 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → (𝑁 ∈ ℕ0 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑃 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑃) = 𝑁))))) |
48 | 1, 47 | mpcom 37 |
. . . . . . 7
⊢ (𝑃 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → (𝑁 ∈ ℕ0 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑃 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑃) = 𝑁)))) |
49 | 15, 48 | syl5com 31 |
. . . . . 6
⊢ (𝑁 ∈ dom {〈𝑛, 𝑡〉 ∣ (𝑛 ∈ ℕ0 ∧ 𝑡 = {𝑤 ∈ (𝑉 ClWWalks 𝐸) ∣ (#‘𝑤) = 𝑛})} → (𝑃 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑃 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑃) = 𝑁)))) |
50 | | df-mpt 4645 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ0
↦ {𝑤 ∈ (𝑉 ClWWalks 𝐸) ∣ (#‘𝑤) = 𝑛}) = {〈𝑛, 𝑡〉 ∣ (𝑛 ∈ ℕ0 ∧ 𝑡 = {𝑤 ∈ (𝑉 ClWWalks 𝐸) ∣ (#‘𝑤) = 𝑛})} |
51 | 50 | dmeqi 5247 |
. . . . . 6
⊢ dom
(𝑛 ∈
ℕ0 ↦ {𝑤 ∈ (𝑉 ClWWalks 𝐸) ∣ (#‘𝑤) = 𝑛}) = dom {〈𝑛, 𝑡〉 ∣ (𝑛 ∈ ℕ0 ∧ 𝑡 = {𝑤 ∈ (𝑉 ClWWalks 𝐸) ∣ (#‘𝑤) = 𝑛})} |
52 | 49, 51 | eleq2s 2706 |
. . . . 5
⊢ (𝑁 ∈ dom (𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝑉 ClWWalks 𝐸) ∣ (#‘𝑤) = 𝑛}) → (𝑃 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑃 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑃) = 𝑁)))) |
53 | 13, 52 | syl6bi 242 |
. . . 4
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V)) → (𝑁 ∈ dom (𝑉 ClWWalksN 𝐸) → (𝑃 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑃 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑃) = 𝑁))))) |
54 | | 3ianor 1048 |
. . . . 5
⊢ (¬
(𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V)) ↔ (¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V ∨ ¬ (𝑉 ∈ V ∧ 𝐸 ∈ V))) |
55 | | df-3or 1032 |
. . . . . 6
⊢ ((¬
𝑉 ∈ V ∨ ¬ 𝐸 ∈ V ∨ ¬ (𝑉 ∈ V ∧ 𝐸 ∈ V)) ↔ ((¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V) ∨ ¬ (𝑉 ∈ V ∧ 𝐸 ∈ V))) |
56 | | ianor 508 |
. . . . . . . 8
⊢ (¬
(𝑉 ∈ V ∧ 𝐸 ∈ V) ↔ (¬ 𝑉 ∈ V ∨ ¬ 𝐸 ∈ V)) |
57 | 41 | dmeqd 5248 |
. . . . . . . . . . 11
⊢ (¬
(𝑉 ∈ V ∧ 𝐸 ∈ V) → dom (𝑉 ClWWalksN 𝐸) = dom ∅) |
58 | 57 | eleq2d 2673 |
. . . . . . . . . 10
⊢ (¬
(𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑁 ∈ dom (𝑉 ClWWalksN 𝐸) ↔ 𝑁 ∈ dom ∅)) |
59 | | dm0 5260 |
. . . . . . . . . . 11
⊢ dom
∅ = ∅ |
60 | 59 | eleq2i 2680 |
. . . . . . . . . 10
⊢ (𝑁 ∈ dom ∅ ↔ 𝑁 ∈
∅) |
61 | 58, 60 | syl6bb 275 |
. . . . . . . . 9
⊢ (¬
(𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑁 ∈ dom (𝑉 ClWWalksN 𝐸) ↔ 𝑁 ∈ ∅)) |
62 | | noel 3878 |
. . . . . . . . . 10
⊢ ¬
𝑁 ∈
∅ |
63 | 62 | pm2.21i 115 |
. . . . . . . . 9
⊢ (𝑁 ∈ ∅ → (𝑃 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑃 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑃) = 𝑁)))) |
64 | 61, 63 | syl6bi 242 |
. . . . . . . 8
⊢ (¬
(𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑁 ∈ dom (𝑉 ClWWalksN 𝐸) → (𝑃 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑃 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑃) = 𝑁))))) |
65 | 56, 64 | sylbir 224 |
. . . . . . 7
⊢ ((¬
𝑉 ∈ V ∨ ¬ 𝐸 ∈ V) → (𝑁 ∈ dom (𝑉 ClWWalksN 𝐸) → (𝑃 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑃 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑃) = 𝑁))))) |
66 | 65, 64 | jaoi 393 |
. . . . . 6
⊢ (((¬
𝑉 ∈ V ∨ ¬ 𝐸 ∈ V) ∨ ¬ (𝑉 ∈ V ∧ 𝐸 ∈ V)) → (𝑁 ∈ dom (𝑉 ClWWalksN 𝐸) → (𝑃 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑃 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑃) = 𝑁))))) |
67 | 55, 66 | sylbi 206 |
. . . . 5
⊢ ((¬
𝑉 ∈ V ∨ ¬ 𝐸 ∈ V ∨ ¬ (𝑉 ∈ V ∧ 𝐸 ∈ V)) → (𝑁 ∈ dom (𝑉 ClWWalksN 𝐸) → (𝑃 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑃 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑃) = 𝑁))))) |
68 | 54, 67 | sylbi 206 |
. . . 4
⊢ (¬
(𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V)) → (𝑁 ∈ dom (𝑉 ClWWalksN 𝐸) → (𝑃 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑃 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑃) = 𝑁))))) |
69 | 53, 68 | pm2.61i 175 |
. . 3
⊢ (𝑁 ∈ dom (𝑉 ClWWalksN 𝐸) → (𝑃 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑃 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑃) = 𝑁)))) |
70 | 1, 3, 69 | 3syl 18 |
. 2
⊢ (𝑃 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → (𝑃 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑃 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑃) = 𝑁)))) |
71 | 70 | pm2.43i 50 |
1
⊢ (𝑃 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑃 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑃) = 𝑁))) |