Step | Hyp | Ref
| Expression |
1 | | ovexd 6680 |
. . 3
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → ((𝑁 + 1) WWalksN 𝐺) ∈ V) |
2 | | rabexg 4812 |
. . 3
⊢ (((𝑁 + 1) WWalksN 𝐺) ∈ V → {𝑡 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸)} ∈ V) |
3 | | mptexg 6484 |
. . 3
⊢ ({𝑡 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸)} ∈ V → (𝑥 ∈ {𝑡 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸)} ↦ ( lastS ‘𝑥)) ∈ V) |
4 | 1, 2, 3 | 3syl 18 |
. 2
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → (𝑥 ∈ {𝑡 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸)} ↦ ( lastS ‘𝑥)) ∈ V) |
5 | | wwlksnextbij.v |
. . . 4
⊢ 𝑉 = (Vtx‘𝐺) |
6 | | wwlksnextbij.e |
. . . 4
⊢ 𝐸 = (Edg‘𝐺) |
7 | | eqid 2622 |
. . . 4
⊢ {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ 𝐸)} = {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ 𝐸)} |
8 | | preq2 4269 |
. . . . . 6
⊢ (𝑛 = 𝑝 → {( lastS ‘𝑊), 𝑛} = {( lastS ‘𝑊), 𝑝}) |
9 | 8 | eleq1d 2686 |
. . . . 5
⊢ (𝑛 = 𝑝 → ({( lastS ‘𝑊), 𝑛} ∈ 𝐸 ↔ {( lastS ‘𝑊), 𝑝} ∈ 𝐸)) |
10 | 9 | cbvrabv 3199 |
. . . 4
⊢ {𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑊), 𝑛} ∈ 𝐸} = {𝑝 ∈ 𝑉 ∣ {( lastS ‘𝑊), 𝑝} ∈ 𝐸} |
11 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑡 = 𝑤 → (#‘𝑡) = (#‘𝑤)) |
12 | 11 | eqeq1d 2624 |
. . . . . . 7
⊢ (𝑡 = 𝑤 → ((#‘𝑡) = (𝑁 + 2) ↔ (#‘𝑤) = (𝑁 + 2))) |
13 | | oveq1 6657 |
. . . . . . . 8
⊢ (𝑡 = 𝑤 → (𝑡 substr 〈0, (𝑁 + 1)〉) = (𝑤 substr 〈0, (𝑁 + 1)〉)) |
14 | 13 | eqeq1d 2624 |
. . . . . . 7
⊢ (𝑡 = 𝑤 → ((𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ↔ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊)) |
15 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑡 = 𝑤 → ( lastS ‘𝑡) = ( lastS ‘𝑤)) |
16 | 15 | preq2d 4275 |
. . . . . . . 8
⊢ (𝑡 = 𝑤 → {( lastS ‘𝑊), ( lastS ‘𝑡)} = {( lastS ‘𝑊), ( lastS ‘𝑤)}) |
17 | 16 | eleq1d 2686 |
. . . . . . 7
⊢ (𝑡 = 𝑤 → ({( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸 ↔ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ 𝐸)) |
18 | 12, 14, 17 | 3anbi123d 1399 |
. . . . . 6
⊢ (𝑡 = 𝑤 → (((#‘𝑡) = (𝑁 + 2) ∧ (𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸) ↔ ((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ 𝐸))) |
19 | 18 | cbvrabv 3199 |
. . . . 5
⊢ {𝑡 ∈ Word 𝑉 ∣ ((#‘𝑡) = (𝑁 + 2) ∧ (𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸)} = {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ 𝐸)} |
20 | 19 | mpteq1i 4739 |
. . . 4
⊢ (𝑥 ∈ {𝑡 ∈ Word 𝑉 ∣ ((#‘𝑡) = (𝑁 + 2) ∧ (𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸)} ↦ ( lastS ‘𝑥)) = (𝑥 ∈ {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ 𝐸)} ↦ ( lastS ‘𝑥)) |
21 | 5, 6, 7, 10, 20 | wwlksnextbij0 26796 |
. . 3
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → (𝑥 ∈ {𝑡 ∈ Word 𝑉 ∣ ((#‘𝑡) = (𝑁 + 2) ∧ (𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸)} ↦ ( lastS ‘𝑥)):{𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ 𝐸)}–1-1-onto→{𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑊), 𝑛} ∈ 𝐸}) |
22 | | eqid 2622 |
. . . . . . 7
⊢ {𝑡 ∈ Word 𝑉 ∣ ((#‘𝑡) = (𝑁 + 2) ∧ (𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸)} = {𝑡 ∈ Word 𝑉 ∣ ((#‘𝑡) = (𝑁 + 2) ∧ (𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸)} |
23 | 5, 6, 22 | wwlksnextwrd 26792 |
. . . . . 6
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → {𝑡 ∈ Word 𝑉 ∣ ((#‘𝑡) = (𝑁 + 2) ∧ (𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸)} = {𝑡 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸)}) |
24 | 23 | eqcomd 2628 |
. . . . 5
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → {𝑡 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸)} = {𝑡 ∈ Word 𝑉 ∣ ((#‘𝑡) = (𝑁 + 2) ∧ (𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸)}) |
25 | 24 | mpteq1d 4738 |
. . . 4
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → (𝑥 ∈ {𝑡 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸)} ↦ ( lastS ‘𝑥)) = (𝑥 ∈ {𝑡 ∈ Word 𝑉 ∣ ((#‘𝑡) = (𝑁 + 2) ∧ (𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸)} ↦ ( lastS ‘𝑥))) |
26 | 5, 6, 7 | wwlksnextwrd 26792 |
. . . . 5
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ 𝐸)} = {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ 𝐸)}) |
27 | 26 | eqcomd 2628 |
. . . 4
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ 𝐸)} = {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ 𝐸)}) |
28 | | eqidd 2623 |
. . . 4
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → {𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑊), 𝑛} ∈ 𝐸} = {𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑊), 𝑛} ∈ 𝐸}) |
29 | 25, 27, 28 | f1oeq123d 6133 |
. . 3
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → ((𝑥 ∈ {𝑡 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸)} ↦ ( lastS ‘𝑥)):{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ 𝐸)}–1-1-onto→{𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑊), 𝑛} ∈ 𝐸} ↔ (𝑥 ∈ {𝑡 ∈ Word 𝑉 ∣ ((#‘𝑡) = (𝑁 + 2) ∧ (𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸)} ↦ ( lastS ‘𝑥)):{𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ 𝐸)}–1-1-onto→{𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑊), 𝑛} ∈ 𝐸})) |
30 | 21, 29 | mpbird 247 |
. 2
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → (𝑥 ∈ {𝑡 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸)} ↦ ( lastS ‘𝑥)):{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ 𝐸)}–1-1-onto→{𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑊), 𝑛} ∈ 𝐸}) |
31 | | f1oeq1 6127 |
. 2
⊢ (𝑓 = (𝑥 ∈ {𝑡 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸)} ↦ ( lastS ‘𝑥)) → (𝑓:{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ 𝐸)}–1-1-onto→{𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑊), 𝑛} ∈ 𝐸} ↔ (𝑥 ∈ {𝑡 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸)} ↦ ( lastS ‘𝑥)):{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ 𝐸)}–1-1-onto→{𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑊), 𝑛} ∈ 𝐸})) |
32 | 4, 30, 31 | elabd 3352 |
1
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → ∃𝑓 𝑓:{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ 𝐸)}–1-1-onto→{𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑊), 𝑛} ∈ 𝐸}) |