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