Proof of Theorem wwlksnextprop
Step | Hyp | Ref
| Expression |
1 | | eqidd 2623 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) ∧ (𝑥‘0) = 𝑃) → (𝑥 substr 〈0, (𝑁 + 1)〉) = (𝑥 substr 〈0, (𝑁 + 1)〉)) |
2 | | wwlksnextprop.x |
. . . . . . . . 9
⊢ 𝑋 = ((𝑁 + 1) WWalksN 𝐺) |
3 | 2 | wwlksnextproplem1 26804 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) → ((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = (𝑥‘0)) |
4 | 3 | ancoms 469 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) → ((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = (𝑥‘0)) |
5 | 4 | adantr 481 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) ∧ (𝑥‘0) = 𝑃) → ((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = (𝑥‘0)) |
6 | | eqeq2 2633 |
. . . . . . 7
⊢ ((𝑥‘0) = 𝑃 → (((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = (𝑥‘0) ↔ ((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = 𝑃)) |
7 | 6 | adantl 482 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) ∧ (𝑥‘0) = 𝑃) → (((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = (𝑥‘0) ↔ ((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = 𝑃)) |
8 | 5, 7 | mpbid 222 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) ∧ (𝑥‘0) = 𝑃) → ((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = 𝑃) |
9 | | wwlksnextprop.e |
. . . . . . . 8
⊢ 𝐸 = (Edg‘𝐺) |
10 | 2, 9 | wwlksnextproplem2 26805 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) → {( lastS
‘(𝑥 substr 〈0,
(𝑁 + 1)〉)), ( lastS
‘𝑥)} ∈ 𝐸) |
11 | 10 | ancoms 469 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) → {( lastS ‘(𝑥 substr 〈0, (𝑁 + 1)〉)), ( lastS
‘𝑥)} ∈ 𝐸) |
12 | 11 | adantr 481 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) ∧ (𝑥‘0) = 𝑃) → {( lastS ‘(𝑥 substr 〈0, (𝑁 + 1)〉)), ( lastS ‘𝑥)} ∈ 𝐸) |
13 | | simpr 477 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
14 | 13 | adantr 481 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) ∧ (𝑥‘0) = 𝑃) → 𝑥 ∈ 𝑋) |
15 | | simpr 477 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) ∧ (𝑥‘0) = 𝑃) → (𝑥‘0) = 𝑃) |
16 | | simpll 790 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) ∧ (𝑥‘0) = 𝑃) → 𝑁 ∈
ℕ0) |
17 | | wwlksnextprop.y |
. . . . . . . 8
⊢ 𝑌 = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} |
18 | 2, 9, 17 | wwlksnextproplem3 26806 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑥‘0) = 𝑃 ∧ 𝑁 ∈ ℕ0) → (𝑥 substr 〈0, (𝑁 + 1)〉) ∈ 𝑌) |
19 | 14, 15, 16, 18 | syl3anc 1326 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) ∧ (𝑥‘0) = 𝑃) → (𝑥 substr 〈0, (𝑁 + 1)〉) ∈ 𝑌) |
20 | | eqeq2 2633 |
. . . . . . . 8
⊢ (𝑦 = (𝑥 substr 〈0, (𝑁 + 1)〉) → ((𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑦 ↔ (𝑥 substr 〈0, (𝑁 + 1)〉) = (𝑥 substr 〈0, (𝑁 + 1)〉))) |
21 | | fveq1 6190 |
. . . . . . . . 9
⊢ (𝑦 = (𝑥 substr 〈0, (𝑁 + 1)〉) → (𝑦‘0) = ((𝑥 substr 〈0, (𝑁 + 1)〉)‘0)) |
22 | 21 | eqeq1d 2624 |
. . . . . . . 8
⊢ (𝑦 = (𝑥 substr 〈0, (𝑁 + 1)〉) → ((𝑦‘0) = 𝑃 ↔ ((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = 𝑃)) |
23 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑦 = (𝑥 substr 〈0, (𝑁 + 1)〉) → ( lastS ‘𝑦) = ( lastS ‘(𝑥 substr 〈0, (𝑁 + 1)〉))) |
24 | 23 | preq1d 4274 |
. . . . . . . . 9
⊢ (𝑦 = (𝑥 substr 〈0, (𝑁 + 1)〉) → {( lastS ‘𝑦), ( lastS ‘𝑥)} = {( lastS ‘(𝑥 substr 〈0, (𝑁 + 1)〉)), ( lastS
‘𝑥)}) |
25 | 24 | eleq1d 2686 |
. . . . . . . 8
⊢ (𝑦 = (𝑥 substr 〈0, (𝑁 + 1)〉) → ({( lastS ‘𝑦), ( lastS ‘𝑥)} ∈ 𝐸 ↔ {( lastS ‘(𝑥 substr 〈0, (𝑁 + 1)〉)), ( lastS ‘𝑥)} ∈ 𝐸)) |
26 | 20, 22, 25 | 3anbi123d 1399 |
. . . . . . 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 482 |
. . . . . 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 3313 |
. . . . 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 1427 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) ∧ (𝑥‘0) = 𝑃) → ∃𝑦 ∈ 𝑌 ((𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑥)} ∈ 𝐸)) |
30 | 29 | ex 450 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) → ((𝑥‘0) = 𝑃 → ∃𝑦 ∈ 𝑌 ((𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑥)} ∈ 𝐸))) |
31 | 21 | eqcoms 2630 |
. . . . . . . . 9
⊢ ((𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑦 → (𝑦‘0) = ((𝑥 substr 〈0, (𝑁 + 1)〉)‘0)) |
32 | 31 | eqeq1d 2624 |
. . . . . . . 8
⊢ ((𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑦 → ((𝑦‘0) = 𝑃 ↔ ((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = 𝑃)) |
33 | 3 | eqcomd 2628 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) → (𝑥‘0) = ((𝑥 substr 〈0, (𝑁 + 1)〉)‘0)) |
34 | 33 | ancoms 469 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) → (𝑥‘0) = ((𝑥 substr 〈0, (𝑁 + 1)〉)‘0)) |
35 | 34 | adantr 481 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌) → (𝑥‘0) = ((𝑥 substr 〈0, (𝑁 + 1)〉)‘0)) |
36 | | eqeq2 2633 |
. . . . . . . . . 10
⊢ (𝑃 = ((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) → ((𝑥‘0) = 𝑃 ↔ (𝑥‘0) = ((𝑥 substr 〈0, (𝑁 + 1)〉)‘0))) |
37 | 36 | eqcoms 2630 |
. . . . . . . . 9
⊢ (((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = 𝑃 → ((𝑥‘0) = 𝑃 ↔ (𝑥‘0) = ((𝑥 substr 〈0, (𝑁 + 1)〉)‘0))) |
38 | 35, 37 | syl5ibr 236 |
. . . . . . . 8
⊢ (((𝑥 substr 〈0, (𝑁 + 1)〉)‘0) = 𝑃 → (((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌) → (𝑥‘0) = 𝑃)) |
39 | 32, 38 | syl6bi 243 |
. . . . . . 7
⊢ ((𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑦 → ((𝑦‘0) = 𝑃 → (((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌) → (𝑥‘0) = 𝑃))) |
40 | 39 | imp 445 |
. . . . . 6
⊢ (((𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃) → (((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌) → (𝑥‘0) = 𝑃)) |
41 | 40 | 3adant3 1081 |
. . . . 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 3031 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) → (∃𝑦 ∈ 𝑌 ((𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑥)} ∈ 𝐸) → (𝑥‘0) = 𝑃)) |
44 | 30, 43 | impbid 202 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) → ((𝑥‘0) = 𝑃 ↔ ∃𝑦 ∈ 𝑌 ((𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑥)} ∈ 𝐸))) |
45 | 44 | rabbidva 3188 |
1
⊢ (𝑁 ∈ ℕ0
→ {𝑥 ∈ 𝑋 ∣ (𝑥‘0) = 𝑃} = {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑌 ((𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑥)} ∈ 𝐸)}) |