Step | Hyp | Ref
| Expression |
1 | | clwwlkbij.d |
. . 3
⊢ 𝐷 = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑤) = (𝑤‘0)} |
2 | | clwwlkbij.f |
. . 3
⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡 substr 〈0, 𝑁〉)) |
3 | 1, 2 | clwwlkf 26322 |
. 2
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → 𝐹:𝐷⟶((𝑉 ClWWalksN 𝐸)‘𝑁)) |
4 | | clwwlknimp 26304 |
. . . . . . 7
⊢ (𝑝 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑝‘𝑖), (𝑝‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑝), (𝑝‘0)} ∈ ran 𝐸)) |
5 | | simpr 476 |
. . . . . . . . . 10
⊢ ((((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑝‘𝑖), (𝑝‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑝), (𝑝‘0)} ∈ ran 𝐸) ∧ (𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ)) → (𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ)) |
6 | | simpl1 1057 |
. . . . . . . . . 10
⊢ ((((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑝‘𝑖), (𝑝‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑝), (𝑝‘0)} ∈ ran 𝐸) ∧ (𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ)) → (𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁)) |
7 | | 3simpc 1053 |
. . . . . . . . . . 11
⊢ (((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑝‘𝑖), (𝑝‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑝), (𝑝‘0)} ∈ ran 𝐸) → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑝‘𝑖), (𝑝‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑝), (𝑝‘0)} ∈ ran 𝐸)) |
8 | 7 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑝‘𝑖), (𝑝‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑝), (𝑝‘0)} ∈ ran 𝐸) ∧ (𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ)) → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑝‘𝑖), (𝑝‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑝), (𝑝‘0)} ∈ ran 𝐸)) |
9 | 1 | clwwlkel 26321 |
. . . . . . . . . 10
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ (𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑝‘𝑖), (𝑝‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑝), (𝑝‘0)} ∈ ran 𝐸)) → (𝑝 ++ 〈“(𝑝‘0)”〉) ∈ 𝐷) |
10 | 5, 6, 8, 9 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑝‘𝑖), (𝑝‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑝), (𝑝‘0)} ∈ ran 𝐸) ∧ (𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ)) → (𝑝 ++ 〈“(𝑝‘0)”〉) ∈ 𝐷) |
11 | | opeq2 4341 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 = (#‘𝑝) → 〈0, 𝑁〉 = 〈0, (#‘𝑝)〉) |
12 | 11 | eqcoms 2618 |
. . . . . . . . . . . . . 14
⊢
((#‘𝑝) = 𝑁 → 〈0, 𝑁〉 = 〈0, (#‘𝑝)〉) |
13 | 12 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢
((#‘𝑝) = 𝑁 → ((𝑝 ++ 〈“(𝑝‘0)”〉) substr 〈0, 𝑁〉) = ((𝑝 ++ 〈“(𝑝‘0)”〉) substr 〈0,
(#‘𝑝)〉)) |
14 | 13 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) → ((𝑝 ++ 〈“(𝑝‘0)”〉) substr 〈0, 𝑁〉) = ((𝑝 ++ 〈“(𝑝‘0)”〉) substr 〈0,
(#‘𝑝)〉)) |
15 | 14 | 3ad2ant1 1075 |
. . . . . . . . . . 11
⊢ (((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑝‘𝑖), (𝑝‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑝), (𝑝‘0)} ∈ ran 𝐸) → ((𝑝 ++ 〈“(𝑝‘0)”〉) substr 〈0, 𝑁〉) = ((𝑝 ++ 〈“(𝑝‘0)”〉) substr 〈0,
(#‘𝑝)〉)) |
16 | 15 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑝‘𝑖), (𝑝‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑝), (𝑝‘0)} ∈ ran 𝐸) ∧ (𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ)) → ((𝑝 ++ 〈“(𝑝‘0)”〉) substr
〈0, 𝑁〉) = ((𝑝 ++ 〈“(𝑝‘0)”〉) substr
〈0, (#‘𝑝)〉)) |
17 | | simpll 786 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ 𝑁 ∈ ℕ) → 𝑝 ∈ Word 𝑉) |
18 | | fstwrdne0 13200 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℕ ∧ (𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁)) → (𝑝‘0) ∈ 𝑉) |
19 | 18 | ancoms 468 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ 𝑁 ∈ ℕ) → (𝑝‘0) ∈ 𝑉) |
20 | 19 | s1cld 13236 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ 𝑁 ∈ ℕ) → 〈“(𝑝‘0)”〉 ∈
Word 𝑉) |
21 | 17, 20 | jca 553 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ 𝑁 ∈ ℕ) → (𝑝 ∈ Word 𝑉 ∧ 〈“(𝑝‘0)”〉 ∈ Word 𝑉)) |
22 | 21 | ex 449 |
. . . . . . . . . . . . . . 15
⊢ ((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) → (𝑁 ∈ ℕ → (𝑝 ∈ Word 𝑉 ∧ 〈“(𝑝‘0)”〉 ∈ Word 𝑉))) |
23 | 22 | 3ad2ant1 1075 |
. . . . . . . . . . . . . 14
⊢ (((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑝‘𝑖), (𝑝‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑝), (𝑝‘0)} ∈ ran 𝐸) → (𝑁 ∈ ℕ → (𝑝 ∈ Word 𝑉 ∧ 〈“(𝑝‘0)”〉 ∈ Word 𝑉))) |
24 | 23 | com12 32 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → (((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑝‘𝑖), (𝑝‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑝), (𝑝‘0)} ∈ ran 𝐸) → (𝑝 ∈ Word 𝑉 ∧ 〈“(𝑝‘0)”〉 ∈ Word 𝑉))) |
25 | 24 | 3ad2ant3 1077 |
. . . . . . . . . . . 12
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → (((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑝‘𝑖), (𝑝‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑝), (𝑝‘0)} ∈ ran 𝐸) → (𝑝 ∈ Word 𝑉 ∧ 〈“(𝑝‘0)”〉 ∈ Word 𝑉))) |
26 | 25 | impcom 445 |
. . . . . . . . . . 11
⊢ ((((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑝‘𝑖), (𝑝‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑝), (𝑝‘0)} ∈ ran 𝐸) ∧ (𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ)) → (𝑝 ∈ Word 𝑉 ∧ 〈“(𝑝‘0)”〉 ∈ Word 𝑉)) |
27 | | swrdccat1 13309 |
. . . . . . . . . . 11
⊢ ((𝑝 ∈ Word 𝑉 ∧ 〈“(𝑝‘0)”〉 ∈ Word 𝑉) → ((𝑝 ++ 〈“(𝑝‘0)”〉) substr 〈0,
(#‘𝑝)〉) = 𝑝) |
28 | 26, 27 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑝‘𝑖), (𝑝‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑝), (𝑝‘0)} ∈ ran 𝐸) ∧ (𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ)) → ((𝑝 ++ 〈“(𝑝‘0)”〉) substr
〈0, (#‘𝑝)〉)
= 𝑝) |
29 | 16, 28 | eqtr2d 2645 |
. . . . . . . . 9
⊢ ((((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑝‘𝑖), (𝑝‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑝), (𝑝‘0)} ∈ ran 𝐸) ∧ (𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ)) → 𝑝 = ((𝑝 ++ 〈“(𝑝‘0)”〉) substr 〈0, 𝑁〉)) |
30 | 10, 29 | jca 553 |
. . . . . . . 8
⊢ ((((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑝‘𝑖), (𝑝‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑝), (𝑝‘0)} ∈ ran 𝐸) ∧ (𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ)) → ((𝑝 ++ 〈“(𝑝‘0)”〉) ∈
𝐷 ∧ 𝑝 = ((𝑝 ++ 〈“(𝑝‘0)”〉) substr 〈0, 𝑁〉))) |
31 | 30 | ex 449 |
. . . . . . 7
⊢ (((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑝‘𝑖), (𝑝‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑝), (𝑝‘0)} ∈ ran 𝐸) → ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → ((𝑝 ++ 〈“(𝑝‘0)”〉) ∈ 𝐷 ∧ 𝑝 = ((𝑝 ++ 〈“(𝑝‘0)”〉) substr 〈0, 𝑁〉)))) |
32 | 4, 31 | syl 17 |
. . . . . 6
⊢ (𝑝 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → ((𝑝 ++ 〈“(𝑝‘0)”〉) ∈ 𝐷 ∧ 𝑝 = ((𝑝 ++ 〈“(𝑝‘0)”〉) substr 〈0, 𝑁〉)))) |
33 | 32 | impcom 445 |
. . . . 5
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ 𝑝 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) → ((𝑝 ++ 〈“(𝑝‘0)”〉) ∈ 𝐷 ∧ 𝑝 = ((𝑝 ++ 〈“(𝑝‘0)”〉) substr 〈0, 𝑁〉))) |
34 | | oveq1 6556 |
. . . . . . 7
⊢ (𝑥 = (𝑝 ++ 〈“(𝑝‘0)”〉) → (𝑥 substr 〈0, 𝑁〉) = ((𝑝 ++ 〈“(𝑝‘0)”〉) substr 〈0, 𝑁〉)) |
35 | 34 | eqeq2d 2620 |
. . . . . 6
⊢ (𝑥 = (𝑝 ++ 〈“(𝑝‘0)”〉) → (𝑝 = (𝑥 substr 〈0, 𝑁〉) ↔ 𝑝 = ((𝑝 ++ 〈“(𝑝‘0)”〉) substr 〈0, 𝑁〉))) |
36 | 35 | rspcev 3282 |
. . . . 5
⊢ (((𝑝 ++ 〈“(𝑝‘0)”〉) ∈
𝐷 ∧ 𝑝 = ((𝑝 ++ 〈“(𝑝‘0)”〉) substr 〈0, 𝑁〉)) → ∃𝑥 ∈ 𝐷 𝑝 = (𝑥 substr 〈0, 𝑁〉)) |
37 | 33, 36 | syl 17 |
. . . 4
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ 𝑝 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) → ∃𝑥 ∈ 𝐷 𝑝 = (𝑥 substr 〈0, 𝑁〉)) |
38 | 1, 2 | clwwlkfv 26323 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → (𝐹‘𝑥) = (𝑥 substr 〈0, 𝑁〉)) |
39 | 38 | eqeq2d 2620 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → (𝑝 = (𝐹‘𝑥) ↔ 𝑝 = (𝑥 substr 〈0, 𝑁〉))) |
40 | 39 | adantl 481 |
. . . . 5
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ 𝑝 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) ∧ 𝑥 ∈ 𝐷) → (𝑝 = (𝐹‘𝑥) ↔ 𝑝 = (𝑥 substr 〈0, 𝑁〉))) |
41 | 40 | rexbidva 3031 |
. . . 4
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ 𝑝 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) → (∃𝑥 ∈ 𝐷 𝑝 = (𝐹‘𝑥) ↔ ∃𝑥 ∈ 𝐷 𝑝 = (𝑥 substr 〈0, 𝑁〉))) |
42 | 37, 41 | mpbird 246 |
. . 3
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ 𝑝 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) → ∃𝑥 ∈ 𝐷 𝑝 = (𝐹‘𝑥)) |
43 | 42 | ralrimiva 2949 |
. 2
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → ∀𝑝 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)∃𝑥 ∈ 𝐷 𝑝 = (𝐹‘𝑥)) |
44 | | dffo3 6282 |
. 2
⊢ (𝐹:𝐷–onto→((𝑉 ClWWalksN 𝐸)‘𝑁) ↔ (𝐹:𝐷⟶((𝑉 ClWWalksN 𝐸)‘𝑁) ∧ ∀𝑝 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)∃𝑥 ∈ 𝐷 𝑝 = (𝐹‘𝑥))) |
45 | 3, 43, 44 | sylanbrc 695 |
1
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → 𝐹:𝐷–onto→((𝑉 ClWWalksN 𝐸)‘𝑁)) |