Proof of Theorem wwlkextprop
Step | Hyp | Ref
| Expression |
1 | | eqidd 2611 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) ∧ (𝑥‘0) = 𝑃) → (𝑥 substr 〈0, (𝑁 + 1)〉) = (𝑥 substr 〈0, (𝑁 + 1)〉)) |
2 | | wwlkextprop.x |
. . . . . . . . 9
⊢ 𝑋 = ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) |
3 | 2 | wwlkextproplem1 26269 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) → ((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = (𝑥‘0)) |
4 | 3 | ancoms 468 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) → ((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = (𝑥‘0)) |
5 | 4 | adantr 480 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) ∧ (𝑥‘0) = 𝑃) → ((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = (𝑥‘0)) |
6 | | eqeq2 2621 |
. . . . . . 7
⊢ ((𝑥‘0) = 𝑃 → (((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = (𝑥‘0) ↔ ((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = 𝑃)) |
7 | 6 | adantl 481 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) ∧ (𝑥‘0) = 𝑃) → (((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = (𝑥‘0) ↔ ((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = 𝑃)) |
8 | 5, 7 | mpbid 221 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) ∧ (𝑥‘0) = 𝑃) → ((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = 𝑃) |
9 | 2 | wwlkextproplem2 26270 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) → {( lastS
‘(𝑥 substr 〈0,
(𝑁 + 1)〉)), ( lastS
‘𝑥)} ∈ ran 𝐸) |
10 | 9 | ancoms 468 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) → {( lastS ‘(𝑥 substr 〈0, (𝑁 + 1)〉)), ( lastS
‘𝑥)} ∈ ran 𝐸) |
11 | 10 | adantr 480 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) ∧ (𝑥‘0) = 𝑃) → {( lastS ‘(𝑥 substr 〈0, (𝑁 + 1)〉)), ( lastS ‘𝑥)} ∈ ran 𝐸) |
12 | | simpr 476 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
13 | 12 | adantr 480 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) ∧ (𝑥‘0) = 𝑃) → 𝑥 ∈ 𝑋) |
14 | | simpr 476 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) ∧ (𝑥‘0) = 𝑃) → (𝑥‘0) = 𝑃) |
15 | | simpll 786 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) ∧ (𝑥‘0) = 𝑃) → 𝑁 ∈
ℕ0) |
16 | | wwlkextprop.y |
. . . . . . . 8
⊢ 𝑌 = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃} |
17 | 2, 16 | wwlkextproplem3 26271 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑥‘0) = 𝑃 ∧ 𝑁 ∈ ℕ0) → (𝑥 substr 〈0, (𝑁 + 1)〉) ∈ 𝑌) |
18 | 13, 14, 15, 17 | syl3anc 1318 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) ∧ (𝑥‘0) = 𝑃) → (𝑥 substr 〈0, (𝑁 + 1)〉) ∈ 𝑌) |
19 | | eqeq2 2621 |
. . . . . . . 8
⊢ (𝑦 = (𝑥 substr 〈0, (𝑁 + 1)〉) → ((𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑦 ↔ (𝑥 substr 〈0, (𝑁 + 1)〉) = (𝑥 substr 〈0, (𝑁 + 1)〉))) |
20 | | fveq1 6102 |
. . . . . . . . 9
⊢ (𝑦 = (𝑥 substr 〈0, (𝑁 + 1)〉) → (𝑦‘0) = ((𝑥 substr 〈0, (𝑁 + 1)〉)‘0)) |
21 | 20 | eqeq1d 2612 |
. . . . . . . 8
⊢ (𝑦 = (𝑥 substr 〈0, (𝑁 + 1)〉) → ((𝑦‘0) = 𝑃 ↔ ((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = 𝑃)) |
22 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑦 = (𝑥 substr 〈0, (𝑁 + 1)〉) → ( lastS ‘𝑦) = ( lastS ‘(𝑥 substr 〈0, (𝑁 + 1)〉))) |
23 | 22 | preq1d 4218 |
. . . . . . . . 9
⊢ (𝑦 = (𝑥 substr 〈0, (𝑁 + 1)〉) → {( lastS ‘𝑦), ( lastS ‘𝑥)} = {( lastS ‘(𝑥 substr 〈0, (𝑁 + 1)〉)), ( lastS
‘𝑥)}) |
24 | 23 | eleq1d 2672 |
. . . . . . . 8
⊢ (𝑦 = (𝑥 substr 〈0, (𝑁 + 1)〉) → ({( lastS ‘𝑦), ( lastS ‘𝑥)} ∈ ran 𝐸 ↔ {( lastS ‘(𝑥 substr 〈0, (𝑁 + 1)〉)), ( lastS ‘𝑥)} ∈ ran 𝐸)) |
25 | 19, 21, 24 | 3anbi123d 1391 |
. . . . . . 7
⊢ (𝑦 = (𝑥 substr 〈0, (𝑁 + 1)〉) → (((𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑥)} ∈ ran 𝐸) ↔ ((𝑥 substr 〈0, (𝑁 + 1)〉) = (𝑥 substr 〈0, (𝑁 + 1)〉) ∧ ((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = 𝑃 ∧ {( lastS ‘(𝑥 substr 〈0, (𝑁 + 1)〉)), ( lastS ‘𝑥)} ∈ ran 𝐸))) |
26 | 25 | adantl 481 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) ∧ (𝑥‘0) = 𝑃) ∧ 𝑦 = (𝑥 substr 〈0, (𝑁 + 1)〉)) → (((𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑥)} ∈ ran 𝐸) ↔ ((𝑥 substr 〈0, (𝑁 + 1)〉) = (𝑥 substr 〈0, (𝑁 + 1)〉) ∧ ((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = 𝑃 ∧ {( lastS ‘(𝑥 substr 〈0, (𝑁 + 1)〉)), ( lastS ‘𝑥)} ∈ ran 𝐸))) |
27 | 18, 26 | rspcedv 3286 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) ∧ (𝑥‘0) = 𝑃) → (((𝑥 substr 〈0, (𝑁 + 1)〉) = (𝑥 substr 〈0, (𝑁 + 1)〉) ∧ ((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = 𝑃 ∧ {( lastS ‘(𝑥 substr 〈0, (𝑁 + 1)〉)), ( lastS ‘𝑥)} ∈ ran 𝐸) → ∃𝑦 ∈ 𝑌 ((𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑥)} ∈ ran 𝐸))) |
28 | 1, 8, 11, 27 | mp3and 1419 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) ∧ (𝑥‘0) = 𝑃) → ∃𝑦 ∈ 𝑌 ((𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑥)} ∈ ran 𝐸)) |
29 | 28 | ex 449 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) → ((𝑥‘0) = 𝑃 → ∃𝑦 ∈ 𝑌 ((𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑥)} ∈ ran 𝐸))) |
30 | 20 | eqcoms 2618 |
. . . . . . . . 9
⊢ ((𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑦 → (𝑦‘0) = ((𝑥 substr 〈0, (𝑁 + 1)〉)‘0)) |
31 | 30 | eqeq1d 2612 |
. . . . . . . 8
⊢ ((𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑦 → ((𝑦‘0) = 𝑃 ↔ ((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = 𝑃)) |
32 | 3 | eqcomd 2616 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) → (𝑥‘0) = ((𝑥 substr 〈0, (𝑁 + 1)〉)‘0)) |
33 | 32 | ancoms 468 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) → (𝑥‘0) = ((𝑥 substr 〈0, (𝑁 + 1)〉)‘0)) |
34 | 33 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌) → (𝑥‘0) = ((𝑥 substr 〈0, (𝑁 + 1)〉)‘0)) |
35 | | eqeq2 2621 |
. . . . . . . . . 10
⊢ (𝑃 = ((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) → ((𝑥‘0) = 𝑃 ↔ (𝑥‘0) = ((𝑥 substr 〈0, (𝑁 + 1)〉)‘0))) |
36 | 35 | eqcoms 2618 |
. . . . . . . . 9
⊢ (((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = 𝑃 → ((𝑥‘0) = 𝑃 ↔ (𝑥‘0) = ((𝑥 substr 〈0, (𝑁 + 1)〉)‘0))) |
37 | 34, 36 | syl5ibr 235 |
. . . . . . . 8
⊢ (((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = 𝑃 → (((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌) → (𝑥‘0) = 𝑃)) |
38 | 31, 37 | syl6bi 242 |
. . . . . . 7
⊢ ((𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑦 → ((𝑦‘0) = 𝑃 → (((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌) → (𝑥‘0) = 𝑃))) |
39 | 38 | imp 444 |
. . . . . 6
⊢ (((𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃) → (((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌) → (𝑥‘0) = 𝑃)) |
40 | 39 | 3adant3 1074 |
. . . . 5
⊢ (((𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑥)} ∈ ran 𝐸) → (((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌) → (𝑥‘0) = 𝑃)) |
41 | 40 | com12 32 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌) → (((𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑥)} ∈ ran 𝐸) → (𝑥‘0) = 𝑃)) |
42 | 41 | rexlimdva 3013 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) → (∃𝑦 ∈ 𝑌 ((𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑥)} ∈ ran 𝐸) → (𝑥‘0) = 𝑃)) |
43 | 29, 42 | impbid 201 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) → ((𝑥‘0) = 𝑃 ↔ ∃𝑦 ∈ 𝑌 ((𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑥)} ∈ ran 𝐸))) |
44 | 43 | rabbidva 3163 |
1
⊢ (𝑁 ∈ ℕ0
→ {𝑥 ∈ 𝑋 ∣ (𝑥‘0) = 𝑃} = {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑌 ((𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑥)} ∈ ran 𝐸)}) |