Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  clwwlknclwwlkdifsOLD Structured version   Visualization version   GIF version

Theorem clwwlknclwwlkdifsOLD 27272
 Description: Obsolete version of clwwlknclwwlkdif 27270 as of 8-Mar-2022. (Contributed by Alexander van der Vekens, 30-Sep-2018.) (Revised by AV, 7-May-2021.) (New usage is discouraged.) (Proof modification is discouraged.)
Hypotheses
Ref Expression
clwwlknclwwlkdifsOLD.a 𝐴 = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋)}
clwwlknclwwlkdifsOLD.b 𝐵 = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((lastS‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋)}
Assertion
Ref Expression
clwwlknclwwlkdifsOLD 𝐴 = ({𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑋} ∖ 𝐵)

Proof of Theorem clwwlknclwwlkdifsOLD
StepHypRef Expression
1 clwwlknclwwlkdifsOLD.a . 2 𝐴 = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋)}
2 clwwlknclwwlkdifsOLD.b . . . 4 𝐵 = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((lastS‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋)}
32difeq2i 3923 . . 3 ({𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑋} ∖ 𝐵) = ({𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑋} ∖ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((lastS‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋)})
4 difrab 4101 . . 3 ({𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑋} ∖ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((lastS‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋)}) = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ ¬ ((lastS‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋))}
5 ianor 1005 . . . . . . . 8 (¬ ((lastS‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋) ↔ (¬ (lastS‘𝑤) = (𝑤‘0) ∨ ¬ (𝑤‘0) = 𝑋))
6 eqeq2 2810 . . . . . . . . . . . 12 ((𝑤‘0) = 𝑋 → ((lastS‘𝑤) = (𝑤‘0) ↔ (lastS‘𝑤) = 𝑋))
76notbid 310 . . . . . . . . . . 11 ((𝑤‘0) = 𝑋 → (¬ (lastS‘𝑤) = (𝑤‘0) ↔ ¬ (lastS‘𝑤) = 𝑋))
8 neqne 2979 . . . . . . . . . . . . 13 (¬ (lastS‘𝑤) = 𝑋 → (lastS‘𝑤) ≠ 𝑋)
98anim2i 611 . . . . . . . . . . . 12 (((𝑤‘0) = 𝑋 ∧ ¬ (lastS‘𝑤) = 𝑋) → ((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋))
109ex 402 . . . . . . . . . . 11 ((𝑤‘0) = 𝑋 → (¬ (lastS‘𝑤) = 𝑋 → ((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋)))
117, 10sylbid 232 . . . . . . . . . 10 ((𝑤‘0) = 𝑋 → (¬ (lastS‘𝑤) = (𝑤‘0) → ((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋)))
1211com12 32 . . . . . . . . 9 (¬ (lastS‘𝑤) = (𝑤‘0) → ((𝑤‘0) = 𝑋 → ((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋)))
13 pm2.21 121 . . . . . . . . 9 (¬ (𝑤‘0) = 𝑋 → ((𝑤‘0) = 𝑋 → ((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋)))
1412, 13jaoi 884 . . . . . . . 8 ((¬ (lastS‘𝑤) = (𝑤‘0) ∨ ¬ (𝑤‘0) = 𝑋) → ((𝑤‘0) = 𝑋 → ((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋)))
155, 14sylbi 209 . . . . . . 7 (¬ ((lastS‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋) → ((𝑤‘0) = 𝑋 → ((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋)))
1615impcom 397 . . . . . 6 (((𝑤‘0) = 𝑋 ∧ ¬ ((lastS‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋)) → ((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋))
17 simpl 475 . . . . . . 7 (((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋) → (𝑤‘0) = 𝑋)
18 neeq2 3034 . . . . . . . . . . 11 (𝑋 = (𝑤‘0) → ((lastS‘𝑤) ≠ 𝑋 ↔ (lastS‘𝑤) ≠ (𝑤‘0)))
1918eqcoms 2807 . . . . . . . . . 10 ((𝑤‘0) = 𝑋 → ((lastS‘𝑤) ≠ 𝑋 ↔ (lastS‘𝑤) ≠ (𝑤‘0)))
20 neneq 2977 . . . . . . . . . 10 ((lastS‘𝑤) ≠ (𝑤‘0) → ¬ (lastS‘𝑤) = (𝑤‘0))
2119, 20syl6bi 245 . . . . . . . . 9 ((𝑤‘0) = 𝑋 → ((lastS‘𝑤) ≠ 𝑋 → ¬ (lastS‘𝑤) = (𝑤‘0)))
2221imp 396 . . . . . . . 8 (((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋) → ¬ (lastS‘𝑤) = (𝑤‘0))
2322intnanrd 484 . . . . . . 7 (((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋) → ¬ ((lastS‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋))
2417, 23jca 508 . . . . . 6 (((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋) → ((𝑤‘0) = 𝑋 ∧ ¬ ((lastS‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋)))
2516, 24impbii 201 . . . . 5 (((𝑤‘0) = 𝑋 ∧ ¬ ((lastS‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋)) ↔ ((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋))
2625a1i 11 . . . 4 (𝑤 ∈ (𝑁 WWalksN 𝐺) → (((𝑤‘0) = 𝑋 ∧ ¬ ((lastS‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋)) ↔ ((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋)))
2726rabbiia 3368 . . 3 {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ ¬ ((lastS‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋))} = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋)}
283, 4, 273eqtrri 2826 . 2 {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋)} = ({𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑋} ∖ 𝐵)
291, 28eqtri 2821 1 𝐴 = ({𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑋} ∖ 𝐵)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∧ wa 385   ∨ wo 874   = wceq 1653   ∈ wcel 2157   ≠ wne 2971  {crab 3093   ∖ cdif 3766  ‘cfv 6101  (class class class)co 6878  0cc0 10224  lastSclsw 13582   WWalksN cwwlksn 27077 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2777 This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-ne 2972  df-ral 3094  df-rab 3098  df-v 3387  df-dif 3772 This theorem is referenced by:  clwwlknclwwlkdifnumOLD  27273
 Copyright terms: Public domain W3C validator