Theorem numclwwlk3lemOLD 27580

Description: Obsolete version of numclwwlk3lem2 27583 as of 1-May-2022. (Contributed by Alexander van der Vekens, 6-Oct-2018.) (Revised by AV, 1-Jun-2021.) (Revised by AV, 6-Mar-2022.) (Proof shortened by AV, 28-Mar-2022.) (New usage is discouraged.) (Proof modification is discouraged.)

Hypotheses

Ref	Expression
numclwwlkOLD.v	⊢ 𝑉 = (Vtx‘𝐺)
numclwwlkOLD.q	⊢ 𝑄 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑣 ∧ (lastS‘𝑤) ≠ 𝑣)})
numclwwlkOLD.h	⊢ 𝐻 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑣 ∧ (𝑤‘(𝑛 − 2)) ≠ (𝑤‘0))})
numclwwlkOLD.c	⊢ 𝐶 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2) ↦ {𝑤 ∈ (𝑛 ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑣 ∧ (𝑤‘(𝑛 − 2)) = (𝑤‘0))})

Assertion

Ref	Expression
numclwwlk3lemOLD	⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2)) → (♯‘(𝑋(ClWWalksNOn‘𝐺)𝑁)) = ((♯‘(𝑋𝐻𝑁)) + (♯‘(𝑋𝐶𝑁))))

Distinct variable groups:   𝑛,𝐺,𝑣,𝑤   𝑛,𝑁,𝑣,𝑤   𝑛,𝑉,𝑣   𝑛,𝑋,𝑣,𝑤   𝑤,𝑉

Allowed substitution hints:   𝐶(𝑤,𝑣,𝑛)   𝑄(𝑤,𝑣,𝑛)   𝐻(𝑤,𝑣,𝑛)

Proof of Theorem numclwwlk3lemOLD

