incexclem - Metamath Proof Explorer

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

Theorem incexclem 14407

Description: Lemma for incexc 14408. (Contributed by Mario Carneiro, 7-Aug-2017.)

**Assertion**
Ref	Expression
incexclem	⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((#‘𝐵) − (#‘(𝐵 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(#‘𝑠)) · (#‘(𝐵 ∩ ∩ 𝑠))))

Distinct variable groups: 𝐴,𝑠 𝐵,𝑠

Proof of Theorem incexclem Dummy variables 𝑏 𝑡 𝑢 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		unieq 4380	. . . . . . . . . . 11 ⊢ (𝑥 = ∅ → ∪ 𝑥 = ∪ ∅)
2		uni0 4401	. . . . . . . . . . 11 ⊢ ∪ ∅ = ∅
3	1, 2	syl6eq 2660	. . . . . . . . . 10 ⊢ (𝑥 = ∅ → ∪ 𝑥 = ∅)
4	3	ineq2d 3776	. . . . . . . . 9 ⊢ (𝑥 = ∅ → (𝑏 ∩ ∪ 𝑥) = (𝑏 ∩ ∅))
5		in0 3920	. . . . . . . . 9 ⊢ (𝑏 ∩ ∅) = ∅
6	4, 5	syl6eq 2660	. . . . . . . 8 ⊢ (𝑥 = ∅ → (𝑏 ∩ ∪ 𝑥) = ∅)
7	6	fveq2d 6107	. . . . . . 7 ⊢ (𝑥 = ∅ → (#‘(𝑏 ∩ ∪ 𝑥)) = (#‘∅))
8		hash0 13019	. . . . . . 7 ⊢ (#‘∅) = 0
9	7, 8	syl6eq 2660	. . . . . 6 ⊢ (𝑥 = ∅ → (#‘(𝑏 ∩ ∪ 𝑥)) = 0)
10	9	oveq2d 6565	. . . . 5 ⊢ (𝑥 = ∅ → ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑥))) = ((#‘𝑏) − 0))
11		pweq 4111	. . . . . . 7 ⊢ (𝑥 = ∅ → 𝒫 𝑥 = 𝒫 ∅)
12		pw0 4283	. . . . . . 7 ⊢ 𝒫 ∅ = {∅}
13	11, 12	syl6eq 2660	. . . . . 6 ⊢ (𝑥 = ∅ → 𝒫 𝑥 = {∅})
14	13	sumeq1d 14279	. . . . 5 ⊢ (𝑥 = ∅ → Σ𝑠 ∈ 𝒫 𝑥((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) = Σ𝑠 ∈ {∅} ((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))))
15	10, 14	eqeq12d 2625	. . . 4 ⊢ (𝑥 = ∅ → (((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) ↔ ((#‘𝑏) − 0) = Σ𝑠 ∈ {∅} ((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠)))))
16	15	ralbidv 2969	. . 3 ⊢ (𝑥 = ∅ → (∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) ↔ ∀𝑏 ∈ Fin ((#‘𝑏) − 0) = Σ𝑠 ∈ {∅} ((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠)))))
17		unieq 4380	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ∪ 𝑥 = ∪ 𝑦)
18	17	ineq2d 3776	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑏 ∩ ∪ 𝑥) = (𝑏 ∩ ∪ 𝑦))
19	18	fveq2d 6107	. . . . . 6 ⊢ (𝑥 = 𝑦 → (#‘(𝑏 ∩ ∪ 𝑥)) = (#‘(𝑏 ∩ ∪ 𝑦)))
20	19	oveq2d 6565	. . . . 5 ⊢ (𝑥 = 𝑦 → ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑥))) = ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑦))))
21		pweq 4111	. . . . . 6 ⊢ (𝑥 = 𝑦 → 𝒫 𝑥 = 𝒫 𝑦)
22	21	sumeq1d 14279	. . . . 5 ⊢ (𝑥 = 𝑦 → Σ𝑠 ∈ 𝒫 𝑥((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))))
23	20, 22	eqeq12d 2625	. . . 4 ⊢ (𝑥 = 𝑦 → (((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) ↔ ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠)))))
24	23	ralbidv 2969	. . 3 ⊢ (𝑥 = 𝑦 → (∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) ↔ ∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠)))))
25		unieq 4380	. . . . . . . . 9 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ∪ 𝑥 = ∪ (𝑦 ∪ {𝑧}))
26		uniun 4392	. . . . . . . . . 10 ⊢ ∪ (𝑦 ∪ {𝑧}) = (∪ 𝑦 ∪ ∪ {𝑧})
27		vex 3176	. . . . . . . . . . . 12 ⊢ 𝑧 ∈ V
28	27	unisn 4387	. . . . . . . . . . 11 ⊢ ∪ {𝑧} = 𝑧
29	28	uneq2i 3726	. . . . . . . . . 10 ⊢ (∪ 𝑦 ∪ ∪ {𝑧}) = (∪ 𝑦 ∪ 𝑧)
30	26, 29	eqtri 2632	. . . . . . . . 9 ⊢ ∪ (𝑦 ∪ {𝑧}) = (∪ 𝑦 ∪ 𝑧)
31	25, 30	syl6eq 2660	. . . . . . . 8 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ∪ 𝑥 = (∪ 𝑦 ∪ 𝑧))
32	31	ineq2d 3776	. . . . . . 7 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑏 ∩ ∪ 𝑥) = (𝑏 ∩ (∪ 𝑦 ∪ 𝑧)))
33	32	fveq2d 6107	. . . . . 6 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (#‘(𝑏 ∩ ∪ 𝑥)) = (#‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧))))
34	33	oveq2d 6565	. . . . 5 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑥))) = ((#‘𝑏) − (#‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧)))))
35		pweq 4111	. . . . . 6 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → 𝒫 𝑥 = 𝒫 (𝑦 ∪ {𝑧}))
36	35	sumeq1d 14279	. . . . 5 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → Σ𝑠 ∈ 𝒫 𝑥((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))))
37	34, 36	eqeq12d 2625	. . . 4 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) ↔ ((#‘𝑏) − (#‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠)))))
38	37	ralbidv 2969	. . 3 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) ↔ ∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠)))))
39		unieq 4380	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴)
40	39	ineq2d 3776	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (𝑏 ∩ ∪ 𝑥) = (𝑏 ∩ ∪ 𝐴))
41	40	fveq2d 6107	. . . . . 6 ⊢ (𝑥 = 𝐴 → (#‘(𝑏 ∩ ∪ 𝑥)) = (#‘(𝑏 ∩ ∪ 𝐴)))
42	41	oveq2d 6565	. . . . 5 ⊢ (𝑥 = 𝐴 → ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑥))) = ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝐴))))
43		pweq 4111	. . . . . 6 ⊢ (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴)
44	43	sumeq1d 14279	. . . . 5 ⊢ (𝑥 = 𝐴 → Σ𝑠 ∈ 𝒫 𝑥((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))))
45	42, 44	eqeq12d 2625	. . . 4 ⊢ (𝑥 = 𝐴 → (((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) ↔ ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠)))))
46	45	ralbidv 2969	. . 3 ⊢ (𝑥 = 𝐴 → (∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) ↔ ∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠)))))
47		hashcl 13009	. . . . . . 7 ⊢ (𝑏 ∈ Fin → (#‘𝑏) ∈ ℕ₀)
48	47	nn0cnd 11230	. . . . . 6 ⊢ (𝑏 ∈ Fin → (#‘𝑏) ∈ ℂ)
49	48	mulid2d 9937	. . . . 5 ⊢ (𝑏 ∈ Fin → (1 · (#‘𝑏)) = (#‘𝑏))
50		0ex 4718	. . . . . 6 ⊢ ∅ ∈ V
51	49, 48	eqeltrd 2688	. . . . . 6 ⊢ (𝑏 ∈ Fin → (1 · (#‘𝑏)) ∈ ℂ)
52		fveq2 6103	. . . . . . . . . . 11 ⊢ (𝑠 = ∅ → (#‘𝑠) = (#‘∅))
53	52, 8	syl6eq 2660	. . . . . . . . . 10 ⊢ (𝑠 = ∅ → (#‘𝑠) = 0)
54	53	oveq2d 6565	. . . . . . . . 9 ⊢ (𝑠 = ∅ → (-1↑(#‘𝑠)) = (-1↑0))
55		neg1cn 11001	. . . . . . . . . 10 ⊢ -1 ∈ ℂ
56		exp0 12726	. . . . . . . . . 10 ⊢ (-1 ∈ ℂ → (-1↑0) = 1)
57	55, 56	ax-mp 5	. . . . . . . . 9 ⊢ (-1↑0) = 1
58	54, 57	syl6eq 2660	. . . . . . . 8 ⊢ (𝑠 = ∅ → (-1↑(#‘𝑠)) = 1)
59		rint0 4452	. . . . . . . . 9 ⊢ (𝑠 = ∅ → (𝑏 ∩ ∩ 𝑠) = 𝑏)
60	59	fveq2d 6107	. . . . . . . 8 ⊢ (𝑠 = ∅ → (#‘(𝑏 ∩ ∩ 𝑠)) = (#‘𝑏))
61	58, 60	oveq12d 6567	. . . . . . 7 ⊢ (𝑠 = ∅ → ((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) = (1 · (#‘𝑏)))
62	61	sumsn 14319	. . . . . 6 ⊢ ((∅ ∈ V ∧ (1 · (#‘𝑏)) ∈ ℂ) → Σ𝑠 ∈ {∅} ((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) = (1 · (#‘𝑏)))
63	50, 51, 62	sylancr 694	. . . . 5 ⊢ (𝑏 ∈ Fin → Σ𝑠 ∈ {∅} ((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) = (1 · (#‘𝑏)))
64	48	subid1d 10260	. . . . 5 ⊢ (𝑏 ∈ Fin → ((#‘𝑏) − 0) = (#‘𝑏))
65	49, 63, 64	3eqtr4rd 2655	. . . 4 ⊢ (𝑏 ∈ Fin → ((#‘𝑏) − 0) = Σ𝑠 ∈ {∅} ((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))))
66	65	rgen 2906	. . 3 ⊢ ∀𝑏 ∈ Fin ((#‘𝑏) − 0) = Σ𝑠 ∈ {∅} ((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠)))
67		fveq2 6103	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑥 → (#‘𝑏) = (#‘𝑥))
68		ineq1 3769	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑥 → (𝑏 ∩ ∪ 𝑦) = (𝑥 ∩ ∪ 𝑦))
69	68	fveq2d 6107	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑥 → (#‘(𝑏 ∩ ∪ 𝑦)) = (#‘(𝑥 ∩ ∪ 𝑦)))
70	67, 69	oveq12d 6567	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑥 → ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑦))) = ((#‘𝑥) − (#‘(𝑥 ∩ ∪ 𝑦))))
71		simpl 472	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 = 𝑥 ∧ 𝑠 ∈ 𝒫 𝑦) → 𝑏 = 𝑥)
72	71	ineq1d 3775	. . . . . . . . . . . . . 14 ⊢ ((𝑏 = 𝑥 ∧ 𝑠 ∈ 𝒫 𝑦) → (𝑏 ∩ ∩ 𝑠) = (𝑥 ∩ ∩ 𝑠))
73	72	fveq2d 6107	. . . . . . . . . . . . 13 ⊢ ((𝑏 = 𝑥 ∧ 𝑠 ∈ 𝒫 𝑦) → (#‘(𝑏 ∩ ∩ 𝑠)) = (#‘(𝑥 ∩ ∩ 𝑠)))
74	73	oveq2d 6565	. . . . . . . . . . . 12 ⊢ ((𝑏 = 𝑥 ∧ 𝑠 ∈ 𝒫 𝑦) → ((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) = ((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠))))
75	74	sumeq2dv 14281	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑥 → Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠))))
76	70, 75	eqeq12d 2625	. . . . . . . . . 10 ⊢ (𝑏 = 𝑥 → (((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) ↔ ((#‘𝑥) − (#‘(𝑥 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠)))))
77	76	rspcva 3280	. . . . . . . . 9 ⊢ ((𝑥 ∈ Fin ∧ ∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠)))) → ((#‘𝑥) − (#‘(𝑥 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠))))
78	77	adantll 746	. . . . . . . 8 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠)))) → ((#‘𝑥) − (#‘(𝑥 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠))))
79		simpr 476	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → 𝑥 ∈ Fin)
80		inss1 3795	. . . . . . . . . 10 ⊢ (𝑥 ∩ 𝑧) ⊆ 𝑥
81		ssfi 8065	. . . . . . . . . 10 ⊢ ((𝑥 ∈ Fin ∧ (𝑥 ∩ 𝑧) ⊆ 𝑥) → (𝑥 ∩ 𝑧) ∈ Fin)
82	79, 80, 81	sylancl 693	. . . . . . . . 9 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (𝑥 ∩ 𝑧) ∈ Fin)
83		fveq2 6103	. . . . . . . . . . . 12 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → (#‘𝑏) = (#‘(𝑥 ∩ 𝑧)))
84		ineq1 3769	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → (𝑏 ∩ ∪ 𝑦) = ((𝑥 ∩ 𝑧) ∩ ∪ 𝑦))
85		in32 3787	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∩ 𝑧) ∩ ∪ 𝑦) = ((𝑥 ∩ ∪ 𝑦) ∩ 𝑧)
86		inass 3785	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∩ ∪ 𝑦) ∩ 𝑧) = (𝑥 ∩ (∪ 𝑦 ∩ 𝑧))
87	85, 86	eqtri 2632	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∩ 𝑧) ∩ ∪ 𝑦) = (𝑥 ∩ (∪ 𝑦 ∩ 𝑧))
88	84, 87	syl6eq 2660	. . . . . . . . . . . . 13 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → (𝑏 ∩ ∪ 𝑦) = (𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))
89	88	fveq2d 6107	. . . . . . . . . . . 12 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → (#‘(𝑏 ∩ ∪ 𝑦)) = (#‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))))
90	83, 89	oveq12d 6567	. . . . . . . . . . 11 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑦))) = ((#‘(𝑥 ∩ 𝑧)) − (#‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))))
91		ineq1 3769	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → (𝑏 ∩ ∩ 𝑠) = ((𝑥 ∩ 𝑧) ∩ ∩ 𝑠))
92		in32 3787	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∩ 𝑧) ∩ ∩ 𝑠) = ((𝑥 ∩ ∩ 𝑠) ∩ 𝑧)
93		inass 3785	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∩ ∩ 𝑠) ∩ 𝑧) = (𝑥 ∩ (∩ 𝑠 ∩ 𝑧))
94	92, 93	eqtri 2632	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∩ 𝑧) ∩ ∩ 𝑠) = (𝑥 ∩ (∩ 𝑠 ∩ 𝑧))
95	91, 94	syl6eq 2660	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → (𝑏 ∩ ∩ 𝑠) = (𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))
96	95	fveq2d 6107	. . . . . . . . . . . . 13 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → (#‘(𝑏 ∩ ∩ 𝑠)) = (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))))
97	96	oveq2d 6565	. . . . . . . . . . . 12 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → ((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) = ((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
98	97	sumeq2sdv 14282	. . . . . . . . . . 11 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
99	90, 98	eqeq12d 2625	. . . . . . . . . 10 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → (((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) ↔ ((#‘(𝑥 ∩ 𝑧)) − (#‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))))))
100	99	rspcva 3280	. . . . . . . . 9 ⊢ (((𝑥 ∩ 𝑧) ∈ Fin ∧ ∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠)))) → ((#‘(𝑥 ∩ 𝑧)) − (#‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
101	82, 100	sylan 487	. . . . . . . 8 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠)))) → ((#‘(𝑥 ∩ 𝑧)) − (#‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
102	78, 101	oveq12d 6567	. . . . . . 7 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠)))) → (((#‘𝑥) − (#‘(𝑥 ∩ ∪ 𝑦))) − ((#‘(𝑥 ∩ 𝑧)) − (#‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))))) = (Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠))) − Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))))))
103		inss1 3795	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∩ ∪ 𝑦) ⊆ 𝑥
104		ssfi 8065	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ Fin ∧ (𝑥 ∩ ∪ 𝑦) ⊆ 𝑥) → (𝑥 ∩ ∪ 𝑦) ∈ Fin)
105	79, 103, 104	sylancl 693	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (𝑥 ∩ ∪ 𝑦) ∈ Fin)
106		hashun3 13034	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∩ ∪ 𝑦) ∈ Fin ∧ (𝑥 ∩ 𝑧) ∈ Fin) → (#‘((𝑥 ∩ ∪ 𝑦) ∪ (𝑥 ∩ 𝑧))) = (((#‘(𝑥 ∩ ∪ 𝑦)) + (#‘(𝑥 ∩ 𝑧))) − (#‘((𝑥 ∩ ∪ 𝑦) ∩ (𝑥 ∩ 𝑧)))))
107	105, 82, 106	syl2anc 691	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (#‘((𝑥 ∩ ∪ 𝑦) ∪ (𝑥 ∩ 𝑧))) = (((#‘(𝑥 ∩ ∪ 𝑦)) + (#‘(𝑥 ∩ 𝑧))) − (#‘((𝑥 ∩ ∪ 𝑦) ∩ (𝑥 ∩ 𝑧)))))
108		indi 3832	. . . . . . . . . . . . 13 ⊢ (𝑥 ∩ (∪ 𝑦 ∪ 𝑧)) = ((𝑥 ∩ ∪ 𝑦) ∪ (𝑥 ∩ 𝑧))
109	108	fveq2i 6106	. . . . . . . . . . . 12 ⊢ (#‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧))) = (#‘((𝑥 ∩ ∪ 𝑦) ∪ (𝑥 ∩ 𝑧)))
110		inindi 3792	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∩ (∪ 𝑦 ∩ 𝑧)) = ((𝑥 ∩ ∪ 𝑦) ∩ (𝑥 ∩ 𝑧))
111	110	fveq2i 6106	. . . . . . . . . . . . 13 ⊢ (#‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))) = (#‘((𝑥 ∩ ∪ 𝑦) ∩ (𝑥 ∩ 𝑧)))
112	111	oveq2i 6560	. . . . . . . . . . . 12 ⊢ (((#‘(𝑥 ∩ ∪ 𝑦)) + (#‘(𝑥 ∩ 𝑧))) − (#‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))) = (((#‘(𝑥 ∩ ∪ 𝑦)) + (#‘(𝑥 ∩ 𝑧))) − (#‘((𝑥 ∩ ∪ 𝑦) ∩ (𝑥 ∩ 𝑧))))
113	107, 109, 112	3eqtr4g 2669	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (#‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧))) = (((#‘(𝑥 ∩ ∪ 𝑦)) + (#‘(𝑥 ∩ 𝑧))) − (#‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))))
114		hashcl 13009	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∩ ∪ 𝑦) ∈ Fin → (#‘(𝑥 ∩ ∪ 𝑦)) ∈ ℕ₀)
115	105, 114	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (#‘(𝑥 ∩ ∪ 𝑦)) ∈ ℕ₀)
116	115	nn0cnd 11230	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (#‘(𝑥 ∩ ∪ 𝑦)) ∈ ℂ)
117		hashcl 13009	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∩ 𝑧) ∈ Fin → (#‘(𝑥 ∩ 𝑧)) ∈ ℕ₀)
118	82, 117	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (#‘(𝑥 ∩ 𝑧)) ∈ ℕ₀)
119	118	nn0cnd 11230	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (#‘(𝑥 ∩ 𝑧)) ∈ ℂ)
120		inss1 3795	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∩ (∪ 𝑦 ∩ 𝑧)) ⊆ 𝑥
121		ssfi 8065	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ Fin ∧ (𝑥 ∩ (∪ 𝑦 ∩ 𝑧)) ⊆ 𝑥) → (𝑥 ∩ (∪ 𝑦 ∩ 𝑧)) ∈ Fin)
122	79, 120, 121	sylancl 693	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (𝑥 ∩ (∪ 𝑦 ∩ 𝑧)) ∈ Fin)
123		hashcl 13009	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∩ (∪ 𝑦 ∩ 𝑧)) ∈ Fin → (#‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))) ∈ ℕ₀)
124	122, 123	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (#‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))) ∈ ℕ₀)
125	124	nn0cnd 11230	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (#‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))) ∈ ℂ)
126	116, 119, 125	addsubassd 10291	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (((#‘(𝑥 ∩ ∪ 𝑦)) + (#‘(𝑥 ∩ 𝑧))) − (#‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))) = ((#‘(𝑥 ∩ ∪ 𝑦)) + ((#‘(𝑥 ∩ 𝑧)) − (#‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))))))
127	113, 126	eqtrd 2644	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (#‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧))) = ((#‘(𝑥 ∩ ∪ 𝑦)) + ((#‘(𝑥 ∩ 𝑧)) − (#‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))))))
128	127	oveq2d 6565	. . . . . . . . 9 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → ((#‘𝑥) − (#‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))) = ((#‘𝑥) − ((#‘(𝑥 ∩ ∪ 𝑦)) + ((#‘(𝑥 ∩ 𝑧)) − (#‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))))))
129		hashcl 13009	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ Fin → (#‘𝑥) ∈ ℕ₀)
130	129	adantl 481	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (#‘𝑥) ∈ ℕ₀)
131	130	nn0cnd 11230	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (#‘𝑥) ∈ ℂ)
132	119, 125	subcld 10271	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → ((#‘(𝑥 ∩ 𝑧)) − (#‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))) ∈ ℂ)
133	131, 116, 132	subsub4d 10302	. . . . . . . . 9 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (((#‘𝑥) − (#‘(𝑥 ∩ ∪ 𝑦))) − ((#‘(𝑥 ∩ 𝑧)) − (#‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))))) = ((#‘𝑥) − ((#‘(𝑥 ∩ ∪ 𝑦)) + ((#‘(𝑥 ∩ 𝑧)) − (#‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))))))
134	128, 133	eqtr4d 2647	. . . . . . . 8 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → ((#‘𝑥) − (#‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))) = (((#‘𝑥) − (#‘(𝑥 ∩ ∪ 𝑦))) − ((#‘(𝑥 ∩ 𝑧)) − (#‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))))))
135	134	adantr 480	. . . . . . 7 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠)))) → ((#‘𝑥) − (#‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))) = (((#‘𝑥) − (#‘(𝑥 ∩ ∪ 𝑦))) − ((#‘(𝑥 ∩ 𝑧)) − (#‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))))))
136		disjdif 3992	. . . . . . . . . . 11 ⊢ (𝒫 𝑦 ∩ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) = ∅
137	136	a1i 11	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (𝒫 𝑦 ∩ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) = ∅)
138		ssun1 3738	. . . . . . . . . . . . . 14 ⊢ 𝑦 ⊆ (𝑦 ∪ {𝑧})
139		sspwb 4844	. . . . . . . . . . . . . 14 ⊢ (𝑦 ⊆ (𝑦 ∪ {𝑧}) ↔ 𝒫 𝑦 ⊆ 𝒫 (𝑦 ∪ {𝑧}))
140	138, 139	mpbi 219	. . . . . . . . . . . . 13 ⊢ 𝒫 𝑦 ⊆ 𝒫 (𝑦 ∪ {𝑧})
141		undif 4001	. . . . . . . . . . . . 13 ⊢ (𝒫 𝑦 ⊆ 𝒫 (𝑦 ∪ {𝑧}) ↔ (𝒫 𝑦 ∪ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) = 𝒫 (𝑦 ∪ {𝑧}))
142	140, 141	mpbi 219	. . . . . . . . . . . 12 ⊢ (𝒫 𝑦 ∪ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) = 𝒫 (𝑦 ∪ {𝑧})
143	142	eqcomi 2619	. . . . . . . . . . 11 ⊢ 𝒫 (𝑦 ∪ {𝑧}) = (𝒫 𝑦 ∪ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))
144	143	a1i 11	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → 𝒫 (𝑦 ∪ {𝑧}) = (𝒫 𝑦 ∪ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)))
145		simpll 786	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → 𝑦 ∈ Fin)
146		snfi 7923	. . . . . . . . . . . 12 ⊢ {𝑧} ∈ Fin
147		unfi 8112	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝑦 ∪ {𝑧}) ∈ Fin)
148	145, 146, 147	sylancl 693	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (𝑦 ∪ {𝑧}) ∈ Fin)
149		pwfi 8144	. . . . . . . . . . 11 ⊢ ((𝑦 ∪ {𝑧}) ∈ Fin ↔ 𝒫 (𝑦 ∪ {𝑧}) ∈ Fin)
150	148, 149	sylib 207	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → 𝒫 (𝑦 ∪ {𝑧}) ∈ Fin)
151	55	a1i 11	. . . . . . . . . . . 12 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → -1 ∈ ℂ)
152		elpwi 4117	. . . . . . . . . . . . . 14 ⊢ (𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧}) → 𝑠 ⊆ (𝑦 ∪ {𝑧}))
153		ssfi 8065	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∪ {𝑧}) ∈ Fin ∧ 𝑠 ⊆ (𝑦 ∪ {𝑧})) → 𝑠 ∈ Fin)
154	148, 152, 153	syl2an 493	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → 𝑠 ∈ Fin)
155		hashcl 13009	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ Fin → (#‘𝑠) ∈ ℕ₀)
156	154, 155	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (#‘𝑠) ∈ ℕ₀)
157	151, 156	expcld 12870	. . . . . . . . . . 11 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (-1↑(#‘𝑠)) ∈ ℂ)
158		simplr 788	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → 𝑥 ∈ Fin)
159		inss1 3795	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∩ ∩ 𝑠) ⊆ 𝑥
160		ssfi 8065	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ Fin ∧ (𝑥 ∩ ∩ 𝑠) ⊆ 𝑥) → (𝑥 ∩ ∩ 𝑠) ∈ Fin)
161	158, 159, 160	sylancl 693	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (𝑥 ∩ ∩ 𝑠) ∈ Fin)
162		hashcl 13009	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∩ ∩ 𝑠) ∈ Fin → (#‘(𝑥 ∩ ∩ 𝑠)) ∈ ℕ₀)
163	161, 162	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (#‘(𝑥 ∩ ∩ 𝑠)) ∈ ℕ₀)
164	163	nn0cnd 11230	. . . . . . . . . . 11 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (#‘(𝑥 ∩ ∩ 𝑠)) ∈ ℂ)
165	157, 164	mulcld 9939	. . . . . . . . . 10 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → ((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠))) ∈ ℂ)
166	137, 144, 150, 165	fsumsplit 14318	. . . . . . . . 9 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠))) = (Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠))) + Σ𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠)))))
167		fveq2 6103	. . . . . . . . . . . . . 14 ⊢ (𝑠 = (𝑡 ∪ {𝑧}) → (#‘𝑠) = (#‘(𝑡 ∪ {𝑧})))
168	167	oveq2d 6565	. . . . . . . . . . . . 13 ⊢ (𝑠 = (𝑡 ∪ {𝑧}) → (-1↑(#‘𝑠)) = (-1↑(#‘(𝑡 ∪ {𝑧}))))
169		inteq 4413	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = (𝑡 ∪ {𝑧}) → ∩ 𝑠 = ∩ (𝑡 ∪ {𝑧}))
170	27	intunsn 4451	. . . . . . . . . . . . . . . 16 ⊢ ∩ (𝑡 ∪ {𝑧}) = (∩ 𝑡 ∩ 𝑧)
171	169, 170	syl6eq 2660	. . . . . . . . . . . . . . 15 ⊢ (𝑠 = (𝑡 ∪ {𝑧}) → ∩ 𝑠 = (∩ 𝑡 ∩ 𝑧))
172	171	ineq2d 3776	. . . . . . . . . . . . . 14 ⊢ (𝑠 = (𝑡 ∪ {𝑧}) → (𝑥 ∩ ∩ 𝑠) = (𝑥 ∩ (∩ 𝑡 ∩ 𝑧)))
173	172	fveq2d 6107	. . . . . . . . . . . . 13 ⊢ (𝑠 = (𝑡 ∪ {𝑧}) → (#‘(𝑥 ∩ ∩ 𝑠)) = (#‘(𝑥 ∩ (∩ 𝑡 ∩ 𝑧))))
174	168, 173	oveq12d 6567	. . . . . . . . . . . 12 ⊢ (𝑠 = (𝑡 ∪ {𝑧}) → ((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠))) = ((-1↑(#‘(𝑡 ∪ {𝑧}))) · (#‘(𝑥 ∩ (∩ 𝑡 ∩ 𝑧)))))
175		pwfi 8144	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ Fin ↔ 𝒫 𝑦 ∈ Fin)
176	145, 175	sylib 207	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → 𝒫 𝑦 ∈ Fin)
177		eqid 2610	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ 𝒫 𝑦 ↦ (𝑢 ∪ {𝑧})) = (𝑢 ∈ 𝒫 𝑦 ↦ (𝑢 ∪ {𝑧}))
178		elpwi 4117	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 ∈ 𝒫 𝑦 → 𝑢 ⊆ 𝑦)
179	178	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → 𝑢 ⊆ 𝑦)
180		unss1 3744	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 ⊆ 𝑦 → (𝑢 ∪ {𝑧}) ⊆ (𝑦 ∪ {𝑧}))
181	179, 180	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → (𝑢 ∪ {𝑧}) ⊆ (𝑦 ∪ {𝑧}))
182		vex 3176	. . . . . . . . . . . . . . . . 17 ⊢ 𝑢 ∈ V
183		snex 4835	. . . . . . . . . . . . . . . . 17 ⊢ {𝑧} ∈ V
184	182, 183	unex 6854	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 ∪ {𝑧}) ∈ V
185	184	elpw 4114	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 ∪ {𝑧}) ∈ 𝒫 (𝑦 ∪ {𝑧}) ↔ (𝑢 ∪ {𝑧}) ⊆ (𝑦 ∪ {𝑧}))
186	181, 185	sylibr 223	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → (𝑢 ∪ {𝑧}) ∈ 𝒫 (𝑦 ∪ {𝑧}))
187		simpllr 795	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → ¬ 𝑧 ∈ 𝑦)
188		elpwi 4117	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 ∪ {𝑧}) ∈ 𝒫 𝑦 → (𝑢 ∪ {𝑧}) ⊆ 𝑦)
189		ssun2 3739	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑧} ⊆ (𝑢 ∪ {𝑧})
190	27	snss 4259	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ (𝑢 ∪ {𝑧}) ↔ {𝑧} ⊆ (𝑢 ∪ {𝑧}))
191	189, 190	mpbir 220	. . . . . . . . . . . . . . . . 17 ⊢ 𝑧 ∈ (𝑢 ∪ {𝑧})
192	191	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → 𝑧 ∈ (𝑢 ∪ {𝑧}))
193		ssel 3562	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 ∪ {𝑧}) ⊆ 𝑦 → (𝑧 ∈ (𝑢 ∪ {𝑧}) → 𝑧 ∈ 𝑦))
194	188, 192, 193	syl2imc 40	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → ((𝑢 ∪ {𝑧}) ∈ 𝒫 𝑦 → 𝑧 ∈ 𝑦))
195	187, 194	mtod 188	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → ¬ (𝑢 ∪ {𝑧}) ∈ 𝒫 𝑦)
196	186, 195	eldifd 3551	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → (𝑢 ∪ {𝑧}) ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))
197		eldifi 3694	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦) → 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧}))
198	197	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧}))
199	198	elpwid 4118	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → 𝑠 ⊆ (𝑦 ∪ {𝑧}))
200		uncom 3719	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∪ {𝑧}) = ({𝑧} ∪ 𝑦)
201	199, 200	syl6sseq 3614	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → 𝑠 ⊆ ({𝑧} ∪ 𝑦))
202		ssundif 4004	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ⊆ ({𝑧} ∪ 𝑦) ↔ (𝑠 ∖ {𝑧}) ⊆ 𝑦)
203	201, 202	sylib 207	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → (𝑠 ∖ {𝑧}) ⊆ 𝑦)
204		vex 3176	. . . . . . . . . . . . . . 15 ⊢ 𝑦 ∈ V
205	204	elpw2 4755	. . . . . . . . . . . . . 14 ⊢ ((𝑠 ∖ {𝑧}) ∈ 𝒫 𝑦 ↔ (𝑠 ∖ {𝑧}) ⊆ 𝑦)
206	203, 205	sylibr 223	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → (𝑠 ∖ {𝑧}) ∈ 𝒫 𝑦)
207		elpwunsn 4171	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦) → 𝑧 ∈ 𝑠)
208	207	ad2antll 761	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → 𝑧 ∈ 𝑠)
209	208	snssd 4281	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → {𝑧} ⊆ 𝑠)
210		ssequn2 3748	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑧} ⊆ 𝑠 ↔ (𝑠 ∪ {𝑧}) = 𝑠)
211	209, 210	sylib 207	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → (𝑠 ∪ {𝑧}) = 𝑠)
212	211	eqcomd 2616	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → 𝑠 = (𝑠 ∪ {𝑧}))
213		uneq1 3722	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = (𝑠 ∖ {𝑧}) → (𝑢 ∪ {𝑧}) = ((𝑠 ∖ {𝑧}) ∪ {𝑧}))
214		undif1 3995	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑠 ∖ {𝑧}) ∪ {𝑧}) = (𝑠 ∪ {𝑧})
215	213, 214	syl6eq 2660	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = (𝑠 ∖ {𝑧}) → (𝑢 ∪ {𝑧}) = (𝑠 ∪ {𝑧}))
216	215	eqeq2d 2620	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = (𝑠 ∖ {𝑧}) → (𝑠 = (𝑢 ∪ {𝑧}) ↔ 𝑠 = (𝑠 ∪ {𝑧})))
217	212, 216	syl5ibrcom 236	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → (𝑢 = (𝑠 ∖ {𝑧}) → 𝑠 = (𝑢 ∪ {𝑧})))
218	178	ad2antrl 760	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → 𝑢 ⊆ 𝑦)
219		simpllr 795	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → ¬ 𝑧 ∈ 𝑦)
220	218, 219	ssneldd 3571	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → ¬ 𝑧 ∈ 𝑢)
221		difsnb 4278	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑧 ∈ 𝑢 ↔ (𝑢 ∖ {𝑧}) = 𝑢)
222	220, 221	sylib 207	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → (𝑢 ∖ {𝑧}) = 𝑢)
223	222	eqcomd 2616	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → 𝑢 = (𝑢 ∖ {𝑧}))
224		difeq1 3683	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = (𝑢 ∪ {𝑧}) → (𝑠 ∖ {𝑧}) = ((𝑢 ∪ {𝑧}) ∖ {𝑧}))
225		difun2 4000	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∪ {𝑧}) ∖ {𝑧}) = (𝑢 ∖ {𝑧})
226	224, 225	syl6eq 2660	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = (𝑢 ∪ {𝑧}) → (𝑠 ∖ {𝑧}) = (𝑢 ∖ {𝑧}))
227	226	eqeq2d 2620	. . . . . . . . . . . . . . 15 ⊢ (𝑠 = (𝑢 ∪ {𝑧}) → (𝑢 = (𝑠 ∖ {𝑧}) ↔ 𝑢 = (𝑢 ∖ {𝑧})))
228	223, 227	syl5ibrcom 236	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → (𝑠 = (𝑢 ∪ {𝑧}) → 𝑢 = (𝑠 ∖ {𝑧})))
229	217, 228	impbid 201	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → (𝑢 = (𝑠 ∖ {𝑧}) ↔ 𝑠 = (𝑢 ∪ {𝑧})))
230	177, 196, 206, 229	f1o2d 6785	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (𝑢 ∈ 𝒫 𝑦 ↦ (𝑢 ∪ {𝑧})):𝒫 𝑦–1-1-onto→(𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))
231		uneq1 3722	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝑡 → (𝑢 ∪ {𝑧}) = (𝑡 ∪ {𝑧}))
232		vex 3176	. . . . . . . . . . . . . . 15 ⊢ 𝑡 ∈ V
233	232, 183	unex 6854	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∪ {𝑧}) ∈ V
234	231, 177, 233	fvmpt 6191	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ 𝒫 𝑦 → ((𝑢 ∈ 𝒫 𝑦 ↦ (𝑢 ∪ {𝑧}))‘𝑡) = (𝑡 ∪ {𝑧}))
235	234	adantl 481	. . . . . . . . . . . 12 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑡 ∈ 𝒫 𝑦) → ((𝑢 ∈ 𝒫 𝑦 ↦ (𝑢 ∪ {𝑧}))‘𝑡) = (𝑡 ∪ {𝑧}))
236	197, 165	sylan2 490	. . . . . . . . . . . 12 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → ((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠))) ∈ ℂ)
237	174, 176, 230, 235, 236	fsumf1o 14301	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠))) = Σ𝑡 ∈ 𝒫 𝑦((-1↑(#‘(𝑡 ∪ {𝑧}))) · (#‘(𝑥 ∩ (∩ 𝑡 ∩ 𝑧)))))
238		uneq1 3722	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑠 → (𝑡 ∪ {𝑧}) = (𝑠 ∪ {𝑧}))
239	238	fveq2d 6107	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑠 → (#‘(𝑡 ∪ {𝑧})) = (#‘(𝑠 ∪ {𝑧})))
240	239	oveq2d 6565	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑠 → (-1↑(#‘(𝑡 ∪ {𝑧}))) = (-1↑(#‘(𝑠 ∪ {𝑧}))))
241		inteq 4413	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑠 → ∩ 𝑡 = ∩ 𝑠)
242	241	ineq1d 3775	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑠 → (∩ 𝑡 ∩ 𝑧) = (∩ 𝑠 ∩ 𝑧))
243	242	ineq2d 3776	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑠 → (𝑥 ∩ (∩ 𝑡 ∩ 𝑧)) = (𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))
244	243	fveq2d 6107	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑠 → (#‘(𝑥 ∩ (∩ 𝑡 ∩ 𝑧))) = (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))))
245	240, 244	oveq12d 6567	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑠 → ((-1↑(#‘(𝑡 ∪ {𝑧}))) · (#‘(𝑥 ∩ (∩ 𝑡 ∩ 𝑧)))) = ((-1↑(#‘(𝑠 ∪ {𝑧}))) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
246	245	cbvsumv 14274	. . . . . . . . . . . 12 ⊢ Σ𝑡 ∈ 𝒫 𝑦((-1↑(#‘(𝑡 ∪ {𝑧}))) · (#‘(𝑥 ∩ (∩ 𝑡 ∩ 𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘(𝑠 ∪ {𝑧}))) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))))
247	55	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → -1 ∈ ℂ)
248		elpwi 4117	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 ∈ 𝒫 𝑦 → 𝑠 ⊆ 𝑦)
249		ssfi 8065	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ Fin ∧ 𝑠 ⊆ 𝑦) → 𝑠 ∈ Fin)
250	145, 248, 249	syl2an 493	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → 𝑠 ∈ Fin)
251	250, 155	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (#‘𝑠) ∈ ℕ₀)
252	247, 251	expp1d 12871	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1↑((#‘𝑠) + 1)) = ((-1↑(#‘𝑠)) · -1))
253	248	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → 𝑠 ⊆ 𝑦)
254		simpllr 795	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ¬ 𝑧 ∈ 𝑦)
255	253, 254	ssneldd 3571	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ¬ 𝑧 ∈ 𝑠)
256		hashunsng 13042	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ V → ((𝑠 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑠) → (#‘(𝑠 ∪ {𝑧})) = ((#‘𝑠) + 1)))
257	27, 256	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑠 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑠) → (#‘(𝑠 ∪ {𝑧})) = ((#‘𝑠) + 1))
258	250, 255, 257	syl2anc 691	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (#‘(𝑠 ∪ {𝑧})) = ((#‘𝑠) + 1))
259	258	oveq2d 6565	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1↑(#‘(𝑠 ∪ {𝑧}))) = (-1↑((#‘𝑠) + 1)))
260	140	sseli 3564	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 ∈ 𝒫 𝑦 → 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧}))
261	260, 157	sylan2 490	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1↑(#‘𝑠)) ∈ ℂ)
262	247, 261	mulcomd 9940	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1 · (-1↑(#‘𝑠))) = ((-1↑(#‘𝑠)) · -1))
263	252, 259, 262	3eqtr4d 2654	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1↑(#‘(𝑠 ∪ {𝑧}))) = (-1 · (-1↑(#‘𝑠))))
264	261	mulm1d 10361	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1 · (-1↑(#‘𝑠))) = -(-1↑(#‘𝑠)))
265	263, 264	eqtrd 2644	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1↑(#‘(𝑠 ∪ {𝑧}))) = -(-1↑(#‘𝑠)))
266	265	oveq1d 6564	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ((-1↑(#‘(𝑠 ∪ {𝑧}))) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))) = (-(-1↑(#‘𝑠)) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
267		inss1 3795	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∩ (∩ 𝑠 ∩ 𝑧)) ⊆ 𝑥
268		ssfi 8065	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ Fin ∧ (𝑥 ∩ (∩ 𝑠 ∩ 𝑧)) ⊆ 𝑥) → (𝑥 ∩ (∩ 𝑠 ∩ 𝑧)) ∈ Fin)
269	158, 267, 268	sylancl 693	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (𝑥 ∩ (∩ 𝑠 ∩ 𝑧)) ∈ Fin)
270		hashcl 13009	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∩ (∩ 𝑠 ∩ 𝑧)) ∈ Fin → (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))) ∈ ℕ₀)
271	269, 270	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))) ∈ ℕ₀)
272	271	nn0cnd 11230	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))) ∈ ℂ)
273	260, 272	sylan2 490	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))) ∈ ℂ)
274	261, 273	mulneg1d 10362	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-(-1↑(#‘𝑠)) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))) = -((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
275	266, 274	eqtrd 2644	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ((-1↑(#‘(𝑠 ∪ {𝑧}))) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))) = -((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
276	275	sumeq2dv 14281	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘(𝑠 ∪ {𝑧}))) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦-((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
277	246, 276	syl5eq 2656	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑡 ∈ 𝒫 𝑦((-1↑(#‘(𝑡 ∪ {𝑧}))) · (#‘(𝑥 ∩ (∩ 𝑡 ∩ 𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦-((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
278	157, 272	mulcld 9939	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → ((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))) ∈ ℂ)
279	260, 278	sylan2 490	. . . . . . . . . . . 12 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))) ∈ ℂ)
280	176, 279	fsumneg 14361	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 𝑦-((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))) = -Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
281	237, 277, 280	3eqtrd 2648	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠))) = -Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
282	281	oveq2d 6565	. . . . . . . . 9 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠))) + Σ𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠)))) = (Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠))) + -Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))))))
283	140	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → 𝒫 𝑦 ⊆ 𝒫 (𝑦 ∪ {𝑧}))
284	283	sselda 3568	. . . . . . . . . . . 12 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧}))
285	284, 165	syldan 486	. . . . . . . . . . 11 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠))) ∈ ℂ)
286	176, 285	fsumcl 14311	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠))) ∈ ℂ)
287	284, 278	syldan 486	. . . . . . . . . . 11 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))) ∈ ℂ)
288	176, 287	fsumcl 14311	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))) ∈ ℂ)
289	286, 288	negsubd 10277	. . . . . . . . 9 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠))) + -Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))))) = (Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠))) − Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))))))
290	166, 282, 289	3eqtrd 2648	. . . . . . . 8 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠))) = (Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠))) − Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))))))
291	290	adantr 480	. . . . . . 7 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠)))) → Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠))) = (Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠))) − Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))))))
292	102, 135, 291	3eqtr4d 2654	. . . . . 6 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠)))) → ((#‘𝑥) − (#‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠))))
293	292	ex 449	. . . . 5 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) → ((#‘𝑥) − (#‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠)))))
294	293	ralrimdva 2952	. . . 4 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) → ∀𝑥 ∈ Fin ((#‘𝑥) − (#‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠)))))
295		ineq1 3769	. . . . . . . 8 ⊢ (𝑏 = 𝑥 → (𝑏 ∩ (∪ 𝑦 ∪ 𝑧)) = (𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))
296	295	fveq2d 6107	. . . . . . 7 ⊢ (𝑏 = 𝑥 → (#‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧))) = (#‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧))))
297	67, 296	oveq12d 6567	. . . . . 6 ⊢ (𝑏 = 𝑥 → ((#‘𝑏) − (#‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧)))) = ((#‘𝑥) − (#‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))))
298		ineq1 3769	. . . . . . . . 9 ⊢ (𝑏 = 𝑥 → (𝑏 ∩ ∩ 𝑠) = (𝑥 ∩ ∩ 𝑠))
299	298	fveq2d 6107	. . . . . . . 8 ⊢ (𝑏 = 𝑥 → (#‘(𝑏 ∩ ∩ 𝑠)) = (#‘(𝑥 ∩ ∩ 𝑠)))
300	299	oveq2d 6565	. . . . . . 7 ⊢ (𝑏 = 𝑥 → ((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) = ((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠))))
301	300	sumeq2sdv 14282	. . . . . 6 ⊢ (𝑏 = 𝑥 → Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠))))
302	297, 301	eqeq12d 2625	. . . . 5 ⊢ (𝑏 = 𝑥 → (((#‘𝑏) − (#‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) ↔ ((#‘𝑥) − (#‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠)))))
303	302	cbvralv 3147	. . . 4 ⊢ (∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) ↔ ∀𝑥 ∈ Fin ((#‘𝑥) − (#‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠))))
304	294, 303	syl6ibr 241	. . 3 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) → ∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠)))))
305	16, 24, 38, 46, 66, 304	findcard2s 8086	. 2 ⊢ (𝐴 ∈ Fin → ∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))))
306		fveq2 6103	. . . . 5 ⊢ (𝑏 = 𝐵 → (#‘𝑏) = (#‘𝐵))
307		ineq1 3769	. . . . . 6 ⊢ (𝑏 = 𝐵 → (𝑏 ∩ ∪ 𝐴) = (𝐵 ∩ ∪ 𝐴))
308	307	fveq2d 6107	. . . . 5 ⊢ (𝑏 = 𝐵 → (#‘(𝑏 ∩ ∪ 𝐴)) = (#‘(𝐵 ∩ ∪ 𝐴)))
309	306, 308	oveq12d 6567	. . . 4 ⊢ (𝑏 = 𝐵 → ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝐴))) = ((#‘𝐵) − (#‘(𝐵 ∩ ∪ 𝐴))))
310		simpl 472	. . . . . . . 8 ⊢ ((𝑏 = 𝐵 ∧ 𝑠 ∈ 𝒫 𝐴) → 𝑏 = 𝐵)
311	310	ineq1d 3775	. . . . . . 7 ⊢ ((𝑏 = 𝐵 ∧ 𝑠 ∈ 𝒫 𝐴) → (𝑏 ∩ ∩ 𝑠) = (𝐵 ∩ ∩ 𝑠))
312	311	fveq2d 6107	. . . . . 6 ⊢ ((𝑏 = 𝐵 ∧ 𝑠 ∈ 𝒫 𝐴) → (#‘(𝑏 ∩ ∩ 𝑠)) = (#‘(𝐵 ∩ ∩ 𝑠)))
313	312	oveq2d 6565	. . . . 5 ⊢ ((𝑏 = 𝐵 ∧ 𝑠 ∈ 𝒫 𝐴) → ((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) = ((-1↑(#‘𝑠)) · (#‘(𝐵 ∩ ∩ 𝑠))))
314	313	sumeq2dv 14281	. . . 4 ⊢ (𝑏 = 𝐵 → Σ𝑠 ∈ 𝒫 𝐴((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(#‘𝑠)) · (#‘(𝐵 ∩ ∩ 𝑠))))
315	309, 314	eqeq12d 2625	. . 3 ⊢ (𝑏 = 𝐵 → (((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) ↔ ((#‘𝐵) − (#‘(𝐵 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(#‘𝑠)) · (#‘(𝐵 ∩ ∩ 𝑠)))))
316	315	rspccva 3281	. 2 ⊢ ((∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) ∧ 𝐵 ∈ Fin) → ((#‘𝐵) − (#‘(𝐵 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(#‘𝑠)) · (#‘(𝐵 ∩ ∩ 𝑠))))
317	305, 316	sylan 487	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((#‘𝐵) − (#‘(𝐵 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(#‘𝑠)) · (#‘(𝐵 ∩ ∩ 𝑠))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 383 = wceq 1475 ∈ wcel 1977 ∀wral 2896 Vcvv 3173 ∖ cdif 3537 ∪ cun 3538 ∩ cin 3539 ⊆ wss 3540 ∅c0 3874 𝒫 cpw 4108 {csn 4125 ∪ cuni 4372 ∩ cint 4410 ↦ cmpt 4643 ‘cfv 5804 (class class class)co 6549 Fincfn 7841 ℂcc 9813 0cc0 9815 1c1 9816 + caddc 9818 · cmul 9820 − cmin 10145 -cneg 10146 ℕ₀cn0 11169 ↑cexp 12722 #chash 12979 Σcsu 14264

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-inf2 8421 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892 ax-pre-sup 9893

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-fal 1481 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-int 4411 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-se 4998 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-isom 5813 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-om 6958 df-1st 7059 df-2nd 7060 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-1o 7447 df-2o 7448 df-oadd 7451 df-er 7629 df-map 7746 df-en 7842 df-dom 7843 df-sdom 7844 df-fin 7845 df-sup 8231 df-oi 8298 df-card 8648 df-cda 8873 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-div 10564 df-nn 10898 df-2 10956 df-3 10957 df-n0 11170 df-z 11255 df-uz 11564 df-rp 11709 df-fz 12198 df-fzo 12335 df-seq 12664 df-exp 12723 df-hash 12980 df-cj 13687 df-re 13688 df-im 13689 df-sqrt 13823 df-abs 13824 df-clim 14067 df-sum 14265

This theorem is referenced by: incexc 14408

W3C validator