Proof of Theorem wwlksnextprop
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqidd 2738 | . . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) ∧ (𝑥‘0) = 𝑃) → (𝑥 prefix (𝑁 + 1)) = (𝑥 prefix (𝑁 + 1))) | 
| 2 |  | wwlksnextprop.x | . . . . . . . . 9
⊢ 𝑋 = ((𝑁 + 1) WWalksN 𝐺) | 
| 3 | 2 | wwlksnextproplem1 29929 | . . . . . . . 8
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) → ((𝑥 prefix (𝑁 + 1))‘0) = (𝑥‘0)) | 
| 4 | 3 | ancoms 458 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) → ((𝑥 prefix (𝑁 + 1))‘0) = (𝑥‘0)) | 
| 5 | 4 | adantr 480 | . . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) ∧ (𝑥‘0) = 𝑃) → ((𝑥 prefix (𝑁 + 1))‘0) = (𝑥‘0)) | 
| 6 |  | eqeq2 2749 | . . . . . . 7
⊢ ((𝑥‘0) = 𝑃 → (((𝑥 prefix (𝑁 + 1))‘0) = (𝑥‘0) ↔ ((𝑥 prefix (𝑁 + 1))‘0) = 𝑃)) | 
| 7 | 6 | adantl 481 | . . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) ∧ (𝑥‘0) = 𝑃) → (((𝑥 prefix (𝑁 + 1))‘0) = (𝑥‘0) ↔ ((𝑥 prefix (𝑁 + 1))‘0) = 𝑃)) | 
| 8 | 5, 7 | mpbid 232 | . . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) ∧ (𝑥‘0) = 𝑃) → ((𝑥 prefix (𝑁 + 1))‘0) = 𝑃) | 
| 9 |  | wwlksnextprop.e | . . . . . . . 8
⊢ 𝐸 = (Edg‘𝐺) | 
| 10 | 2, 9 | wwlksnextproplem2 29930 | . . . . . . 7
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) →
{(lastS‘(𝑥 prefix
(𝑁 + 1))),
(lastS‘𝑥)} ∈
𝐸) | 
| 11 | 10 | ancoms 458 | . . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) → {(lastS‘(𝑥 prefix (𝑁 + 1))), (lastS‘𝑥)} ∈ 𝐸) | 
| 12 | 11 | adantr 480 | . . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) ∧ (𝑥‘0) = 𝑃) → {(lastS‘(𝑥 prefix (𝑁 + 1))), (lastS‘𝑥)} ∈ 𝐸) | 
| 13 |  | simpr 484 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) | 
| 14 | 13 | adantr 480 | . . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) ∧ (𝑥‘0) = 𝑃) → 𝑥 ∈ 𝑋) | 
| 15 |  | simpr 484 | . . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) ∧ (𝑥‘0) = 𝑃) → (𝑥‘0) = 𝑃) | 
| 16 |  | simpll 767 | . . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) ∧ (𝑥‘0) = 𝑃) → 𝑁 ∈
ℕ0) | 
| 17 |  | wwlksnextprop.y | . . . . . . . 8
⊢ 𝑌 = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} | 
| 18 | 2, 9, 17 | wwlksnextproplem3 29931 | . . . . . . 7
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑥‘0) = 𝑃 ∧ 𝑁 ∈ ℕ0) → (𝑥 prefix (𝑁 + 1)) ∈ 𝑌) | 
| 19 | 14, 15, 16, 18 | syl3anc 1373 | . . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) ∧ (𝑥‘0) = 𝑃) → (𝑥 prefix (𝑁 + 1)) ∈ 𝑌) | 
| 20 |  | eqeq2 2749 | . . . . . . . 8
⊢ (𝑦 = (𝑥 prefix (𝑁 + 1)) → ((𝑥 prefix (𝑁 + 1)) = 𝑦 ↔ (𝑥 prefix (𝑁 + 1)) = (𝑥 prefix (𝑁 + 1)))) | 
| 21 |  | fveq1 6905 | . . . . . . . . 9
⊢ (𝑦 = (𝑥 prefix (𝑁 + 1)) → (𝑦‘0) = ((𝑥 prefix (𝑁 + 1))‘0)) | 
| 22 | 21 | eqeq1d 2739 | . . . . . . . 8
⊢ (𝑦 = (𝑥 prefix (𝑁 + 1)) → ((𝑦‘0) = 𝑃 ↔ ((𝑥 prefix (𝑁 + 1))‘0) = 𝑃)) | 
| 23 |  | fveq2 6906 | . . . . . . . . . 10
⊢ (𝑦 = (𝑥 prefix (𝑁 + 1)) → (lastS‘𝑦) = (lastS‘(𝑥 prefix (𝑁 + 1)))) | 
| 24 | 23 | preq1d 4739 | . . . . . . . . 9
⊢ (𝑦 = (𝑥 prefix (𝑁 + 1)) → {(lastS‘𝑦), (lastS‘𝑥)} = {(lastS‘(𝑥 prefix (𝑁 + 1))), (lastS‘𝑥)}) | 
| 25 | 24 | eleq1d 2826 | . . . . . . . 8
⊢ (𝑦 = (𝑥 prefix (𝑁 + 1)) → ({(lastS‘𝑦), (lastS‘𝑥)} ∈ 𝐸 ↔ {(lastS‘(𝑥 prefix (𝑁 + 1))), (lastS‘𝑥)} ∈ 𝐸)) | 
| 26 | 20, 22, 25 | 3anbi123d 1438 | . . . . . . 7
⊢ (𝑦 = (𝑥 prefix (𝑁 + 1)) → (((𝑥 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑥)} ∈ 𝐸) ↔ ((𝑥 prefix (𝑁 + 1)) = (𝑥 prefix (𝑁 + 1)) ∧ ((𝑥 prefix (𝑁 + 1))‘0) = 𝑃 ∧ {(lastS‘(𝑥 prefix (𝑁 + 1))), (lastS‘𝑥)} ∈ 𝐸))) | 
| 27 | 26 | adantl 481 | . . . . . 6
⊢ ((((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) ∧ (𝑥‘0) = 𝑃) ∧ 𝑦 = (𝑥 prefix (𝑁 + 1))) → (((𝑥 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑥)} ∈ 𝐸) ↔ ((𝑥 prefix (𝑁 + 1)) = (𝑥 prefix (𝑁 + 1)) ∧ ((𝑥 prefix (𝑁 + 1))‘0) = 𝑃 ∧ {(lastS‘(𝑥 prefix (𝑁 + 1))), (lastS‘𝑥)} ∈ 𝐸))) | 
| 28 | 19, 27 | rspcedv 3615 | . . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) ∧ (𝑥‘0) = 𝑃) → (((𝑥 prefix (𝑁 + 1)) = (𝑥 prefix (𝑁 + 1)) ∧ ((𝑥 prefix (𝑁 + 1))‘0) = 𝑃 ∧ {(lastS‘(𝑥 prefix (𝑁 + 1))), (lastS‘𝑥)} ∈ 𝐸) → ∃𝑦 ∈ 𝑌 ((𝑥 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑥)} ∈ 𝐸))) | 
| 29 | 1, 8, 12, 28 | mp3and 1466 | . . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) ∧ (𝑥‘0) = 𝑃) → ∃𝑦 ∈ 𝑌 ((𝑥 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑥)} ∈ 𝐸)) | 
| 30 | 29 | ex 412 | . . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) → ((𝑥‘0) = 𝑃 → ∃𝑦 ∈ 𝑌 ((𝑥 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑥)} ∈ 𝐸))) | 
| 31 | 21 | eqcoms 2745 | . . . . . . . . 9
⊢ ((𝑥 prefix (𝑁 + 1)) = 𝑦 → (𝑦‘0) = ((𝑥 prefix (𝑁 + 1))‘0)) | 
| 32 | 31 | eqeq1d 2739 | . . . . . . . 8
⊢ ((𝑥 prefix (𝑁 + 1)) = 𝑦 → ((𝑦‘0) = 𝑃 ↔ ((𝑥 prefix (𝑁 + 1))‘0) = 𝑃)) | 
| 33 | 3 | eqcomd 2743 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) → (𝑥‘0) = ((𝑥 prefix (𝑁 + 1))‘0)) | 
| 34 | 33 | ancoms 458 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) → (𝑥‘0) = ((𝑥 prefix (𝑁 + 1))‘0)) | 
| 35 | 34 | adantr 480 | . . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌) → (𝑥‘0) = ((𝑥 prefix (𝑁 + 1))‘0)) | 
| 36 |  | eqeq2 2749 | . . . . . . . . . 10
⊢ (𝑃 = ((𝑥 prefix (𝑁 + 1))‘0) → ((𝑥‘0) = 𝑃 ↔ (𝑥‘0) = ((𝑥 prefix (𝑁 + 1))‘0))) | 
| 37 | 36 | eqcoms 2745 | . . . . . . . . 9
⊢ (((𝑥 prefix (𝑁 + 1))‘0) = 𝑃 → ((𝑥‘0) = 𝑃 ↔ (𝑥‘0) = ((𝑥 prefix (𝑁 + 1))‘0))) | 
| 38 | 35, 37 | imbitrrid 246 | . . . . . . . 8
⊢ (((𝑥 prefix (𝑁 + 1))‘0) = 𝑃 → (((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌) → (𝑥‘0) = 𝑃)) | 
| 39 | 32, 38 | biimtrdi 253 | . . . . . . 7
⊢ ((𝑥 prefix (𝑁 + 1)) = 𝑦 → ((𝑦‘0) = 𝑃 → (((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌) → (𝑥‘0) = 𝑃))) | 
| 40 | 39 | imp 406 | . . . . . 6
⊢ (((𝑥 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃) → (((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌) → (𝑥‘0) = 𝑃)) | 
| 41 | 40 | 3adant3 1133 | . . . . 5
⊢ (((𝑥 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑥)} ∈ 𝐸) → (((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌) → (𝑥‘0) = 𝑃)) | 
| 42 | 41 | com12 32 | . . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌) → (((𝑥 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑥)} ∈ 𝐸) → (𝑥‘0) = 𝑃)) | 
| 43 | 42 | rexlimdva 3155 | . . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) → (∃𝑦 ∈ 𝑌 ((𝑥 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑥)} ∈ 𝐸) → (𝑥‘0) = 𝑃)) | 
| 44 | 30, 43 | impbid 212 | . 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ 𝑋) → ((𝑥‘0) = 𝑃 ↔ ∃𝑦 ∈ 𝑌 ((𝑥 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑥)} ∈ 𝐸))) | 
| 45 | 44 | rabbidva 3443 | 1
⊢ (𝑁 ∈ ℕ0
→ {𝑥 ∈ 𝑋 ∣ (𝑥‘0) = 𝑃} = {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑌 ((𝑥 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑥)} ∈ 𝐸)}) |