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

Step	Hyp	Ref	Expression
1		clwwlknclwwlkdifsOLD.a	. 2 ⊢ 𝐴 = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋)}
2		clwwlknclwwlkdifsOLD.b	. . . 4 ⊢ 𝐵 = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((lastS‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋)}
3	2	difeq2i 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‘𝑤) = 𝑋))
7	6	notbid 310	. . . . . . . . . . 11 ⊢ ((𝑤‘0) = 𝑋 → (¬ (lastS‘𝑤) = (𝑤‘0) ↔ ¬ (lastS‘𝑤) = 𝑋))
8		neqne 2979	. . . . . . . . . . . . 13 ⊢ (¬ (lastS‘𝑤) = 𝑋 → (lastS‘𝑤) ≠ 𝑋)
9	8	anim2i 611	. . . . . . . . . . . 12 ⊢ (((𝑤‘0) = 𝑋 ∧ ¬ (lastS‘𝑤) = 𝑋) → ((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋))
10	9	ex 402	. . . . . . . . . . 11 ⊢ ((𝑤‘0) = 𝑋 → (¬ (lastS‘𝑤) = 𝑋 → ((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋)))
11	7, 10	sylbid 232	. . . . . . . . . 10 ⊢ ((𝑤‘0) = 𝑋 → (¬ (lastS‘𝑤) = (𝑤‘0) → ((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋)))
12	11	com12 32	. . . . . . . . 9 ⊢ (¬ (lastS‘𝑤) = (𝑤‘0) → ((𝑤‘0) = 𝑋 → ((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋)))
13		pm2.21 121	. . . . . . . . 9 ⊢ (¬ (𝑤‘0) = 𝑋 → ((𝑤‘0) = 𝑋 → ((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋)))
14	12, 13	jaoi 884	. . . . . . . 8 ⊢ ((¬ (lastS‘𝑤) = (𝑤‘0) ∨ ¬ (𝑤‘0) = 𝑋) → ((𝑤‘0) = 𝑋 → ((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋)))
15	5, 14	sylbi 209	. . . . . . 7 ⊢ (¬ ((lastS‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋) → ((𝑤‘0) = 𝑋 → ((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋)))
16	15	impcom 397	. . . . . 6 ⊢ (((𝑤‘0) = 𝑋 ∧ ¬ ((lastS‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋)) → ((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋))
17		simpl 475	. . . . . . 7 ⊢ (((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋) → (𝑤‘0) = 𝑋)
18		neeq2 3034	. . . . . . . . . . 11 ⊢ (𝑋 = (𝑤‘0) → ((lastS‘𝑤) ≠ 𝑋 ↔ (lastS‘𝑤) ≠ (𝑤‘0)))
19	18	eqcoms 2807	. . . . . . . . . 10 ⊢ ((𝑤‘0) = 𝑋 → ((lastS‘𝑤) ≠ 𝑋 ↔ (lastS‘𝑤) ≠ (𝑤‘0)))
20		neneq 2977	. . . . . . . . . 10 ⊢ ((lastS‘𝑤) ≠ (𝑤‘0) → ¬ (lastS‘𝑤) = (𝑤‘0))
21	19, 20	syl6bi 245	. . . . . . . . 9 ⊢ ((𝑤‘0) = 𝑋 → ((lastS‘𝑤) ≠ 𝑋 → ¬ (lastS‘𝑤) = (𝑤‘0)))
22	21	imp 396	. . . . . . . 8 ⊢ (((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋) → ¬ (lastS‘𝑤) = (𝑤‘0))
23	22	intnanrd 484	. . . . . . 7 ⊢ (((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋) → ¬ ((lastS‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋))
24	17, 23	jca 508	. . . . . 6 ⊢ (((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋) → ((𝑤‘0) = 𝑋 ∧ ¬ ((lastS‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋)))
25	16, 24	impbii 201	. . . . 5 ⊢ (((𝑤‘0) = 𝑋 ∧ ¬ ((lastS‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋)) ↔ ((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋))
26	25	a1i 11	. . . 4 ⊢ (𝑤 ∈ (𝑁 WWalksN 𝐺) → (((𝑤‘0) = 𝑋 ∧ ¬ ((lastS‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋)) ↔ ((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋)))
27	26	rabbiia 3368	. . 3 ⊢ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ ¬ ((lastS‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋))} = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋)}
28	3, 4, 27	3eqtrri 2826	. 2 ⊢ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋)} = ({𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑋} ∖ 𝐵)
29	1, 28	eqtri 2821	1 ⊢ 𝐴 = ({𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑋} ∖ 𝐵)

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