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 16005

Description: Lemma for incexc 16006. (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 4877	. . . . . . . . . . 11 ⊢ (𝑥 = ∅ → ∪ 𝑥 = ∪ ∅)
2		uni0 4895	. . . . . . . . . . 11 ⊢ ∪ ∅ = ∅
3	1, 2	eqtrdi 2811	. . . . . . . . . 10 ⊢ (𝑥 = ∅ → ∪ 𝑥 = ∅)
4	3	ineq2d 4117	. . . . . . . . 9 ⊢ (𝑥 = ∅ → (𝑏 ∩ ∪ 𝑥) = (𝑏 ∩ ∅))
5		in0 4344	. . . . . . . . 9 ⊢ (𝑏 ∩ ∅) = ∅
6	4, 5	eqtrdi 2811	. . . . . . . 8 ⊢ (𝑥 = ∅ → (𝑏 ∩ ∪ 𝑥) = ∅)
7	6	fveq2d 6889	. . . . . . 7 ⊢ (𝑥 = ∅ → (♯‘(𝑏 ∩ ∪ 𝑥)) = (♯‘∅))
8		hash0 14511	. . . . . . 7 ⊢ (♯‘∅) = 0
9	7, 8	eqtrdi 2811	. . . . . 6 ⊢ (𝑥 = ∅ → (♯‘(𝑏 ∩ ∪ 𝑥)) = 0)
10	9	oveq2d 7436	. . . . 5 ⊢ (𝑥 = ∅ → ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = ((♯‘𝑏) − 0))
11		pweq 4570	. . . . . . 7 ⊢ (𝑥 = ∅ → 𝒫 𝑥 = 𝒫 ∅)
12		pw0 4772	. . . . . . 7 ⊢ 𝒫 ∅ = {∅}
13	11, 12	eqtrdi 2811	. . . . . 6 ⊢ (𝑥 = ∅ → 𝒫 𝑥 = {∅})
14	13	sumeq1d 15867	. . . . 5 ⊢ (𝑥 = ∅ → Σ𝑠 ∈ 𝒫 𝑥(( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) = Σ𝑠 ∈ {∅} (( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))))
15	10, 14	eqeq12d 2776	. . . 4 ⊢ (𝑥 = ∅ → (((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥(( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) ↔ ((♯‘𝑏) − 0) = Σ𝑠 ∈ {∅} (( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))))
16	15	ralbidv 3185	. . 3 ⊢ (𝑥 = ∅ → (∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥(( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) ↔ ∀𝑏 ∈ Fin ((♯‘𝑏) − 0) = Σ𝑠 ∈ {∅} (( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))))
17		unieq 4877	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ∪ 𝑥 = ∪ 𝑦)
18	17	ineq2d 4117	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑏 ∩ ∪ 𝑥) = (𝑏 ∩ ∪ 𝑦))
19	18	fveq2d 6889	. . . . . 6 ⊢ (𝑥 = 𝑦 → (♯‘(𝑏 ∩ ∪ 𝑥)) = (♯‘(𝑏 ∩ ∪ 𝑦)))
20	19	oveq2d 7436	. . . . 5 ⊢ (𝑥 = 𝑦 → ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))))
21		pweq 4570	. . . . . 6 ⊢ (𝑥 = 𝑦 → 𝒫 𝑥 = 𝒫 𝑦)
22	21	sumeq1d 15867	. . . . 5 ⊢ (𝑥 = 𝑦 → Σ𝑠 ∈ 𝒫 𝑥(( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) = Σ𝑠 ∈ 𝒫 𝑦(( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))))
23	20, 22	eqeq12d 2776	. . . 4 ⊢ (𝑥 = 𝑦 → (((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥(( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) ↔ ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦(( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))))
24	23	ralbidv 3185	. . 3 ⊢ (𝑥 = 𝑦 → (∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥(( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) ↔ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦(( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))))
25		unieq 4877	. . . . . . . . 9 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ∪ 𝑥 = ∪ (𝑦 ∪ {𝑧}))
26		uniun 4889	. . . . . . . . . 10 ⊢ ∪ (𝑦 ∪ {𝑧}) = (∪ 𝑦 ∪ ∪ {𝑧})
27		unisnv 4886	. . . . . . . . . . 11 ⊢ ∪ {𝑧} = 𝑧
28	27	uneq2i 4164	. . . . . . . . . 10 ⊢ (∪ 𝑦 ∪ ∪ {𝑧}) = (∪ 𝑦 ∪ 𝑧)
29	26, 28	eqtri 2783	. . . . . . . . 9 ⊢ ∪ (𝑦 ∪ {𝑧}) = (∪ 𝑦 ∪ 𝑧)
30	25, 29	eqtrdi 2811	. . . . . . . 8 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ∪ 𝑥 = (∪ 𝑦 ∪ 𝑧))
31	30	ineq2d 4117	. . . . . . 7 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑏 ∩ ∪ 𝑥) = (𝑏 ∩ (∪ 𝑦 ∪ 𝑧)))
32	31	fveq2d 6889	. . . . . 6 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (♯‘(𝑏 ∩ ∪ 𝑥)) = (♯‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧))))
33	32	oveq2d 7436	. . . . 5 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = ((♯‘𝑏) − (♯‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧)))))
34		pweq 4570	. . . . . 6 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → 𝒫 𝑥 = 𝒫 (𝑦 ∪ {𝑧}))
35	34	sumeq1d 15867	. . . . 5 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → Σ𝑠 ∈ 𝒫 𝑥(( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})(( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))))
36	33, 35	eqeq12d 2776	. . . 4 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥(( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) ↔ ((♯‘𝑏) − (♯‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})(( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))))
37	36	ralbidv 3185	. . 3 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥(( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) ↔ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})(( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))))
38		unieq 4877	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴)
39	38	ineq2d 4117	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (𝑏 ∩ ∪ 𝑥) = (𝑏 ∩ ∪ 𝐴))
40	39	fveq2d 6889	. . . . . 6 ⊢ (𝑥 = 𝐴 → (♯‘(𝑏 ∩ ∪ 𝑥)) = (♯‘(𝑏 ∩ ∪ 𝐴)))
41	40	oveq2d 7436	. . . . 5 ⊢ (𝑥 = 𝐴 → ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝐴))))
42		pweq 4570	. . . . . 6 ⊢ (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴)
43	42	sumeq1d 15867	. . . . 5 ⊢ (𝑥 = 𝐴 → Σ𝑠 ∈ 𝒫 𝑥(( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) = Σ𝑠 ∈ 𝒫 𝐴(( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))))
44	41, 43	eqeq12d 2776	. . . 4 ⊢ (𝑥 = 𝐴 → (((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥(( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) ↔ ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴(( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))))
45	44	ralbidv 3185	. . 3 ⊢ (𝑥 = 𝐴 → (∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥(( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) ↔ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴(( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))))
46		hashcl 14500	. . . . . . 7 ⊢ (𝑏 ∈ Fin → (♯‘𝑏) ∈ ℕ₀)
47	46	nn0cnd 12669	. . . . . 6 ⊢ (𝑏 ∈ Fin → (♯‘𝑏) ∈ ℂ)
48	47	mullidd 11327	. . . . 5 ⊢ (𝑏 ∈ Fin → (1 · (♯‘𝑏)) = (♯‘𝑏))
49		0ex 5260	. . . . . 6 ⊢ ∅ ∈ V
50	48, 47	eqeltrd 2860	. . . . . 6 ⊢ (𝑏 ∈ Fin → (1 · (♯‘𝑏)) ∈ ℂ)
51		fveq2 6885	. . . . . . . . . . 11 ⊢ (𝑠 = ∅ → (♯‘𝑠) = (♯‘∅))
52	51, 8	eqtrdi 2811	. . . . . . . . . 10 ⊢ (𝑠 = ∅ → (♯‘𝑠) = 0)
53	52	oveq2d 7436	. . . . . . . . 9 ⊢ (𝑠 = ∅ → ( -1↑(♯‘𝑠)) = ( -1↑0))
54		neg1cn 12305	. . . . . . . . . 10 ⊢ -1 ∈ ℂ
55		exp0 14208	. . . . . . . . . 10 ⊢ ( -1 ∈ ℂ → ( -1↑0) = 1)
56	54, 55	ax-mp 5	. . . . . . . . 9 ⊢ ( -1↑0) = 1
57	53, 56	eqtrdi 2811	. . . . . . . 8 ⊢ (𝑠 = ∅ → ( -1↑(♯‘𝑠)) = 1)
58		rint0 4947	. . . . . . . . 9 ⊢ (𝑠 = ∅ → (𝑏 ∩ ∩ 𝑠) = 𝑏)
59	58	fveq2d 6889	. . . . . . . 8 ⊢ (𝑠 = ∅ → (♯‘(𝑏 ∩ ∩ 𝑠)) = (♯‘𝑏))
60	57, 59	oveq12d 7438	. . . . . . 7 ⊢ (𝑠 = ∅ → (( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) = (1 · (♯‘𝑏)))
61	60	sumsn 15912	. . . . . 6 ⊢ ((∅ ∈ V ∧ (1 · (♯‘𝑏)) ∈ ℂ) → Σ𝑠 ∈ {∅} (( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) = (1 · (♯‘𝑏)))
62	49, 50, 61	sylancr 599	. . . . 5 ⊢ (𝑏 ∈ Fin → Σ𝑠 ∈ {∅} (( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) = (1 · (♯‘𝑏)))
63	47	subid1d 11658	. . . . 5 ⊢ (𝑏 ∈ Fin → ((♯‘𝑏) − 0) = (♯‘𝑏))
64	48, 62, 63	3eqtr4rd 2806	. . . 4 ⊢ (𝑏 ∈ Fin → ((♯‘𝑏) − 0) = Σ𝑠 ∈ {∅} (( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))))
65	64	rgen 3078	. . 3 ⊢ ∀𝑏 ∈ Fin ((♯‘𝑏) − 0) = Σ𝑠 ∈ {∅} (( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))
66		fveq2 6885	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑥 → (♯‘𝑏) = (♯‘𝑥))
67		ineq1 4110	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑥 → (𝑏 ∩ ∪ 𝑦) = (𝑥 ∩ ∪ 𝑦))
68	67	fveq2d 6889	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑥 → (♯‘(𝑏 ∩ ∪ 𝑦)) = (♯‘(𝑥 ∩ ∪ 𝑦)))
69	66, 68	oveq12d 7438	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑥 → ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = ((♯‘𝑥) − (♯‘(𝑥 ∩ ∪ 𝑦))))
70		simpl 488	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 = 𝑥 ∧ 𝑠 ∈ 𝒫 𝑦) → 𝑏 = 𝑥)
71	70	ineq1d 4116	. . . . . . . . . . . . . 14 ⊢ ((𝑏 = 𝑥 ∧ 𝑠 ∈ 𝒫 𝑦) → (𝑏 ∩ ∩ 𝑠) = (𝑥 ∩ ∩ 𝑠))
72	71	fveq2d 6889	. . . . . . . . . . . . 13 ⊢ ((𝑏 = 𝑥 ∧ 𝑠 ∈ 𝒫 𝑦) → (♯‘(𝑏 ∩ ∩ 𝑠)) = (♯‘(𝑥 ∩ ∩ 𝑠)))
73	72	oveq2d 7436	. . . . . . . . . . . 12 ⊢ ((𝑏 = 𝑥 ∧ 𝑠 ∈ 𝒫 𝑦) → (( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) = (( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))))
74	73	sumeq2dv 15869	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑥 → Σ𝑠 ∈ 𝒫 𝑦(( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) = Σ𝑠 ∈ 𝒫 𝑦(( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))))
75	69, 74	eqeq12d 2776	. . . . . . . . . 10 ⊢ (𝑏 = 𝑥 → (((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦(( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) ↔ ((♯‘𝑥) − (♯‘(𝑥 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦(( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))))
76	75	rspcva 3574	. . . . . . . . 9 ⊢ ((𝑥 ∈ Fin ∧ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦(( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) → ((♯‘𝑥) − (♯‘(𝑥 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦(( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))))
77	76	adantll 727	. . . . . . . 8 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦(( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) → ((♯‘𝑥) − (♯‘(𝑥 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦(( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))))
78		simpr 490	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → 𝑥 ∈ Fin)
79		inss1 4133	. . . . . . . . . 10 ⊢ (𝑥 ∩ 𝑧) ⊆ 𝑥
80		ssfi 9188	. . . . . . . . . 10 ⊢ ((𝑥 ∈ Fin ∧ (𝑥 ∩ 𝑧) ⊆ 𝑥) → (𝑥 ∩ 𝑧) ∈ Fin)
81	78, 79, 80	sylancl 598	. . . . . . . . 9 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (𝑥 ∩ 𝑧) ∈ Fin)
82		fveq2 6885	. . . . . . . . . . . 12 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → (♯‘𝑏) = (♯‘(𝑥 ∩ 𝑧)))
83		ineq1 4110	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → (𝑏 ∩ ∪ 𝑦) = ((𝑥 ∩ 𝑧) ∩ ∪ 𝑦))
84		in32 4126	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∩ 𝑧) ∩ ∪ 𝑦) = ((𝑥 ∩ ∪ 𝑦) ∩ 𝑧)
85		inass 4124	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∩ ∪ 𝑦) ∩ 𝑧) = (𝑥 ∩ (∪ 𝑦 ∩ 𝑧))
86	84, 85	eqtri 2783	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∩ 𝑧) ∩ ∪ 𝑦) = (𝑥 ∩ (∪ 𝑦 ∩ 𝑧))
87	83, 86	eqtrdi 2811	. . . . . . . . . . . . 13 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → (𝑏 ∩ ∪ 𝑦) = (𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))
88	87	fveq2d 6889	. . . . . . . . . . . 12 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → (♯‘(𝑏 ∩ ∪ 𝑦)) = (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))))
89	82, 88	oveq12d 7438	. . . . . . . . . . 11 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))))
90		ineq1 4110	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → (𝑏 ∩ ∩ 𝑠) = ((𝑥 ∩ 𝑧) ∩ ∩ 𝑠))
91		in32 4126	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∩ 𝑧) ∩ ∩ 𝑠) = ((𝑥 ∩ ∩ 𝑠) ∩ 𝑧)
92		inass 4124	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∩ ∩ 𝑠) ∩ 𝑧) = (𝑥 ∩ (∩ 𝑠 ∩ 𝑧))
93	91, 92	eqtri 2783	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∩ 𝑧) ∩ ∩ 𝑠) = (𝑥 ∩ (∩ 𝑠 ∩ 𝑧))
94	90, 93	eqtrdi 2811	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → (𝑏 ∩ ∩ 𝑠) = (𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))
95	94	fveq2d 6889	. . . . . . . . . . . . 13 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → (♯‘(𝑏 ∩ ∩ 𝑠)) = (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))))
96	95	oveq2d 7436	. . . . . . . . . . . 12 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → (( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) = (( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
97	96	sumeq2sdv 15870	. . . . . . . . . . 11 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → Σ𝑠 ∈ 𝒫 𝑦(( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) = Σ𝑠 ∈ 𝒫 𝑦(( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
98	89, 97	eqeq12d 2776	. . . . . . . . . 10 ⊢ (𝑏 = (𝑥 ∩ 𝑧) → (((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦(( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) ↔ ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦(( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))))))
99	98	rspcva 3574	. . . . . . . . 9 ⊢ (((𝑥 ∩ 𝑧) ∈ Fin ∧ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦(( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) → ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦(( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
100	81, 99	sylan 592	. . . . . . . 8 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦(( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) → ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦(( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
101	77, 100	oveq12d 7438	. . . . . . 7 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦(( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) → (((♯‘𝑥) − (♯‘(𝑥 ∩ ∪ 𝑦))) − ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))))) = (Σ𝑠 ∈ 𝒫 𝑦(( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) − Σ𝑠 ∈ 𝒫 𝑦(( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))))))
102		inss1 4133	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∩ ∪ 𝑦) ⊆ 𝑥
103		ssfi 9188	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ Fin ∧ (𝑥 ∩ ∪ 𝑦) ⊆ 𝑥) → (𝑥 ∩ ∪ 𝑦) ∈ Fin)
104	78, 102, 103	sylancl 598	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (𝑥 ∩ ∪ 𝑦) ∈ Fin)
105		hashcl 14500	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∩ ∪ 𝑦) ∈ Fin → (♯‘(𝑥 ∩ ∪ 𝑦)) ∈ ℕ₀)
106	104, 105	syl 18	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘(𝑥 ∩ ∪ 𝑦)) ∈ ℕ₀)
107	106	nn0cnd 12669	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘(𝑥 ∩ ∪ 𝑦)) ∈ ℂ)
108		hashcl 14500	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∩ 𝑧) ∈ Fin → (♯‘(𝑥 ∩ 𝑧)) ∈ ℕ₀)
109	81, 108	syl 18	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘(𝑥 ∩ 𝑧)) ∈ ℕ₀)
110	109	nn0cnd 12669	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘(𝑥 ∩ 𝑧)) ∈ ℂ)
111		inss1 4133	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∩ (∪ 𝑦 ∩ 𝑧)) ⊆ 𝑥
112		ssfi 9188	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ Fin ∧ (𝑥 ∩ (∪ 𝑦 ∩ 𝑧)) ⊆ 𝑥) → (𝑥 ∩ (∪ 𝑦 ∩ 𝑧)) ∈ Fin)
113	78, 111, 112	sylancl 598	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (𝑥 ∩ (∪ 𝑦 ∩ 𝑧)) ∈ Fin)
114		hashcl 14500	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∩ (∪ 𝑦 ∩ 𝑧)) ∈ Fin → (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))) ∈ ℕ₀)
115	113, 114	syl 18	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))) ∈ ℕ₀)
116	115	nn0cnd 12669	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))) ∈ ℂ)
117		hashun3 14528	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∩ ∪ 𝑦) ∈ Fin ∧ (𝑥 ∩ 𝑧) ∈ Fin) → (♯‘((𝑥 ∩ ∪ 𝑦) ∪ (𝑥 ∩ 𝑧))) = (((♯‘(𝑥 ∩ ∪ 𝑦)) + (♯‘(𝑥 ∩ 𝑧))) − (♯‘((𝑥 ∩ ∪ 𝑦) ∩ (𝑥 ∩ 𝑧)))))
118	104, 81, 117	syl2anc 596	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘((𝑥 ∩ ∪ 𝑦) ∪ (𝑥 ∩ 𝑧))) = (((♯‘(𝑥 ∩ ∪ 𝑦)) + (♯‘(𝑥 ∩ 𝑧))) − (♯‘((𝑥 ∩ ∪ 𝑦) ∩ (𝑥 ∩ 𝑧)))))
119		indi 4229	. . . . . . . . . . . . 13 ⊢ (𝑥 ∩ (∪ 𝑦 ∪ 𝑧)) = ((𝑥 ∩ ∪ 𝑦) ∪ (𝑥 ∩ 𝑧))
120	119	fveq2i 6888	. . . . . . . . . . . 12 ⊢ (♯‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧))) = (♯‘((𝑥 ∩ ∪ 𝑦) ∪ (𝑥 ∩ 𝑧)))
121		inindi 4131	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∩ (∪ 𝑦 ∩ 𝑧)) = ((𝑥 ∩ ∪ 𝑦) ∩ (𝑥 ∩ 𝑧))
122	121	fveq2i 6888	. . . . . . . . . . . . 13 ⊢ (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))) = (♯‘((𝑥 ∩ ∪ 𝑦) ∩ (𝑥 ∩ 𝑧)))
123	122	oveq2i 7431	. . . . . . . . . . . 12 ⊢ (((♯‘(𝑥 ∩ ∪ 𝑦)) + (♯‘(𝑥 ∩ 𝑧))) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))) = (((♯‘(𝑥 ∩ ∪ 𝑦)) + (♯‘(𝑥 ∩ 𝑧))) − (♯‘((𝑥 ∩ ∪ 𝑦) ∩ (𝑥 ∩ 𝑧))))
124	118, 120, 123	3eqtr4g 2820	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧))) = (((♯‘(𝑥 ∩ ∪ 𝑦)) + (♯‘(𝑥 ∩ 𝑧))) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))))
125	107, 110, 116, 124	assraddsubd 11730	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧))) = ((♯‘(𝑥 ∩ ∪ 𝑦)) + ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))))))
126	125	oveq2d 7436	. . . . . . . . 9 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → ((♯‘𝑥) − (♯‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))) = ((♯‘𝑥) − ((♯‘(𝑥 ∩ ∪ 𝑦)) + ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))))))
127		hashcl 14500	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ Fin → (♯‘𝑥) ∈ ℕ₀)
128	127	adantl 487	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘𝑥) ∈ ℕ₀)
129	128	nn0cnd 12669	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (♯‘𝑥) ∈ ℂ)
130	110, 116	subcld 11669	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))) ∈ ℂ)
131	129, 107, 130	subsub4d 11700	. . . . . . . . 9 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (((♯‘𝑥) − (♯‘(𝑥 ∩ ∪ 𝑦))) − ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))))) = ((♯‘𝑥) − ((♯‘(𝑥 ∩ ∪ 𝑦)) + ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧)))))))
132	126, 131	eqtr4d 2798	. . . . . . . 8 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → ((♯‘𝑥) − (♯‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))) = (((♯‘𝑥) − (♯‘(𝑥 ∩ ∪ 𝑦))) − ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))))))
133	132	adantr 486	. . . . . . 7 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦(( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) → ((♯‘𝑥) − (♯‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))) = (((♯‘𝑥) − (♯‘(𝑥 ∩ ∪ 𝑦))) − ((♯‘(𝑥 ∩ 𝑧)) − (♯‘(𝑥 ∩ (∪ 𝑦 ∩ 𝑧))))))
134		disjdif 4425	. . . . . . . . . . 11 ⊢ (𝒫 𝑦 ∩ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) = ∅
135	134	a1i 11	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (𝒫 𝑦 ∩ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) = ∅)
136		ssun1 4176	. . . . . . . . . . . . . 14 ⊢ 𝑦 ⊆ (𝑦 ∪ {𝑧})
137	136	sspwi 4568	. . . . . . . . . . . . 13 ⊢ 𝒫 𝑦 ⊆ 𝒫 (𝑦 ∪ {𝑧})
138		undif 4437	. . . . . . . . . . . . 13 ⊢ (𝒫 𝑦 ⊆ 𝒫 (𝑦 ∪ {𝑧}) ↔ (𝒫 𝑦 ∪ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) = 𝒫 (𝑦 ∪ {𝑧}))
139	137, 138	mpbi 233	. . . . . . . . . . . 12 ⊢ (𝒫 𝑦 ∪ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) = 𝒫 (𝑦 ∪ {𝑧})
140	139	eqcomi 2769	. . . . . . . . . . 11 ⊢ 𝒫 (𝑦 ∪ {𝑧}) = (𝒫 𝑦 ∪ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))
141	140	a1i 11	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → 𝒫 (𝑦 ∪ {𝑧}) = (𝒫 𝑦 ∪ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)))
142		simpll 779	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → 𝑦 ∈ Fin)
143		snfi 9071	. . . . . . . . . . . 12 ⊢ {𝑧} ∈ Fin
144		unfi 9186	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝑦 ∪ {𝑧}) ∈ Fin)
145	142, 143, 144	sylancl 598	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (𝑦 ∪ {𝑧}) ∈ Fin)
146		pwfi 9310	. . . . . . . . . . 11 ⊢ ((𝑦 ∪ {𝑧}) ∈ Fin ↔ 𝒫 (𝑦 ∪ {𝑧}) ∈ Fin)
147	145, 146	sylib 221	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → 𝒫 (𝑦 ∪ {𝑧}) ∈ Fin)
148	54	a1i 11	. . . . . . . . . . . 12 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → -1 ∈ ℂ)
149		elpwi 4563	. . . . . . . . . . . . . 14 ⊢ (𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧}) → 𝑠 ⊆ (𝑦 ∪ {𝑧}))
150		ssfi 9188	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∪ {𝑧}) ∈ Fin ∧ 𝑠 ⊆ (𝑦 ∪ {𝑧})) → 𝑠 ∈ Fin)
151	145, 149, 150	syl2an 608	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → 𝑠 ∈ Fin)
152		hashcl 14500	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ Fin → (♯‘𝑠) ∈ ℕ₀)
153	151, 152	syl 18	. . . . . . . . . . . 12 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (♯‘𝑠) ∈ ℕ₀)
154	148, 153	expcld 14289	. . . . . . . . . . 11 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → ( -1↑(♯‘𝑠)) ∈ ℂ)
155		simplr 781	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → 𝑥 ∈ Fin)
156		inss1 4133	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∩ ∩ 𝑠) ⊆ 𝑥
157		ssfi 9188	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ Fin ∧ (𝑥 ∩ ∩ 𝑠) ⊆ 𝑥) → (𝑥 ∩ ∩ 𝑠) ∈ Fin)
158	155, 156, 157	sylancl 598	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (𝑥 ∩ ∩ 𝑠) ∈ Fin)
159		hashcl 14500	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∩ ∩ 𝑠) ∈ Fin → (♯‘(𝑥 ∩ ∩ 𝑠)) ∈ ℕ₀)
160	158, 159	syl 18	. . . . . . . . . . . 12 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (♯‘(𝑥 ∩ ∩ 𝑠)) ∈ ℕ₀)
161	160	nn0cnd 12669	. . . . . . . . . . 11 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (♯‘(𝑥 ∩ ∩ 𝑠)) ∈ ℂ)
162	154, 161	mulcld 11329	. . . . . . . . . 10 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) ∈ ℂ)
163	135, 141, 147, 162	fsumsplit 15907	. . . . . . . . 9 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})(( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) = (Σ𝑠 ∈ 𝒫 𝑦(( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) + Σ𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)(( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))))
164		fveq2 6885	. . . . . . . . . . . . . 14 ⊢ (𝑠 = (𝑡 ∪ {𝑧}) → (♯‘𝑠) = (♯‘(𝑡 ∪ {𝑧})))
165	164	oveq2d 7436	. . . . . . . . . . . . 13 ⊢ (𝑠 = (𝑡 ∪ {𝑧}) → ( -1↑(♯‘𝑠)) = ( -1↑(♯‘(𝑡 ∪ {𝑧}))))
166		inteq 4909	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = (𝑡 ∪ {𝑧}) → ∩ 𝑠 = ∩ (𝑡 ∪ {𝑧}))
167		vex 3454	. . . . . . . . . . . . . . . . 17 ⊢ 𝑧 ∈ V
168	167	intunsn 4946	. . . . . . . . . . . . . . . 16 ⊢ ∩ (𝑡 ∪ {𝑧}) = (∩ 𝑡 ∩ 𝑧)
169	166, 168	eqtrdi 2811	. . . . . . . . . . . . . . 15 ⊢ (𝑠 = (𝑡 ∪ {𝑧}) → ∩ 𝑠 = (∩ 𝑡 ∩ 𝑧))
170	169	ineq2d 4117	. . . . . . . . . . . . . 14 ⊢ (𝑠 = (𝑡 ∪ {𝑧}) → (𝑥 ∩ ∩ 𝑠) = (𝑥 ∩ (∩ 𝑡 ∩ 𝑧)))
171	170	fveq2d 6889	. . . . . . . . . . . . 13 ⊢ (𝑠 = (𝑡 ∪ {𝑧}) → (♯‘(𝑥 ∩ ∩ 𝑠)) = (♯‘(𝑥 ∩ (∩ 𝑡 ∩ 𝑧))))
172	165, 171	oveq12d 7438	. . . . . . . . . . . 12 ⊢ (𝑠 = (𝑡 ∪ {𝑧}) → (( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) = (( -1↑(♯‘(𝑡 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑡 ∩ 𝑧)))))
173		pwfi 9310	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ Fin ↔ 𝒫 𝑦 ∈ Fin)
174	142, 173	sylib 221	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → 𝒫 𝑦 ∈ Fin)
175		eqid 2760	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ 𝒫 𝑦 ↦ (𝑢 ∪ {𝑧})) = (𝑢 ∈ 𝒫 𝑦 ↦ (𝑢 ∪ {𝑧}))
176		elpwi 4563	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 ∈ 𝒫 𝑦 → 𝑢 ⊆ 𝑦)
177	176	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → 𝑢 ⊆ 𝑦)
178		unss1 4183	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 ⊆ 𝑦 → (𝑢 ∪ {𝑧}) ⊆ (𝑦 ∪ {𝑧}))
179	177, 178	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → (𝑢 ∪ {𝑧}) ⊆ (𝑦 ∪ {𝑧}))
180		vex 3454	. . . . . . . . . . . . . . . . 17 ⊢ 𝑢 ∈ V
181		vsnex 5392	. . . . . . . . . . . . . . . . 17 ⊢ {𝑧} ∈ V
182	180, 181	unex 7761	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 ∪ {𝑧}) ∈ V
183	182	elpw 4560	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 ∪ {𝑧}) ∈ 𝒫 (𝑦 ∪ {𝑧}) ↔ (𝑢 ∪ {𝑧}) ⊆ (𝑦 ∪ {𝑧}))
184	179, 183	sylibr 237	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → (𝑢 ∪ {𝑧}) ∈ 𝒫 (𝑦 ∪ {𝑧}))
185		simpllr 788	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → ¬ 𝑧 ∈ 𝑦)
186		elpwi 4563	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 ∪ {𝑧}) ∈ 𝒫 𝑦 → (𝑢 ∪ {𝑧}) ⊆ 𝑦)
187		ssun2 4177	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑧} ⊆ (𝑢 ∪ {𝑧})
188	167	snss 4744	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ (𝑢 ∪ {𝑧}) ↔ {𝑧} ⊆ (𝑢 ∪ {𝑧}))
189	187, 188	mpbir 234	. . . . . . . . . . . . . . . . 17 ⊢ 𝑧 ∈ (𝑢 ∪ {𝑧})
190	189	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → 𝑧 ∈ (𝑢 ∪ {𝑧}))
191		ssel 3902	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 ∪ {𝑧}) ⊆ 𝑦 → (𝑧 ∈ (𝑢 ∪ {𝑧}) → 𝑧 ∈ 𝑦))
192	186, 190, 191	syl2imc 42	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → ((𝑢 ∪ {𝑧}) ∈ 𝒫 𝑦 → 𝑧 ∈ 𝑦))
193	185, 192	mtod 201	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → ¬ (𝑢 ∪ {𝑧}) ∈ 𝒫 𝑦)
194	184, 193	eldifd 4050	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → (𝑢 ∪ {𝑧}) ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))
195		eldifi 4067	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦) → 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧}))
196	195	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧}))
197	196	elpwid 4565	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → 𝑠 ⊆ (𝑦 ∪ {𝑧}))
198		uncom 4157	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∪ {𝑧}) = ({𝑧} ∪ 𝑦)
199	197, 198	sseqtrdi 3948	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → 𝑠 ⊆ ({𝑧} ∪ 𝑦))
200		ssundif 4442	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ⊆ ({𝑧} ∪ 𝑦) ↔ (𝑠 ∖ {𝑧}) ⊆ 𝑦)
201	199, 200	sylib 221	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → (𝑠 ∖ {𝑧}) ⊆ 𝑦)
202		vex 3454	. . . . . . . . . . . . . . 15 ⊢ 𝑦 ∈ V
203	202	elpw2 5295	. . . . . . . . . . . . . 14 ⊢ ((𝑠 ∖ {𝑧}) ∈ 𝒫 𝑦 ↔ (𝑠 ∖ {𝑧}) ⊆ 𝑦)
204	201, 203	sylibr 237	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → (𝑠 ∖ {𝑧}) ∈ 𝒫 𝑦)
205		elpwunsn 4644	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦) → 𝑧 ∈ 𝑠)
206	205	ad2antll 742	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → 𝑧 ∈ 𝑠)
207	206	snssd 4746	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → {𝑧} ⊆ 𝑠)
208		ssequn2 4187	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑧} ⊆ 𝑠 ↔ (𝑠 ∪ {𝑧}) = 𝑠)
209	207, 208	sylib 221	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → (𝑠 ∪ {𝑧}) = 𝑠)
210	209	eqcomd 2766	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → 𝑠 = (𝑠 ∪ {𝑧}))
211		uneq1 4160	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = (𝑠 ∖ {𝑧}) → (𝑢 ∪ {𝑧}) = ((𝑠 ∖ {𝑧}) ∪ {𝑧}))
212		undif1 4429	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑠 ∖ {𝑧}) ∪ {𝑧}) = (𝑠 ∪ {𝑧})
213	211, 212	eqtrdi 2811	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = (𝑠 ∖ {𝑧}) → (𝑢 ∪ {𝑧}) = (𝑠 ∪ {𝑧}))
214	213	eqeq2d 2771	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = (𝑠 ∖ {𝑧}) → (𝑠 = (𝑢 ∪ {𝑧}) ↔ 𝑠 = (𝑠 ∪ {𝑧})))
215	210, 214	syl5ibrcom 250	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → (𝑢 = (𝑠 ∖ {𝑧}) → 𝑠 = (𝑢 ∪ {𝑧})))
216	176	ad2antrl 741	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → 𝑢 ⊆ 𝑦)
217		simpllr 788	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → ¬ 𝑧 ∈ 𝑦)
218	216, 217	ssneldd 3911	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → ¬ 𝑧 ∈ 𝑢)
219		difsnb 4768	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑧 ∈ 𝑢 ↔ (𝑢 ∖ {𝑧}) = 𝑢)
220	218, 219	sylib 221	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → (𝑢 ∖ {𝑧}) = 𝑢)
221	220	eqcomd 2766	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → 𝑢 = (𝑢 ∖ {𝑧}))
222		difeq1 4056	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = (𝑢 ∪ {𝑧}) → (𝑠 ∖ {𝑧}) = ((𝑢 ∪ {𝑧}) ∖ {𝑧}))
223		difun2 4436	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∪ {𝑧}) ∖ {𝑧}) = (𝑢 ∖ {𝑧})
224	222, 223	eqtrdi 2811	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = (𝑢 ∪ {𝑧}) → (𝑠 ∖ {𝑧}) = (𝑢 ∖ {𝑧}))
225	224	eqeq2d 2771	. . . . . . . . . . . . . . 15 ⊢ (𝑠 = (𝑢 ∪ {𝑧}) → (𝑢 = (𝑠 ∖ {𝑧}) ↔ 𝑢 = (𝑢 ∖ {𝑧})))
226	221, 225	syl5ibrcom 250	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → (𝑠 = (𝑢 ∪ {𝑧}) → 𝑢 = (𝑠 ∖ {𝑧})))
227	215, 226	impbid 215	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦 ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → (𝑢 = (𝑠 ∖ {𝑧}) ↔ 𝑠 = (𝑢 ∪ {𝑧})))
228	175, 194, 204, 227	f1o2d 7675	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (𝑢 ∈ 𝒫 𝑦 ↦ (𝑢 ∪ {𝑧})):𝒫 𝑦–1-1-onto→(𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))
229		uneq1 4160	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝑡 → (𝑢 ∪ {𝑧}) = (𝑡 ∪ {𝑧}))
230		vex 3454	. . . . . . . . . . . . . . 15 ⊢ 𝑡 ∈ V
231	230, 181	unex 7761	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∪ {𝑧}) ∈ V
232	229, 175, 231	fvmpt 6993	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ 𝒫 𝑦 → ((𝑢 ∈ 𝒫 𝑦 ↦ (𝑢 ∪ {𝑧}))‘𝑡) = (𝑡 ∪ {𝑧}))
233	232	adantl 487	. . . . . . . . . . . 12 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑡 ∈ 𝒫 𝑦) → ((𝑢 ∈ 𝒫 𝑦 ↦ (𝑢 ∪ {𝑧}))‘𝑡) = (𝑡 ∪ {𝑧}))
234	195, 162	sylan2 605	. . . . . . . . . . . 12 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → (( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) ∈ ℂ)
235	172, 174, 228, 233, 234	fsumf1o 15889	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)(( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) = Σ𝑡 ∈ 𝒫 𝑦(( -1↑(♯‘(𝑡 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑡 ∩ 𝑧)))))
236		uneq1 4160	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑠 → (𝑡 ∪ {𝑧}) = (𝑠 ∪ {𝑧}))
237	236	fveq2d 6889	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑠 → (♯‘(𝑡 ∪ {𝑧})) = (♯‘(𝑠 ∪ {𝑧})))
238	237	oveq2d 7436	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑠 → ( -1↑(♯‘(𝑡 ∪ {𝑧}))) = ( -1↑(♯‘(𝑠 ∪ {𝑧}))))
239		inteq 4909	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑠 → ∩ 𝑡 = ∩ 𝑠)
240	239	ineq1d 4116	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑠 → (∩ 𝑡 ∩ 𝑧) = (∩ 𝑠 ∩ 𝑧))
241	240	ineq2d 4117	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑠 → (𝑥 ∩ (∩ 𝑡 ∩ 𝑧)) = (𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))
242	241	fveq2d 6889	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑠 → (♯‘(𝑥 ∩ (∩ 𝑡 ∩ 𝑧))) = (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))))
243	238, 242	oveq12d 7438	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑠 → (( -1↑(♯‘(𝑡 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑡 ∩ 𝑧)))) = (( -1↑(♯‘(𝑠 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
244	243	cbvsumv 15863	. . . . . . . . . . . 12 ⊢ Σ𝑡 ∈ 𝒫 𝑦(( -1↑(♯‘(𝑡 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑡 ∩ 𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦(( -1↑(♯‘(𝑠 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))))
245	54	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → -1 ∈ ℂ)
246		elpwi 4563	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 ∈ 𝒫 𝑦 → 𝑠 ⊆ 𝑦)
247		ssfi 9188	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ Fin ∧ 𝑠 ⊆ 𝑦) → 𝑠 ∈ Fin)
248	142, 246, 247	syl2an 608	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → 𝑠 ∈ Fin)
249	248, 152	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (♯‘𝑠) ∈ ℕ₀)
250	245, 249	expp1d 14290	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ( -1↑((♯‘𝑠) + 1)) = (( -1↑(♯‘𝑠)) · -1))
251	246	adantl 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → 𝑠 ⊆ 𝑦)
252		simpllr 788	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ¬ 𝑧 ∈ 𝑦)
253	251, 252	ssneldd 3911	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ¬ 𝑧 ∈ 𝑠)
254		hashunsng 14536	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ V → ((𝑠 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑠) → (♯‘(𝑠 ∪ {𝑧})) = ((♯‘𝑠) + 1)))
255	254	elv 3455	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑠 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑠) → (♯‘(𝑠 ∪ {𝑧})) = ((♯‘𝑠) + 1))
256	248, 253, 255	syl2anc 596	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (♯‘(𝑠 ∪ {𝑧})) = ((♯‘𝑠) + 1))
257	256	oveq2d 7436	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ( -1↑(♯‘(𝑠 ∪ {𝑧}))) = ( -1↑((♯‘𝑠) + 1)))
258	137	sseli 3904	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 ∈ 𝒫 𝑦 → 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧}))
259	258, 154	sylan2 605	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ( -1↑(♯‘𝑠)) ∈ ℂ)
260	245, 259	mulcomd 11330	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ( -1 · ( -1↑(♯‘𝑠))) = (( -1↑(♯‘𝑠)) · -1))
261	250, 257, 260	3eqtr4d 2805	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ( -1↑(♯‘(𝑠 ∪ {𝑧}))) = ( -1 · ( -1↑(♯‘𝑠))))
262	259	mulm1d 11768	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ( -1 · ( -1↑(♯‘𝑠))) = -( -1↑(♯‘𝑠)))
263	261, 262	eqtrd 2795	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ( -1↑(♯‘(𝑠 ∪ {𝑧}))) = -( -1↑(♯‘𝑠)))
264	263	oveq1d 7435	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (( -1↑(♯‘(𝑠 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))) = ( -( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
265		inss1 4133	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∩ (∩ 𝑠 ∩ 𝑧)) ⊆ 𝑥
266		ssfi 9188	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ Fin ∧ (𝑥 ∩ (∩ 𝑠 ∩ 𝑧)) ⊆ 𝑥) → (𝑥 ∩ (∩ 𝑠 ∩ 𝑧)) ∈ Fin)
267	155, 265, 266	sylancl 598	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (𝑥 ∩ (∩ 𝑠 ∩ 𝑧)) ∈ Fin)
268		hashcl 14500	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∩ (∩ 𝑠 ∩ 𝑧)) ∈ Fin → (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))) ∈ ℕ₀)
269	267, 268	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))) ∈ ℕ₀)
270	269	nn0cnd 12669	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))) ∈ ℂ)
271	258, 270	sylan2 605	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))) ∈ ℂ)
272	259, 271	mulneg1d 11769	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ( -( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))) = -(( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
273	264, 272	eqtrd 2795	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (( -1↑(♯‘(𝑠 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))) = -(( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
274	273	sumeq2dv 15869	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 𝑦(( -1↑(♯‘(𝑠 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦 -(( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
275	244, 274	eqtrid 2807	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑡 ∈ 𝒫 𝑦(( -1↑(♯‘(𝑡 ∪ {𝑧}))) · (♯‘(𝑥 ∩ (∩ 𝑡 ∩ 𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦 -(( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
276	154, 270	mulcld 11329	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))) ∈ ℂ)
277	258, 276	sylan2 605	. . . . . . . . . . . 12 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))) ∈ ℂ)
278	174, 277	fsumneg 15953	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 𝑦 -(( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))) = -Σ𝑠 ∈ 𝒫 𝑦(( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
279	235, 275, 278	3eqtrd 2799	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)(( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) = -Σ𝑠 ∈ 𝒫 𝑦(( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))))
280	279	oveq2d 7436	. . . . . . . . 9 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (Σ𝑠 ∈ 𝒫 𝑦(( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) + Σ𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)(( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))) = (Σ𝑠 ∈ 𝒫 𝑦(( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) + -Σ𝑠 ∈ 𝒫 𝑦(( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))))))
281	137	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → 𝒫 𝑦 ⊆ 𝒫 (𝑦 ∪ {𝑧}))
282	281	sselda 3908	. . . . . . . . . . . 12 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧}))
283	282, 162	syldan 603	. . . . . . . . . . 11 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) ∈ ℂ)
284	174, 283	fsumcl 15899	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 𝑦(( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) ∈ ℂ)
285	282, 276	syldan 603	. . . . . . . . . . 11 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))) ∈ ℂ)
286	174, 285	fsumcl 15899	. . . . . . . . . 10 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 𝑦(( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧)))) ∈ ℂ)
287	284, 286	negsubd 11675	. . . . . . . . 9 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (Σ𝑠 ∈ 𝒫 𝑦(( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) + -Σ𝑠 ∈ 𝒫 𝑦(( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))))) = (Σ𝑠 ∈ 𝒫 𝑦(( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) − Σ𝑠 ∈ 𝒫 𝑦(( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))))))
288	163, 280, 287	3eqtrd 2799	. . . . . . . 8 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})(( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) = (Σ𝑠 ∈ 𝒫 𝑦(( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) − Σ𝑠 ∈ 𝒫 𝑦(( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))))))
289	288	adantr 486	. . . . . . 7 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦(( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) → Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})(( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) = (Σ𝑠 ∈ 𝒫 𝑦(( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))) − Σ𝑠 ∈ 𝒫 𝑦(( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ (∩ 𝑠 ∩ 𝑧))))))
290	101, 133, 289	3eqtr4d 2805	. . . . . 6 ⊢ ((((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦(( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))) → ((♯‘𝑥) − (♯‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})(( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))))
291	290	ex 418	. . . . 5 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑥 ∈ Fin) → (∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦(( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) → ((♯‘𝑥) − (♯‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})(( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))))
292	291	ralrimdva 3162	. . . 4 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦(( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) → ∀𝑥 ∈ Fin ((♯‘𝑥) − (♯‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})(( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))))
293		ineq1 4110	. . . . . . . 8 ⊢ (𝑏 = 𝑥 → (𝑏 ∩ (∪ 𝑦 ∪ 𝑧)) = (𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))
294	293	fveq2d 6889	. . . . . . 7 ⊢ (𝑏 = 𝑥 → (♯‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧))) = (♯‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧))))
295	66, 294	oveq12d 7438	. . . . . 6 ⊢ (𝑏 = 𝑥 → ((♯‘𝑏) − (♯‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧)))) = ((♯‘𝑥) − (♯‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))))
296		ineq1 4110	. . . . . . . . 9 ⊢ (𝑏 = 𝑥 → (𝑏 ∩ ∩ 𝑠) = (𝑥 ∩ ∩ 𝑠))
297	296	fveq2d 6889	. . . . . . . 8 ⊢ (𝑏 = 𝑥 → (♯‘(𝑏 ∩ ∩ 𝑠)) = (♯‘(𝑥 ∩ ∩ 𝑠)))
298	297	oveq2d 7436	. . . . . . 7 ⊢ (𝑏 = 𝑥 → (( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) = (( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))))
299	298	sumeq2sdv 15870	. . . . . 6 ⊢ (𝑏 = 𝑥 → Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})(( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})(( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))))
300	295, 299	eqeq12d 2776	. . . . 5 ⊢ (𝑏 = 𝑥 → (((♯‘𝑏) − (♯‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})(( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) ↔ ((♯‘𝑥) − (♯‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})(( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠)))))
301	300	cbvralvw 3240	. . . 4 ⊢ (∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})(( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) ↔ ∀𝑥 ∈ Fin ((♯‘𝑥) − (♯‘(𝑥 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})(( -1↑(♯‘𝑠)) · (♯‘(𝑥 ∩ ∩ 𝑠))))
302	292, 301	imbitrrdi 255	. . 3 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦(( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) → ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ (∪ 𝑦 ∪ 𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})(( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠)))))
303	16, 24, 37, 45, 65, 302	findcard2s 9181	. 2 ⊢ (𝐴 ∈ Fin → ∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴(( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))))
304		fveq2 6885	. . . . 5 ⊢ (𝑏 = 𝐵 → (♯‘𝑏) = (♯‘𝐵))
305		ineq1 4110	. . . . . 6 ⊢ (𝑏 = 𝐵 → (𝑏 ∩ ∪ 𝐴) = (𝐵 ∩ ∪ 𝐴))
306	305	fveq2d 6889	. . . . 5 ⊢ (𝑏 = 𝐵 → (♯‘(𝑏 ∩ ∪ 𝐴)) = (♯‘(𝐵 ∩ ∪ 𝐴)))
307	304, 306	oveq12d 7438	. . . 4 ⊢ (𝑏 = 𝐵 → ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝐴))) = ((♯‘𝐵) − (♯‘(𝐵 ∩ ∪ 𝐴))))
308		simpl 488	. . . . . . . 8 ⊢ ((𝑏 = 𝐵 ∧ 𝑠 ∈ 𝒫 𝐴) → 𝑏 = 𝐵)
309	308	ineq1d 4116	. . . . . . 7 ⊢ ((𝑏 = 𝐵 ∧ 𝑠 ∈ 𝒫 𝐴) → (𝑏 ∩ ∩ 𝑠) = (𝐵 ∩ ∩ 𝑠))
310	309	fveq2d 6889	. . . . . 6 ⊢ ((𝑏 = 𝐵 ∧ 𝑠 ∈ 𝒫 𝐴) → (♯‘(𝑏 ∩ ∩ 𝑠)) = (♯‘(𝐵 ∩ ∩ 𝑠)))
311	310	oveq2d 7436	. . . . 5 ⊢ ((𝑏 = 𝐵 ∧ 𝑠 ∈ 𝒫 𝐴) → (( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) = (( -1↑(♯‘𝑠)) · (♯‘(𝐵 ∩ ∩ 𝑠))))
312	311	sumeq2dv 15869	. . . 4 ⊢ (𝑏 = 𝐵 → Σ𝑠 ∈ 𝒫 𝐴(( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) = Σ𝑠 ∈ 𝒫 𝐴(( -1↑(♯‘𝑠)) · (♯‘(𝐵 ∩ ∩ 𝑠))))
313	307, 312	eqeq12d 2776	. . 3 ⊢ (𝑏 = 𝐵 → (((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴(( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) ↔ ((♯‘𝐵) − (♯‘(𝐵 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴(( -1↑(♯‘𝑠)) · (♯‘(𝐵 ∩ ∩ 𝑠)))))
314	313	rspccva 3575	. 2 ⊢ ((∀𝑏 ∈ Fin ((♯‘𝑏) − (♯‘(𝑏 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴(( -1↑(♯‘𝑠)) · (♯‘(𝑏 ∩ ∩ 𝑠))) ∧ 𝐵 ∈ Fin) → ((♯‘𝐵) − (♯‘(𝐵 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴(( -1↑(♯‘𝑠)) · (♯‘(𝐵 ∩ ∩ 𝑠))))
315	303, 314	sylan 592	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((♯‘𝐵) − (♯‘(𝐵 ∩ ∪ 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴(( -1↑(♯‘𝑠)) · (♯‘(𝐵 ∩ ∩ 𝑠))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 401 = wceq 1569 ∈ wcel 2144 ∀wral 3076 Vcvv 3450 ⊆ wss 3895 ∖ cdif 4045 ∩ cin 4089 ∪ cun 4149 ∅c0 4278 𝒫 cpw 4556 {csn 4583 ∪ cuni 4866 ∩ cint 4906 ↦ cmpt 5185 ‘cfv 6538 (class class class)co 7420 Fincfn 8973 ℂcc 11198 0cc0 11200 1c1 11201 + caddc 11203 · cmul 11205 − cmin 11541 -cneg 11542 ℕ₀cn0 12606 ↑cexp 14204 ♯chash 14474 Σcsu 15853

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751 ax-inf2 9642 ax-cnex 11256 ax-resscn 11257 ax-1cn 11258 ax-icn 11259 ax-addcl 11260 ax-addrcl 11261 ax-mulcl 11262 ax-mulrcl 11263 ax-mulcom 11264 ax-addass 11265 ax-mulass 11266 ax-distr 11267 ax-i2m1 11268 ax-1ne0 11269 ax-1rid 11270 ax-rnegex 11271 ax-rrecex 11272 ax-cnre 11273 ax-pre-lttri 11274 ax-pre-lttrn 11275 ax-pre-ltadd 11276 ax-pre-mulgt0 11277 ax-pre-sup 11278

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4584 df-pr 4586 df-op 4590 df-uni 4867 df-int 4907 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-se 5604 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-isom 6547 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-om 7878 df-1st 8001 df-2nd 8002 df-frecs 8299 df-wrecs 8330 df-recs 8379 df-rdg 8418 df-1o 8476 df-oadd 8480 df-er 8717 df-en 8974 df-dom 8975 df-sdom 8976 df-fin 8977 df-sup 9434 df-oi 9504 df-dju 9982 df-card 10020 df-pnf 11345 df-mnf 11346 df-xr 11347 df-ltxr 11348 df-le 11349 df-sub 11543 df-neg 11544 df-div 11974 df-nn 12336 df-2 12405 df-3 12406 df-n0 12607 df-z 12694 df-uz 12966 df-rp 13121 df-fz 13640 df-fzo 13789 df-seq 14145 df-exp 14205 df-hash 14475 df-cj 15266 df-re 15267 df-im 15268 df-sqrt 15402 df-abs 15403 df-clim 15655 df-sum 15854

This theorem is used by: incexc 16006

W3C validator