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 14568

Description: Lemma for incexc 14569. (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 4444	. . . . . . . . . . 11 ⊢ (𝑥 = ∅ → ∪ 𝑥 = ∪ ∅)
2		uni0 4465	. . . . . . . . . . 11 ⊢ ∪ ∅ = ∅
3	1, 2	syl6eq 2672	. . . . . . . . . 10 ⊢ (𝑥 = ∅ → ∪ 𝑥 = ∅)
4	3	ineq2d 3814	. . . . . . . . 9 ⊢ (𝑥 = ∅ → (𝑏 ∩ ∪ 𝑥) = (𝑏 ∩ ∅))
5		in0 3968	. . . . . . . . 9 ⊢ (𝑏 ∩ ∅) = ∅
6	4, 5	syl6eq 2672	. . . . . . . 8 ⊢ (𝑥 = ∅ → (𝑏 ∩ ∪ 𝑥) = ∅)
7	6	fveq2d 6195	. . . . . . 7 ⊢ (𝑥 = ∅ → (#‘(𝑏 ∩ ∪ 𝑥)) = (#‘∅))
8		hash0 13158	. . . . . . 7 ⊢ (#‘∅) = 0
9	7, 8	syl6eq 2672	. . . . . 6 ⊢ (𝑥 = ∅ → (#‘(𝑏 ∩ ∪ 𝑥)) = 0)
10	9	oveq2d 6666	. . . . 5 ⊢ (𝑥 = ∅ → ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑥))) = ((#‘𝑏) − 0))
11		pweq 4161	. . . . . . 7 ⊢ (𝑥 = ∅ → 𝒫 𝑥 = 𝒫 ∅)
12		pw0 4343	. . . . . . 7 ⊢ 𝒫 ∅ = {∅}
13	11, 12	syl6eq 2672	. . . . . 6 ⊢ (𝑥 = ∅ → 𝒫 𝑥 = {∅})
14	13	sumeq1d 14431	. . . . 5 ⊢ (𝑥 = ∅ → Σ𝑠 ∈ 𝒫 𝑥((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) = Σ𝑠 ∈ {∅} ((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))))
15	10, 14	eqeq12d 2637	. . . 4 ⊢ (𝑥 = ∅ → (((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) ↔ ((#‘𝑏) − 0) = Σ𝑠 ∈ {∅} ((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠)))))
16	15	ralbidv 2986	. . 3 ⊢ (𝑥 = ∅ → (∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) ↔ ∀𝑏 ∈ Fin ((#‘𝑏) − 0) = Σ𝑠 ∈ {∅} ((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠)))))
17		unieq 4444	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ∪ 𝑥 = ∪ 𝑦)
18	17	ineq2d 3814	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑏 ∩ ∪ 𝑥) = (𝑏 ∩ ∪ 𝑦))
19	18	fveq2d 6195	. . . . . 6 ⊢ (𝑥 = 𝑦 → (#‘(𝑏 ∩ ∪ 𝑥)) = (#‘(𝑏 ∩ ∪ 𝑦)))
20	19	oveq2d 6666	. . . . 5 ⊢ (𝑥 = 𝑦 → ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑥))) = ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑦))))
21		pweq 4161	. . . . . 6 ⊢ (𝑥 = 𝑦 → 𝒫 𝑥 = 𝒫 𝑦)
22	21	sumeq1d 14431	. . . . 5 ⊢ (𝑥 = 𝑦 → Σ𝑠 ∈ 𝒫 𝑥((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))))
23	20, 22	eqeq12d 2637	. . . 4 ⊢ (𝑥 = 𝑦 → (((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) ↔ ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠)))))
24	23	ralbidv 2986	. . 3 ⊢ (𝑥 = 𝑦 → (∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) ↔ ∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠)))))
25		unieq 4444	. . . . . . . . 9 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ∪ 𝑥 = ∪ (𝑦 ∪ {𝑧}))
26		uniun 4456	. . . . . . . . . 10 ⊢ ∪ (𝑦 ∪ {𝑧}) = (∪ 𝑦 ∪ ∪ {𝑧})
27		vex 3203	. . . . . . . . . . . 12 ⊢ 𝑧 ∈ V
28	27	unisn 4451	. . . . . . . . . . 11 ⊢ ∪ {𝑧} = 𝑧
29	28	uneq2i 3764	. . . . . . . . . 10 ⊢ (∪ 𝑦 ∪ ∪ {𝑧}) = (∪ 𝑦 ∪ 𝑧)
30	26, 29	eqtri 2644	. . . . . . . . 9 ⊢ ∪ (𝑦 ∪ {𝑧}) = (∪ 𝑦 ∪ 𝑧)
31	25, 30	syl6eq 2672	. . . . . . . 8 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ∪ 𝑥 = (∪ 𝑦 ∪ 𝑧))
32	31	ineq2d 3814	. . . . . . 7 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑏 ∩ ∪ 𝑥) = (𝑏 ∩ (∪ 𝑦 ∪ 𝑧)))
33	32	fveq2d 6195	. . . . . 6 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (#‘(𝑏 ∩ ∪ 𝑥)) = (#‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧))))
34	33	oveq2d 6666	. . . . 5 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑥))) = ((#‘𝑏) − (#‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧)))))
35		pweq 4161	. . . . . 6 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → 𝒫 𝑥 = 𝒫 (𝑦 ∪ {𝑧}))
36	35	sumeq1d 14431	. . . . 5 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → Σ𝑠 ∈ 𝒫 𝑥((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))))
37	34, 36	eqeq12d 2637	. . . 4 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) ↔ ((#‘𝑏) − (#‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠)))))
38	37	ralbidv 2986	. . 3 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) ↔ ∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠)))))
39		unieq 4444	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴)
40	39	ineq2d 3814	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (𝑏 ∩ ∪ 𝑥) = (𝑏 ∩ ∪ 𝐴))
41	40	fveq2d 6195	. . . . . 6 ⊢ (𝑥 = 𝐴 → (#‘(𝑏 ∩ ∪ 𝑥)) = (#‘(𝑏 ∩ ∪ 𝐴)))
42	41	oveq2d 6666	. . . . 5 ⊢ (𝑥 = 𝐴 → ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑥))) = ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝐴))))
43		pweq 4161	. . . . . 6 ⊢ (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴)
44	43	sumeq1d 14431	. . . . 5 ⊢ (𝑥 = 𝐴 → Σ𝑠 ∈ 𝒫 𝑥((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))))
45	42, 44	eqeq12d 2637	. . . 4 ⊢ (𝑥 = 𝐴 → (((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) ↔ ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠)))))
46	45	ralbidv 2986	. . 3 ⊢ (𝑥 = 𝐴 → (∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) ↔ ∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠)))))
47		hashcl 13147	. . . . . . 7 ⊢ (𝑏 ∈ Fin → (#‘𝑏) ∈ ℕ₀)
48	47	nn0cnd 11353	. . . . . 6 ⊢ (𝑏 ∈ Fin → (#‘𝑏) ∈ ℂ)
49	48	mulid2d 10058	. . . . 5 ⊢ (𝑏 ∈ Fin → (1 · (#‘𝑏)) = (#‘𝑏))
50		0ex 4790	. . . . . 6 ⊢ ∅ ∈ V
51	49, 48	eqeltrd 2701	. . . . . 6 ⊢ (𝑏 ∈ Fin → (1 · (#‘𝑏)) ∈ ℂ)
52		fveq2 6191	. . . . . . . . . . 11 ⊢ (𝑠 = ∅ → (#‘𝑠) = (#‘∅))
53	52, 8	syl6eq 2672	. . . . . . . . . 10 ⊢ (𝑠 = ∅ → (#‘𝑠) = 0)
54	53	oveq2d 6666	. . . . . . . . 9 ⊢ (𝑠 = ∅ → (-1↑(#‘𝑠)) = (-1↑0))
55		neg1cn 11124	. . . . . . . . . 10 ⊢ -1 ∈ ℂ
56		exp0 12864	. . . . . . . . . 10 ⊢ (-1 ∈ ℂ → (-1↑0) = 1)
57	55, 56	ax-mp 5	. . . . . . . . 9 ⊢ (-1↑0) = 1
58	54, 57	syl6eq 2672	. . . . . . . 8 ⊢ (𝑠 = ∅ → (-1↑(#‘𝑠)) = 1)
59		rint0 4517	. . . . . . . . 9 ⊢ (𝑠 = ∅ → (𝑏 ∩ ∩ 𝑠) = 𝑏)
60	59	fveq2d 6195	. . . . . . . 8 ⊢ (𝑠 = ∅ → (#‘(𝑏 ∩ ∩ 𝑠)) = (#‘𝑏))
61	58, 60	oveq12d 6668	. . . . . . 7 ⊢ (𝑠 = ∅ → ((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) = (1 · (#‘𝑏)))
62	61	sumsn 14475	. . . . . 6 ⊢ ((∅ ∈ V ∧ (1 · (#‘𝑏)) ∈ ℂ) → Σ𝑠 ∈ {∅} ((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) = (1 · (#‘𝑏)))
63	50, 51, 62	sylancr 695	. . . . 5 ⊢ (𝑏 ∈ Fin → Σ𝑠 ∈ {∅} ((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) = (1 · (#‘𝑏)))
64	48	subid1d 10381	. . . . 5 ⊢ (𝑏 ∈ Fin → ((#‘𝑏) − 0) = (#‘𝑏))
65	49, 63, 64	3eqtr4rd 2667	. . . 4 ⊢ (𝑏 ∈ Fin → ((#‘𝑏) − 0) = Σ𝑠 ∈ {∅} ((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))))
66	65	rgen 2922	. . 3 ⊢ ∀𝑏 ∈ Fin ((#‘𝑏) − 0) = Σ𝑠 ∈ {∅} ((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠)))
67		fveq2 6191	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑥 → (#‘𝑏) = (#‘𝑥))
68		ineq1 3807	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑥 → (𝑏 ∩ ∪ 𝑦) = (𝑥 ∩ ∪ 𝑦))
69	68	fveq2d 6195	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑥 → (#‘(𝑏 ∩ ∪ 𝑦)) = (#‘(𝑥 ∩ ∪ 𝑦)))
70	67, 69	oveq12d 6668	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑥 → ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑦))) = ((#‘𝑥) − (#‘(𝑥 ∩ ∪ 𝑦))))
71		simpl 473	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 = 𝑥 ∧ 𝑠 ∈ 𝒫 𝑦) → 𝑏 = 𝑥)
72	71	ineq1d 3813	. . . . . . . . . . . . . 14 ⊢ ((𝑏 = 𝑥 ∧ 𝑠 ∈ 𝒫 𝑦) → (𝑏 ∩ ∩ 𝑠) = (𝑥 ∩ ∩ 𝑠))
73	72	fveq2d 6195	. . . . . . . . . . . . 13 ⊢ ((𝑏 = 𝑥 ∧ 𝑠 ∈ 𝒫 𝑦) → (#‘(𝑏 ∩ ∩ 𝑠)) = (#‘(𝑥 ∩ ∩ 𝑠)))
74	73	oveq2d 6666	. . . . . . . . . . . 12 ⊢ ((𝑏 = 𝑥 ∧ 𝑠 ∈ 𝒫 𝑦) → ((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) = ((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠))))
75	74	sumeq2dv 14433	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑥 → Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠))))
76	70, 75	eqeq12d 2637	. . . . . . . . . 10 ⊢ (𝑏 = 𝑥 → (((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) ↔ ((#‘𝑥) − (#‘(𝑥 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠)))))
77	76	rspcva 3307	. . . . . . . . 9 ⊢ ((𝑥 ∈ Fin ∧ ∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠)))) → ((#‘𝑥) − (#‘(𝑥 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠))))
78	77	adantll 750	. . . . . . . 8 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠)))) → ((#‘𝑥) − (#‘(𝑥 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠))))
79		simpr 477	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → 𝑥 ∈ Fin)
80		inss1 3833	. . . . . . . . . 10 ⊢ (𝑥 ∩ 𝑧) ⊆ 𝑥
81		ssfi 8180	. . . . . . . . . 10 ⊢ ((𝑥 ∈ Fin ∧ (𝑥 ∩ 𝑧) ⊆ 𝑥) → (𝑥 ∩ 𝑧) ∈ Fin)
82	79, 80, 81	sylancl 694	. . . . . . . . 9 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (𝑥 ∩ 𝑧) ∈ Fin)
83		fveq2 6191	. . . . . . . . . . . 12 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → (#‘𝑏) = (#‘(𝑥 ∩ 𝑧)))
84		ineq1 3807	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → (𝑏 ∩ ∪ 𝑦) = ((𝑥 ∩ 𝑧) ∩ ∪ 𝑦))
85		in32 3825	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∩ 𝑧) ∩ ∪ 𝑦) = ((𝑥 ∩ ∪ 𝑦) ∩ 𝑧)
86		inass 3823	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∩ ∪ 𝑦) ∩ 𝑧) = (𝑥 ∩ (∪ 𝑦 ∩ 𝑧))
87	85, 86	eqtri 2644	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∩ 𝑧) ∩ ∪ 𝑦) = (𝑥 ∩ (∪ 𝑦 ∩ 𝑧))
88	84, 87	syl6eq 2672	. . . . . . . . . . . . 13 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → (𝑏 ∩ ∪ 𝑦) = (𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))
89	88	fveq2d 6195	. . . . . . . . . . . 12 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → (#‘(𝑏 ∩ ∪ 𝑦)) = (#‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))))
90	83, 89	oveq12d 6668	. . . . . . . . . . 11 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑦))) = ((#‘(𝑥 ∩ 𝑧)) − (#‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))))
91		ineq1 3807	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → (𝑏 ∩ ∩ 𝑠) = ((𝑥 ∩ 𝑧) ∩ ∩ 𝑠))
92		in32 3825	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∩ 𝑧) ∩ ∩ 𝑠) = ((𝑥 ∩ ∩ 𝑠) ∩ 𝑧)
93		inass 3823	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∩ ∩ 𝑠) ∩ 𝑧) = (𝑥 ∩ (∩ 𝑠 ∩ 𝑧))
94	92, 93	eqtri 2644	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∩ 𝑧) ∩ ∩ 𝑠) = (𝑥 ∩ (∩ 𝑠 ∩ 𝑧))
95	91, 94	syl6eq 2672	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → (𝑏 ∩ ∩ 𝑠) = (𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))
96	95	fveq2d 6195	. . . . . . . . . . . . 13 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → (#‘(𝑏 ∩ ∩ 𝑠)) = (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))))
97	96	oveq2d 6666	. . . . . . . . . . . 12 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → ((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) = ((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
98	97	sumeq2sdv 14435	. . . . . . . . . . 11 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
99	90, 98	eqeq12d 2637	. . . . . . . . . 10 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → (((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) ↔ ((#‘(𝑥 ∩ 𝑧)) − (#‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))))))
100	99	rspcva 3307	. . . . . . . . 9 ⊢ (((𝑥 ∩ 𝑧) ∈ Fin ∧ ∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠)))) → ((#‘(𝑥 ∩ 𝑧)) − (#‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
101	82, 100	sylan 488	. . . . . . . 8 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠)))) → ((#‘(𝑥 ∩ 𝑧)) − (#‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
102	78, 101	oveq12d 6668	. . . . . . 7 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠)))) → (((#‘𝑥) − (#‘(𝑥 ∩ ∪ 𝑦))) − ((#‘(𝑥 ∩ 𝑧)) − (#‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))))) = (Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠))) − Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))))))
103		inss1 3833	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∩ ∪ 𝑦) ⊆ 𝑥
104		ssfi 8180	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ Fin ∧ (𝑥 ∩ ∪ 𝑦) ⊆ 𝑥) → (𝑥 ∩ ∪ 𝑦) ∈ Fin)
105	79, 103, 104	sylancl 694	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (𝑥 ∩ ∪ 𝑦) ∈ Fin)
106		hashun3 13173	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∩ ∪ 𝑦) ∈ Fin ∧ (𝑥 ∩ 𝑧) ∈ Fin) → (#‘((𝑥 ∩ ∪ 𝑦) ∪ (𝑥 ∩ 𝑧))) = (((#‘(𝑥 ∩ ∪ 𝑦)) + (#‘(𝑥 ∩ 𝑧))) − (#‘((𝑥 ∩ ∪ 𝑦) ∩ (𝑥 ∩ 𝑧)))))
107	105, 82, 106	syl2anc 693	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (#‘((𝑥 ∩ ∪ 𝑦) ∪ (𝑥 ∩ 𝑧))) = (((#‘(𝑥 ∩ ∪ 𝑦)) + (#‘(𝑥 ∩ 𝑧))) − (#‘((𝑥 ∩ ∪ 𝑦) ∩ (𝑥 ∩ 𝑧)))))
108		indi 3873	. . . . . . . . . . . . 13 ⊢ (𝑥 ∩ (∪ 𝑦 ∪ 𝑧)) = ((𝑥 ∩ ∪ 𝑦) ∪ (𝑥 ∩ 𝑧))
109	108	fveq2i 6194	. . . . . . . . . . . 12 ⊢ (#‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧))) = (#‘((𝑥 ∩ ∪ 𝑦) ∪ (𝑥 ∩ 𝑧)))
110		inindi 3830	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∩ (∪ 𝑦 ∩ 𝑧)) = ((𝑥 ∩ ∪ 𝑦) ∩ (𝑥 ∩ 𝑧))
111	110	fveq2i 6194	. . . . . . . . . . . . 13 ⊢ (#‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))) = (#‘((𝑥 ∩ ∪ 𝑦) ∩ (𝑥 ∩ 𝑧)))
112	111	oveq2i 6661	. . . . . . . . . . . 12 ⊢ (((#‘(𝑥 ∩ ∪ 𝑦)) + (#‘(𝑥 ∩ 𝑧))) − (#‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))) = (((#‘(𝑥 ∩ ∪ 𝑦)) + (#‘(𝑥 ∩ 𝑧))) − (#‘((𝑥 ∩ ∪ 𝑦) ∩ (𝑥 ∩ 𝑧))))
113	107, 109, 112	3eqtr4g 2681	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (#‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧))) = (((#‘(𝑥 ∩ ∪ 𝑦)) + (#‘(𝑥 ∩ 𝑧))) − (#‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))))
114		hashcl 13147	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∩ ∪ 𝑦) ∈ Fin → (#‘(𝑥 ∩ ∪ 𝑦)) ∈ ℕ₀)
115	105, 114	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (#‘(𝑥 ∩ ∪ 𝑦)) ∈ ℕ₀)
116	115	nn0cnd 11353	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (#‘(𝑥 ∩ ∪ 𝑦)) ∈ ℂ)
117		hashcl 13147	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∩ 𝑧) ∈ Fin → (#‘(𝑥 ∩ 𝑧)) ∈ ℕ₀)
118	82, 117	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (#‘(𝑥 ∩ 𝑧)) ∈ ℕ₀)
119	118	nn0cnd 11353	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (#‘(𝑥 ∩ 𝑧)) ∈ ℂ)
120		inss1 3833	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∩ (∪ 𝑦 ∩ 𝑧)) ⊆ 𝑥
121		ssfi 8180	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ Fin ∧ (𝑥 ∩ (∪ 𝑦 ∩ 𝑧)) ⊆ 𝑥) → (𝑥 ∩ (∪ 𝑦 ∩ 𝑧)) ∈ Fin)
122	79, 120, 121	sylancl 694	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (𝑥 ∩ (∪ 𝑦 ∩ 𝑧)) ∈ Fin)
123		hashcl 13147	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∩ (∪ 𝑦 ∩ 𝑧)) ∈ Fin → (#‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))) ∈ ℕ₀)
124	122, 123	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (#‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))) ∈ ℕ₀)
125	124	nn0cnd 11353	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (#‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))) ∈ ℂ)
126	116, 119, 125	addsubassd 10412	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (((#‘(𝑥 ∩ ∪ 𝑦)) + (#‘(𝑥 ∩ 𝑧))) − (#‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))) = ((#‘(𝑥 ∩ ∪ 𝑦)) + ((#‘(𝑥 ∩ 𝑧)) − (#‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))))))
127	113, 126	eqtrd 2656	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (#‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧))) = ((#‘(𝑥 ∩ ∪ 𝑦)) + ((#‘(𝑥 ∩ 𝑧)) − (#‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))))))
128	127	oveq2d 6666	. . . . . . . . 9 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → ((#‘𝑥) − (#‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))) = ((#‘𝑥) − ((#‘(𝑥 ∩ ∪ 𝑦)) + ((#‘(𝑥 ∩ 𝑧)) − (#‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))))))
129		hashcl 13147	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ Fin → (#‘𝑥) ∈ ℕ₀)
130	129	adantl 482	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (#‘𝑥) ∈ ℕ₀)
131	130	nn0cnd 11353	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (#‘𝑥) ∈ ℂ)
132	119, 125	subcld 10392	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → ((#‘(𝑥 ∩ 𝑧)) − (#‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))) ∈ ℂ)
133	131, 116, 132	subsub4d 10423	. . . . . . . . 9 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (((#‘𝑥) − (#‘(𝑥 ∩ ∪ 𝑦))) − ((#‘(𝑥 ∩ 𝑧)) − (#‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))))) = ((#‘𝑥) − ((#‘(𝑥 ∩ ∪ 𝑦)) + ((#‘(𝑥 ∩ 𝑧)) − (#‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))))))
134	128, 133	eqtr4d 2659	. . . . . . . 8 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → ((#‘𝑥) − (#‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))) = (((#‘𝑥) − (#‘(𝑥 ∩ ∪ 𝑦))) − ((#‘(𝑥 ∩ 𝑧)) − (#‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))))))
135	134	adantr 481	. . . . . . 7 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠)))) → ((#‘𝑥) − (#‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))) = (((#‘𝑥) − (#‘(𝑥 ∩ ∪ 𝑦))) − ((#‘(𝑥 ∩ 𝑧)) − (#‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))))))
136		disjdif 4040	. . . . . . . . . . 11 ⊢ (𝒫 𝑦 ∩ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) = ∅
137	136	a1i 11	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (𝒫 𝑦 ∩ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) = ∅)
138		ssun1 3776	. . . . . . . . . . . . . 14 ⊢ 𝑦 ⊆ (𝑦 ∪ {𝑧})
139		sspwb 4917	. . . . . . . . . . . . . 14 ⊢ (𝑦 ⊆ (𝑦 ∪ {𝑧}) ↔ 𝒫 𝑦 ⊆ 𝒫 (𝑦 ∪ {𝑧}))
140	138, 139	mpbi 220	. . . . . . . . . . . . 13 ⊢ 𝒫 𝑦 ⊆ 𝒫 (𝑦 ∪ {𝑧})
141		undif 4049	. . . . . . . . . . . . 13 ⊢ (𝒫 𝑦 ⊆ 𝒫 (𝑦 ∪ {𝑧}) ↔ (𝒫 𝑦 ∪ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) = 𝒫 (𝑦 ∪ {𝑧}))
142	140, 141	mpbi 220	. . . . . . . . . . . 12 ⊢ (𝒫 𝑦 ∪ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) = 𝒫 (𝑦 ∪ {𝑧})
143	142	eqcomi 2631	. . . . . . . . . . 11 ⊢ 𝒫 (𝑦 ∪ {𝑧}) = (𝒫 𝑦 ∪ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))
144	143	a1i 11	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → 𝒫 (𝑦 ∪ {𝑧}) = (𝒫 𝑦 ∪ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)))
145		simpll 790	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → 𝑦 ∈ Fin)
146		snfi 8038	. . . . . . . . . . . 12 ⊢ {𝑧} ∈ Fin
147		unfi 8227	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝑦 ∪ {𝑧}) ∈ Fin)
148	145, 146, 147	sylancl 694	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (𝑦 ∪ {𝑧}) ∈ Fin)
149		pwfi 8261	. . . . . . . . . . 11 ⊢ ((𝑦 ∪ {𝑧}) ∈ Fin ↔ 𝒫 (𝑦 ∪ {𝑧}) ∈ Fin)
150	148, 149	sylib 208	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → 𝒫 (𝑦 ∪ {𝑧}) ∈ Fin)
151	55	a1i 11	. . . . . . . . . . . 12 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → -1 ∈ ℂ)
152		elpwi 4168	. . . . . . . . . . . . . 14 ⊢ (𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧}) → 𝑠 ⊆ (𝑦 ∪ {𝑧}))
153		ssfi 8180	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∪ {𝑧}) ∈ Fin ∧ 𝑠 ⊆ (𝑦 ∪ {𝑧})) → 𝑠 ∈ Fin)
154	148, 152, 153	syl2an 494	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → 𝑠 ∈ Fin)
155		hashcl 13147	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ Fin → (#‘𝑠) ∈ ℕ₀)
156	154, 155	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (#‘𝑠) ∈ ℕ₀)
157	151, 156	expcld 13008	. . . . . . . . . . 11 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (-1↑(#‘𝑠)) ∈ ℂ)
158		simplr 792	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → 𝑥 ∈ Fin)
159		inss1 3833	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∩ ∩ 𝑠) ⊆ 𝑥
160		ssfi 8180	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ Fin ∧ (𝑥 ∩ ∩ 𝑠) ⊆ 𝑥) → (𝑥 ∩ ∩ 𝑠) ∈ Fin)
161	158, 159, 160	sylancl 694	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (𝑥 ∩ ∩ 𝑠) ∈ Fin)
162		hashcl 13147	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∩ ∩ 𝑠) ∈ Fin → (#‘(𝑥 ∩ ∩ 𝑠)) ∈ ℕ₀)
163	161, 162	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (#‘(𝑥 ∩ ∩ 𝑠)) ∈ ℕ₀)
164	163	nn0cnd 11353	. . . . . . . . . . 11 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (#‘(𝑥 ∩ ∩ 𝑠)) ∈ ℂ)
165	157, 164	mulcld 10060	. . . . . . . . . 10 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → ((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠))) ∈ ℂ)
166	137, 144, 150, 165	fsumsplit 14471	. . . . . . . . 9 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠))) = (Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠))) + Σ𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠)))))
167		fveq2 6191	. . . . . . . . . . . . . 14 ⊢ (𝑠 = (𝑡 ∪ {𝑧}) → (#‘𝑠) = (#‘(𝑡 ∪ {𝑧})))
168	167	oveq2d 6666	. . . . . . . . . . . . 13 ⊢ (𝑠 = (𝑡 ∪ {𝑧}) → (-1↑(#‘𝑠)) = (-1↑(#‘(𝑡 ∪ {𝑧}))))
169		inteq 4478	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = (𝑡 ∪ {𝑧}) → ∩ 𝑠 = ∩ (𝑡 ∪ {𝑧}))
170	27	intunsn 4516	. . . . . . . . . . . . . . . 16 ⊢ ∩ (𝑡 ∪ {𝑧}) = (∩ 𝑡 ∩ 𝑧)
171	169, 170	syl6eq 2672	. . . . . . . . . . . . . . 15 ⊢ (𝑠 = (𝑡 ∪ {𝑧}) → ∩ 𝑠 = (∩ 𝑡 ∩ 𝑧))
172	171	ineq2d 3814	. . . . . . . . . . . . . 14 ⊢ (𝑠 = (𝑡 ∪ {𝑧}) → (𝑥 ∩ ∩ 𝑠) = (𝑥 ∩ (∩ 𝑡 ∩ 𝑧)))
173	172	fveq2d 6195	. . . . . . . . . . . . 13 ⊢ (𝑠 = (𝑡 ∪ {𝑧}) → (#‘(𝑥 ∩ ∩ 𝑠)) = (#‘(𝑥 ∩ (∩ 𝑡 ∩ 𝑧))))
174	168, 173	oveq12d 6668	. . . . . . . . . . . 12 ⊢ (𝑠 = (𝑡 ∪ {𝑧}) → ((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠))) = ((-1↑(#‘(𝑡 ∪ {𝑧}))) · (#‘(𝑥 ∩ (∩ 𝑡 ∩ 𝑧)))))
175		pwfi 8261	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ Fin ↔ 𝒫 𝑦 ∈ Fin)
176	145, 175	sylib 208	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → 𝒫 𝑦 ∈ Fin)
177		eqid 2622	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ 𝒫 𝑦 ↦ (𝑢 ∪ {𝑧})) = (𝑢 ∈ 𝒫 𝑦 ↦ (𝑢 ∪ {𝑧}))
178		elpwi 4168	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 ∈ 𝒫 𝑦 → 𝑢 ⊆ 𝑦)
179	178	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → 𝑢 ⊆ 𝑦)
180		unss1 3782	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 ⊆ 𝑦 → (𝑢 ∪ {𝑧}) ⊆ (𝑦 ∪ {𝑧}))
181	179, 180	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → (𝑢 ∪ {𝑧}) ⊆ (𝑦 ∪ {𝑧}))
182		vex 3203	. . . . . . . . . . . . . . . . 17 ⊢ 𝑢 ∈ V
183		snex 4908	. . . . . . . . . . . . . . . . 17 ⊢ {𝑧} ∈ V
184	182, 183	unex 6956	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 ∪ {𝑧}) ∈ V
185	184	elpw 4164	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 ∪ {𝑧}) ∈ 𝒫 (𝑦 ∪ {𝑧}) ↔ (𝑢 ∪ {𝑧}) ⊆ (𝑦 ∪ {𝑧}))
186	181, 185	sylibr 224	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → (𝑢 ∪ {𝑧}) ∈ 𝒫 (𝑦 ∪ {𝑧}))
187		simpllr 799	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → ¬ 𝑧 ∈ 𝑦)
188		elpwi 4168	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 ∪ {𝑧}) ∈ 𝒫 𝑦 → (𝑢 ∪ {𝑧}) ⊆ 𝑦)
189		ssun2 3777	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑧} ⊆ (𝑢 ∪ {𝑧})
190	27	snss 4316	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ (𝑢 ∪ {𝑧}) ↔ {𝑧} ⊆ (𝑢 ∪ {𝑧}))
191	189, 190	mpbir 221	. . . . . . . . . . . . . . . . 17 ⊢ 𝑧 ∈ (𝑢 ∪ {𝑧})
192	191	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → 𝑧 ∈ (𝑢 ∪ {𝑧}))
193		ssel 3597	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 ∪ {𝑧}) ⊆ 𝑦 → (𝑧 ∈ (𝑢 ∪ {𝑧}) → 𝑧 ∈ 𝑦))
194	188, 192, 193	syl2imc 41	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → ((𝑢 ∪ {𝑧}) ∈ 𝒫 𝑦 → 𝑧 ∈ 𝑦))
195	187, 194	mtod 189	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → ¬ (𝑢 ∪ {𝑧}) ∈ 𝒫 𝑦)
196	186, 195	eldifd 3585	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → (𝑢 ∪ {𝑧}) ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))
197		eldifi 3732	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦) → 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧}))
198	197	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧}))
199	198	elpwid 4170	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → 𝑠 ⊆ (𝑦 ∪ {𝑧}))
200		uncom 3757	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∪ {𝑧}) = ({𝑧} ∪ 𝑦)
201	199, 200	syl6sseq 3651	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → 𝑠 ⊆ ({𝑧} ∪ 𝑦))
202		ssundif 4052	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ⊆ ({𝑧} ∪ 𝑦) ↔ (𝑠 ∖ {𝑧}) ⊆ 𝑦)
203	201, 202	sylib 208	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → (𝑠 ∖ {𝑧}) ⊆ 𝑦)
204		vex 3203	. . . . . . . . . . . . . . 15 ⊢ 𝑦 ∈ V
205	204	elpw2 4828	. . . . . . . . . . . . . 14 ⊢ ((𝑠 ∖ {𝑧}) ∈ 𝒫 𝑦 ↔ (𝑠 ∖ {𝑧}) ⊆ 𝑦)
206	203, 205	sylibr 224	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → (𝑠 ∖ {𝑧}) ∈ 𝒫 𝑦)
207		elpwunsn 4224	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦) → 𝑧 ∈ 𝑠)
208	207	ad2antll 765	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → 𝑧 ∈ 𝑠)
209	208	snssd 4340	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → {𝑧} ⊆ 𝑠)
210		ssequn2 3786	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑧} ⊆ 𝑠 ↔ (𝑠 ∪ {𝑧}) = 𝑠)
211	209, 210	sylib 208	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → (𝑠 ∪ {𝑧}) = 𝑠)
212	211	eqcomd 2628	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → 𝑠 = (𝑠 ∪ {𝑧}))
213		uneq1 3760	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = (𝑠 ∖ {𝑧}) → (𝑢 ∪ {𝑧}) = ((𝑠 ∖ {𝑧}) ∪ {𝑧}))
214		undif1 4043	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑠 ∖ {𝑧}) ∪ {𝑧}) = (𝑠 ∪ {𝑧})
215	213, 214	syl6eq 2672	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = (𝑠 ∖ {𝑧}) → (𝑢 ∪ {𝑧}) = (𝑠 ∪ {𝑧}))
216	215	eqeq2d 2632	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = (𝑠 ∖ {𝑧}) → (𝑠 = (𝑢 ∪ {𝑧}) ↔ 𝑠 = (𝑠 ∪ {𝑧})))
217	212, 216	syl5ibrcom 237	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → (𝑢 = (𝑠 ∖ {𝑧}) → 𝑠 = (𝑢 ∪ {𝑧})))
218	178	ad2antrl 764	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → 𝑢 ⊆ 𝑦)
219		simpllr 799	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → ¬ 𝑧 ∈ 𝑦)
220	218, 219	ssneldd 3606	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → ¬ 𝑧 ∈ 𝑢)
221		difsnb 4337	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑧 ∈ 𝑢 ↔ (𝑢 ∖ {𝑧}) = 𝑢)
222	220, 221	sylib 208	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → (𝑢 ∖ {𝑧}) = 𝑢)
223	222	eqcomd 2628	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → 𝑢 = (𝑢 ∖ {𝑧}))
224		difeq1 3721	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = (𝑢 ∪ {𝑧}) → (𝑠 ∖ {𝑧}) = ((𝑢 ∪ {𝑧}) ∖ {𝑧}))
225		difun2 4048	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∪ {𝑧}) ∖ {𝑧}) = (𝑢 ∖ {𝑧})
226	224, 225	syl6eq 2672	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = (𝑢 ∪ {𝑧}) → (𝑠 ∖ {𝑧}) = (𝑢 ∖ {𝑧}))
227	226	eqeq2d 2632	. . . . . . . . . . . . . . 15 ⊢ (𝑠 = (𝑢 ∪ {𝑧}) → (𝑢 = (𝑠 ∖ {𝑧}) ↔ 𝑢 = (𝑢 ∖ {𝑧})))
228	223, 227	syl5ibrcom 237	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → (𝑠 = (𝑢 ∪ {𝑧}) → 𝑢 = (𝑠 ∖ {𝑧})))
229	217, 228	impbid 202	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → (𝑢 = (𝑠 ∖ {𝑧}) ↔ 𝑠 = (𝑢 ∪ {𝑧})))
230	177, 196, 206, 229	f1o2d 6887	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (𝑢 ∈ 𝒫 𝑦 ↦ (𝑢 ∪ {𝑧})):𝒫 𝑦–1-1-onto→(𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))
231		uneq1 3760	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝑡 → (𝑢 ∪ {𝑧}) = (𝑡 ∪ {𝑧}))
232		vex 3203	. . . . . . . . . . . . . . 15 ⊢ 𝑡 ∈ V
233	232, 183	unex 6956	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∪ {𝑧}) ∈ V
234	231, 177, 233	fvmpt 6282	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ 𝒫 𝑦 → ((𝑢 ∈ 𝒫 𝑦 ↦ (𝑢 ∪ {𝑧}))‘𝑡) = (𝑡 ∪ {𝑧}))
235	234	adantl 482	. . . . . . . . . . . 12 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑡 ∈ 𝒫 𝑦) → ((𝑢 ∈ 𝒫 𝑦 ↦ (𝑢 ∪ {𝑧}))‘𝑡) = (𝑡 ∪ {𝑧}))
236	197, 165	sylan2 491	. . . . . . . . . . . 12 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → ((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠))) ∈ ℂ)
237	174, 176, 230, 235, 236	fsumf1o 14454	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠))) = Σ𝑡 ∈ 𝒫 𝑦((-1↑(#‘(𝑡 ∪ {𝑧}))) · (#‘(𝑥 ∩ (∩ 𝑡 ∩ 𝑧)))))
238		uneq1 3760	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑠 → (𝑡 ∪ {𝑧}) = (𝑠 ∪ {𝑧}))
239	238	fveq2d 6195	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑠 → (#‘(𝑡 ∪ {𝑧})) = (#‘(𝑠 ∪ {𝑧})))
240	239	oveq2d 6666	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑠 → (-1↑(#‘(𝑡 ∪ {𝑧}))) = (-1↑(#‘(𝑠 ∪ {𝑧}))))
241		inteq 4478	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑠 → ∩ 𝑡 = ∩ 𝑠)
242	241	ineq1d 3813	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑠 → (∩ 𝑡 ∩ 𝑧) = (∩ 𝑠 ∩ 𝑧))
243	242	ineq2d 3814	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑠 → (𝑥 ∩ (∩ 𝑡 ∩ 𝑧)) = (𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))
244	243	fveq2d 6195	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑠 → (#‘(𝑥 ∩ (∩ 𝑡 ∩ 𝑧))) = (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))))
245	240, 244	oveq12d 6668	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑠 → ((-1↑(#‘(𝑡 ∪ {𝑧}))) · (#‘(𝑥 ∩ (∩ 𝑡 ∩ 𝑧)))) = ((-1↑(#‘(𝑠 ∪ {𝑧}))) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
246	245	cbvsumv 14426	. . . . . . . . . . . 12 ⊢ Σ𝑡 ∈ 𝒫 𝑦((-1↑(#‘(𝑡 ∪ {𝑧}))) · (#‘(𝑥 ∩ (∩ 𝑡 ∩ 𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘(𝑠 ∪ {𝑧}))) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))))
247	55	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → -1 ∈ ℂ)
248		elpwi 4168	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 ∈ 𝒫 𝑦 → 𝑠 ⊆ 𝑦)
249		ssfi 8180	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ Fin ∧ 𝑠 ⊆ 𝑦) → 𝑠 ∈ Fin)
250	145, 248, 249	syl2an 494	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → 𝑠 ∈ Fin)
251	250, 155	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (#‘𝑠) ∈ ℕ₀)
252	247, 251	expp1d 13009	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1↑((#‘𝑠) + 1)) = ((-1↑(#‘𝑠)) · -1))
253	248	adantl 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → 𝑠 ⊆ 𝑦)
254		simpllr 799	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ¬ 𝑧 ∈ 𝑦)
255	253, 254	ssneldd 3606	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ¬ 𝑧 ∈ 𝑠)
256		hashunsng 13181	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ V → ((𝑠 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑠) → (#‘(𝑠 ∪ {𝑧})) = ((#‘𝑠) + 1)))
257	27, 256	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑠 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑠) → (#‘(𝑠 ∪ {𝑧})) = ((#‘𝑠) + 1))
258	250, 255, 257	syl2anc 693	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (#‘(𝑠 ∪ {𝑧})) = ((#‘𝑠) + 1))
259	258	oveq2d 6666	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1↑(#‘(𝑠 ∪ {𝑧}))) = (-1↑((#‘𝑠) + 1)))
260	140	sseli 3599	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 ∈ 𝒫 𝑦 → 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧}))
261	260, 157	sylan2 491	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1↑(#‘𝑠)) ∈ ℂ)
262	247, 261	mulcomd 10061	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1 · (-1↑(#‘𝑠))) = ((-1↑(#‘𝑠)) · -1))
263	252, 259, 262	3eqtr4d 2666	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1↑(#‘(𝑠 ∪ {𝑧}))) = (-1 · (-1↑(#‘𝑠))))
264	261	mulm1d 10482	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1 · (-1↑(#‘𝑠))) = -(-1↑(#‘𝑠)))
265	263, 264	eqtrd 2656	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1↑(#‘(𝑠 ∪ {𝑧}))) = -(-1↑(#‘𝑠)))
266	265	oveq1d 6665	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ((-1↑(#‘(𝑠 ∪ {𝑧}))) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))) = (-(-1↑(#‘𝑠)) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
267		inss1 3833	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∩ (∩ 𝑠 ∩ 𝑧)) ⊆ 𝑥
268		ssfi 8180	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ Fin ∧ (𝑥 ∩ (∩ 𝑠 ∩ 𝑧)) ⊆ 𝑥) → (𝑥 ∩ (∩ 𝑠 ∩ 𝑧)) ∈ Fin)
269	158, 267, 268	sylancl 694	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (𝑥 ∩ (∩ 𝑠 ∩ 𝑧)) ∈ Fin)
270		hashcl 13147	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∩ (∩ 𝑠 ∩ 𝑧)) ∈ Fin → (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))) ∈ ℕ₀)
271	269, 270	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))) ∈ ℕ₀)
272	271	nn0cnd 11353	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))) ∈ ℂ)
273	260, 272	sylan2 491	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))) ∈ ℂ)
274	261, 273	mulneg1d 10483	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-(-1↑(#‘𝑠)) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))) = -((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
275	266, 274	eqtrd 2656	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ((-1↑(#‘(𝑠 ∪ {𝑧}))) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))) = -((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
276	275	sumeq2dv 14433	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘(𝑠 ∪ {𝑧}))) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦-((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
277	246, 276	syl5eq 2668	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑡 ∈ 𝒫 𝑦((-1↑(#‘(𝑡 ∪ {𝑧}))) · (#‘(𝑥 ∩ (∩ 𝑡 ∩ 𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦-((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
278	157, 272	mulcld 10060	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → ((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))) ∈ ℂ)
279	260, 278	sylan2 491	. . . . . . . . . . . 12 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))) ∈ ℂ)
280	176, 279	fsumneg 14519	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 𝑦-((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))) = -Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
281	237, 277, 280	3eqtrd 2660	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠))) = -Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
282	281	oveq2d 6666	. . . . . . . . 9 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠))) + Σ𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠)))) = (Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠))) + -Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))))))
283	140	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → 𝒫 𝑦 ⊆ 𝒫 (𝑦 ∪ {𝑧}))
284	283	sselda 3603	. . . . . . . . . . . 12 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧}))
285	284, 165	syldan 487	. . . . . . . . . . 11 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠))) ∈ ℂ)
286	176, 285	fsumcl 14464	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠))) ∈ ℂ)
287	284, 278	syldan 487	. . . . . . . . . . 11 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))) ∈ ℂ)
288	176, 287	fsumcl 14464	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))) ∈ ℂ)
289	286, 288	negsubd 10398	. . . . . . . . 9 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠))) + -Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))))) = (Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠))) − Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))))))
290	166, 282, 289	3eqtrd 2660	. . . . . . . 8 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠))) = (Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠))) − Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))))))
291	290	adantr 481	. . . . . . 7 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠)))) → Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠))) = (Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠))) − Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))))))
292	102, 135, 291	3eqtr4d 2666	. . . . . 6 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠)))) → ((#‘𝑥) − (#‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠))))
293	292	ex 450	. . . . 5 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) → ((#‘𝑥) − (#‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠)))))
294	293	ralrimdva 2969	. . . 4 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) → ∀𝑥 ∈ Fin ((#‘𝑥) − (#‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠)))))
295		ineq1 3807	. . . . . . . 8 ⊢ (𝑏 = 𝑥 → (𝑏 ∩ (∪ 𝑦 ∪ 𝑧)) = (𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))
296	295	fveq2d 6195	. . . . . . 7 ⊢ (𝑏 = 𝑥 → (#‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧))) = (#‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧))))
297	67, 296	oveq12d 6668	. . . . . 6 ⊢ (𝑏 = 𝑥 → ((#‘𝑏) − (#‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧)))) = ((#‘𝑥) − (#‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))))
298		ineq1 3807	. . . . . . . . 9 ⊢ (𝑏 = 𝑥 → (𝑏 ∩ ∩ 𝑠) = (𝑥 ∩ ∩ 𝑠))
299	298	fveq2d 6195	. . . . . . . 8 ⊢ (𝑏 = 𝑥 → (#‘(𝑏 ∩ ∩ 𝑠)) = (#‘(𝑥 ∩ ∩ 𝑠)))
300	299	oveq2d 6666	. . . . . . 7 ⊢ (𝑏 = 𝑥 → ((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) = ((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠))))
301	300	sumeq2sdv 14435	. . . . . 6 ⊢ (𝑏 = 𝑥 → Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠))))
302	297, 301	eqeq12d 2637	. . . . 5 ⊢ (𝑏 = 𝑥 → (((#‘𝑏) − (#‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) ↔ ((#‘𝑥) − (#‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠)))))
303	302	cbvralv 3171	. . . 4 ⊢ (∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) ↔ ∀𝑥 ∈ Fin ((#‘𝑥) − (#‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ∩ 𝑠))))
304	294, 303	syl6ibr 242	. . 3 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) → ∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠)))))
305	16, 24, 38, 46, 66, 304	findcard2s 8201	. 2 ⊢ (𝐴 ∈ Fin → ∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))))
306		fveq2 6191	. . . . 5 ⊢ (𝑏 = 𝐵 → (#‘𝑏) = (#‘𝐵))
307		ineq1 3807	. . . . . 6 ⊢ (𝑏 = 𝐵 → (𝑏 ∩ ∪ 𝐴) = (𝐵 ∩ ∪ 𝐴))
308	307	fveq2d 6195	. . . . 5 ⊢ (𝑏 = 𝐵 → (#‘(𝑏 ∩ ∪ 𝐴)) = (#‘(𝐵 ∩ ∪ 𝐴)))
309	306, 308	oveq12d 6668	. . . 4 ⊢ (𝑏 = 𝐵 → ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝐴))) = ((#‘𝐵) − (#‘(𝐵 ∩ ∪ 𝐴))))
310		simpl 473	. . . . . . . 8 ⊢ ((𝑏 = 𝐵 ∧ 𝑠 ∈ 𝒫 𝐴) → 𝑏 = 𝐵)
311	310	ineq1d 3813	. . . . . . 7 ⊢ ((𝑏 = 𝐵 ∧ 𝑠 ∈ 𝒫 𝐴) → (𝑏 ∩ ∩ 𝑠) = (𝐵 ∩ ∩ 𝑠))
312	311	fveq2d 6195	. . . . . 6 ⊢ ((𝑏 = 𝐵 ∧ 𝑠 ∈ 𝒫 𝐴) → (#‘(𝑏 ∩ ∩ 𝑠)) = (#‘(𝐵 ∩ ∩ 𝑠)))
313	312	oveq2d 6666	. . . . 5 ⊢ ((𝑏 = 𝐵 ∧ 𝑠 ∈ 𝒫 𝐴) → ((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) = ((-1↑(#‘𝑠)) · (#‘(𝐵 ∩ ∩ 𝑠))))
314	313	sumeq2dv 14433	. . . 4 ⊢ (𝑏 = 𝐵 → Σ𝑠 ∈ 𝒫 𝐴((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(#‘𝑠)) · (#‘(𝐵 ∩ ∩ 𝑠))))
315	309, 314	eqeq12d 2637	. . 3 ⊢ (𝑏 = 𝐵 → (((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) ↔ ((#‘𝐵) − (#‘(𝐵 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(#‘𝑠)) · (#‘(𝐵 ∩ ∩ 𝑠)))))
316	315	rspccva 3308	. 2 ⊢ ((∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(#‘𝑠)) · (#‘(𝑏 ∩ ∩ 𝑠))) ∧ 𝐵 ∈ Fin) → ((#‘𝐵) − (#‘(𝐵 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(#‘𝑠)) · (#‘(𝐵 ∩ ∩ 𝑠))))
317	305, 316	sylan 488	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((#‘𝐵) − (#‘(𝐵 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(#‘𝑠)) · (#‘(𝐵 ∩ ∩ 𝑠))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 384 = wceq 1483 ∈ wcel 1990 ∀wral 2912 Vcvv 3200 ∖ cdif 3571 ∪ cun 3572 ∩ cin 3573 ⊆ wss 3574 ∅c0 3915 𝒫 cpw 4158 {csn 4177 ∪ cuni 4436 ∩ cint 4475 ↦ cmpt 4729 ‘cfv 5888 (class class class)co 6650 Fincfn 7955 ℂcc 9934 0cc0 9936 1c1 9937 + caddc 9939 · cmul 9941 − cmin 10266 -cneg 10267 ℕ₀cn0 11292 ↑cexp 12860 #chash 13117 Σcsu 14416

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-2o 7561 df-oadd 7564 df-er 7742 df-map 7859 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-sup 8348 df-oi 8415 df-card 8765 df-cda 8990 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-n0 11293 df-z 11378 df-uz 11688 df-rp 11833 df-fz 12327 df-fzo 12466 df-seq 12802 df-exp 12861 df-hash 13118 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-clim 14219 df-sum 14417

This theorem is referenced by: incexc 14569

W3C validator