Proof of Theorem clwwlknclwwlkdifs
Step | Hyp | Ref
| Expression |
1 | | clwwlknclwwlkdif.a |
. 2
⊢ 𝐴 = {𝑤 ∈ (𝑁 WWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋)} |
2 | | clwwlknclwwlkdif.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 | | neqne 2790 |
. . . . . . . . . . . . 13
⊢ (¬ (
lastS ‘𝑤) = 𝑋 → ( lastS ‘𝑤) ≠ 𝑋) |
9 | 8 | anim2i 591 |
. . . . . . . . . . . 12
⊢ (((𝑤‘0) = 𝑋 ∧ ¬ ( lastS ‘𝑤) = 𝑋) → ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋)) |
10 | 9 | ex 449 |
. . . . . . . . . . 11
⊢ ((𝑤‘0) = 𝑋 → (¬ ( lastS ‘𝑤) = 𝑋 → ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋))) |
11 | 7, 10 | sylbid 229 |
. . . . . . . . . 10
⊢ ((𝑤‘0) = 𝑋 → (¬ ( lastS ‘𝑤) = (𝑤‘0) → ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋))) |
12 | 11 | com12 32 |
. . . . . . . . 9
⊢ (¬ (
lastS ‘𝑤) = (𝑤‘0) → ((𝑤‘0) = 𝑋 → ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋))) |
13 | | pm2.21 119 |
. . . . . . . . 9
⊢ (¬
(𝑤‘0) = 𝑋 → ((𝑤‘0) = 𝑋 → ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋))) |
14 | 12, 13 | jaoi 393 |
. . . . . . . 8
⊢ ((¬ (
lastS ‘𝑤) = (𝑤‘0) ∨ ¬ (𝑤‘0) = 𝑋) → ((𝑤‘0) = 𝑋 → ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋))) |
15 | 5, 14 | sylbi 206 |
. . . . . . 7
⊢ (¬ ((
lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋) → ((𝑤‘0) = 𝑋 → ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋))) |
16 | 15 | impcom 445 |
. . . . . 6
⊢ (((𝑤‘0) = 𝑋 ∧ ¬ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋)) → ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋)) |
17 | | simpl 472 |
. . . . . . 7
⊢ (((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋) → (𝑤‘0) = 𝑋) |
18 | | neeq2 2845 |
. . . . . . . . . . 11
⊢ (𝑋 = (𝑤‘0) → (( lastS ‘𝑤) ≠ 𝑋 ↔ ( lastS ‘𝑤) ≠ (𝑤‘0))) |
19 | 18 | eqcoms 2618 |
. . . . . . . . . 10
⊢ ((𝑤‘0) = 𝑋 → (( lastS ‘𝑤) ≠ 𝑋 ↔ ( lastS ‘𝑤) ≠ (𝑤‘0))) |
20 | | neneq 2788 |
. . . . . . . . . 10
⊢ (( lastS
‘𝑤) ≠ (𝑤‘0) → ¬ ( lastS
‘𝑤) = (𝑤‘0)) |
21 | 19, 20 | syl6bi 242 |
. . . . . . . . 9
⊢ ((𝑤‘0) = 𝑋 → (( lastS ‘𝑤) ≠ 𝑋 → ¬ ( lastS ‘𝑤) = (𝑤‘0))) |
22 | 21 | imp 444 |
. . . . . . . 8
⊢ (((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋) → ¬ ( lastS ‘𝑤) = (𝑤‘0)) |
23 | 22 | intnanrd 954 |
. . . . . . 7
⊢ (((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋) → ¬ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋)) |
24 | 17, 23 | jca 553 |
. . . . . 6
⊢ (((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋) → ((𝑤‘0) = 𝑋 ∧ ¬ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋))) |
25 | 16, 24 | impbii 198 |
. . . . 5
⊢ (((𝑤‘0) = 𝑋 ∧ ¬ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋)) ↔ ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋)) |
26 | 25 | a1i 11 |
. . . 4
⊢ (𝑤 ∈ (𝑁 WWalkSN 𝐺) → (((𝑤‘0) = 𝑋 ∧ ¬ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋)) ↔ ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋))) |
27 | 26 | rabbiia 3161 |
. . 3
⊢ {𝑤 ∈ (𝑁 WWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ ¬ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋))} = {𝑤 ∈ (𝑁 WWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋)} |
28 | 3, 4, 27 | 3eqtrri 2637 |
. 2
⊢ {𝑤 ∈ (𝑁 WWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋)} = ({𝑤 ∈ (𝑁 WWalkSN 𝐺) ∣ (𝑤‘0) = 𝑋} ∖ 𝐵) |
29 | 1, 28 | eqtri 2632 |
1
⊢ 𝐴 = ({𝑤 ∈ (𝑁 WWalkSN 𝐺) ∣ (𝑤‘0) = 𝑋} ∖ 𝐵) |