Proof of Theorem clwlknclwlkdifs
Step | Hyp | Ref
| Expression |
1 | | clwlknclwlkdif.a |
. 2
⊢ 𝐴 = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋)} |
2 | | clwlknclwlkdif.b |
. . . 4
⊢ 𝐵 = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋)} |
3 | 2 | difeq2i 3687 |
. . 3
⊢ ({𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑋} ∖ 𝐵) = ({𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑋} ∖ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋)}) |
4 | | difrab 3860 |
. . 3
⊢ ({𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑋} ∖ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋)}) = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ ¬ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋))} |
5 | | ianor 508 |
. . . . . . . 8
⊢ (¬ ((
lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋) ↔ (¬ ( lastS ‘𝑤) = (𝑤‘0) ∨ ¬ (𝑤‘0) = 𝑋)) |
6 | | eqeq2 2621 |
. . . . . . . . . . . 12
⊢ ((𝑤‘0) = 𝑋 → (( lastS ‘𝑤) = (𝑤‘0) ↔ ( lastS ‘𝑤) = 𝑋)) |
7 | 6 | notbid 307 |
. . . . . . . . . . 11
⊢ ((𝑤‘0) = 𝑋 → (¬ ( lastS ‘𝑤) = (𝑤‘0) ↔ ¬ ( lastS ‘𝑤) = 𝑋)) |
8 | | df-ne 2782 |
. . . . . . . . . . . . . 14
⊢ (( lastS
‘𝑤) ≠ 𝑋 ↔ ¬ ( lastS
‘𝑤) = 𝑋) |
9 | 8 | biimpri 217 |
. . . . . . . . . . . . 13
⊢ (¬ (
lastS ‘𝑤) = 𝑋 → ( lastS ‘𝑤) ≠ 𝑋) |
10 | 9 | anim2i 591 |
. . . . . . . . . . . 12
⊢ (((𝑤‘0) = 𝑋 ∧ ¬ ( lastS ‘𝑤) = 𝑋) → ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋)) |
11 | 10 | ex 449 |
. . . . . . . . . . 11
⊢ ((𝑤‘0) = 𝑋 → (¬ ( lastS ‘𝑤) = 𝑋 → ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋))) |
12 | 7, 11 | sylbid 229 |
. . . . . . . . . 10
⊢ ((𝑤‘0) = 𝑋 → (¬ ( lastS ‘𝑤) = (𝑤‘0) → ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋))) |
13 | 12 | com12 32 |
. . . . . . . . 9
⊢ (¬ (
lastS ‘𝑤) = (𝑤‘0) → ((𝑤‘0) = 𝑋 → ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋))) |
14 | | pm2.21 119 |
. . . . . . . . 9
⊢ (¬
(𝑤‘0) = 𝑋 → ((𝑤‘0) = 𝑋 → ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋))) |
15 | 13, 14 | jaoi 393 |
. . . . . . . 8
⊢ ((¬ (
lastS ‘𝑤) = (𝑤‘0) ∨ ¬ (𝑤‘0) = 𝑋) → ((𝑤‘0) = 𝑋 → ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋))) |
16 | 5, 15 | sylbi 206 |
. . . . . . 7
⊢ (¬ ((
lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋) → ((𝑤‘0) = 𝑋 → ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋))) |
17 | 16 | impcom 445 |
. . . . . 6
⊢ (((𝑤‘0) = 𝑋 ∧ ¬ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋)) → ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋)) |
18 | | simpl 472 |
. . . . . . 7
⊢ (((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋) → (𝑤‘0) = 𝑋) |
19 | | neeq2 2845 |
. . . . . . . . . . 11
⊢ (𝑋 = (𝑤‘0) → (( lastS ‘𝑤) ≠ 𝑋 ↔ ( lastS ‘𝑤) ≠ (𝑤‘0))) |
20 | 19 | eqcoms 2618 |
. . . . . . . . . 10
⊢ ((𝑤‘0) = 𝑋 → (( lastS ‘𝑤) ≠ 𝑋 ↔ ( lastS ‘𝑤) ≠ (𝑤‘0))) |
21 | | df-ne 2782 |
. . . . . . . . . . 11
⊢ (( lastS
‘𝑤) ≠ (𝑤‘0) ↔ ¬ ( lastS
‘𝑤) = (𝑤‘0)) |
22 | 21 | biimpi 205 |
. . . . . . . . . 10
⊢ (( lastS
‘𝑤) ≠ (𝑤‘0) → ¬ ( lastS
‘𝑤) = (𝑤‘0)) |
23 | 20, 22 | syl6bi 242 |
. . . . . . . . 9
⊢ ((𝑤‘0) = 𝑋 → (( lastS ‘𝑤) ≠ 𝑋 → ¬ ( lastS ‘𝑤) = (𝑤‘0))) |
24 | 23 | imp 444 |
. . . . . . . 8
⊢ (((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋) → ¬ ( lastS ‘𝑤) = (𝑤‘0)) |
25 | 24 | intnanrd 954 |
. . . . . . 7
⊢ (((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋) → ¬ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋)) |
26 | 18, 25 | jca 553 |
. . . . . 6
⊢ (((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋) → ((𝑤‘0) = 𝑋 ∧ ¬ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋))) |
27 | 17, 26 | impbii 198 |
. . . . 5
⊢ (((𝑤‘0) = 𝑋 ∧ ¬ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋)) ↔ ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋)) |
28 | 27 | a1i 11 |
. . . 4
⊢ (𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → (((𝑤‘0) = 𝑋 ∧ ¬ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋)) ↔ ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋))) |
29 | 28 | rabbiia 3161 |
. . 3
⊢ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ ¬ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋))} = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋)} |
30 | 3, 4, 29 | 3eqtrri 2637 |
. 2
⊢ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋)} = ({𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑋} ∖ 𝐵) |
31 | 1, 30 | eqtri 2632 |
1
⊢ 𝐴 = ({𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑋} ∖ 𝐵) |