Step | Hyp | Ref
| Expression |
1 | | fvex 6113 |
. . . 4
⊢ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∈ V |
2 | 1 | a1i 11 |
. . 3
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∈ V) |
3 | | rabexg 4739 |
. . 3
⊢ (((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∈ V → {𝑡 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ ran 𝐸)} ∈ V) |
4 | | mptexg 6389 |
. . 3
⊢ ({𝑡 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ ran 𝐸)} ∈ V → (𝑥 ∈ {𝑡 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ ran 𝐸)} ↦ ( lastS ‘𝑥)) ∈ V) |
5 | 2, 3, 4 | 3syl 18 |
. 2
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → (𝑥 ∈ {𝑡 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ ran 𝐸)} ↦ ( lastS ‘𝑥)) ∈ V) |
6 | | eqid 2610 |
. . . 4
⊢ {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)} = {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)} |
7 | | preq2 4213 |
. . . . . 6
⊢ (𝑛 = 𝑝 → {( lastS ‘𝑊), 𝑛} = {( lastS ‘𝑊), 𝑝}) |
8 | 7 | eleq1d 2672 |
. . . . 5
⊢ (𝑛 = 𝑝 → ({( lastS ‘𝑊), 𝑛} ∈ ran 𝐸 ↔ {( lastS ‘𝑊), 𝑝} ∈ ran 𝐸)) |
9 | 8 | cbvrabv 3172 |
. . . 4
⊢ {𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑊), 𝑛} ∈ ran 𝐸} = {𝑝 ∈ 𝑉 ∣ {( lastS ‘𝑊), 𝑝} ∈ ran 𝐸} |
10 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑡 = 𝑤 → (#‘𝑡) = (#‘𝑤)) |
11 | 10 | eqeq1d 2612 |
. . . . . . 7
⊢ (𝑡 = 𝑤 → ((#‘𝑡) = (𝑁 + 2) ↔ (#‘𝑤) = (𝑁 + 2))) |
12 | | oveq1 6556 |
. . . . . . . 8
⊢ (𝑡 = 𝑤 → (𝑡 substr 〈0, (𝑁 + 1)〉) = (𝑤 substr 〈0, (𝑁 + 1)〉)) |
13 | 12 | eqeq1d 2612 |
. . . . . . 7
⊢ (𝑡 = 𝑤 → ((𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ↔ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊)) |
14 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑡 = 𝑤 → ( lastS ‘𝑡) = ( lastS ‘𝑤)) |
15 | 14 | preq2d 4219 |
. . . . . . . 8
⊢ (𝑡 = 𝑤 → {( lastS ‘𝑊), ( lastS ‘𝑡)} = {( lastS ‘𝑊), ( lastS ‘𝑤)}) |
16 | 15 | eleq1d 2672 |
. . . . . . 7
⊢ (𝑡 = 𝑤 → ({( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ ran 𝐸 ↔ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)) |
17 | 11, 13, 16 | 3anbi123d 1391 |
. . . . . 6
⊢ (𝑡 = 𝑤 → (((#‘𝑡) = (𝑁 + 2) ∧ (𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ ran 𝐸) ↔ ((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸))) |
18 | 17 | cbvrabv 3172 |
. . . . 5
⊢ {𝑡 ∈ Word 𝑉 ∣ ((#‘𝑡) = (𝑁 + 2) ∧ (𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ ran 𝐸)} = {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)} |
19 | | mpteq1 4665 |
. . . . 5
⊢ ({𝑡 ∈ Word 𝑉 ∣ ((#‘𝑡) = (𝑁 + 2) ∧ (𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ ran 𝐸)} = {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)} → (𝑥 ∈ {𝑡 ∈ Word 𝑉 ∣ ((#‘𝑡) = (𝑁 + 2) ∧ (𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ ran 𝐸)} ↦ ( lastS ‘𝑥)) = (𝑥 ∈ {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)} ↦ ( lastS ‘𝑥))) |
20 | 18, 19 | ax-mp 5 |
. . . 4
⊢ (𝑥 ∈ {𝑡 ∈ Word 𝑉 ∣ ((#‘𝑡) = (𝑁 + 2) ∧ (𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ ran 𝐸)} ↦ ( lastS ‘𝑥)) = (𝑥 ∈ {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)} ↦ ( lastS ‘𝑥)) |
21 | 6, 9, 20 | wwlkextbij0 26260 |
. . 3
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → (𝑥 ∈ {𝑡 ∈ Word 𝑉 ∣ ((#‘𝑡) = (𝑁 + 2) ∧ (𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ ran 𝐸)} ↦ ( lastS ‘𝑥)):{𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)}–1-1-onto→{𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑊), 𝑛} ∈ ran 𝐸}) |
22 | | eqid 2610 |
. . . . . . 7
⊢ {𝑡 ∈ Word 𝑉 ∣ ((#‘𝑡) = (𝑁 + 2) ∧ (𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ ran 𝐸)} = {𝑡 ∈ Word 𝑉 ∣ ((#‘𝑡) = (𝑁 + 2) ∧ (𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ ran 𝐸)} |
23 | 22 | wwlkextwrd 26256 |
. . . . . 6
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → {𝑡 ∈ Word 𝑉 ∣ ((#‘𝑡) = (𝑁 + 2) ∧ (𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ ran 𝐸)} = {𝑡 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ ran 𝐸)}) |
24 | 23 | eqcomd 2616 |
. . . . 5
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → {𝑡 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ ran 𝐸)} = {𝑡 ∈ Word 𝑉 ∣ ((#‘𝑡) = (𝑁 + 2) ∧ (𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ ran 𝐸)}) |
25 | 24 | mpteq1d 4666 |
. . . 4
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → (𝑥 ∈ {𝑡 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ ran 𝐸)} ↦ ( lastS ‘𝑥)) = (𝑥 ∈ {𝑡 ∈ Word 𝑉 ∣ ((#‘𝑡) = (𝑁 + 2) ∧ (𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ ran 𝐸)} ↦ ( lastS ‘𝑥))) |
26 | 6 | wwlkextwrd 26256 |
. . . . 5
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)} = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)}) |
27 | 26 | eqcomd 2616 |
. . . 4
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)} = {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)}) |
28 | | eqidd 2611 |
. . . 4
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → {𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑊), 𝑛} ∈ ran 𝐸} = {𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑊), 𝑛} ∈ ran 𝐸}) |
29 | 25, 27, 28 | f1oeq123d 6046 |
. . 3
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → ((𝑥 ∈ {𝑡 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ ran 𝐸)} ↦ ( lastS ‘𝑥)):{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)}–1-1-onto→{𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑊), 𝑛} ∈ ran 𝐸} ↔ (𝑥 ∈ {𝑡 ∈ Word 𝑉 ∣ ((#‘𝑡) = (𝑁 + 2) ∧ (𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ ran 𝐸)} ↦ ( lastS ‘𝑥)):{𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)}–1-1-onto→{𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑊), 𝑛} ∈ ran 𝐸})) |
30 | 21, 29 | mpbird 246 |
. 2
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → (𝑥 ∈ {𝑡 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ ran 𝐸)} ↦ ( lastS ‘𝑥)):{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)}–1-1-onto→{𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑊), 𝑛} ∈ ran 𝐸}) |
31 | | f1oeq1 6040 |
. . 3
⊢ (𝑓 = (𝑥 ∈ {𝑡 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ ran 𝐸)} ↦ ( lastS ‘𝑥)) → (𝑓:{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)}–1-1-onto→{𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑊), 𝑛} ∈ ran 𝐸} ↔ (𝑥 ∈ {𝑡 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ ran 𝐸)} ↦ ( lastS ‘𝑥)):{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)}–1-1-onto→{𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑊), 𝑛} ∈ ran 𝐸})) |
32 | 31 | spcegv 3267 |
. 2
⊢ ((𝑥 ∈ {𝑡 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ ran 𝐸)} ↦ ( lastS ‘𝑥)) ∈ V → ((𝑥 ∈ {𝑡 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑡 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑡)} ∈ ran 𝐸)} ↦ ( lastS ‘𝑥)):{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)}–1-1-onto→{𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑊), 𝑛} ∈ ran 𝐸} → ∃𝑓 𝑓:{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)}–1-1-onto→{𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑊), 𝑛} ∈ ran 𝐸})) |
33 | 5, 30, 32 | sylc 63 |
1
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → ∃𝑓 𝑓:{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)}–1-1-onto→{𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑊), 𝑛} ∈ ran 𝐸}) |