Step	Hyp	Ref	Expression
1		clwwlknon 27262	. . . . 5 ⊢ (𝑋(ClWWalksNOn‘𝐺)𝑁) = {𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑋}
2	1	a1i 11	. . . 4 ⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2)) → (𝑋(ClWWalksNOn‘𝐺)𝑁) = {𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑋})
3	2	fveq2d 6336	. . 3 ⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2)) → (♯‘(𝑋(ClWWalksNOn‘𝐺)𝑁)) = (♯‘{𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑋}))
4		pm4.42 1041	. . . . . . . 8 ⊢ ((𝑤‘0) = 𝑋 ↔ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ∨ ((𝑤‘0) = 𝑋 ∧ ¬ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))))
5		nne 2947	. . . . . . . . . 10 ⊢ (¬ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0) ↔ (𝑤‘(𝑁 − 2)) = (𝑤‘0))
6	5	anbi2i 601	. . . . . . . . 9 ⊢ (((𝑤‘0) = 𝑋 ∧ ¬ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ↔ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)))
7	6	orbi2i 886	. . . . . . . 8 ⊢ ((((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ∨ ((𝑤‘0) = 𝑋 ∧ ¬ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))) ↔ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ∨ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))))
8	4, 7	bitri 264	. . . . . . 7 ⊢ ((𝑤‘0) = 𝑋 ↔ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ∨ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))))
9	8	a1i 11	. . . . . 6 ⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2)) → ((𝑤‘0) = 𝑋 ↔ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ∨ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)))))
10	9	rabbidv 3339	. . . . 5 ⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2)) → {𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑋} = {𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ∨ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)))})
11		unrab 4046	. . . . 5 ⊢ ({𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))} ∪ {𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))}) = {𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ∨ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)))}
12	10, 11	syl6eqr 2823	. . . 4 ⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2)) → {𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑋} = ({𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))} ∪ {𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))}))
13	12	fveq2d 6336	. . 3 ⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2)) → (♯‘{𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑋}) = (♯‘({𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))} ∪ {𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))})))
14		numclwwlkOLD.v	. . . . . . 7 ⊢ 𝑉 = (Vtx‘𝐺)
15	14	fusgrvtxfi 26434	. . . . . . . 8 ⊢ (𝐺 ∈ FinUSGraph → 𝑉 ∈ Fin)
16	15	ad2antrr 697	. . . . . . 7 ⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2)) → 𝑉 ∈ Fin)
17	14, 16	syl5eqelr 2855	. . . . . 6 ⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2)) → (Vtx‘𝐺) ∈ Fin)
18		clwwlknfi 27201	. . . . . 6 ⊢ ((Vtx‘𝐺) ∈ Fin → (𝑁 ClWWalksN 𝐺) ∈ Fin)
19	17, 18	syl 17	. . . . 5 ⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2)) → (𝑁 ClWWalksN 𝐺) ∈ Fin)
20		rabfi 8341	. . . . 5 ⊢ ((𝑁 ClWWalksN 𝐺) ∈ Fin → {𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))} ∈ Fin)
21	19, 20	syl 17	. . . 4 ⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2)) → {𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))} ∈ Fin)
22		rabfi 8341	. . . . 5 ⊢ ((𝑁 ClWWalksN 𝐺) ∈ Fin → {𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))} ∈ Fin)
23	19, 22	syl 17	. . . 4 ⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2)) → {𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))} ∈ Fin)
24		inrab 4047	. . . . 5 ⊢ ({𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))} ∩ {𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))}) = {𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)))}
25		neneq 2949	. . . . . . . . . . . 12 ⊢ ((𝑤‘(𝑁 − 2)) ≠ (𝑤‘0) → ¬ (𝑤‘(𝑁 − 2)) = (𝑤‘0))
26	25	adantl 467	. . . . . . . . . . 11 ⊢ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) → ¬ (𝑤‘(𝑁 − 2)) = (𝑤‘0))
27	26	intnand 999	. . . . . . . . . 10 ⊢ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) → ¬ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)))
28	27	imori 833	. . . . . . . . 9 ⊢ (¬ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ∨ ¬ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)))
29		ianor 940	. . . . . . . . 9 ⊢ (¬ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) ↔ (¬ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ∨ ¬ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))))
30	28, 29	mpbir 221	. . . . . . . 8 ⊢ ¬ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)))
31	30	a1i 11	. . . . . . 7 ⊢ ((((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2)) ∧ 𝑤 ∈ (𝑁 ClWWalksN 𝐺)) → ¬ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))))
32	31	ralrimiva 3115	. . . . . 6 ⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2)) → ∀𝑤 ∈ (𝑁 ClWWalksN 𝐺) ¬ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))))
33		rabeq0 4103	. . . . . 6 ⊢ ({𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)))} = ∅ ↔ ∀𝑤 ∈ (𝑁 ClWWalksN 𝐺) ¬ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))))
34	32, 33	sylibr 224	. . . . 5 ⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2)) → {𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)))} = ∅)
35	24, 34	syl5eq 2817	. . . 4 ⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2)) → ({𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))} ∩ {𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))}) = ∅)
36		hashun 13373	. . . 4 ⊢ (({𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))} ∈ Fin ∧ {𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))} ∈ Fin ∧ ({𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))} ∩ {𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))}) = ∅) → (♯‘({𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))} ∪ {𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))})) = ((♯‘{𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))}) + (♯‘{𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))})))
37	21, 23, 35, 36	syl3anc 1476	. . 3 ⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2)) → (♯‘({𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))} ∪ {𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))})) = ((♯‘{𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))}) + (♯‘{𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))})))
38	3, 13, 37	3eqtrd 2809	. 2 ⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2)) → (♯‘(𝑋(ClWWalksNOn‘𝐺)𝑁)) = ((♯‘{𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))}) + (♯‘{𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))})))
39		simpr 471	. . . . 5 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ 𝑉)
40		eluz2nn 11928	. . . . 5 ⊢ (𝑁 ∈ (ℤ≥‘2) → 𝑁 ∈ ℕ)
41		numclwwlkOLD.q	. . . . . 6 ⊢ 𝑄 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑣 ∧ (lastS‘𝑤) ≠ 𝑣)})
42		numclwwlkOLD.h	. . . . . 6 ⊢ 𝐻 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑣 ∧ (𝑤‘(𝑛 − 2)) ≠ (𝑤‘0))})
43	14, 41, 42	numclwwlkovhOLD 27573	. . . . 5 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑋𝐻𝑁) = {𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))})
44	39, 40, 43	syl2an 575	. . . 4 ⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2)) → (𝑋𝐻𝑁) = {𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))})
45	44	fveq2d 6336	. . 3 ⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2)) → (♯‘(𝑋𝐻𝑁)) = (♯‘{𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))}))
46		numclwwlkOLD.c	. . . . . 6 ⊢ 𝐶 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2) ↦ {𝑤 ∈ (𝑛 ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑣 ∧ (𝑤‘(𝑛 − 2)) = (𝑤‘0))})
47	46	numclwwlkovgOLD 27535	. . . . 5 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2)) → (𝑋𝐶𝑁) = {𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))})
48	47	adantll 685	. . . 4 ⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2)) → (𝑋𝐶𝑁) = {𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))})
49	48	fveq2d 6336	. . 3 ⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2)) → (♯‘(𝑋𝐶𝑁)) = (♯‘{𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))}))
50	45, 49	oveq12d 6811	. 2 ⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2)) → ((♯‘(𝑋𝐻𝑁)) + (♯‘(𝑋𝐶𝑁))) = ((♯‘{𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))}) + (♯‘{𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))})))
51	38, 50	eqtr4d 2808	1 ⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2)) → (♯‘(𝑋(ClWWalksNOn‘𝐺)𝑁)) = ((♯‘(𝑋𝐻𝑁)) + (♯‘(𝑋𝐶𝑁))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 382   ∨ wo 826   = wceq 1631   ∈ wcel 2145   ≠ wne 2943  ∀wral 3061  {crab 3065   ∪ cun 3721   ∩ cin 3722  ∅c0 4063  ‘cfv 6031  (class class class)co 6793   ↦ cmpt2 6795  Fincfn 8109  0cc0 10138   + caddc 10141   − cmin 10468  ℕcn 11222  2c2 11272  ℤ_≥cuz 11888  ♯chash 13321  lastSclsw 13488  Vtxcvtx 26095  FinUSGraphcfusgr 26431   WWalksN cwwlksn 26954   ClWWalksN cclwwlkn 27174  ClWWalksNOncclwwlknon 27259

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-cnex 10194  ax-resscn 10195  ax-1cn 10196  ax-icn 10197  ax-addcl 10198  ax-addrcl 10199  ax-mulcl 10200  ax-mulrcl 10201  ax-mulcom 10202  ax-addass 10203  ax-mulass 10204  ax-distr 10205  ax-i2m1 10206  ax-1ne0 10207  ax-1rid 10208  ax-rnegex 10209  ax-rrecex 10210  ax-cnre 10211  ax-pre-lttri 10212  ax-pre-lttrn 10213  ax-pre-ltadd 10214  ax-pre-mulgt0 10215

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-riota 6754  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-om 7213  df-1st 7315  df-2nd 7316  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-1o 7713  df-2o 7714  df-oadd 7717  df-er 7896  df-map 8011  df-pm 8012  df-en 8110  df-dom 8111  df-sdom 8112  df-fin 8113  df-card 8965  df-cda 9192  df-pnf 10278  df-mnf 10279  df-xr 10280  df-ltxr 10281  df-le 10282  df-sub 10470  df-neg 10471  df-nn 11223  df-2 11281  df-n0 11495  df-xnn0 11566  df-z 11580  df-uz 11889  df-fz 12534  df-fzo 12674  df-seq 13009  df-exp 13068  df-hash 13322  df-word 13495  df-fusgr 26432  df-clwwlk 27132  df-clwwlkn 27176  df-clwwlknon 27260

This theorem is referenced by: (None)