Step | Hyp | Ref
| Expression |
1 | | ovex 6678 |
. . . . . 6
⊢ (𝑁 WWalksN 𝐺) ∈ V |
2 | 1 | mptrabex 6488 |
. . . . 5
⊢ (𝑤 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ↦ (𝑤 substr 〈0, 𝑁〉)) ∈ V |
3 | 2 | resex 5443 |
. . . 4
⊢ ((𝑤 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ↦ (𝑤 substr 〈0, 𝑁〉)) ↾ {𝑤 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∣ (𝑤‘0) = 𝑆}) ∈ V |
4 | | eqid 2622 |
. . . . 5
⊢ (𝑤 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ↦ (𝑤 substr 〈0, 𝑁〉)) = (𝑤 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ↦ (𝑤 substr 〈0, 𝑁〉)) |
5 | | eqid 2622 |
. . . . . 6
⊢ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ ( lastS ‘𝑥) = (𝑥‘0)} = {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ ( lastS ‘𝑥) = (𝑥‘0)} |
6 | 5, 4 | clwwlksf1o 26919 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (𝑤 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ↦ (𝑤 substr 〈0, 𝑁〉)):{𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ ( lastS ‘𝑥) = (𝑥‘0)}–1-1-onto→(𝑁 ClWWalksN 𝐺)) |
7 | | fveq1 6190 |
. . . . . . . 8
⊢ (𝑦 = (𝑤 substr 〈0, 𝑁〉) → (𝑦‘0) = ((𝑤 substr 〈0, 𝑁〉)‘0)) |
8 | 7 | eqeq1d 2624 |
. . . . . . 7
⊢ (𝑦 = (𝑤 substr 〈0, 𝑁〉) → ((𝑦‘0) = 𝑆 ↔ ((𝑤 substr 〈0, 𝑁〉)‘0) = 𝑆)) |
9 | 8 | 3ad2ant3 1084 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑤 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∧ 𝑦 = (𝑤 substr 〈0, 𝑁〉)) → ((𝑦‘0) = 𝑆 ↔ ((𝑤 substr 〈0, 𝑁〉)‘0) = 𝑆)) |
10 | | fveq2 6191 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑤 → ( lastS ‘𝑥) = ( lastS ‘𝑤)) |
11 | | fveq1 6190 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑤 → (𝑥‘0) = (𝑤‘0)) |
12 | 10, 11 | eqeq12d 2637 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑤 → (( lastS ‘𝑥) = (𝑥‘0) ↔ ( lastS ‘𝑤) = (𝑤‘0))) |
13 | 12 | elrab 3363 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ↔ (𝑤 ∈ (𝑁 WWalksN 𝐺) ∧ ( lastS ‘𝑤) = (𝑤‘0))) |
14 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
15 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
16 | 14, 15 | wwlknp 26734 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ (𝑁 WWalksN 𝐺) → (𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
17 | | simpll 790 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → 𝑤 ∈ Word (Vtx‘𝐺)) |
18 | | nnz 11399 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
19 | | uzid 11702 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
(ℤ≥‘𝑁)) |
20 | | peano2uz 11741 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈
(ℤ≥‘𝑁) → (𝑁 + 1) ∈
(ℤ≥‘𝑁)) |
21 | 18, 19, 20 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
(ℤ≥‘𝑁)) |
22 | | elfz1end 12371 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈ (1...𝑁)) |
23 | 22 | biimpi 206 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ → 𝑁 ∈ (1...𝑁)) |
24 | | fzss2 12381 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 + 1) ∈
(ℤ≥‘𝑁) → (1...𝑁) ⊆ (1...(𝑁 + 1))) |
25 | 24 | sselda 3603 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 + 1) ∈
(ℤ≥‘𝑁) ∧ 𝑁 ∈ (1...𝑁)) → 𝑁 ∈ (1...(𝑁 + 1))) |
26 | 21, 23, 25 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ → 𝑁 ∈ (1...(𝑁 + 1))) |
27 | 26 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ (1...(𝑁 + 1))) |
28 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝑤) =
(𝑁 + 1) →
(1...(#‘𝑤)) =
(1...(𝑁 +
1))) |
29 | 28 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘𝑤) =
(𝑁 + 1) → (𝑁 ∈ (1...(#‘𝑤)) ↔ 𝑁 ∈ (1...(𝑁 + 1)))) |
30 | 29 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = (𝑁 + 1)) → (𝑁 ∈ (1...(#‘𝑤)) ↔ 𝑁 ∈ (1...(𝑁 + 1)))) |
31 | 30 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → (𝑁 ∈ (1...(#‘𝑤)) ↔ 𝑁 ∈ (1...(𝑁 + 1)))) |
32 | 27, 31 | mpbird 247 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ (1...(#‘𝑤))) |
33 | 17, 32 | jca 554 |
. . . . . . . . . . . . . . 15
⊢ (((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → (𝑤 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1...(#‘𝑤)))) |
34 | 33 | ex 450 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = (𝑁 + 1)) → (𝑁 ∈ ℕ → (𝑤 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1...(#‘𝑤))))) |
35 | 34 | 3adant3 1081 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑤) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → (𝑁 ∈ ℕ → (𝑤 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1...(#‘𝑤))))) |
36 | 16, 35 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ (𝑁 WWalksN 𝐺) → (𝑁 ∈ ℕ → (𝑤 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1...(#‘𝑤))))) |
37 | 36 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ (𝑁 WWalksN 𝐺) ∧ ( lastS ‘𝑤) = (𝑤‘0)) → (𝑁 ∈ ℕ → (𝑤 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1...(#‘𝑤))))) |
38 | 13, 37 | sylbi 207 |
. . . . . . . . . 10
⊢ (𝑤 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ ( lastS ‘𝑥) = (𝑥‘0)} → (𝑁 ∈ ℕ → (𝑤 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1...(#‘𝑤))))) |
39 | 38 | impcom 446 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑤 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ ( lastS ‘𝑥) = (𝑥‘0)}) → (𝑤 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1...(#‘𝑤)))) |
40 | | swrd0fv0 13440 |
. . . . . . . . 9
⊢ ((𝑤 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ (1...(#‘𝑤))) → ((𝑤 substr 〈0, 𝑁〉)‘0) = (𝑤‘0)) |
41 | 39, 40 | syl 17 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑤 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ ( lastS ‘𝑥) = (𝑥‘0)}) → ((𝑤 substr 〈0, 𝑁〉)‘0) = (𝑤‘0)) |
42 | 41 | eqeq1d 2624 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑤 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ ( lastS ‘𝑥) = (𝑥‘0)}) → (((𝑤 substr 〈0, 𝑁〉)‘0) = 𝑆 ↔ (𝑤‘0) = 𝑆)) |
43 | 42 | 3adant3 1081 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑤 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∧ 𝑦 = (𝑤 substr 〈0, 𝑁〉)) → (((𝑤 substr 〈0, 𝑁〉)‘0) = 𝑆 ↔ (𝑤‘0) = 𝑆)) |
44 | 9, 43 | bitrd 268 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑤 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∧ 𝑦 = (𝑤 substr 〈0, 𝑁〉)) → ((𝑦‘0) = 𝑆 ↔ (𝑤‘0) = 𝑆)) |
45 | 4, 6, 44 | f1oresrab 6395 |
. . . 4
⊢ (𝑁 ∈ ℕ → ((𝑤 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ↦ (𝑤 substr 〈0, 𝑁〉)) ↾ {𝑤 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∣ (𝑤‘0) = 𝑆}):{𝑤 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∣ (𝑤‘0) = 𝑆}–1-1-onto→{𝑦 ∈ (𝑁 ClWWalksN 𝐺) ∣ (𝑦‘0) = 𝑆}) |
46 | | f1oeq1 6127 |
. . . . 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) = 𝑆})) |
47 | 46 | spcegv 3294 |
. . . 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) = 𝑆})) |
48 | 3, 45, 47 | mpsyl 68 |
. . 3
⊢ (𝑁 ∈ ℕ →
∃𝑓 𝑓:{𝑤 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∣ (𝑤‘0) = 𝑆}–1-1-onto→{𝑦 ∈ (𝑁 ClWWalksN 𝐺) ∣ (𝑦‘0) = 𝑆}) |
49 | | fveq1 6190 |
. . . . . . 7
⊢ (𝑤 = 𝑦 → (𝑤‘0) = (𝑦‘0)) |
50 | 49 | eqeq1d 2624 |
. . . . . 6
⊢ (𝑤 = 𝑦 → ((𝑤‘0) = 𝑆 ↔ (𝑦‘0) = 𝑆)) |
51 | 50 | cbvrabv 3199 |
. . . . 5
⊢ {𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑆} = {𝑦 ∈ (𝑁 ClWWalksN 𝐺) ∣ (𝑦‘0) = 𝑆} |
52 | | f1oeq3 6129 |
. . . . 5
⊢ ({𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑆} = {𝑦 ∈ (𝑁 ClWWalksN 𝐺) ∣ (𝑦‘0) = 𝑆} → (𝑓:{𝑤 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∣ (𝑤‘0) = 𝑆}–1-1-onto→{𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑆} ↔ 𝑓:{𝑤 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∣ (𝑤‘0) = 𝑆}–1-1-onto→{𝑦 ∈ (𝑁 ClWWalksN 𝐺) ∣ (𝑦‘0) = 𝑆})) |
53 | 51, 52 | mp1i 13 |
. . . 4
⊢ (𝑁 ∈ ℕ → (𝑓:{𝑤 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∣ (𝑤‘0) = 𝑆}–1-1-onto→{𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑆} ↔ 𝑓:{𝑤 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∣ (𝑤‘0) = 𝑆}–1-1-onto→{𝑦 ∈ (𝑁 ClWWalksN 𝐺) ∣ (𝑦‘0) = 𝑆})) |
54 | 53 | exbidv 1850 |
. . 3
⊢ (𝑁 ∈ ℕ →
(∃𝑓 𝑓:{𝑤 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∣ (𝑤‘0) = 𝑆}–1-1-onto→{𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑆} ↔ ∃𝑓 𝑓:{𝑤 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∣ (𝑤‘0) = 𝑆}–1-1-onto→{𝑦 ∈ (𝑁 ClWWalksN 𝐺) ∣ (𝑦‘0) = 𝑆})) |
55 | 48, 54 | mpbird 247 |
. 2
⊢ (𝑁 ∈ ℕ →
∃𝑓 𝑓:{𝑤 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∣ (𝑤‘0) = 𝑆}–1-1-onto→{𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑆}) |
56 | | df-rab 2921 |
. . . . 5
⊢ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑆)} = {𝑤 ∣ (𝑤 ∈ (𝑁 WWalksN 𝐺) ∧ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑆))} |
57 | | anass 681 |
. . . . . . 7
⊢ (((𝑤 ∈ (𝑁 WWalksN 𝐺) ∧ ( lastS ‘𝑤) = (𝑤‘0)) ∧ (𝑤‘0) = 𝑆) ↔ (𝑤 ∈ (𝑁 WWalksN 𝐺) ∧ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑆))) |
58 | 57 | bicomi 214 |
. . . . . 6
⊢ ((𝑤 ∈ (𝑁 WWalksN 𝐺) ∧ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑆)) ↔ ((𝑤 ∈ (𝑁 WWalksN 𝐺) ∧ ( lastS ‘𝑤) = (𝑤‘0)) ∧ (𝑤‘0) = 𝑆)) |
59 | 58 | abbii 2739 |
. . . . 5
⊢ {𝑤 ∣ (𝑤 ∈ (𝑁 WWalksN 𝐺) ∧ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑆))} = {𝑤 ∣ ((𝑤 ∈ (𝑁 WWalksN 𝐺) ∧ ( lastS ‘𝑤) = (𝑤‘0)) ∧ (𝑤‘0) = 𝑆)} |
60 | 13 | bicomi 214 |
. . . . . . . 8
⊢ ((𝑤 ∈ (𝑁 WWalksN 𝐺) ∧ ( lastS ‘𝑤) = (𝑤‘0)) ↔ 𝑤 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ ( lastS ‘𝑥) = (𝑥‘0)}) |
61 | 60 | anbi1i 731 |
. . . . . . 7
⊢ (((𝑤 ∈ (𝑁 WWalksN 𝐺) ∧ ( lastS ‘𝑤) = (𝑤‘0)) ∧ (𝑤‘0) = 𝑆) ↔ (𝑤 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∧ (𝑤‘0) = 𝑆)) |
62 | 61 | abbii 2739 |
. . . . . 6
⊢ {𝑤 ∣ ((𝑤 ∈ (𝑁 WWalksN 𝐺) ∧ ( lastS ‘𝑤) = (𝑤‘0)) ∧ (𝑤‘0) = 𝑆)} = {𝑤 ∣ (𝑤 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∧ (𝑤‘0) = 𝑆)} |
63 | | df-rab 2921 |
. . . . . 6
⊢ {𝑤 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∣ (𝑤‘0) = 𝑆} = {𝑤 ∣ (𝑤 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∧ (𝑤‘0) = 𝑆)} |
64 | 62, 63 | eqtr4i 2647 |
. . . . 5
⊢ {𝑤 ∣ ((𝑤 ∈ (𝑁 WWalksN 𝐺) ∧ ( lastS ‘𝑤) = (𝑤‘0)) ∧ (𝑤‘0) = 𝑆)} = {𝑤 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∣ (𝑤‘0) = 𝑆} |
65 | 56, 59, 64 | 3eqtri 2648 |
. . . 4
⊢ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑆)} = {𝑤 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∣ (𝑤‘0) = 𝑆} |
66 | | f1oeq2 6128 |
. . . 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) = 𝑆})) |
67 | 65, 66 | mp1i 13 |
. . 3
⊢ (𝑁 ∈ ℕ → (𝑓:{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑆)}–1-1-onto→{𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑆} ↔ 𝑓:{𝑤 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∣ (𝑤‘0) = 𝑆}–1-1-onto→{𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑆})) |
68 | 67 | exbidv 1850 |
. 2
⊢ (𝑁 ∈ ℕ →
(∃𝑓 𝑓:{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑆)}–1-1-onto→{𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑆} ↔ ∃𝑓 𝑓:{𝑤 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ ( lastS ‘𝑥) = (𝑥‘0)} ∣ (𝑤‘0) = 𝑆}–1-1-onto→{𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑆})) |
69 | 55, 68 | mpbird 247 |
1
⊢ (𝑁 ∈ ℕ →
∃𝑓 𝑓:{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑆)}–1-1-onto→{𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑆}) |