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 15802

Description: Lemma for incexc 15803. (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 4882	. . . . . . . . . . 11 ⊢ (𝑥 = ∅ → ∪ 𝑥 = ∪ ∅)
2		uni0 4899	. . . . . . . . . . 11 ⊢ ∪ ∅ = ∅
3	1, 2	eqtrdi 2780	. . . . . . . . . 10 ⊢ (𝑥 = ∅ → ∪ 𝑥 = ∅)
4	3	ineq2d 4183	. . . . . . . . 9 ⊢ (𝑥 = ∅ → (𝑏 ∩ ∪ 𝑥) = (𝑏 ∩ ∅))
5		in0 4358	. . . . . . . . 9 ⊢ (𝑏 ∩ ∅) = ∅
6	4, 5	eqtrdi 2780	. . . . . . . 8 ⊢ (𝑥 = ∅ → (𝑏 ∩ ∪ 𝑥) = ∅)
7	6	fveq2d 6862	. . . . . . 7 ⊢ (𝑥 = ∅ → (♯‘(𝑏 ∩ ∪ 𝑥)) = (♯‘∅))
8		hash0 14332	. . . . . . 7 ⊢ (♯‘∅) = 0
9	7, 8	eqtrdi 2780	. . . . . 6 ⊢ (𝑥 = ∅ → (♯‘(𝑏 ∩ ∪ 𝑥)) = 0)
10	9	oveq2d 7403	. . . . 5 ⊢ (𝑥 = ∅ → ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = ((♯‘𝑏) − 0))
11		pweq 4577	. . . . . . 7 ⊢ (𝑥 = ∅ → 𝒫 𝑥 = 𝒫 ∅)
12		pw0 4776	. . . . . . 7 ⊢ 𝒫 ∅ = {∅}
13	11, 12	eqtrdi 2780	. . . . . 6 ⊢ (𝑥 = ∅ → 𝒫 𝑥 = {∅})
14	13	sumeq1d 15666	. . . . 5 ⊢ (𝑥 = ∅ → Σ𝑠 ∈ 𝒫 𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) = Σ𝑠 ∈ {∅} ((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))))
15	10, 14	eqeq12d 2745	. . . 4 ⊢ (𝑥 = ∅ → (((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) ↔ ((♯‘𝑏) − 0) = Σ𝑠 ∈ {∅} ((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))))
16	15	ralbidv 3156	. . 3 ⊢ (𝑥 = ∅ → (∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) ↔ ∀𝑏 ∈ Fin ((♯‘𝑏) − 0) = Σ𝑠 ∈ {∅} ((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))))
17		unieq 4882	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ∪ 𝑥 = ∪ 𝑦)
18	17	ineq2d 4183	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑏 ∩ ∪ 𝑥) = (𝑏 ∩ ∪ 𝑦))
19	18	fveq2d 6862	. . . . . 6 ⊢ (𝑥 = 𝑦 → (♯‘(𝑏 ∩ ∪ 𝑥)) = (♯‘(𝑏 ∩ ∪ 𝑦)))
20	19	oveq2d 7403	. . . . 5 ⊢ (𝑥 = 𝑦 → ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))))
21		pweq 4577	. . . . . 6 ⊢ (𝑥 = 𝑦 → 𝒫 𝑥 = 𝒫 𝑦)
22	21	sumeq1d 15666	. . . . 5 ⊢ (𝑥 = 𝑦 → Σ𝑠 ∈ 𝒫 𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))))
23	20, 22	eqeq12d 2745	. . . 4 ⊢ (𝑥 = 𝑦 → (((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) ↔ ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))))
24	23	ralbidv 3156	. . 3 ⊢ (𝑥 = 𝑦 → (∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) ↔ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))))
25		unieq 4882	. . . . . . . . 9 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ∪ 𝑥 = ∪ (𝑦 ∪ {𝑧}))
26		uniun 4894	. . . . . . . . . 10 ⊢ ∪ (𝑦 ∪ {𝑧}) = (∪ 𝑦 ∪ ∪ {𝑧})
27		unisnv 4891	. . . . . . . . . . 11 ⊢ ∪ {𝑧} = 𝑧
28	27	uneq2i 4128	. . . . . . . . . 10 ⊢ (∪ 𝑦 ∪ ∪ {𝑧}) = (∪ 𝑦 ∪ 𝑧)
29	26, 28	eqtri 2752	. . . . . . . . 9 ⊢ ∪ (𝑦 ∪ {𝑧}) = (∪ 𝑦 ∪ 𝑧)
30	25, 29	eqtrdi 2780	. . . . . . . 8 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ∪ 𝑥 = (∪ 𝑦 ∪ 𝑧))
31	30	ineq2d 4183	. . . . . . 7 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑏 ∩ ∪ 𝑥) = (𝑏 ∩ (∪ 𝑦 ∪ 𝑧)))
32	31	fveq2d 6862	. . . . . 6 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (♯‘(𝑏 ∩ ∪ 𝑥)) = (♯‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧))))
33	32	oveq2d 7403	. . . . 5 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = ((♯‘𝑏) − (♯‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧)))))
34		pweq 4577	. . . . . 6 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → 𝒫 𝑥 = 𝒫 (𝑦 ∪ {𝑧}))
35	34	sumeq1d 15666	. . . . 5 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → Σ𝑠 ∈ 𝒫 𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))))
36	33, 35	eqeq12d 2745	. . . 4 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) ↔ ((♯‘𝑏) − (♯‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))))
37	36	ralbidv 3156	. . 3 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) ↔ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))))
38		unieq 4882	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴)
39	38	ineq2d 4183	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (𝑏 ∩ ∪ 𝑥) = (𝑏 ∩ ∪ 𝐴))
40	39	fveq2d 6862	. . . . . 6 ⊢ (𝑥 = 𝐴 → (♯‘(𝑏 ∩ ∪ 𝑥)) = (♯‘(𝑏 ∩ ∪ 𝐴)))
41	40	oveq2d 7403	. . . . 5 ⊢ (𝑥 = 𝐴 → ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝐴))))
42		pweq 4577	. . . . . 6 ⊢ (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴)
43	42	sumeq1d 15666	. . . . 5 ⊢ (𝑥 = 𝐴 → Σ𝑠 ∈ 𝒫 𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))))
44	41, 43	eqeq12d 2745	. . . 4 ⊢ (𝑥 = 𝐴 → (((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) ↔ ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))))
45	44	ralbidv 3156	. . 3 ⊢ (𝑥 = 𝐴 → (∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) ↔ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))))
46		hashcl 14321	. . . . . . 7 ⊢ (𝑏 ∈ Fin → (♯‘𝑏) ∈ ℕ₀)
47	46	nn0cnd 12505	. . . . . 6 ⊢ (𝑏 ∈ Fin → (♯‘𝑏) ∈ ℂ)
48	47	mullidd 11192	. . . . 5 ⊢ (𝑏 ∈ Fin → (1 · (♯‘𝑏)) = (♯‘𝑏))
49		0ex 5262	. . . . . 6 ⊢ ∅ ∈ V
50	48, 47	eqeltrd 2828	. . . . . 6 ⊢ (𝑏 ∈ Fin → (1 · (♯‘𝑏)) ∈ ℂ)
51		fveq2 6858	. . . . . . . . . . 11 ⊢ (𝑠 = ∅ → (♯‘𝑠) = (♯‘∅))
52	51, 8	eqtrdi 2780	. . . . . . . . . 10 ⊢ (𝑠 = ∅ → (♯‘𝑠) = 0)
53	52	oveq2d 7403	. . . . . . . . 9 ⊢ (𝑠 = ∅ → (-1↑(♯‘𝑠)) = (-1↑0))
54		neg1cn 12171	. . . . . . . . . 10 ⊢ -1 ∈ ℂ
55		exp0 14030	. . . . . . . . . 10 ⊢ (-1 ∈ ℂ → (-1↑0) = 1)
56	54, 55	ax-mp 5	. . . . . . . . 9 ⊢ (-1↑0) = 1
57	53, 56	eqtrdi 2780	. . . . . . . 8 ⊢ (𝑠 = ∅ → (-1↑(♯‘𝑠)) = 1)
58		rint0 4952	. . . . . . . . 9 ⊢ (𝑠 = ∅ → (𝑏 ∩ ∩ 𝑠) = 𝑏)
59	58	fveq2d 6862	. . . . . . . 8 ⊢ (𝑠 = ∅ → (♯‘(𝑏 ∩ ∩ 𝑠)) = (♯‘𝑏))
60	57, 59	oveq12d 7405	. . . . . . 7 ⊢ (𝑠 = ∅ → ((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) = (1 · (♯‘𝑏)))
61	60	sumsn 15712	. . . . . 6 ⊢ ((∅ ∈ V ∧ (1 · (♯‘𝑏)) ∈ ℂ) → Σ𝑠 ∈ {∅} ((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) = (1 · (♯‘𝑏)))
62	49, 50, 61	sylancr 587	. . . . 5 ⊢ (𝑏 ∈ Fin → Σ𝑠 ∈ {∅} ((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) = (1 · (♯‘𝑏)))
63	47	subid1d 11522	. . . . 5 ⊢ (𝑏 ∈ Fin → ((♯‘𝑏) − 0) = (♯‘𝑏))
64	48, 62, 63	3eqtr4rd 2775	. . . 4 ⊢ (𝑏 ∈ Fin → ((♯‘𝑏) − 0) = Σ𝑠 ∈ {∅} ((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))))
65	64	rgen 3046	. . 3 ⊢ ∀𝑏 ∈ Fin ((♯‘𝑏) − 0) = Σ𝑠 ∈ {∅} ((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
66		fveq2 6858	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑥 → (♯‘𝑏) = (♯‘𝑥))
67		ineq1 4176	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑥 → (𝑏 ∩ ∪ 𝑦) = (𝑥 ∩ ∪ 𝑦))
68	67	fveq2d 6862	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑥 → (♯‘(𝑏 ∩ ∪ 𝑦)) = (♯‘(𝑥 ∩ ∪ 𝑦)))
69	66, 68	oveq12d 7405	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑥 → ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = ((♯‘𝑥) − (♯‘(𝑥 ∩ ∪ 𝑦))))
70		simpl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 = 𝑥 ∧ 𝑠 ∈ 𝒫 𝑦) → 𝑏 = 𝑥)
71	70	ineq1d 4182	. . . . . . . . . . . . . 14 ⊢ ((𝑏 = 𝑥 ∧ 𝑠 ∈ 𝒫 𝑦) → (𝑏 ∩ ∩ 𝑠) = (𝑥 ∩ ∩ 𝑠))
72	71	fveq2d 6862	. . . . . . . . . . . . 13 ⊢ ((𝑏 = 𝑥 ∧ 𝑠 ∈ 𝒫 𝑦) → (♯‘(𝑏 ∩ ∩ 𝑠)) = (♯‘(𝑥 ∩ ∩ 𝑠)))
73	72	oveq2d 7403	. . . . . . . . . . . 12 ⊢ ((𝑏 = 𝑥 ∧ 𝑠 ∈ 𝒫 𝑦) → ((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) = ((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))))
74	73	sumeq2dv 15668	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑥 → Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))))
75	69, 74	eqeq12d 2745	. . . . . . . . . 10 ⊢ (𝑏 = 𝑥 → (((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) ↔ ((♯‘𝑥) − (♯‘(𝑥 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))))
76	75	rspcva 3586	. . . . . . . . 9 ⊢ ((𝑥 ∈ Fin ∧ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) → ((♯‘𝑥) − (♯‘(𝑥 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))))
77	76	adantll 714	. . . . . . . 8 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) → ((♯‘𝑥) − (♯‘(𝑥 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))))
78		simpr 484	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → 𝑥 ∈ Fin)
79		inss1 4200	. . . . . . . . . 10 ⊢ (𝑥 ∩ 𝑧) ⊆ 𝑥
80		ssfi 9137	. . . . . . . . . 10 ⊢ ((𝑥 ∈ Fin ∧ (𝑥 ∩ 𝑧) ⊆ 𝑥) → (𝑥 ∩ 𝑧) ∈ Fin)
81	78, 79, 80	sylancl 586	. . . . . . . . 9 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (𝑥 ∩ 𝑧) ∈ Fin)
82		fveq2 6858	. . . . . . . . . . . 12 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → (♯‘𝑏) = (♯‘(𝑥 ∩ 𝑧)))
83		ineq1 4176	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → (𝑏 ∩ ∪ 𝑦) = ((𝑥 ∩ 𝑧) ∩ ∪ 𝑦))
84		in32 4193	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∩ 𝑧) ∩ ∪ 𝑦) = ((𝑥 ∩ ∪ 𝑦) ∩ 𝑧)
85		inass 4191	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∩ ∪ 𝑦) ∩ 𝑧) = (𝑥 ∩ (∪ 𝑦 ∩ 𝑧))
86	84, 85	eqtri 2752	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∩ 𝑧) ∩ ∪ 𝑦) = (𝑥 ∩ (∪ 𝑦 ∩ 𝑧))
87	83, 86	eqtrdi 2780	. . . . . . . . . . . . 13 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → (𝑏 ∩ ∪ 𝑦) = (𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))
88	87	fveq2d 6862	. . . . . . . . . . . 12 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → (♯‘(𝑏 ∩ ∪ 𝑦)) = (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))))
89	82, 88	oveq12d 7405	. . . . . . . . . . 11 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))))
90		ineq1 4176	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → (𝑏 ∩ ∩ 𝑠) = ((𝑥 ∩ 𝑧) ∩ ∩ 𝑠))
91		in32 4193	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∩ 𝑧) ∩ ∩ 𝑠) = ((𝑥 ∩ ∩ 𝑠) ∩ 𝑧)
92		inass 4191	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∩ ∩ 𝑠) ∩ 𝑧) = (𝑥 ∩ (∩ 𝑠 ∩ 𝑧))
93	91, 92	eqtri 2752	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∩ 𝑧) ∩ ∩ 𝑠) = (𝑥 ∩ (∩ 𝑠 ∩ 𝑧))
94	90, 93	eqtrdi 2780	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → (𝑏 ∩ ∩ 𝑠) = (𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))
95	94	fveq2d 6862	. . . . . . . . . . . . 13 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → (♯‘(𝑏 ∩ ∩ 𝑠)) = (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))))
96	95	oveq2d 7403	. . . . . . . . . . . 12 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → ((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) = ((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
97	96	sumeq2sdv 15669	. . . . . . . . . . 11 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
98	89, 97	eqeq12d 2745	. . . . . . . . . 10 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → (((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) ↔ ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))))))
99	98	rspcva 3586	. . . . . . . . 9 ⊢ (((𝑥 ∩ 𝑧) ∈ Fin ∧ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) → ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
100	81, 99	sylan 580	. . . . . . . 8 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) → ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
101	77, 100	oveq12d 7405	. . . . . . 7 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) → (((♯‘𝑥) − (♯‘(𝑥 ∩ ∪ 𝑦))) − ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))))) = (Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) − Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))))))
102		inss1 4200	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∩ ∪ 𝑦) ⊆ 𝑥
103		ssfi 9137	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ Fin ∧ (𝑥 ∩ ∪ 𝑦) ⊆ 𝑥) → (𝑥 ∩ ∪ 𝑦) ∈ Fin)
104	78, 102, 103	sylancl 586	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (𝑥 ∩ ∪ 𝑦) ∈ Fin)
105		hashcl 14321	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∩ ∪ 𝑦) ∈ Fin → (♯‘(𝑥 ∩ ∪ 𝑦)) ∈ ℕ₀)
106	104, 105	syl 17	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘(𝑥 ∩ ∪ 𝑦)) ∈ ℕ₀)
107	106	nn0cnd 12505	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘(𝑥 ∩ ∪ 𝑦)) ∈ ℂ)
108		hashcl 14321	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∩ 𝑧) ∈ Fin → (♯‘(𝑥 ∩ 𝑧)) ∈ ℕ₀)
109	81, 108	syl 17	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘(𝑥 ∩ 𝑧)) ∈ ℕ₀)
110	109	nn0cnd 12505	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘(𝑥 ∩ 𝑧)) ∈ ℂ)
111		inss1 4200	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∩ (∪ 𝑦 ∩ 𝑧)) ⊆ 𝑥
112		ssfi 9137	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ Fin ∧ (𝑥 ∩ (∪ 𝑦 ∩ 𝑧)) ⊆ 𝑥) → (𝑥 ∩ (∪ 𝑦 ∩ 𝑧)) ∈ Fin)
113	78, 111, 112	sylancl 586	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (𝑥 ∩ (∪ 𝑦 ∩ 𝑧)) ∈ Fin)
114		hashcl 14321	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∩ (∪ 𝑦 ∩ 𝑧)) ∈ Fin → (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))) ∈ ℕ₀)
115	113, 114	syl 17	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))) ∈ ℕ₀)
116	115	nn0cnd 12505	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))) ∈ ℂ)
117		hashun3 14349	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∩ ∪ 𝑦) ∈ Fin ∧ (𝑥 ∩ 𝑧) ∈ Fin) → (♯‘((𝑥 ∩ ∪ 𝑦) ∪ (𝑥 ∩ 𝑧))) = (((♯‘(𝑥 ∩ ∪ 𝑦)) + (♯‘(𝑥 ∩ 𝑧))) − (♯‘((𝑥 ∩ ∪ 𝑦) ∩ (𝑥 ∩ 𝑧)))))
118	104, 81, 117	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘((𝑥 ∩ ∪ 𝑦) ∪ (𝑥 ∩ 𝑧))) = (((♯‘(𝑥 ∩ ∪ 𝑦)) + (♯‘(𝑥 ∩ 𝑧))) − (♯‘((𝑥 ∩ ∪ 𝑦) ∩ (𝑥 ∩ 𝑧)))))
119		indi 4247	. . . . . . . . . . . . 13 ⊢ (𝑥 ∩ (∪ 𝑦 ∪ 𝑧)) = ((𝑥 ∩ ∪ 𝑦) ∪ (𝑥 ∩ 𝑧))
120	119	fveq2i 6861	. . . . . . . . . . . 12 ⊢ (♯‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧))) = (♯‘((𝑥 ∩ ∪ 𝑦) ∪ (𝑥 ∩ 𝑧)))
121		inindi 4198	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∩ (∪ 𝑦 ∩ 𝑧)) = ((𝑥 ∩ ∪ 𝑦) ∩ (𝑥 ∩ 𝑧))
122	121	fveq2i 6861	. . . . . . . . . . . . 13 ⊢ (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))) = (♯‘((𝑥 ∩ ∪ 𝑦) ∩ (𝑥 ∩ 𝑧)))
123	122	oveq2i 7398	. . . . . . . . . . . 12 ⊢ (((♯‘(𝑥 ∩ ∪ 𝑦)) + (♯‘(𝑥 ∩ 𝑧))) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))) = (((♯‘(𝑥 ∩ ∪ 𝑦)) + (♯‘(𝑥 ∩ 𝑧))) − (♯‘((𝑥 ∩ ∪ 𝑦) ∩ (𝑥 ∩ 𝑧))))
124	118, 120, 123	3eqtr4g 2789	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧))) = (((♯‘(𝑥 ∩ ∪ 𝑦)) + (♯‘(𝑥 ∩ 𝑧))) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))))
125	107, 110, 116, 124	assraddsubd 11592	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧))) = ((♯‘(𝑥 ∩ ∪ 𝑦)) + ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))))))
126	125	oveq2d 7403	. . . . . . . . 9 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → ((♯‘𝑥) − (♯‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))) = ((♯‘𝑥) − ((♯‘(𝑥 ∩ ∪ 𝑦)) + ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))))))
127		hashcl 14321	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ Fin → (♯‘𝑥) ∈ ℕ₀)
128	127	adantl 481	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘𝑥) ∈ ℕ₀)
129	128	nn0cnd 12505	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘𝑥) ∈ ℂ)
130	110, 116	subcld 11533	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))) ∈ ℂ)
131	129, 107, 130	subsub4d 11564	. . . . . . . . 9 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (((♯‘𝑥) − (♯‘(𝑥 ∩ ∪ 𝑦))) − ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))))) = ((♯‘𝑥) − ((♯‘(𝑥 ∩ ∪ 𝑦)) + ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))))))
132	126, 131	eqtr4d 2767	. . . . . . . 8 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → ((♯‘𝑥) − (♯‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))) = (((♯‘𝑥) − (♯‘(𝑥 ∩ ∪ 𝑦))) − ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))))))
133	132	adantr 480	. . . . . . 7 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) → ((♯‘𝑥) − (♯‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))) = (((♯‘𝑥) − (♯‘(𝑥 ∩ ∪ 𝑦))) − ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))))))
134		disjdif 4435	. . . . . . . . . . 11 ⊢ (𝒫 𝑦 ∩ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) = ∅
135	134	a1i 11	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (𝒫 𝑦 ∩ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) = ∅)
136		ssun1 4141	. . . . . . . . . . . . . 14 ⊢ 𝑦 ⊆ (𝑦 ∪ {𝑧})
137	136	sspwi 4575	. . . . . . . . . . . . 13 ⊢ 𝒫 𝑦 ⊆ 𝒫 (𝑦 ∪ {𝑧})
138		undif 4445	. . . . . . . . . . . . 13 ⊢ (𝒫 𝑦 ⊆ 𝒫 (𝑦 ∪ {𝑧}) ↔ (𝒫 𝑦 ∪ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) = 𝒫 (𝑦 ∪ {𝑧}))
139	137, 138	mpbi 230	. . . . . . . . . . . 12 ⊢ (𝒫 𝑦 ∪ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) = 𝒫 (𝑦 ∪ {𝑧})
140	139	eqcomi 2738	. . . . . . . . . . 11 ⊢ 𝒫 (𝑦 ∪ {𝑧}) = (𝒫 𝑦 ∪ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))
141	140	a1i 11	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → 𝒫 (𝑦 ∪ {𝑧}) = (𝒫 𝑦 ∪ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)))
142		simpll 766	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → 𝑦 ∈ Fin)
143		snfi 9014	. . . . . . . . . . . 12 ⊢ {𝑧} ∈ Fin
144		unfi 9135	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝑦 ∪ {𝑧}) ∈ Fin)
145	142, 143, 144	sylancl 586	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (𝑦 ∪ {𝑧}) ∈ Fin)
146		pwfi 9268	. . . . . . . . . . 11 ⊢ ((𝑦 ∪ {𝑧}) ∈ Fin ↔ 𝒫 (𝑦 ∪ {𝑧}) ∈ Fin)
147	145, 146	sylib 218	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → 𝒫 (𝑦 ∪ {𝑧}) ∈ Fin)
148	54	a1i 11	. . . . . . . . . . . 12 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → -1 ∈ ℂ)
149		elpwi 4570	. . . . . . . . . . . . . 14 ⊢ (𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧}) → 𝑠 ⊆ (𝑦 ∪ {𝑧}))
150		ssfi 9137	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∪ {𝑧}) ∈ Fin ∧ 𝑠 ⊆ (𝑦 ∪ {𝑧})) → 𝑠 ∈ Fin)
151	145, 149, 150	syl2an 596	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → 𝑠 ∈ Fin)
152		hashcl 14321	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ Fin → (♯‘𝑠) ∈ ℕ₀)
153	151, 152	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (♯‘𝑠) ∈ ℕ₀)
154	148, 153	expcld 14111	. . . . . . . . . . 11 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (-1↑(♯‘𝑠)) ∈ ℂ)
155		simplr 768	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → 𝑥 ∈ Fin)
156		inss1 4200	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∩ ∩ 𝑠) ⊆ 𝑥
157		ssfi 9137	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ Fin ∧ (𝑥 ∩ ∩ 𝑠) ⊆ 𝑥) → (𝑥 ∩ ∩ 𝑠) ∈ Fin)
158	155, 156, 157	sylancl 586	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (𝑥 ∩ ∩ 𝑠) ∈ Fin)
159		hashcl 14321	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∩ ∩ 𝑠) ∈ Fin → (♯‘(𝑥 ∩ ∩ 𝑠)) ∈ ℕ₀)
160	158, 159	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (♯‘(𝑥 ∩ ∩ 𝑠)) ∈ ℕ₀)
161	160	nn0cnd 12505	. . . . . . . . . . 11 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (♯‘(𝑥 ∩ ∩ 𝑠)) ∈ ℂ)
162	154, 161	mulcld 11194	. . . . . . . . . 10 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → ((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) ∈ ℂ)
163	135, 141, 147, 162	fsumsplit 15707	. . . . . . . . 9 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) = (Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) + Σ𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))))
164		fveq2 6858	. . . . . . . . . . . . . 14 ⊢ (𝑠 = (𝑡 ∪ {𝑧}) → (♯‘𝑠) = (♯‘(𝑡 ∪ {𝑧})))
165	164	oveq2d 7403	. . . . . . . . . . . . 13 ⊢ (𝑠 = (𝑡 ∪ {𝑧}) → (-1↑(♯‘𝑠)) = (-1↑(♯‘(𝑡 ∪ {𝑧}))))
166		inteq 4913	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = (𝑡 ∪ {𝑧}) → ∩ 𝑠 = ∩ (𝑡 ∪ {𝑧}))
167		vex 3451	. . . . . . . . . . . . . . . . 17 ⊢ 𝑧 ∈ V
168	167	intunsn 4951	. . . . . . . . . . . . . . . 16 ⊢ ∩ (𝑡 ∪ {𝑧}) = (∩ 𝑡 ∩ 𝑧)
169	166, 168	eqtrdi 2780	. . . . . . . . . . . . . . 15 ⊢ (𝑠 = (𝑡 ∪ {𝑧}) → ∩ 𝑠 = (∩ 𝑡 ∩ 𝑧))
170	169	ineq2d 4183	. . . . . . . . . . . . . 14 ⊢ (𝑠 = (𝑡 ∪ {𝑧}) → (𝑥 ∩ ∩ 𝑠) = (𝑥 ∩ (∩ 𝑡 ∩ 𝑧)))
171	170	fveq2d 6862	. . . . . . . . . . . . 13 ⊢ (𝑠 = (𝑡 ∪ {𝑧}) → (♯‘(𝑥 ∩ ∩ 𝑠)) = (♯‘(𝑥 ∩ (∩ 𝑡 ∩ 𝑧))))
172	165, 171	oveq12d 7405	. . . . . . . . . . . 12 ⊢ (𝑠 = (𝑡 ∪ {𝑧}) → ((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) = ((-1↑(♯‘(𝑡 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑡 ∩ 𝑧)))))
173		pwfi 9268	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ Fin ↔ 𝒫 𝑦 ∈ Fin)
174	142, 173	sylib 218	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → 𝒫 𝑦 ∈ Fin)
175		eqid 2729	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ 𝒫 𝑦 ↦ (𝑢 ∪ {𝑧})) = (𝑢 ∈ 𝒫 𝑦 ↦ (𝑢 ∪ {𝑧}))
176		elpwi 4570	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 ∈ 𝒫 𝑦 → 𝑢 ⊆ 𝑦)
177	176	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → 𝑢 ⊆ 𝑦)
178		unss1 4148	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 ⊆ 𝑦 → (𝑢 ∪ {𝑧}) ⊆ (𝑦 ∪ {𝑧}))
179	177, 178	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → (𝑢 ∪ {𝑧}) ⊆ (𝑦 ∪ {𝑧}))
180		vex 3451	. . . . . . . . . . . . . . . . 17 ⊢ 𝑢 ∈ V
181		vsnex 5389	. . . . . . . . . . . . . . . . 17 ⊢ {𝑧} ∈ V
182	180, 181	unex 7720	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 ∪ {𝑧}) ∈ V
183	182	elpw 4567	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 ∪ {𝑧}) ∈ 𝒫 (𝑦 ∪ {𝑧}) ↔ (𝑢 ∪ {𝑧}) ⊆ (𝑦 ∪ {𝑧}))
184	179, 183	sylibr 234	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → (𝑢 ∪ {𝑧}) ∈ 𝒫 (𝑦 ∪ {𝑧}))
185		simpllr 775	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → ¬ 𝑧 ∈ 𝑦)
186		elpwi 4570	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 ∪ {𝑧}) ∈ 𝒫 𝑦 → (𝑢 ∪ {𝑧}) ⊆ 𝑦)
187		ssun2 4142	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑧} ⊆ (𝑢 ∪ {𝑧})
188	167	snss 4749	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ (𝑢 ∪ {𝑧}) ↔ {𝑧} ⊆ (𝑢 ∪ {𝑧}))
189	187, 188	mpbir 231	. . . . . . . . . . . . . . . . 17 ⊢ 𝑧 ∈ (𝑢 ∪ {𝑧})
190	189	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → 𝑧 ∈ (𝑢 ∪ {𝑧}))
191		ssel 3940	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 ∪ {𝑧}) ⊆ 𝑦 → (𝑧 ∈ (𝑢 ∪ {𝑧}) → 𝑧 ∈ 𝑦))
192	186, 190, 191	syl2imc 41	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → ((𝑢 ∪ {𝑧}) ∈ 𝒫 𝑦 → 𝑧 ∈ 𝑦))
193	185, 192	mtod 198	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → ¬ (𝑢 ∪ {𝑧}) ∈ 𝒫 𝑦)
194	184, 193	eldifd 3925	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → (𝑢 ∪ {𝑧}) ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))
195		eldifi 4094	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦) → 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧}))
196	195	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧}))
197	196	elpwid 4572	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → 𝑠 ⊆ (𝑦 ∪ {𝑧}))
198		uncom 4121	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∪ {𝑧}) = ({𝑧} ∪ 𝑦)
199	197, 198	sseqtrdi 3987	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → 𝑠 ⊆ ({𝑧} ∪ 𝑦))
200		ssundif 4451	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ⊆ ({𝑧} ∪ 𝑦) ↔ (𝑠 ∖ {𝑧}) ⊆ 𝑦)
201	199, 200	sylib 218	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → (𝑠 ∖ {𝑧}) ⊆ 𝑦)
202		vex 3451	. . . . . . . . . . . . . . 15 ⊢ 𝑦 ∈ V
203	202	elpw2 5289	. . . . . . . . . . . . . 14 ⊢ ((𝑠 ∖ {𝑧}) ∈ 𝒫 𝑦 ↔ (𝑠 ∖ {𝑧}) ⊆ 𝑦)
204	201, 203	sylibr 234	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → (𝑠 ∖ {𝑧}) ∈ 𝒫 𝑦)
205		elpwunsn 4648	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦) → 𝑧 ∈ 𝑠)
206	205	ad2antll 729	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → 𝑧 ∈ 𝑠)
207	206	snssd 4773	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → {𝑧} ⊆ 𝑠)
208		ssequn2 4152	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑧} ⊆ 𝑠 ↔ (𝑠 ∪ {𝑧}) = 𝑠)
209	207, 208	sylib 218	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → (𝑠 ∪ {𝑧}) = 𝑠)
210	209	eqcomd 2735	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → 𝑠 = (𝑠 ∪ {𝑧}))
211		uneq1 4124	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = (𝑠 ∖ {𝑧}) → (𝑢 ∪ {𝑧}) = ((𝑠 ∖ {𝑧}) ∪ {𝑧}))
212		undif1 4439	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑠 ∖ {𝑧}) ∪ {𝑧}) = (𝑠 ∪ {𝑧})
213	211, 212	eqtrdi 2780	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = (𝑠 ∖ {𝑧}) → (𝑢 ∪ {𝑧}) = (𝑠 ∪ {𝑧}))
214	213	eqeq2d 2740	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = (𝑠 ∖ {𝑧}) → (𝑠 = (𝑢 ∪ {𝑧}) ↔ 𝑠 = (𝑠 ∪ {𝑧})))
215	210, 214	syl5ibrcom 247	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → (𝑢 = (𝑠 ∖ {𝑧}) → 𝑠 = (𝑢 ∪ {𝑧})))
216	176	ad2antrl 728	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → 𝑢 ⊆ 𝑦)
217		simpllr 775	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → ¬ 𝑧 ∈ 𝑦)
218	216, 217	ssneldd 3949	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → ¬ 𝑧 ∈ 𝑢)
219		difsnb 4770	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑧 ∈ 𝑢 ↔ (𝑢 ∖ {𝑧}) = 𝑢)
220	218, 219	sylib 218	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → (𝑢 ∖ {𝑧}) = 𝑢)
221	220	eqcomd 2735	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → 𝑢 = (𝑢 ∖ {𝑧}))
222		difeq1 4082	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = (𝑢 ∪ {𝑧}) → (𝑠 ∖ {𝑧}) = ((𝑢 ∪ {𝑧}) ∖ {𝑧}))
223		difun2 4444	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∪ {𝑧}) ∖ {𝑧}) = (𝑢 ∖ {𝑧})
224	222, 223	eqtrdi 2780	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = (𝑢 ∪ {𝑧}) → (𝑠 ∖ {𝑧}) = (𝑢 ∖ {𝑧}))
225	224	eqeq2d 2740	. . . . . . . . . . . . . . 15 ⊢ (𝑠 = (𝑢 ∪ {𝑧}) → (𝑢 = (𝑠 ∖ {𝑧}) ↔ 𝑢 = (𝑢 ∖ {𝑧})))
226	221, 225	syl5ibrcom 247	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → (𝑠 = (𝑢 ∪ {𝑧}) → 𝑢 = (𝑠 ∖ {𝑧})))
227	215, 226	impbid 212	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → (𝑢 = (𝑠 ∖ {𝑧}) ↔ 𝑠 = (𝑢 ∪ {𝑧})))
228	175, 194, 204, 227	f1o2d 7643	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (𝑢 ∈ 𝒫 𝑦 ↦ (𝑢 ∪ {𝑧})):𝒫 𝑦–1-1-onto→(𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))
229		uneq1 4124	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝑡 → (𝑢 ∪ {𝑧}) = (𝑡 ∪ {𝑧}))
230		vex 3451	. . . . . . . . . . . . . . 15 ⊢ 𝑡 ∈ V
231	230, 181	unex 7720	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∪ {𝑧}) ∈ V
232	229, 175, 231	fvmpt 6968	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ 𝒫 𝑦 → ((𝑢 ∈ 𝒫 𝑦 ↦ (𝑢 ∪ {𝑧}))‘𝑡) = (𝑡 ∪ {𝑧}))
233	232	adantl 481	. . . . . . . . . . . 12 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑡 ∈ 𝒫 𝑦) → ((𝑢 ∈ 𝒫 𝑦 ↦ (𝑢 ∪ {𝑧}))‘𝑡) = (𝑡 ∪ {𝑧}))
234	195, 162	sylan2 593	. . . . . . . . . . . 12 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → ((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) ∈ ℂ)
235	172, 174, 228, 233, 234	fsumf1o 15689	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) = Σ𝑡 ∈ 𝒫 𝑦((-1↑(♯‘(𝑡 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑡 ∩ 𝑧)))))
236		uneq1 4124	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑠 → (𝑡 ∪ {𝑧}) = (𝑠 ∪ {𝑧}))
237	236	fveq2d 6862	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑠 → (♯‘(𝑡 ∪ {𝑧})) = (♯‘(𝑠 ∪ {𝑧})))
238	237	oveq2d 7403	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑠 → (-1↑(♯‘(𝑡 ∪ {𝑧}))) = (-1↑(♯‘(𝑠 ∪ {𝑧}))))
239		inteq 4913	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑠 → ∩ 𝑡 = ∩ 𝑠)
240	239	ineq1d 4182	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑠 → (∩ 𝑡 ∩ 𝑧) = (∩ 𝑠 ∩ 𝑧))
241	240	ineq2d 4183	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑠 → (𝑥 ∩ (∩ 𝑡 ∩ 𝑧)) = (𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))
242	241	fveq2d 6862	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑠 → (♯‘(𝑥 ∩ (∩ 𝑡 ∩ 𝑧))) = (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))))
243	238, 242	oveq12d 7405	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑠 → ((-1↑(♯‘(𝑡 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑡 ∩ 𝑧)))) = ((-1↑(♯‘(𝑠 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
244	243	cbvsumv 15662	. . . . . . . . . . . 12 ⊢ Σ𝑡 ∈ 𝒫 𝑦((-1↑(♯‘(𝑡 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑡 ∩ 𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘(𝑠 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))))
245	54	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → -1 ∈ ℂ)
246		elpwi 4570	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 ∈ 𝒫 𝑦 → 𝑠 ⊆ 𝑦)
247		ssfi 9137	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ Fin ∧ 𝑠 ⊆ 𝑦) → 𝑠 ∈ Fin)
248	142, 246, 247	syl2an 596	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → 𝑠 ∈ Fin)
249	248, 152	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (♯‘𝑠) ∈ ℕ₀)
250	245, 249	expp1d 14112	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1↑((♯‘𝑠) + 1)) = ((-1↑(♯‘𝑠)) · -1))
251	246	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → 𝑠 ⊆ 𝑦)
252		simpllr 775	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ¬ 𝑧 ∈ 𝑦)
253	251, 252	ssneldd 3949	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ¬ 𝑧 ∈ 𝑠)
254		hashunsng 14357	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ V → ((𝑠 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑠) → (♯‘(𝑠 ∪ {𝑧})) = ((♯‘𝑠) + 1)))
255	254	elv 3452	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑠 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑠) → (♯‘(𝑠 ∪ {𝑧})) = ((♯‘𝑠) + 1))
256	248, 253, 255	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (♯‘(𝑠 ∪ {𝑧})) = ((♯‘𝑠) + 1))
257	256	oveq2d 7403	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1↑(♯‘(𝑠 ∪ {𝑧}))) = (-1↑((♯‘𝑠) + 1)))
258	137	sseli 3942	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 ∈ 𝒫 𝑦 → 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧}))
259	258, 154	sylan2 593	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1↑(♯‘𝑠)) ∈ ℂ)
260	245, 259	mulcomd 11195	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1 · (-1↑(♯‘𝑠))) = ((-1↑(♯‘𝑠)) · -1))
261	250, 257, 260	3eqtr4d 2774	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1↑(♯‘(𝑠 ∪ {𝑧}))) = (-1 · (-1↑(♯‘𝑠))))
262	259	mulm1d 11630	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1 · (-1↑(♯‘𝑠))) = -(-1↑(♯‘𝑠)))
263	261, 262	eqtrd 2764	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1↑(♯‘(𝑠 ∪ {𝑧}))) = -(-1↑(♯‘𝑠)))
264	263	oveq1d 7402	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ((-1↑(♯‘(𝑠 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))) = (-(-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
265		inss1 4200	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∩ (∩ 𝑠 ∩ 𝑧)) ⊆ 𝑥
266		ssfi 9137	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ Fin ∧ (𝑥 ∩ (∩ 𝑠 ∩ 𝑧)) ⊆ 𝑥) → (𝑥 ∩ (∩ 𝑠 ∩ 𝑧)) ∈ Fin)
267	155, 265, 266	sylancl 586	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (𝑥 ∩ (∩ 𝑠 ∩ 𝑧)) ∈ Fin)
268		hashcl 14321	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∩ (∩ 𝑠 ∩ 𝑧)) ∈ Fin → (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))) ∈ ℕ₀)
269	267, 268	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))) ∈ ℕ₀)
270	269	nn0cnd 12505	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))) ∈ ℂ)
271	258, 270	sylan2 593	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))) ∈ ℂ)
272	259, 271	mulneg1d 11631	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-(-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))) = -((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
273	264, 272	eqtrd 2764	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ((-1↑(♯‘(𝑠 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))) = -((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
274	273	sumeq2dv 15668	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘(𝑠 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦-((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
275	244, 274	eqtrid 2776	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑡 ∈ 𝒫 𝑦((-1↑(♯‘(𝑡 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑡 ∩ 𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦-((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
276	154, 270	mulcld 11194	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → ((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))) ∈ ℂ)
277	258, 276	sylan2 593	. . . . . . . . . . . 12 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))) ∈ ℂ)
278	174, 277	fsumneg 15753	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 𝑦-((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))) = -Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
279	235, 275, 278	3eqtrd 2768	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) = -Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
280	279	oveq2d 7403	. . . . . . . . 9 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) + Σ𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))) = (Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) + -Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))))))
281	137	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → 𝒫 𝑦 ⊆ 𝒫 (𝑦 ∪ {𝑧}))
282	281	sselda 3946	. . . . . . . . . . . 12 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧}))
283	282, 162	syldan 591	. . . . . . . . . . 11 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) ∈ ℂ)
284	174, 283	fsumcl 15699	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) ∈ ℂ)
285	282, 276	syldan 591	. . . . . . . . . . 11 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))) ∈ ℂ)
286	174, 285	fsumcl 15699	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))) ∈ ℂ)
287	284, 286	negsubd 11539	. . . . . . . . 9 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) + -Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))))) = (Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) − Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))))))
288	163, 280, 287	3eqtrd 2768	. . . . . . . 8 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) = (Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) − Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))))))
289	288	adantr 480	. . . . . . 7 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) → Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) = (Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) − Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))))))
290	101, 133, 289	3eqtr4d 2774	. . . . . 6 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) → ((♯‘𝑥) − (♯‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))))
291	290	ex 412	. . . . 5 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) → ((♯‘𝑥) − (♯‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))))
292	291	ralrimdva 3133	. . . 4 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) → ∀𝑥 ∈ Fin ((♯‘𝑥) − (♯‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))))
293		ineq1 4176	. . . . . . . 8 ⊢ (𝑏 = 𝑥 → (𝑏 ∩ (∪ 𝑦 ∪ 𝑧)) = (𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))
294	293	fveq2d 6862	. . . . . . 7 ⊢ (𝑏 = 𝑥 → (♯‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧))) = (♯‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧))))
295	66, 294	oveq12d 7405	. . . . . 6 ⊢ (𝑏 = 𝑥 → ((♯‘𝑏) − (♯‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧)))) = ((♯‘𝑥) − (♯‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))))
296		ineq1 4176	. . . . . . . . 9 ⊢ (𝑏 = 𝑥 → (𝑏 ∩ ∩ 𝑠) = (𝑥 ∩ ∩ 𝑠))
297	296	fveq2d 6862	. . . . . . . 8 ⊢ (𝑏 = 𝑥 → (♯‘(𝑏 ∩ ∩ 𝑠)) = (♯‘(𝑥 ∩ ∩ 𝑠)))
298	297	oveq2d 7403	. . . . . . 7 ⊢ (𝑏 = 𝑥 → ((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) = ((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))))
299	298	sumeq2sdv 15669	. . . . . 6 ⊢ (𝑏 = 𝑥 → Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))))
300	295, 299	eqeq12d 2745	. . . . 5 ⊢ (𝑏 = 𝑥 → (((♯‘𝑏) − (♯‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) ↔ ((♯‘𝑥) − (♯‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))))
301	300	cbvralvw 3215	. . . 4 ⊢ (∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) ↔ ∀𝑥 ∈ Fin ((♯‘𝑥) − (♯‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))))
302	292, 301	imbitrrdi 252	. . 3 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) → ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))))
303	16, 24, 37, 45, 65, 302	findcard2s 9129	. 2 ⊢ (𝐴 ∈ Fin → ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))))
304		fveq2 6858	. . . . 5 ⊢ (𝑏 = 𝐵 → (♯‘𝑏) = (♯‘𝐵))
305		ineq1 4176	. . . . . 6 ⊢ (𝑏 = 𝐵 → (𝑏 ∩ ∪ 𝐴) = (𝐵 ∩ ∪ 𝐴))
306	305	fveq2d 6862	. . . . 5 ⊢ (𝑏 = 𝐵 → (♯‘(𝑏 ∩ ∪ 𝐴)) = (♯‘(𝐵 ∩ ∪ 𝐴)))
307	304, 306	oveq12d 7405	. . . 4 ⊢ (𝑏 = 𝐵 → ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝐴))) = ((♯‘𝐵) − (♯‘(𝐵 ∩ ∪ 𝐴))))
308		simpl 482	. . . . . . . 8 ⊢ ((𝑏 = 𝐵 ∧ 𝑠 ∈ 𝒫 𝐴) → 𝑏 = 𝐵)
309	308	ineq1d 4182	. . . . . . 7 ⊢ ((𝑏 = 𝐵 ∧ 𝑠 ∈ 𝒫 𝐴) → (𝑏 ∩ ∩ 𝑠) = (𝐵 ∩ ∩ 𝑠))
310	309	fveq2d 6862	. . . . . 6 ⊢ ((𝑏 = 𝐵 ∧ 𝑠 ∈ 𝒫 𝐴) → (♯‘(𝑏 ∩ ∩ 𝑠)) = (♯‘(𝐵 ∩ ∩ 𝑠)))
311	310	oveq2d 7403	. . . . 5 ⊢ ((𝑏 = 𝐵 ∧ 𝑠 ∈ 𝒫 𝐴) → ((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) = ((-1↑(♯‘𝑠)) · (♯‘(𝐵 ∩ ∩ 𝑠))))
312	311	sumeq2dv 15668	. . . 4 ⊢ (𝑏 = 𝐵 → Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(𝐵 ∩ ∩ 𝑠))))
313	307, 312	eqeq12d 2745	. . 3 ⊢ (𝑏 = 𝐵 → (((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) ↔ ((♯‘𝐵) − (♯‘(𝐵 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(𝐵 ∩ ∩ 𝑠)))))
314	313	rspccva 3587	. 2 ⊢ ((∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) ∧ 𝐵 ∈ Fin) → ((♯‘𝐵) − (♯‘(𝐵 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(𝐵 ∩ ∩ 𝑠))))
315	303, 314	sylan 580	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((♯‘𝐵) − (♯‘(𝐵 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(♯‘𝑠)) · (♯‘(𝐵 ∩ ∩ 𝑠))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2109 ∀wral 3044 Vcvv 3447 ∖ cdif 3911 ∪ cun 3912 ∩ cin 3913 ⊆ wss 3914 ∅c0 4296 𝒫 cpw 4563 {csn 4589 ∪ cuni 4871 ∩ cint 4910 ↦ cmpt 5188 ‘cfv 6511 (class class class)co 7387 Fincfn 8918 ℂcc 11066 0cc0 11068 1c1 11069 + caddc 11071 · cmul 11073 − cmin 11405 -cneg 11406 ℕ₀cn0 12442 ↑cexp 14026 ♯chash 14295 Σcsu 15652

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 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5234 ax-sep 5251 ax-nul 5261 ax-pow 5320 ax-pr 5387 ax-un 7711 ax-inf2 9594 ax-cnex 11124 ax-resscn 11125 ax-1cn 11126 ax-icn 11127 ax-addcl 11128 ax-addrcl 11129 ax-mulcl 11130 ax-mulrcl 11131 ax-mulcom 11132 ax-addass 11133 ax-mulass 11134 ax-distr 11135 ax-i2m1 11136 ax-1ne0 11137 ax-1rid 11138 ax-rnegex 11139 ax-rrecex 11140 ax-cnre 11141 ax-pre-lttri 11142 ax-pre-lttrn 11143 ax-pre-ltadd 11144 ax-pre-mulgt0 11145 ax-pre-sup 11146

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3354 df-reu 3355 df-rab 3406 df-v 3449 df-sbc 3754 df-csb 3863 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-pss 3934 df-nul 4297 df-if 4489 df-pw 4565 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4872 df-int 4911 df-iun 4957 df-br 5108 df-opab 5170 df-mpt 5189 df-tr 5215 df-id 5533 df-eprel 5538 df-po 5546 df-so 5547 df-fr 5591 df-se 5592 df-we 5593 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-pred 6274 df-ord 6335 df-on 6336 df-lim 6337 df-suc 6338 df-iota 6464 df-fun 6513 df-fn 6514 df-f 6515 df-f1 6516 df-fo 6517 df-f1o 6518 df-fv 6519 df-isom 6520 df-riota 7344 df-ov 7390 df-oprab 7391 df-mpo 7392 df-om 7843 df-1st 7968 df-2nd 7969 df-frecs 8260 df-wrecs 8291 df-recs 8340 df-rdg 8378 df-1o 8434 df-oadd 8438 df-er 8671 df-en 8919 df-dom 8920 df-sdom 8921 df-fin 8922 df-sup 9393 df-oi 9463 df-dju 9854 df-card 9892 df-pnf 11210 df-mnf 11211 df-xr 11212 df-ltxr 11213 df-le 11214 df-sub 11407 df-neg 11408 df-div 11836 df-nn 12187 df-2 12249 df-3 12250 df-n0 12443 df-z 12530 df-uz 12794 df-rp 12952 df-fz 13469 df-fzo 13616 df-seq 13967 df-exp 14027 df-hash 14296 df-cj 15065 df-re 15066 df-im 15067 df-sqrt 15201 df-abs 15202 df-clim 15454 df-sum 15653

This theorem is referenced by: incexc 15803

W3C validator