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 15194

Description: Lemma for incexc 15195. (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 4852	. . . . . . . . . . 11 ⊢ (𝑥 = ∅ → ∪ 𝑥 = ∪ ∅)
2		uni0 4869	. . . . . . . . . . 11 ⊢ ∪ ∅ = ∅
3	1, 2	syl6eq 2875	. . . . . . . . . 10 ⊢ (𝑥 = ∅ → ∪ 𝑥 = ∅)
4	3	ineq2d 4192	. . . . . . . . 9 ⊢ (𝑥 = ∅ → (𝑏 ∩ ∪ 𝑥) = (𝑏 ∩ ∅))
5		in0 4348	. . . . . . . . 9 ⊢ (𝑏 ∩ ∅) = ∅
6	4, 5	syl6eq 2875	. . . . . . . 8 ⊢ (𝑥 = ∅ → (𝑏 ∩ ∪ 𝑥) = ∅)
7	6	fveq2d 6677	. . . . . . 7 ⊢ (𝑥 = ∅ → (♯‘(𝑏 ∩ ∪ 𝑥)) = (♯‘∅))
8		hash0 13731	. . . . . . 7 ⊢ (♯‘∅) = 0
9	7, 8	syl6eq 2875	. . . . . 6 ⊢ (𝑥 = ∅ → (♯‘(𝑏 ∩ ∪ 𝑥)) = 0)
10	9	oveq2d 7175	. . . . 5 ⊢ (𝑥 = ∅ → ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = ((♯‘𝑏) − 0))
11		pweq 4558	. . . . . . 7 ⊢ (𝑥 = ∅ → 𝒫 𝑥 = 𝒫 ∅)
12		pw0 4748	. . . . . . 7 ⊢ 𝒫 ∅ = {∅}
13	11, 12	syl6eq 2875	. . . . . 6 ⊢ (𝑥 = ∅ → 𝒫 𝑥 = {∅})
14	13	sumeq1d 15061	. . . . 5 ⊢ (𝑥 = ∅ → Σ𝑠 ∈ 𝒫 𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) = Σ𝑠 ∈ {∅} ((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))))
15	10, 14	eqeq12d 2840	. . . 4 ⊢ (𝑥 = ∅ → (((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) ↔ ((♯‘𝑏) − 0) = Σ𝑠 ∈ {∅} ((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))))
16	15	ralbidv 3200	. . 3 ⊢ (𝑥 = ∅ → (∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) ↔ ∀𝑏 ∈ Fin ((♯‘𝑏) − 0) = Σ𝑠 ∈ {∅} ((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))))
17		unieq 4852	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ∪ 𝑥 = ∪ 𝑦)
18	17	ineq2d 4192	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑏 ∩ ∪ 𝑥) = (𝑏 ∩ ∪ 𝑦))
19	18	fveq2d 6677	. . . . . 6 ⊢ (𝑥 = 𝑦 → (♯‘(𝑏 ∩ ∪ 𝑥)) = (♯‘(𝑏 ∩ ∪ 𝑦)))
20	19	oveq2d 7175	. . . . 5 ⊢ (𝑥 = 𝑦 → ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))))
21		pweq 4558	. . . . . 6 ⊢ (𝑥 = 𝑦 → 𝒫 𝑥 = 𝒫 𝑦)
22	21	sumeq1d 15061	. . . . 5 ⊢ (𝑥 = 𝑦 → Σ𝑠 ∈ 𝒫 𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))))
23	20, 22	eqeq12d 2840	. . . 4 ⊢ (𝑥 = 𝑦 → (((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) ↔ ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))))
24	23	ralbidv 3200	. . 3 ⊢ (𝑥 = 𝑦 → (∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) ↔ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))))
25		unieq 4852	. . . . . . . . 9 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ∪ 𝑥 = ∪ (𝑦 ∪ {𝑧}))
26		uniun 4864	. . . . . . . . . 10 ⊢ ∪ (𝑦 ∪ {𝑧}) = (∪ 𝑦 ∪ ∪ {𝑧})
27		vex 3500	. . . . . . . . . . . 12 ⊢ 𝑧 ∈ V
28	27	unisn 4861	. . . . . . . . . . 11 ⊢ ∪ {𝑧} = 𝑧
29	28	uneq2i 4139	. . . . . . . . . 10 ⊢ (∪ 𝑦 ∪ ∪ {𝑧}) = (∪ 𝑦 ∪ 𝑧)
30	26, 29	eqtri 2847	. . . . . . . . 9 ⊢ ∪ (𝑦 ∪ {𝑧}) = (∪ 𝑦 ∪ 𝑧)
31	25, 30	syl6eq 2875	. . . . . . . 8 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ∪ 𝑥 = (∪ 𝑦 ∪ 𝑧))
32	31	ineq2d 4192	. . . . . . 7 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑏 ∩ ∪ 𝑥) = (𝑏 ∩ (∪ 𝑦 ∪ 𝑧)))
33	32	fveq2d 6677	. . . . . 6 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (♯‘(𝑏 ∩ ∪ 𝑥)) = (♯‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧))))
34	33	oveq2d 7175	. . . . 5 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = ((♯‘𝑏) − (♯‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧)))))
35		pweq 4558	. . . . . 6 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → 𝒫 𝑥 = 𝒫 (𝑦 ∪ {𝑧}))
36	35	sumeq1d 15061	. . . . 5 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → Σ𝑠 ∈ 𝒫 𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))))
37	34, 36	eqeq12d 2840	. . . 4 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) ↔ ((♯‘𝑏) − (♯‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))))
38	37	ralbidv 3200	. . 3 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) ↔ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))))
39		unieq 4852	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴)
40	39	ineq2d 4192	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (𝑏 ∩ ∪ 𝑥) = (𝑏 ∩ ∪ 𝐴))
41	40	fveq2d 6677	. . . . . 6 ⊢ (𝑥 = 𝐴 → (♯‘(𝑏 ∩ ∪ 𝑥)) = (♯‘(𝑏 ∩ ∪ 𝐴)))
42	41	oveq2d 7175	. . . . 5 ⊢ (𝑥 = 𝐴 → ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝐴))))
43		pweq 4558	. . . . . 6 ⊢ (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴)
44	43	sumeq1d 15061	. . . . 5 ⊢ (𝑥 = 𝐴 → Σ𝑠 ∈ 𝒫 𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))))
45	42, 44	eqeq12d 2840	. . . 4 ⊢ (𝑥 = 𝐴 → (((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) ↔ ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))))
46	45	ralbidv 3200	. . 3 ⊢ (𝑥 = 𝐴 → (∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) ↔ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))))
47		hashcl 13720	. . . . . . 7 ⊢ (𝑏 ∈ Fin → (♯‘𝑏) ∈ ℕ₀)
48	47	nn0cnd 11960	. . . . . 6 ⊢ (𝑏 ∈ Fin → (♯‘𝑏) ∈ ℂ)
49	48	mulid2d 10662	. . . . 5 ⊢ (𝑏 ∈ Fin → (1 · (♯‘𝑏)) = (♯‘𝑏))
50		0ex 5214	. . . . . 6 ⊢ ∅ ∈ V
51	49, 48	eqeltrd 2916	. . . . . 6 ⊢ (𝑏 ∈ Fin → (1 · (♯‘𝑏)) ∈ ℂ)
52		fveq2 6673	. . . . . . . . . . 11 ⊢ (𝑠 = ∅ → (♯‘𝑠) = (♯‘∅))
53	52, 8	syl6eq 2875	. . . . . . . . . 10 ⊢ (𝑠 = ∅ → (♯‘𝑠) = 0)
54	53	oveq2d 7175	. . . . . . . . 9 ⊢ (𝑠 = ∅ → (-1↑(♯‘𝑠)) = (-1↑0))
55		neg1cn 11754	. . . . . . . . . 10 ⊢ -1 ∈ ℂ
56		exp0 13436	. . . . . . . . . 10 ⊢ (-1 ∈ ℂ → (-1↑0) = 1)
57	55, 56	ax-mp 5	. . . . . . . . 9 ⊢ (-1↑0) = 1
58	54, 57	syl6eq 2875	. . . . . . . 8 ⊢ (𝑠 = ∅ → (-1↑(♯‘𝑠)) = 1)
59		rint0 4919	. . . . . . . . 9 ⊢ (𝑠 = ∅ → (𝑏 ∩ ∩ 𝑠) = 𝑏)
60	59	fveq2d 6677	. . . . . . . 8 ⊢ (𝑠 = ∅ → (♯‘(𝑏 ∩ ∩ 𝑠)) = (♯‘𝑏))
61	58, 60	oveq12d 7177	. . . . . . 7 ⊢ (𝑠 = ∅ → ((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) = (1 · (♯‘𝑏)))
62	61	sumsn 15104	. . . . . 6 ⊢ ((∅ ∈ V ∧ (1 · (♯‘𝑏)) ∈ ℂ) → Σ𝑠 ∈ {∅} ((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) = (1 · (♯‘𝑏)))
63	50, 51, 62	sylancr 589	. . . . 5 ⊢ (𝑏 ∈ Fin → Σ𝑠 ∈ {∅} ((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) = (1 · (♯‘𝑏)))
64	48	subid1d 10989	. . . . 5 ⊢ (𝑏 ∈ Fin → ((♯‘𝑏) − 0) = (♯‘𝑏))
65	49, 63, 64	3eqtr4rd 2870	. . . 4 ⊢ (𝑏 ∈ Fin → ((♯‘𝑏) − 0) = Σ𝑠 ∈ {∅} ((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))))
66	65	rgen 3151	. . 3 ⊢ ∀𝑏 ∈ Fin ((♯‘𝑏) − 0) = Σ𝑠 ∈ {∅} ((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
67		fveq2 6673	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑥 → (♯‘𝑏) = (♯‘𝑥))
68		ineq1 4184	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑥 → (𝑏 ∩ ∪ 𝑦) = (𝑥 ∩ ∪ 𝑦))
69	68	fveq2d 6677	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑥 → (♯‘(𝑏 ∩ ∪ 𝑦)) = (♯‘(𝑥 ∩ ∪ 𝑦)))
70	67, 69	oveq12d 7177	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑥 → ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = ((♯‘𝑥) − (♯‘(𝑥 ∩ ∪ 𝑦))))
71		simpl 485	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 = 𝑥 ∧ 𝑠 ∈ 𝒫 𝑦) → 𝑏 = 𝑥)
72	71	ineq1d 4191	. . . . . . . . . . . . . 14 ⊢ ((𝑏 = 𝑥 ∧ 𝑠 ∈ 𝒫 𝑦) → (𝑏 ∩ ∩ 𝑠) = (𝑥 ∩ ∩ 𝑠))
73	72	fveq2d 6677	. . . . . . . . . . . . 13 ⊢ ((𝑏 = 𝑥 ∧ 𝑠 ∈ 𝒫 𝑦) → (♯‘(𝑏 ∩ ∩ 𝑠)) = (♯‘(𝑥 ∩ ∩ 𝑠)))
74	73	oveq2d 7175	. . . . . . . . . . . 12 ⊢ ((𝑏 = 𝑥 ∧ 𝑠 ∈ 𝒫 𝑦) → ((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) = ((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))))
75	74	sumeq2dv 15063	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑥 → Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))))
76	70, 75	eqeq12d 2840	. . . . . . . . . 10 ⊢ (𝑏 = 𝑥 → (((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) ↔ ((♯‘𝑥) − (♯‘(𝑥 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))))
77	76	rspcva 3624	. . . . . . . . 9 ⊢ ((𝑥 ∈ Fin ∧ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) → ((♯‘𝑥) − (♯‘(𝑥 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))))
78	77	adantll 712	. . . . . . . 8 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) → ((♯‘𝑥) − (♯‘(𝑥 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))))
79		simpr 487	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → 𝑥 ∈ Fin)
80		inss1 4208	. . . . . . . . . 10 ⊢ (𝑥 ∩ 𝑧) ⊆ 𝑥
81		ssfi 8741	. . . . . . . . . 10 ⊢ ((𝑥 ∈ Fin ∧ (𝑥 ∩ 𝑧) ⊆ 𝑥) → (𝑥 ∩ 𝑧) ∈ Fin)
82	79, 80, 81	sylancl 588	. . . . . . . . 9 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (𝑥 ∩ 𝑧) ∈ Fin)
83		fveq2 6673	. . . . . . . . . . . 12 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → (♯‘𝑏) = (♯‘(𝑥 ∩ 𝑧)))
84		ineq1 4184	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → (𝑏 ∩ ∪ 𝑦) = ((𝑥 ∩ 𝑧) ∩ ∪ 𝑦))
85		in32 4201	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∩ 𝑧) ∩ ∪ 𝑦) = ((𝑥 ∩ ∪ 𝑦) ∩ 𝑧)
86		inass 4199	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∩ ∪ 𝑦) ∩ 𝑧) = (𝑥 ∩ (∪ 𝑦 ∩ 𝑧))
87	85, 86	eqtri 2847	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∩ 𝑧) ∩ ∪ 𝑦) = (𝑥 ∩ (∪ 𝑦 ∩ 𝑧))
88	84, 87	syl6eq 2875	. . . . . . . . . . . . 13 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → (𝑏 ∩ ∪ 𝑦) = (𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))
89	88	fveq2d 6677	. . . . . . . . . . . 12 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → (♯‘(𝑏 ∩ ∪ 𝑦)) = (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))))
90	83, 89	oveq12d 7177	. . . . . . . . . . 11 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))))
91		ineq1 4184	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → (𝑏 ∩ ∩ 𝑠) = ((𝑥 ∩ 𝑧) ∩ ∩ 𝑠))
92		in32 4201	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∩ 𝑧) ∩ ∩ 𝑠) = ((𝑥 ∩ ∩ 𝑠) ∩ 𝑧)
93		inass 4199	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∩ ∩ 𝑠) ∩ 𝑧) = (𝑥 ∩ (∩ 𝑠 ∩ 𝑧))
94	92, 93	eqtri 2847	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∩ 𝑧) ∩ ∩ 𝑠) = (𝑥 ∩ (∩ 𝑠 ∩ 𝑧))
95	91, 94	syl6eq 2875	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → (𝑏 ∩ ∩ 𝑠) = (𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))
96	95	fveq2d 6677	. . . . . . . . . . . . 13 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → (♯‘(𝑏 ∩ ∩ 𝑠)) = (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))))
97	96	oveq2d 7175	. . . . . . . . . . . 12 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → ((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) = ((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
98	97	sumeq2sdv 15064	. . . . . . . . . . 11 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
99	90, 98	eqeq12d 2840	. . . . . . . . . 10 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → (((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) ↔ ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))))))
100	99	rspcva 3624	. . . . . . . . 9 ⊢ (((𝑥 ∩ 𝑧) ∈ Fin ∧ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) → ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
101	82, 100	sylan 582	. . . . . . . 8 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) → ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
102	78, 101	oveq12d 7177	. . . . . . 7 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) → (((♯‘𝑥) − (♯‘(𝑥 ∩ ∪ 𝑦))) − ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))))) = (Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) − Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))))))
103		inss1 4208	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∩ ∪ 𝑦) ⊆ 𝑥
104		ssfi 8741	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ Fin ∧ (𝑥 ∩ ∪ 𝑦) ⊆ 𝑥) → (𝑥 ∩ ∪ 𝑦) ∈ Fin)
105	79, 103, 104	sylancl 588	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (𝑥 ∩ ∪ 𝑦) ∈ Fin)
106		hashcl 13720	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∩ ∪ 𝑦) ∈ Fin → (♯‘(𝑥 ∩ ∪ 𝑦)) ∈ ℕ₀)
107	105, 106	syl 17	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘(𝑥 ∩ ∪ 𝑦)) ∈ ℕ₀)
108	107	nn0cnd 11960	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘(𝑥 ∩ ∪ 𝑦)) ∈ ℂ)
109		hashcl 13720	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∩ 𝑧) ∈ Fin → (♯‘(𝑥 ∩ 𝑧)) ∈ ℕ₀)
110	82, 109	syl 17	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘(𝑥 ∩ 𝑧)) ∈ ℕ₀)
111	110	nn0cnd 11960	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘(𝑥 ∩ 𝑧)) ∈ ℂ)
112		inss1 4208	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∩ (∪ 𝑦 ∩ 𝑧)) ⊆ 𝑥
113		ssfi 8741	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ Fin ∧ (𝑥 ∩ (∪ 𝑦 ∩ 𝑧)) ⊆ 𝑥) → (𝑥 ∩ (∪ 𝑦 ∩ 𝑧)) ∈ Fin)
114	79, 112, 113	sylancl 588	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (𝑥 ∩ (∪ 𝑦 ∩ 𝑧)) ∈ Fin)
115		hashcl 13720	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∩ (∪ 𝑦 ∩ 𝑧)) ∈ Fin → (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))) ∈ ℕ₀)
116	114, 115	syl 17	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))) ∈ ℕ₀)
117	116	nn0cnd 11960	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))) ∈ ℂ)
118		hashun3 13748	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∩ ∪ 𝑦) ∈ Fin ∧ (𝑥 ∩ 𝑧) ∈ Fin) → (♯‘((𝑥 ∩ ∪ 𝑦) ∪ (𝑥 ∩ 𝑧))) = (((♯‘(𝑥 ∩ ∪ 𝑦)) + (♯‘(𝑥 ∩ 𝑧))) − (♯‘((𝑥 ∩ ∪ 𝑦) ∩ (𝑥 ∩ 𝑧)))))
119	105, 82, 118	syl2anc 586	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘((𝑥 ∩ ∪ 𝑦) ∪ (𝑥 ∩ 𝑧))) = (((♯‘(𝑥 ∩ ∪ 𝑦)) + (♯‘(𝑥 ∩ 𝑧))) − (♯‘((𝑥 ∩ ∪ 𝑦) ∩ (𝑥 ∩ 𝑧)))))
120		indi 4253	. . . . . . . . . . . . 13 ⊢ (𝑥 ∩ (∪ 𝑦 ∪ 𝑧)) = ((𝑥 ∩ ∪ 𝑦) ∪ (𝑥 ∩ 𝑧))
121	120	fveq2i 6676	. . . . . . . . . . . 12 ⊢ (♯‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧))) = (♯‘((𝑥 ∩ ∪ 𝑦) ∪ (𝑥 ∩ 𝑧)))
122		inindi 4206	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∩ (∪ 𝑦 ∩ 𝑧)) = ((𝑥 ∩ ∪ 𝑦) ∩ (𝑥 ∩ 𝑧))
123	122	fveq2i 6676	. . . . . . . . . . . . 13 ⊢ (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))) = (♯‘((𝑥 ∩ ∪ 𝑦) ∩ (𝑥 ∩ 𝑧)))
124	123	oveq2i 7170	. . . . . . . . . . . 12 ⊢ (((♯‘(𝑥 ∩ ∪ 𝑦)) + (♯‘(𝑥 ∩ 𝑧))) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))) = (((♯‘(𝑥 ∩ ∪ 𝑦)) + (♯‘(𝑥 ∩ 𝑧))) − (♯‘((𝑥 ∩ ∪ 𝑦) ∩ (𝑥 ∩ 𝑧))))
125	119, 121, 124	3eqtr4g 2884	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧))) = (((♯‘(𝑥 ∩ ∪ 𝑦)) + (♯‘(𝑥 ∩ 𝑧))) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))))
126	108, 111, 117, 125	assraddsubd 11057	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧))) = ((♯‘(𝑥 ∩ ∪ 𝑦)) + ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))))))
127	126	oveq2d 7175	. . . . . . . . 9 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → ((♯‘𝑥) − (♯‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))) = ((♯‘𝑥) − ((♯‘(𝑥 ∩ ∪ 𝑦)) + ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))))))
128		hashcl 13720	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ Fin → (♯‘𝑥) ∈ ℕ₀)
129	128	adantl 484	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘𝑥) ∈ ℕ₀)
130	129	nn0cnd 11960	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘𝑥) ∈ ℂ)
131	111, 117	subcld 11000	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))) ∈ ℂ)
132	130, 108, 131	subsub4d 11031	. . . . . . . . 9 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (((♯‘𝑥) − (♯‘(𝑥 ∩ ∪ 𝑦))) − ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))))) = ((♯‘𝑥) − ((♯‘(𝑥 ∩ ∪ 𝑦)) + ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))))))
133	127, 132	eqtr4d 2862	. . . . . . . 8 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → ((♯‘𝑥) − (♯‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))) = (((♯‘𝑥) − (♯‘(𝑥 ∩ ∪ 𝑦))) − ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))))))
134	133	adantr 483	. . . . . . 7 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) → ((♯‘𝑥) − (♯‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))) = (((♯‘𝑥) − (♯‘(𝑥 ∩ ∪ 𝑦))) − ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))))))
135		disjdif 4424	. . . . . . . . . . 11 ⊢ (𝒫 𝑦 ∩ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) = ∅
136	135	a1i 11	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (𝒫 𝑦 ∩ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) = ∅)
137		ssun1 4151	. . . . . . . . . . . . . 14 ⊢ 𝑦 ⊆ (𝑦 ∪ {𝑧})
138	137	sspwi 4556	. . . . . . . . . . . . 13 ⊢ 𝒫 𝑦 ⊆ 𝒫 (𝑦 ∪ {𝑧})
139		undif 4433	. . . . . . . . . . . . 13 ⊢ (𝒫 𝑦 ⊆ 𝒫 (𝑦 ∪ {𝑧}) ↔ (𝒫 𝑦 ∪ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) = 𝒫 (𝑦 ∪ {𝑧}))
140	138, 139	mpbi 232	. . . . . . . . . . . 12 ⊢ (𝒫 𝑦 ∪ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) = 𝒫 (𝑦 ∪ {𝑧})
141	140	eqcomi 2833	. . . . . . . . . . 11 ⊢ 𝒫 (𝑦 ∪ {𝑧}) = (𝒫 𝑦 ∪ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))
142	141	a1i 11	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → 𝒫 (𝑦 ∪ {𝑧}) = (𝒫 𝑦 ∪ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)))
143		simpll 765	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → 𝑦 ∈ Fin)
144		snfi 8597	. . . . . . . . . . . 12 ⊢ {𝑧} ∈ Fin
145		unfi 8788	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝑦 ∪ {𝑧}) ∈ Fin)
146	143, 144, 145	sylancl 588	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (𝑦 ∪ {𝑧}) ∈ Fin)
147		pwfi 8822	. . . . . . . . . . 11 ⊢ ((𝑦 ∪ {𝑧}) ∈ Fin ↔ 𝒫 (𝑦 ∪ {𝑧}) ∈ Fin)
148	146, 147	sylib 220	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → 𝒫 (𝑦 ∪ {𝑧}) ∈ Fin)
149	55	a1i 11	. . . . . . . . . . . 12 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → -1 ∈ ℂ)
150		elpwi 4551	. . . . . . . . . . . . . 14 ⊢ (𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧}) → 𝑠 ⊆ (𝑦 ∪ {𝑧}))
151		ssfi 8741	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∪ {𝑧}) ∈ Fin ∧ 𝑠 ⊆ (𝑦 ∪ {𝑧})) → 𝑠 ∈ Fin)
152	146, 150, 151	syl2an 597	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → 𝑠 ∈ Fin)
153		hashcl 13720	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ Fin → (♯‘𝑠) ∈ ℕ₀)
154	152, 153	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (♯‘𝑠) ∈ ℕ₀)
155	149, 154	expcld 13513	. . . . . . . . . . 11 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (-1↑(♯‘𝑠)) ∈ ℂ)
156		simplr 767	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → 𝑥 ∈ Fin)
157		inss1 4208	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∩ ∩ 𝑠) ⊆ 𝑥
158		ssfi 8741	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ Fin ∧ (𝑥 ∩ ∩ 𝑠) ⊆ 𝑥) → (𝑥 ∩ ∩ 𝑠) ∈ Fin)
159	156, 157, 158	sylancl 588	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (𝑥 ∩ ∩ 𝑠) ∈ Fin)
160		hashcl 13720	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∩ ∩ 𝑠) ∈ Fin → (♯‘(𝑥 ∩ ∩ 𝑠)) ∈ ℕ₀)
161	159, 160	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (♯‘(𝑥 ∩ ∩ 𝑠)) ∈ ℕ₀)
162	161	nn0cnd 11960	. . . . . . . . . . 11 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (♯‘(𝑥 ∩ ∩ 𝑠)) ∈ ℂ)
163	155, 162	mulcld 10664	. . . . . . . . . 10 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → ((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) ∈ ℂ)
164	136, 142, 148, 163	fsumsplit 15100	. . . . . . . . 9 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) = (Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) + Σ𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))))
165		fveq2 6673	. . . . . . . . . . . . . 14 ⊢ (𝑠 = (𝑡 ∪ {𝑧}) → (♯‘𝑠) = (♯‘(𝑡 ∪ {𝑧})))
166	165	oveq2d 7175	. . . . . . . . . . . . 13 ⊢ (𝑠 = (𝑡 ∪ {𝑧}) → (-1↑(♯‘𝑠)) = (-1↑(♯‘(𝑡 ∪ {𝑧}))))
167		inteq 4882	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = (𝑡 ∪ {𝑧}) → ∩ 𝑠 = ∩ (𝑡 ∪ {𝑧}))
168	27	intunsn 4918	. . . . . . . . . . . . . . . 16 ⊢ ∩ (𝑡 ∪ {𝑧}) = (∩ 𝑡 ∩ 𝑧)
169	167, 168	syl6eq 2875	. . . . . . . . . . . . . . 15 ⊢ (𝑠 = (𝑡 ∪ {𝑧}) → ∩ 𝑠 = (∩ 𝑡 ∩ 𝑧))
170	169	ineq2d 4192	. . . . . . . . . . . . . 14 ⊢ (𝑠 = (𝑡 ∪ {𝑧}) → (𝑥 ∩ ∩ 𝑠) = (𝑥 ∩ (∩ 𝑡 ∩ 𝑧)))
171	170	fveq2d 6677	. . . . . . . . . . . . 13 ⊢ (𝑠 = (𝑡 ∪ {𝑧}) → (♯‘(𝑥 ∩ ∩ 𝑠)) = (♯‘(𝑥 ∩ (∩ 𝑡 ∩ 𝑧))))
172	166, 171	oveq12d 7177	. . . . . . . . . . . 12 ⊢ (𝑠 = (𝑡 ∪ {𝑧}) → ((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) = ((-1↑(♯‘(𝑡 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑡 ∩ 𝑧)))))
173		pwfi 8822	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ Fin ↔ 𝒫 𝑦 ∈ Fin)
174	143, 173	sylib 220	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → 𝒫 𝑦 ∈ Fin)
175		eqid 2824	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ 𝒫 𝑦 ↦ (𝑢 ∪ {𝑧})) = (𝑢 ∈ 𝒫 𝑦 ↦ (𝑢 ∪ {𝑧}))
176		elpwi 4551	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 ∈ 𝒫 𝑦 → 𝑢 ⊆ 𝑦)
177	176	adantl 484	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → 𝑢 ⊆ 𝑦)
178		unss1 4158	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 ⊆ 𝑦 → (𝑢 ∪ {𝑧}) ⊆ (𝑦 ∪ {𝑧}))
179	177, 178	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → (𝑢 ∪ {𝑧}) ⊆ (𝑦 ∪ {𝑧}))
180		vex 3500	. . . . . . . . . . . . . . . . 17 ⊢ 𝑢 ∈ V
181		snex 5335	. . . . . . . . . . . . . . . . 17 ⊢ {𝑧} ∈ V
182	180, 181	unex 7472	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 ∪ {𝑧}) ∈ V
183	182	elpw 4546	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 ∪ {𝑧}) ∈ 𝒫 (𝑦 ∪ {𝑧}) ↔ (𝑢 ∪ {𝑧}) ⊆ (𝑦 ∪ {𝑧}))
184	179, 183	sylibr 236	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → (𝑢 ∪ {𝑧}) ∈ 𝒫 (𝑦 ∪ {𝑧}))
185		simpllr 774	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → ¬ 𝑧 ∈ 𝑦)
186		elpwi 4551	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 ∪ {𝑧}) ∈ 𝒫 𝑦 → (𝑢 ∪ {𝑧}) ⊆ 𝑦)
187		ssun2 4152	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑧} ⊆ (𝑢 ∪ {𝑧})
188	27	snss 4721	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ (𝑢 ∪ {𝑧}) ↔ {𝑧} ⊆ (𝑢 ∪ {𝑧}))
189	187, 188	mpbir 233	. . . . . . . . . . . . . . . . 17 ⊢ 𝑧 ∈ (𝑢 ∪ {𝑧})
190	189	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → 𝑧 ∈ (𝑢 ∪ {𝑧}))
191		ssel 3964	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 ∪ {𝑧}) ⊆ 𝑦 → (𝑧 ∈ (𝑢 ∪ {𝑧}) → 𝑧 ∈ 𝑦))
192	186, 190, 191	syl2imc 41	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → ((𝑢 ∪ {𝑧}) ∈ 𝒫 𝑦 → 𝑧 ∈ 𝑦))
193	185, 192	mtod 200	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → ¬ (𝑢 ∪ {𝑧}) ∈ 𝒫 𝑦)
194	184, 193	eldifd 3950	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → (𝑢 ∪ {𝑧}) ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))
195		eldifi 4106	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦) → 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧}))
196	195	adantl 484	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧}))
197	196	elpwid 4553	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → 𝑠 ⊆ (𝑦 ∪ {𝑧}))
198		uncom 4132	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∪ {𝑧}) = ({𝑧} ∪ 𝑦)
199	197, 198	sseqtrdi 4020	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → 𝑠 ⊆ ({𝑧} ∪ 𝑦))
200		ssundif 4436	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ⊆ ({𝑧} ∪ 𝑦) ↔ (𝑠 ∖ {𝑧}) ⊆ 𝑦)
201	199, 200	sylib 220	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → (𝑠 ∖ {𝑧}) ⊆ 𝑦)
202		vex 3500	. . . . . . . . . . . . . . 15 ⊢ 𝑦 ∈ V
203	202	elpw2 5251	. . . . . . . . . . . . . 14 ⊢ ((𝑠 ∖ {𝑧}) ∈ 𝒫 𝑦 ↔ (𝑠 ∖ {𝑧}) ⊆ 𝑦)
204	201, 203	sylibr 236	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → (𝑠 ∖ {𝑧}) ∈ 𝒫 𝑦)
205		elpwunsn 4624	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦) → 𝑧 ∈ 𝑠)
206	205	ad2antll 727	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → 𝑧 ∈ 𝑠)
207	206	snssd 4745	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → {𝑧} ⊆ 𝑠)
208		ssequn2 4162	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑧} ⊆ 𝑠 ↔ (𝑠 ∪ {𝑧}) = 𝑠)
209	207, 208	sylib 220	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → (𝑠 ∪ {𝑧}) = 𝑠)
210	209	eqcomd 2830	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → 𝑠 = (𝑠 ∪ {𝑧}))
211		uneq1 4135	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = (𝑠 ∖ {𝑧}) → (𝑢 ∪ {𝑧}) = ((𝑠 ∖ {𝑧}) ∪ {𝑧}))
212		undif1 4427	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑠 ∖ {𝑧}) ∪ {𝑧}) = (𝑠 ∪ {𝑧})
213	211, 212	syl6eq 2875	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = (𝑠 ∖ {𝑧}) → (𝑢 ∪ {𝑧}) = (𝑠 ∪ {𝑧}))
214	213	eqeq2d 2835	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = (𝑠 ∖ {𝑧}) → (𝑠 = (𝑢 ∪ {𝑧}) ↔ 𝑠 = (𝑠 ∪ {𝑧})))
215	210, 214	syl5ibrcom 249	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → (𝑢 = (𝑠 ∖ {𝑧}) → 𝑠 = (𝑢 ∪ {𝑧})))
216	176	ad2antrl 726	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → 𝑢 ⊆ 𝑦)
217		simpllr 774	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → ¬ 𝑧 ∈ 𝑦)
218	216, 217	ssneldd 3973	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → ¬ 𝑧 ∈ 𝑢)
219		difsnb 4742	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑧 ∈ 𝑢 ↔ (𝑢 ∖ {𝑧}) = 𝑢)
220	218, 219	sylib 220	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → (𝑢 ∖ {𝑧}) = 𝑢)
221	220	eqcomd 2830	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → 𝑢 = (𝑢 ∖ {𝑧}))
222		difeq1 4095	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = (𝑢 ∪ {𝑧}) → (𝑠 ∖ {𝑧}) = ((𝑢 ∪ {𝑧}) ∖ {𝑧}))
223		difun2 4432	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∪ {𝑧}) ∖ {𝑧}) = (𝑢 ∖ {𝑧})
224	222, 223	syl6eq 2875	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = (𝑢 ∪ {𝑧}) → (𝑠 ∖ {𝑧}) = (𝑢 ∖ {𝑧}))
225	224	eqeq2d 2835	. . . . . . . . . . . . . . 15 ⊢ (𝑠 = (𝑢 ∪ {𝑧}) → (𝑢 = (𝑠 ∖ {𝑧}) ↔ 𝑢 = (𝑢 ∖ {𝑧})))
226	221, 225	syl5ibrcom 249	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → (𝑠 = (𝑢 ∪ {𝑧}) → 𝑢 = (𝑠 ∖ {𝑧})))
227	215, 226	impbid 214	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → (𝑢 = (𝑠 ∖ {𝑧}) ↔ 𝑠 = (𝑢 ∪ {𝑧})))
228	175, 194, 204, 227	f1o2d 7402	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (𝑢 ∈ 𝒫 𝑦 ↦ (𝑢 ∪ {𝑧})):𝒫 𝑦–1-1-onto→(𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))
229		uneq1 4135	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝑡 → (𝑢 ∪ {𝑧}) = (𝑡 ∪ {𝑧}))
230		vex 3500	. . . . . . . . . . . . . . 15 ⊢ 𝑡 ∈ V
231	230, 181	unex 7472	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∪ {𝑧}) ∈ V
232	229, 175, 231	fvmpt 6771	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ 𝒫 𝑦 → ((𝑢 ∈ 𝒫 𝑦 ↦ (𝑢 ∪ {𝑧}))‘𝑡) = (𝑡 ∪ {𝑧}))
233	232	adantl 484	. . . . . . . . . . . 12 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑡 ∈ 𝒫 𝑦) → ((𝑢 ∈ 𝒫 𝑦 ↦ (𝑢 ∪ {𝑧}))‘𝑡) = (𝑡 ∪ {𝑧}))
234	195, 163	sylan2 594	. . . . . . . . . . . 12 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → ((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) ∈ ℂ)
235	172, 174, 228, 233, 234	fsumf1o 15083	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) = Σ𝑡 ∈ 𝒫 𝑦((-1↑(♯‘(𝑡 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑡 ∩ 𝑧)))))
236		uneq1 4135	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑠 → (𝑡 ∪ {𝑧}) = (𝑠 ∪ {𝑧}))
237	236	fveq2d 6677	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑠 → (♯‘(𝑡 ∪ {𝑧})) = (♯‘(𝑠 ∪ {𝑧})))
238	237	oveq2d 7175	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑠 → (-1↑(♯‘(𝑡 ∪ {𝑧}))) = (-1↑(♯‘(𝑠 ∪ {𝑧}))))
239		inteq 4882	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑠 → ∩ 𝑡 = ∩ 𝑠)
240	239	ineq1d 4191	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑠 → (∩ 𝑡 ∩ 𝑧) = (∩ 𝑠 ∩ 𝑧))
241	240	ineq2d 4192	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑠 → (𝑥 ∩ (∩ 𝑡 ∩ 𝑧)) = (𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))
242	241	fveq2d 6677	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑠 → (♯‘(𝑥 ∩ (∩ 𝑡 ∩ 𝑧))) = (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))))
243	238, 242	oveq12d 7177	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑠 → ((-1↑(♯‘(𝑡 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑡 ∩ 𝑧)))) = ((-1↑(♯‘(𝑠 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
244	243	cbvsumv 15056	. . . . . . . . . . . 12 ⊢ Σ𝑡 ∈ 𝒫 𝑦((-1↑(♯‘(𝑡 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑡 ∩ 𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘(𝑠 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))))
245	55	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → -1 ∈ ℂ)
246		elpwi 4551	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 ∈ 𝒫 𝑦 → 𝑠 ⊆ 𝑦)
247		ssfi 8741	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ Fin ∧ 𝑠 ⊆ 𝑦) → 𝑠 ∈ Fin)
248	143, 246, 247	syl2an 597	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → 𝑠 ∈ Fin)
249	248, 153	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (♯‘𝑠) ∈ ℕ₀)
250	245, 249	expp1d 13514	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1↑((♯‘𝑠) + 1)) = ((-1↑(♯‘𝑠)) · -1))
251	246	adantl 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → 𝑠 ⊆ 𝑦)
252		simpllr 774	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ¬ 𝑧 ∈ 𝑦)
253	251, 252	ssneldd 3973	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ¬ 𝑧 ∈ 𝑠)
254		hashunsng 13756	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ V → ((𝑠 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑠) → (♯‘(𝑠 ∪ {𝑧})) = ((♯‘𝑠) + 1)))
255	254	elv 3502	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑠 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑠) → (♯‘(𝑠 ∪ {𝑧})) = ((♯‘𝑠) + 1))
256	248, 253, 255	syl2anc 586	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (♯‘(𝑠 ∪ {𝑧})) = ((♯‘𝑠) + 1))
257	256	oveq2d 7175	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1↑(♯‘(𝑠 ∪ {𝑧}))) = (-1↑((♯‘𝑠) + 1)))
258	138	sseli 3966	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 ∈ 𝒫 𝑦 → 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧}))
259	258, 155	sylan2 594	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1↑(♯‘𝑠)) ∈ ℂ)
260	245, 259	mulcomd 10665	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1 · (-1↑(♯‘𝑠))) = ((-1↑(♯‘𝑠)) · -1))
261	250, 257, 260	3eqtr4d 2869	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1↑(♯‘(𝑠 ∪ {𝑧}))) = (-1 · (-1↑(♯‘𝑠))))
262	259	mulm1d 11095	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1 · (-1↑(♯‘𝑠))) = -(-1↑(♯‘𝑠)))
263	261, 262	eqtrd 2859	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1↑(♯‘(𝑠 ∪ {𝑧}))) = -(-1↑(♯‘𝑠)))
264	263	oveq1d 7174	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ((-1↑(♯‘(𝑠 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))) = (-(-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
265		inss1 4208	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∩ (∩ 𝑠 ∩ 𝑧)) ⊆ 𝑥
266		ssfi 8741	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ Fin ∧ (𝑥 ∩ (∩ 𝑠 ∩ 𝑧)) ⊆ 𝑥) → (𝑥 ∩ (∩ 𝑠 ∩ 𝑧)) ∈ Fin)
267	156, 265, 266	sylancl 588	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (𝑥 ∩ (∩ 𝑠 ∩ 𝑧)) ∈ Fin)
268		hashcl 13720	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∩ (∩ 𝑠 ∩ 𝑧)) ∈ Fin → (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))) ∈ ℕ₀)
269	267, 268	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))) ∈ ℕ₀)
270	269	nn0cnd 11960	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))) ∈ ℂ)
271	258, 270	sylan2 594	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))) ∈ ℂ)
272	259, 271	mulneg1d 11096	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-(-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))) = -((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
273	264, 272	eqtrd 2859	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ((-1↑(♯‘(𝑠 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))) = -((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
274	273	sumeq2dv 15063	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘(𝑠 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦-((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
275	244, 274	syl5eq 2871	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑡 ∈ 𝒫 𝑦((-1↑(♯‘(𝑡 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑡 ∩ 𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦-((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
276	155, 270	mulcld 10664	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → ((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))) ∈ ℂ)
277	258, 276	sylan2 594	. . . . . . . . . . . 12 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))) ∈ ℂ)
278	174, 277	fsumneg 15145	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 𝑦-((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))) = -Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
279	235, 275, 278	3eqtrd 2863	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) = -Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
280	279	oveq2d 7175	. . . . . . . . 9 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) + Σ𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))) = (Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) + -Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))))))
281	138	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → 𝒫 𝑦 ⊆ 𝒫 (𝑦 ∪ {𝑧}))
282	281	sselda 3970	. . . . . . . . . . . 12 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧}))
283	282, 163	syldan 593	. . . . . . . . . . 11 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) ∈ ℂ)
284	174, 283	fsumcl 15093	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) ∈ ℂ)
285	282, 276	syldan 593	. . . . . . . . . . 11 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))) ∈ ℂ)
286	174, 285	fsumcl 15093	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))) ∈ ℂ)
287	284, 286	negsubd 11006	. . . . . . . . 9 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) + -Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))))) = (Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) − Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))))))
288	164, 280, 287	3eqtrd 2863	. . . . . . . 8 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) = (Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) − Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))))))
289	288	adantr 483	. . . . . . 7 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) → Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) = (Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) − Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))))))
290	102, 134, 289	3eqtr4d 2869	. . . . . 6 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) → ((♯‘𝑥) − (♯‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))))
291	290	ex 415	. . . . 5 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) → ((♯‘𝑥) − (♯‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))))
292	291	ralrimdva 3192	. . . 4 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) → ∀𝑥 ∈ Fin ((♯‘𝑥) − (♯‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))))
293		ineq1 4184	. . . . . . . 8 ⊢ (𝑏 = 𝑥 → (𝑏 ∩ (∪ 𝑦 ∪ 𝑧)) = (𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))
294	293	fveq2d 6677	. . . . . . 7 ⊢ (𝑏 = 𝑥 → (♯‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧))) = (♯‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧))))
295	67, 294	oveq12d 7177	. . . . . 6 ⊢ (𝑏 = 𝑥 → ((♯‘𝑏) − (♯‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧)))) = ((♯‘𝑥) − (♯‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))))
296		ineq1 4184	. . . . . . . . 9 ⊢ (𝑏 = 𝑥 → (𝑏 ∩ ∩ 𝑠) = (𝑥 ∩ ∩ 𝑠))
297	296	fveq2d 6677	. . . . . . . 8 ⊢ (𝑏 = 𝑥 → (♯‘(𝑏 ∩ ∩ 𝑠)) = (♯‘(𝑥 ∩ ∩ 𝑠)))
298	297	oveq2d 7175	. . . . . . 7 ⊢ (𝑏 = 𝑥 → ((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) = ((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))))
299	298	sumeq2sdv 15064	. . . . . 6 ⊢ (𝑏 = 𝑥 → Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))))
300	295, 299	eqeq12d 2840	. . . . 5 ⊢ (𝑏 = 𝑥 → (((♯‘𝑏) − (♯‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) ↔ ((♯‘𝑥) − (♯‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))))
301	300	cbvralvw 3452	. . . 4 ⊢ (∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) ↔ ∀𝑥 ∈ Fin ((♯‘𝑥) − (♯‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))))
302	292, 301	syl6ibr 254	. . 3 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) → ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))))
303	16, 24, 38, 46, 66, 302	findcard2s 8762	. 2 ⊢ (𝐴 ∈ Fin → ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))))
304		fveq2 6673	. . . . 5 ⊢ (𝑏 = 𝐵 → (♯‘𝑏) = (♯‘𝐵))
305		ineq1 4184	. . . . . 6 ⊢ (𝑏 = 𝐵 → (𝑏 ∩ ∪ 𝐴) = (𝐵 ∩ ∪ 𝐴))
306	305	fveq2d 6677	. . . . 5 ⊢ (𝑏 = 𝐵 → (♯‘(𝑏 ∩ ∪ 𝐴)) = (♯‘(𝐵 ∩ ∪ 𝐴)))
307	304, 306	oveq12d 7177	. . . 4 ⊢ (𝑏 = 𝐵 → ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝐴))) = ((♯‘𝐵) − (♯‘(𝐵 ∩ ∪ 𝐴))))
308		simpl 485	. . . . . . . 8 ⊢ ((𝑏 = 𝐵 ∧ 𝑠 ∈ 𝒫 𝐴) → 𝑏 = 𝐵)
309	308	ineq1d 4191	. . . . . . 7 ⊢ ((𝑏 = 𝐵 ∧ 𝑠 ∈ 𝒫 𝐴) → (𝑏 ∩ ∩ 𝑠) = (𝐵 ∩ ∩ 𝑠))
310	309	fveq2d 6677	. . . . . 6 ⊢ ((𝑏 = 𝐵 ∧ 𝑠 ∈ 𝒫 𝐴) → (♯‘(𝑏 ∩ ∩ 𝑠)) = (♯‘(𝐵 ∩ ∩ 𝑠)))
311	310	oveq2d 7175	. . . . 5 ⊢ ((𝑏 = 𝐵 ∧ 𝑠 ∈ 𝒫 𝐴) → ((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) = ((-1↑(♯‘𝑠)) · (♯‘(𝐵 ∩ ∩ 𝑠))))
312	311	sumeq2dv 15063	. . . 4 ⊢ (𝑏 = 𝐵 → Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(𝐵 ∩ ∩ 𝑠))))
313	307, 312	eqeq12d 2840	. . 3 ⊢ (𝑏 = 𝐵 → (((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) ↔ ((♯‘𝐵) − (♯‘(𝐵 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(𝐵 ∩ ∩ 𝑠)))))
314	313	rspccva 3625	. 2 ⊢ ((∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) ∧ 𝐵 ∈ Fin) → ((♯‘𝐵) − (♯‘(𝐵 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(𝐵 ∩ ∩ 𝑠))))
315	303, 314	sylan 582	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((♯‘𝐵) − (♯‘(𝐵 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(𝐵 ∩ ∩ 𝑠))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 398 = wceq 1536 ∈ wcel 2113 ∀wral 3141 Vcvv 3497 ∖ cdif 3936 ∪ cun 3937 ∩ cin 3938 ⊆ wss 3939 ∅c0 4294 𝒫 cpw 4542 {csn 4570 ∪ cuni 4841 ∩ cint 4879 ↦ cmpt 5149 ‘cfv 6358 (class class class)co 7159 Fincfn 8512 ℂcc 10538 0cc0 10540 1c1 10541 + caddc 10543 · cmul 10545 − cmin 10873 -cneg 10874 ℕ₀cn0 11900 ↑cexp 13432 ♯chash 13693 Σcsu 15045

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1969 ax-7 2014 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2160 ax-12 2176 ax-ext 2796 ax-rep 5193 ax-sep 5206 ax-nul 5213 ax-pow 5269 ax-pr 5333 ax-un 7464 ax-inf2 9107 ax-cnex 10596 ax-resscn 10597 ax-1cn 10598 ax-icn 10599 ax-addcl 10600 ax-addrcl 10601 ax-mulcl 10602 ax-mulrcl 10603 ax-mulcom 10604 ax-addass 10605 ax-mulass 10606 ax-distr 10607 ax-i2m1 10608 ax-1ne0 10609 ax-1rid 10610 ax-rnegex 10611 ax-rrecex 10612 ax-cnre 10613 ax-pre-lttri 10614 ax-pre-lttrn 10615 ax-pre-ltadd 10616 ax-pre-mulgt0 10617 ax-pre-sup 10618

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1539 df-fal 1549 df-ex 1780 df-nf 1784 df-sb 2069 df-mo 2621 df-eu 2653 df-clab 2803 df-cleq 2817 df-clel 2896 df-nfc 2966 df-ne 3020 df-nel 3127 df-ral 3146 df-rex 3147 df-reu 3148 df-rmo 3149 df-rab 3150 df-v 3499 df-sbc 3776 df-csb 3887 df-dif 3942 df-un 3944 df-in 3946 df-ss 3955 df-pss 3957 df-nul 4295 df-if 4471 df-pw 4544 df-sn 4571 df-pr 4573 df-tp 4575 df-op 4577 df-uni 4842 df-int 4880 df-iun 4924 df-br 5070 df-opab 5132 df-mpt 5150 df-tr 5176 df-id 5463 df-eprel 5468 df-po 5477 df-so 5478 df-fr 5517 df-se 5518 df-we 5519 df-xp 5564 df-rel 5565 df-cnv 5566 df-co 5567 df-dm 5568 df-rn 5569 df-res 5570 df-ima 5571 df-pred 6151 df-ord 6197 df-on 6198 df-lim 6199 df-suc 6200 df-iota 6317 df-fun 6360 df-fn 6361 df-f 6362 df-f1 6363 df-fo 6364 df-f1o 6365 df-fv 6366 df-isom 6367 df-riota 7117 df-ov 7162 df-oprab 7163 df-mpo 7164 df-om 7584 df-1st 7692 df-2nd 7693 df-wrecs 7950 df-recs 8011 df-rdg 8049 df-1o 8105 df-2o 8106 df-oadd 8109 df-er 8292 df-map 8411 df-en 8513 df-dom 8514 df-sdom 8515 df-fin 8516 df-sup 8909 df-oi 8977 df-dju 9333 df-card 9371 df-pnf 10680 df-mnf 10681 df-xr 10682 df-ltxr 10683 df-le 10684 df-sub 10875 df-neg 10876 df-div 11301 df-nn 11642 df-2 11703 df-3 11704 df-n0 11901 df-z 11985 df-uz 12247 df-rp 12393 df-fz 12896 df-fzo 13037 df-seq 13373 df-exp 13433 df-hash 13694 df-cj 14461 df-re 14462 df-im 14463 df-sqrt 14597 df-abs 14598 df-clim 14848 df-sum 15046

This theorem is referenced by: incexc 15195

W3C validator