Step | Hyp | Ref
| Expression |
1 | | fvex 6113 |
. . . . . 6
⊢ ((𝑉 WWalksN 𝐸)‘𝑁) ∈ V |
2 | 1 | mptrabex 6392 |
. . . . 5
⊢ (𝑤 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ↦ (𝑤 substr 〈0, 𝑁〉)) ∈ V |
3 | 2 | resex 5363 |
. . . 4
⊢ ((𝑤 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ↦ (𝑤 substr 〈0, 𝑁〉)) ↾ {𝑤 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∣ (𝑤‘0) = 𝑆}) ∈ V |
4 | | eqid 2610 |
. . . . 5
⊢ (𝑤 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ↦ (𝑤 substr 〈0, 𝑁〉)) = (𝑤 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ↦ (𝑤 substr 〈0, 𝑁〉)) |
5 | | eqid 2610 |
. . . . . 6
⊢ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)} = {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)} |
6 | 5, 4 | clwwlkf1o 26326 |
. . . . 5
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → (𝑤 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ↦ (𝑤 substr 〈0, 𝑁〉)):{𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)}–1-1-onto→((𝑉 ClWWalksN 𝐸)‘𝑁)) |
7 | | fveq1 6102 |
. . . . . . . 8
⊢ (𝑦 = (𝑤 substr 〈0, 𝑁〉) → (𝑦‘0) = ((𝑤 substr 〈0, 𝑁〉)‘0)) |
8 | 7 | eqeq1d 2612 |
. . . . . . 7
⊢ (𝑦 = (𝑤 substr 〈0, 𝑁〉) → ((𝑦‘0) = 𝑆 ↔ ((𝑤 substr 〈0, 𝑁〉)‘0) = 𝑆)) |
9 | 8 | 3ad2ant3 1077 |
. . . . . 6
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ 𝑤 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∧ 𝑦 = (𝑤 substr 〈0, 𝑁〉)) → ((𝑦‘0) = 𝑆 ↔ ((𝑤 substr 〈0, 𝑁〉)‘0) = 𝑆)) |
10 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑤 → ( lastS ‘𝑥) = ( lastS ‘𝑤)) |
11 | | fveq1 6102 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑤 → (𝑥‘0) = (𝑤‘0)) |
12 | 10, 11 | eqeq12d 2625 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑤 → (( lastS ‘𝑥) = (𝑥‘0) ↔ ( lastS ‘𝑤) = (𝑤‘0))) |
13 | 12 | elrab 3331 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ↔ (𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ ( lastS ‘𝑤) = (𝑤‘0))) |
14 | | wwlknimp 26215 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → (𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸)) |
15 | | simpll 786 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → 𝑤 ∈ Word 𝑉) |
16 | | nnz 11276 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
17 | | uzid 11578 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
(ℤ≥‘𝑁)) |
18 | 16, 17 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
(ℤ≥‘𝑁)) |
19 | | peano2uz 11617 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈
(ℤ≥‘𝑁) → (𝑁 + 1) ∈
(ℤ≥‘𝑁)) |
20 | 18, 19 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
(ℤ≥‘𝑁)) |
21 | | elfz1end 12242 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈ (1...𝑁)) |
22 | 21 | biimpi 205 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ ℕ → 𝑁 ∈ (1...𝑁)) |
23 | 20, 22 | jca 553 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) ∈
(ℤ≥‘𝑁) ∧ 𝑁 ∈ (1...𝑁))) |
24 | | fzss2 12252 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑁 + 1) ∈
(ℤ≥‘𝑁) → (1...𝑁) ⊆ (1...(𝑁 + 1))) |
25 | 24 | sselda 3568 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 + 1) ∈
(ℤ≥‘𝑁) ∧ 𝑁 ∈ (1...𝑁)) → 𝑁 ∈ (1...(𝑁 + 1))) |
26 | 23, 25 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ → 𝑁 ∈ (1...(𝑁 + 1))) |
27 | 26 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ (1...(𝑁 + 1))) |
28 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((#‘𝑤) =
(𝑁 + 1) →
(1...(#‘𝑤)) =
(1...(𝑁 +
1))) |
29 | 28 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘𝑤) =
(𝑁 + 1) → (𝑁 ∈ (1...(#‘𝑤)) ↔ 𝑁 ∈ (1...(𝑁 + 1)))) |
30 | 29 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = (𝑁 + 1)) → (𝑁 ∈ (1...(#‘𝑤)) ↔ 𝑁 ∈ (1...(𝑁 + 1)))) |
31 | 30 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → (𝑁 ∈ (1...(#‘𝑤)) ↔ 𝑁 ∈ (1...(𝑁 + 1)))) |
32 | 27, 31 | mpbird 246 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ (1...(#‘𝑤))) |
33 | 15, 32 | jca 553 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → (𝑤 ∈ Word 𝑉 ∧ 𝑁 ∈ (1...(#‘𝑤)))) |
34 | 33 | ex 449 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = (𝑁 + 1)) → (𝑁 ∈ ℕ → (𝑤 ∈ Word 𝑉 ∧ 𝑁 ∈ (1...(#‘𝑤))))) |
35 | 34 | 3adant3 1074 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸) → (𝑁 ∈ ℕ → (𝑤 ∈ Word 𝑉 ∧ 𝑁 ∈ (1...(#‘𝑤))))) |
36 | 14, 35 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → (𝑁 ∈ ℕ → (𝑤 ∈ Word 𝑉 ∧ 𝑁 ∈ (1...(#‘𝑤))))) |
37 | 36 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ ( lastS ‘𝑤) = (𝑤‘0)) → (𝑁 ∈ ℕ → (𝑤 ∈ Word 𝑉 ∧ 𝑁 ∈ (1...(#‘𝑤))))) |
38 | 13, 37 | sylbi 206 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)} → (𝑁 ∈ ℕ → (𝑤 ∈ Word 𝑉 ∧ 𝑁 ∈ (1...(#‘𝑤))))) |
39 | 38 | com12 32 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → (𝑤 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)} → (𝑤 ∈ Word 𝑉 ∧ 𝑁 ∈ (1...(#‘𝑤))))) |
40 | 39 | 3ad2ant3 1077 |
. . . . . . . . . 10
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → (𝑤 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)} → (𝑤 ∈ Word 𝑉 ∧ 𝑁 ∈ (1...(#‘𝑤))))) |
41 | 40 | imp 444 |
. . . . . . . . 9
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ 𝑤 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)}) → (𝑤 ∈ Word 𝑉 ∧ 𝑁 ∈ (1...(#‘𝑤)))) |
42 | | swrd0fv0 13292 |
. . . . . . . . 9
⊢ ((𝑤 ∈ Word 𝑉 ∧ 𝑁 ∈ (1...(#‘𝑤))) → ((𝑤 substr 〈0, 𝑁〉)‘0) = (𝑤‘0)) |
43 | 41, 42 | syl 17 |
. . . . . . . 8
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ 𝑤 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)}) → ((𝑤 substr 〈0, 𝑁〉)‘0) = (𝑤‘0)) |
44 | 43 | eqeq1d 2612 |
. . . . . . 7
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ 𝑤 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)}) → (((𝑤 substr 〈0, 𝑁〉)‘0) = 𝑆 ↔ (𝑤‘0) = 𝑆)) |
45 | 44 | 3adant3 1074 |
. . . . . 6
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ 𝑤 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∧ 𝑦 = (𝑤 substr 〈0, 𝑁〉)) → (((𝑤 substr 〈0, 𝑁〉)‘0) = 𝑆 ↔ (𝑤‘0) = 𝑆)) |
46 | 9, 45 | bitrd 267 |
. . . . 5
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ 𝑤 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∧ 𝑦 = (𝑤 substr 〈0, 𝑁〉)) → ((𝑦‘0) = 𝑆 ↔ (𝑤‘0) = 𝑆)) |
47 | 4, 6, 46 | f1oresrab 6302 |
. . . 4
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → ((𝑤 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ↦ (𝑤 substr 〈0, 𝑁〉)) ↾ {𝑤 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∣ (𝑤‘0) = 𝑆}):{𝑤 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∣ (𝑤‘0) = 𝑆}–1-1-onto→{𝑦 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∣ (𝑦‘0) = 𝑆}) |
48 | | f1oeq1 6040 |
. . . . 5
⊢ (𝑓 = ((𝑤 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ↦ (𝑤 substr 〈0, 𝑁〉)) ↾ {𝑤 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∣ (𝑤‘0) = 𝑆}) → (𝑓:{𝑤 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∣ (𝑤‘0) = 𝑆}–1-1-onto→{𝑦 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∣ (𝑦‘0) = 𝑆} ↔ ((𝑤 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ↦ (𝑤 substr 〈0, 𝑁〉)) ↾ {𝑤 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∣ (𝑤‘0) = 𝑆}):{𝑤 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∣ (𝑤‘0) = 𝑆}–1-1-onto→{𝑦 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∣ (𝑦‘0) = 𝑆})) |
49 | 48 | spcegv 3267 |
. . . 4
⊢ (((𝑤 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ↦ (𝑤 substr 〈0, 𝑁〉)) ↾ {𝑤 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∣ (𝑤‘0) = 𝑆}) ∈ V → (((𝑤 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ↦ (𝑤 substr 〈0, 𝑁〉)) ↾ {𝑤 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∣ (𝑤‘0) = 𝑆}):{𝑤 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∣ (𝑤‘0) = 𝑆}–1-1-onto→{𝑦 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∣ (𝑦‘0) = 𝑆} → ∃𝑓 𝑓:{𝑤 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∣ (𝑤‘0) = 𝑆}–1-1-onto→{𝑦 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∣ (𝑦‘0) = 𝑆})) |
50 | 3, 47, 49 | mpsyl 66 |
. . 3
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → ∃𝑓 𝑓:{𝑤 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∣ (𝑤‘0) = 𝑆}–1-1-onto→{𝑦 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∣ (𝑦‘0) = 𝑆}) |
51 | | fveq1 6102 |
. . . . . . 7
⊢ (𝑤 = 𝑦 → (𝑤‘0) = (𝑦‘0)) |
52 | 51 | eqeq1d 2612 |
. . . . . 6
⊢ (𝑤 = 𝑦 → ((𝑤‘0) = 𝑆 ↔ (𝑦‘0) = 𝑆)) |
53 | 52 | cbvrabv 3172 |
. . . . 5
⊢ {𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑆} = {𝑦 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∣ (𝑦‘0) = 𝑆} |
54 | | f1oeq3 6042 |
. . . . 5
⊢ ({𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑆} = {𝑦 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∣ (𝑦‘0) = 𝑆} → (𝑓:{𝑤 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∣ (𝑤‘0) = 𝑆}–1-1-onto→{𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑆} ↔ 𝑓:{𝑤 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∣ (𝑤‘0) = 𝑆}–1-1-onto→{𝑦 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∣ (𝑦‘0) = 𝑆})) |
55 | 53, 54 | mp1i 13 |
. . . 4
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → (𝑓:{𝑤 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∣ (𝑤‘0) = 𝑆}–1-1-onto→{𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑆} ↔ 𝑓:{𝑤 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∣ (𝑤‘0) = 𝑆}–1-1-onto→{𝑦 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∣ (𝑦‘0) = 𝑆})) |
56 | 55 | exbidv 1837 |
. . 3
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → (∃𝑓 𝑓:{𝑤 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∣ (𝑤‘0) = 𝑆}–1-1-onto→{𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑆} ↔ ∃𝑓 𝑓:{𝑤 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∣ (𝑤‘0) = 𝑆}–1-1-onto→{𝑦 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∣ (𝑦‘0) = 𝑆})) |
57 | 50, 56 | mpbird 246 |
. 2
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → ∃𝑓 𝑓:{𝑤 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∣ (𝑤‘0) = 𝑆}–1-1-onto→{𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑆}) |
58 | | df-rab 2905 |
. . . . 5
⊢ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑆)} = {𝑤 ∣ (𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑆))} |
59 | | anass 679 |
. . . . . . 7
⊢ (((𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ ( lastS ‘𝑤) = (𝑤‘0)) ∧ (𝑤‘0) = 𝑆) ↔ (𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑆))) |
60 | 59 | bicomi 213 |
. . . . . 6
⊢ ((𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑆)) ↔ ((𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ ( lastS ‘𝑤) = (𝑤‘0)) ∧ (𝑤‘0) = 𝑆)) |
61 | 60 | abbii 2726 |
. . . . 5
⊢ {𝑤 ∣ (𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑆))} = {𝑤 ∣ ((𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ ( lastS ‘𝑤) = (𝑤‘0)) ∧ (𝑤‘0) = 𝑆)} |
62 | 13 | bicomi 213 |
. . . . . . . 8
⊢ ((𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ ( lastS ‘𝑤) = (𝑤‘0)) ↔ 𝑤 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)}) |
63 | 62 | anbi1i 727 |
. . . . . . 7
⊢ (((𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ ( lastS ‘𝑤) = (𝑤‘0)) ∧ (𝑤‘0) = 𝑆) ↔ (𝑤 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∧ (𝑤‘0) = 𝑆)) |
64 | 63 | abbii 2726 |
. . . . . 6
⊢ {𝑤 ∣ ((𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ ( lastS ‘𝑤) = (𝑤‘0)) ∧ (𝑤‘0) = 𝑆)} = {𝑤 ∣ (𝑤 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∧ (𝑤‘0) = 𝑆)} |
65 | | df-rab 2905 |
. . . . . 6
⊢ {𝑤 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∣ (𝑤‘0) = 𝑆} = {𝑤 ∣ (𝑤 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∧ (𝑤‘0) = 𝑆)} |
66 | 64, 65 | eqtr4i 2635 |
. . . . 5
⊢ {𝑤 ∣ ((𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ ( lastS ‘𝑤) = (𝑤‘0)) ∧ (𝑤‘0) = 𝑆)} = {𝑤 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∣ (𝑤‘0) = 𝑆} |
67 | 58, 61, 66 | 3eqtri 2636 |
. . . 4
⊢ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑆)} = {𝑤 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∣ (𝑤‘0) = 𝑆} |
68 | | f1oeq2 6041 |
. . . 4
⊢ ({𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑆)} = {𝑤 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∣ (𝑤‘0) = 𝑆} → (𝑓:{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑆)}–1-1-onto→{𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑆} ↔ 𝑓:{𝑤 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∣ (𝑤‘0) = 𝑆}–1-1-onto→{𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑆})) |
69 | 67, 68 | mp1i 13 |
. . 3
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → (𝑓:{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑆)}–1-1-onto→{𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑆} ↔ 𝑓:{𝑤 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∣ (𝑤‘0) = 𝑆}–1-1-onto→{𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑆})) |
70 | 69 | exbidv 1837 |
. 2
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → (∃𝑓 𝑓:{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑆)}–1-1-onto→{𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑆} ↔ ∃𝑓 𝑓:{𝑤 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∣ (𝑤‘0) = 𝑆}–1-1-onto→{𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑆})) |
71 | 57, 70 | mpbird 246 |
1
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → ∃𝑓 𝑓:{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑆)}–1-1-onto→{𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑆}) |