Step | Hyp | Ref
| Expression |
1 | | ovex 6577 |
. . . 4
⊢ ((𝑁 + 1) WWalkSN 𝐺) ∈ V |
2 | 1 | a1i 11 |
. . 3
⊢ (𝑊 ∈ (𝑁 WWalkSN 𝐺) → ((𝑁 + 1) WWalkSN 𝐺) ∈ V) |
3 | | rabexg 4739 |
. . 3
⊢ (((𝑁 + 1) WWalkSN 𝐺) ∈ V → {𝑡 ∈ ((𝑁 + 1) WWalkSN 𝐺) ∣ ((𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸)} ∈ V) |
4 | | mptexg 6389 |
. . 3
⊢ ({𝑡 ∈ ((𝑁 + 1) WWalkSN 𝐺) ∣ ((𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸)} ∈ V → (𝑥 ∈ {𝑡 ∈ ((𝑁 + 1) WWalkSN 𝐺) ∣ ((𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸)} ↦ ( lastS ‘𝑥)) ∈ V) |
5 | 2, 3, 4 | 3syl 18 |
. 2
⊢ (𝑊 ∈ (𝑁 WWalkSN 𝐺) → (𝑥 ∈ {𝑡 ∈ ((𝑁 + 1) WWalkSN 𝐺) ∣ ((𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸)} ↦ ( lastS ‘𝑥)) ∈ V) |
6 | | wwlksnextbij.v |
. . . 4
⊢ 𝑉 = (Vtx‘𝐺) |
7 | | wwlksnextbij.e |
. . . 4
⊢ 𝐸 = (Edg‘𝐺) |
8 | | eqid 2610 |
. . . 4
⊢ {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ 𝐸)} = {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ 𝐸)} |
9 | | preq2 4213 |
. . . . . 6
⊢ (𝑛 = 𝑝 → {( lastS ‘𝑊), 𝑛} = {( lastS ‘𝑊), 𝑝}) |
10 | 9 | eleq1d 2672 |
. . . . 5
⊢ (𝑛 = 𝑝 → ({( lastS ‘𝑊), 𝑛} ∈ 𝐸 ↔ {( lastS ‘𝑊), 𝑝} ∈ 𝐸)) |
11 | 10 | cbvrabv 3172 |
. . . 4
⊢ {𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑊), 𝑛} ∈ 𝐸} = {𝑝 ∈ 𝑉 ∣ {( lastS ‘𝑊), 𝑝} ∈ 𝐸} |
12 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑡 = 𝑤 → (#‘𝑡) = (#‘𝑤)) |
13 | 12 | eqeq1d 2612 |
. . . . . . 7
⊢ (𝑡 = 𝑤 → ((#‘𝑡) = (𝑁 + 2) ↔ (#‘𝑤) = (𝑁 + 2))) |
14 | | oveq1 6556 |
. . . . . . . 8
⊢ (𝑡 = 𝑤 → (𝑡 substr 〈0, (𝑁 + 1)〉) = (𝑤 substr 〈0, (𝑁 + 1)〉)) |
15 | 14 | eqeq1d 2612 |
. . . . . . 7
⊢ (𝑡 = 𝑤 → ((𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ↔ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊)) |
16 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑡 = 𝑤 → ( lastS ‘𝑡) = ( lastS ‘𝑤)) |
17 | 16 | preq2d 4219 |
. . . . . . . 8
⊢ (𝑡 = 𝑤 → {( lastS ‘𝑊), ( lastS ‘𝑡)} = {( lastS ‘𝑊), ( lastS ‘𝑤)}) |
18 | 17 | eleq1d 2672 |
. . . . . . 7
⊢ (𝑡 = 𝑤 → ({( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸 ↔ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ 𝐸)) |
19 | 13, 15, 18 | 3anbi123d 1391 |
. . . . . 6
⊢ (𝑡 = 𝑤 → (((#‘𝑡) = (𝑁 + 2) ∧ (𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸) ↔ ((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ 𝐸))) |
20 | 19 | cbvrabv 3172 |
. . . . 5
⊢ {𝑡 ∈ Word 𝑉 ∣ ((#‘𝑡) = (𝑁 + 2) ∧ (𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸)} = {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ 𝐸)} |
21 | 20 | mpteq1i 4667 |
. . . 4
⊢ (𝑥 ∈ {𝑡 ∈ Word 𝑉 ∣ ((#‘𝑡) = (𝑁 + 2) ∧ (𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸)} ↦ ( lastS ‘𝑥)) = (𝑥 ∈ {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ 𝐸)} ↦ ( lastS ‘𝑥)) |
22 | 6, 7, 8, 11, 21 | wwlksnextbij0 41107 |
. . 3
⊢ (𝑊 ∈ (𝑁 WWalkSN 𝐺) → (𝑥 ∈ {𝑡 ∈ Word 𝑉 ∣ ((#‘𝑡) = (𝑁 + 2) ∧ (𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸)} ↦ ( lastS ‘𝑥)):{𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ 𝐸)}–1-1-onto→{𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑊), 𝑛} ∈ 𝐸}) |
23 | | eqid 2610 |
. . . . . . 7
⊢ {𝑡 ∈ Word 𝑉 ∣ ((#‘𝑡) = (𝑁 + 2) ∧ (𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸)} = {𝑡 ∈ Word 𝑉 ∣ ((#‘𝑡) = (𝑁 + 2) ∧ (𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸)} |
24 | 6, 7, 23 | wwlksnextwrd 41103 |
. . . . . 6
⊢ (𝑊 ∈ (𝑁 WWalkSN 𝐺) → {𝑡 ∈ Word 𝑉 ∣ ((#‘𝑡) = (𝑁 + 2) ∧ (𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸)} = {𝑡 ∈ ((𝑁 + 1) WWalkSN 𝐺) ∣ ((𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸)}) |
25 | 24 | eqcomd 2616 |
. . . . 5
⊢ (𝑊 ∈ (𝑁 WWalkSN 𝐺) → {𝑡 ∈ ((𝑁 + 1) WWalkSN 𝐺) ∣ ((𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸)} = {𝑡 ∈ Word 𝑉 ∣ ((#‘𝑡) = (𝑁 + 2) ∧ (𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸)}) |
26 | 25 | mpteq1d 4666 |
. . . 4
⊢ (𝑊 ∈ (𝑁 WWalkSN 𝐺) → (𝑥 ∈ {𝑡 ∈ ((𝑁 + 1) WWalkSN 𝐺) ∣ ((𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸)} ↦ ( lastS ‘𝑥)) = (𝑥 ∈ {𝑡 ∈ Word 𝑉 ∣ ((#‘𝑡) = (𝑁 + 2) ∧ (𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸)} ↦ ( lastS ‘𝑥))) |
27 | 6, 7, 8 | wwlksnextwrd 41103 |
. . . . 5
⊢ (𝑊 ∈ (𝑁 WWalkSN 𝐺) → {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ 𝐸)} = {𝑤 ∈ ((𝑁 + 1) WWalkSN 𝐺) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ 𝐸)}) |
28 | 27 | eqcomd 2616 |
. . . 4
⊢ (𝑊 ∈ (𝑁 WWalkSN 𝐺) → {𝑤 ∈ ((𝑁 + 1) WWalkSN 𝐺) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ 𝐸)} = {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ 𝐸)}) |
29 | | eqidd 2611 |
. . . 4
⊢ (𝑊 ∈ (𝑁 WWalkSN 𝐺) → {𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑊), 𝑛} ∈ 𝐸} = {𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑊), 𝑛} ∈ 𝐸}) |
30 | 26, 28, 29 | f1oeq123d 6046 |
. . 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 ‘𝑊), 𝑛} ∈ 𝐸})) |
31 | 22, 30 | mpbird 246 |
. 2
⊢ (𝑊 ∈ (𝑁 WWalkSN 𝐺) → (𝑥 ∈ {𝑡 ∈ ((𝑁 + 1) WWalkSN 𝐺) ∣ ((𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ 𝐸)} ↦ ( lastS ‘𝑥)):{𝑤 ∈ ((𝑁 + 1) WWalkSN 𝐺) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ 𝐸)}–1-1-onto→{𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑊), 𝑛} ∈ 𝐸}) |
32 | | f1oeq1 6040 |
. 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 ‘𝑊), 𝑛} ∈ 𝐸})) |
33 | 5, 31, 32 | elabd 3321 |
1
⊢ (𝑊 ∈ (𝑁 WWalkSN 𝐺) → ∃𝑓 𝑓:{𝑤 ∈ ((𝑁 + 1) WWalkSN 𝐺) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ 𝐸)}–1-1-onto→{𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑊), 𝑛} ∈ 𝐸}) |