Theorem incexclem

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

	Ref	Expression
Assertion	incexclem	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left|B\right|-\left|B\cap \bigcup A\right|=\sum _{s\in 𝒫A}{\left(-1\right)}^{\left|s\right|}\left|B\cap \bigcap s\right|$$

Proof

Step	Hyp	Ref	Expression
1		unieq	$$⊢x=\varnothing \to \bigcup x=\bigcup \varnothing$$
2		uni0	$$⊢\bigcup \varnothing =\varnothing$$
3	1 2	eqtrdi	$$⊢x=\varnothing \to \bigcup x=\varnothing$$
4	3	ineq2d	$$⊢x=\varnothing \to b\cap \bigcup x=b\cap \varnothing$$
5		in0	$$⊢b\cap \varnothing =\varnothing$$
6	4 5	eqtrdi	$$⊢x=\varnothing \to b\cap \bigcup x=\varnothing$$
7	6	fveq2d	$$⊢x=\varnothing \to \left|b\cap \bigcup x\right|=\left|\varnothing \right|$$
8		hash0	$$⊢\left|\varnothing \right|=0$$
9	7 8	eqtrdi	$$⊢x=\varnothing \to \left|b\cap \bigcup x\right|=0$$
10	9	oveq2d	$$⊢x=\varnothing \to \left|b\right|-\left|b\cap \bigcup x\right|=\left|b\right|-0$$
11		pweq	$$⊢x=\varnothing \to 𝒫x=𝒫\varnothing$$
12		pw0	$$⊢𝒫\varnothing =\left\{\varnothing \right\}$$
13	11 12	eqtrdi	$$⊢x=\varnothing \to 𝒫x=\left\{\varnothing \right\}$$
14	13	sumeq1d	$$⊢x=\varnothing \to \sum _{s\in 𝒫x}{\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|=\sum _{s\in \left\{\varnothing \right\}}{\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|$$
15	10 14	eqeq12d	$$⊢x=\varnothing \to \left(\left|b\right|-\left|b\cap \bigcup x\right|=\sum _{s\in 𝒫x}{\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|\leftrightarrow \left|b\right|-0=\sum _{s\in \left\{\varnothing \right\}}{\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|\right)$$
16	15	ralbidv	$$⊢x=\varnothing \to \left(\forall b\in \mathrm{Fin}\left|b\right|-\left|b\cap \bigcup x\right|=\sum _{s\in 𝒫x}{\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|\leftrightarrow \forall b\in \mathrm{Fin}\left|b\right|-0=\sum _{s\in \left\{\varnothing \right\}}{\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|\right)$$
17		unieq	$$⊢x=y\to \bigcup x=\bigcup y$$
18	17	ineq2d	$$⊢x=y\to b\cap \bigcup x=b\cap \bigcup y$$
19	18	fveq2d	$$⊢x=y\to \left|b\cap \bigcup x\right|=\left|b\cap \bigcup y\right|$$
20	19	oveq2d	$$⊢x=y\to \left|b\right|-\left|b\cap \bigcup x\right|=\left|b\right|-\left|b\cap \bigcup y\right|$$
21		pweq	$$⊢x=y\to 𝒫x=𝒫y$$
22	21	sumeq1d	$$⊢x=y\to \sum _{s\in 𝒫x}{\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|=\sum _{s\in 𝒫y}{\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|$$
23	20 22	eqeq12d	$$⊢x=y\to \left(\left|b\right|-\left|b\cap \bigcup x\right|=\sum _{s\in 𝒫x}{\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|\leftrightarrow \left|b\right|-\left|b\cap \bigcup y\right|=\sum _{s\in 𝒫y}{\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|\right)$$
24	23	ralbidv	$$⊢x=y\to \left(\forall b\in \mathrm{Fin}\left|b\right|-\left|b\cap \bigcup x\right|=\sum _{s\in 𝒫x}{\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|\leftrightarrow \forall b\in \mathrm{Fin}\left|b\right|-\left|b\cap \bigcup y\right|=\sum _{s\in 𝒫y}{\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|\right)$$
25		unieq	$$⊢x=y\cup \left\{z\right\}\to \bigcup x=\bigcup \left(y\cup \left\{z\right\}\right)$$
26		uniun	$$⊢\bigcup \left(y\cup \left\{z\right\}\right)=\bigcup y\cup \bigcup \left\{z\right\}$$
27		vex	$$⊢z\in \mathrm{V}$$
28	27	unisn	$$⊢\bigcup \left\{z\right\}=z$$
29	28	uneq2i	$$⊢\bigcup y\cup \bigcup \left\{z\right\}=\bigcup y\cup z$$
30	26 29	eqtri	$$⊢\bigcup \left(y\cup \left\{z\right\}\right)=\bigcup y\cup z$$
31	25 30	eqtrdi	$$⊢x=y\cup \left\{z\right\}\to \bigcup x=\bigcup y\cup z$$
32	31	ineq2d	$$⊢x=y\cup \left\{z\right\}\to b\cap \bigcup x=b\cap \left(\bigcup y\cup z\right)$$
33	32	fveq2d	$$⊢x=y\cup \left\{z\right\}\to \left|b\cap \bigcup x\right|=\left|b\cap \left(\bigcup y\cup z\right)\right|$$
34	33	oveq2d	$$⊢x=y\cup \left\{z\right\}\to \left|b\right|-\left|b\cap \bigcup x\right|=\left|b\right|-\left|b\cap \left(\bigcup y\cup z\right)\right|$$
35		pweq	$$⊢x=y\cup \left\{z\right\}\to 𝒫x=𝒫\left(y\cup \left\{z\right\}\right)$$
36	35	sumeq1d	$$⊢x=y\cup \left\{z\right\}\to \sum _{s\in 𝒫x}{\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|=\sum _{s\in 𝒫\left(y\cup \left\{z\right\}\right)}{\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|$$
37	34 36	eqeq12d	$$⊢x=y\cup \left\{z\right\}\to \left(\left|b\right|-\left|b\cap \bigcup x\right|=\sum _{s\in 𝒫x}{\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|\leftrightarrow \left|b\right|-\left|b\cap \left(\bigcup y\cup z\right)\right|=\sum _{s\in 𝒫\left(y\cup \left\{z\right\}\right)}{\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|\right)$$
38	37	ralbidv	$$⊢x=y\cup \left\{z\right\}\to \left(\forall b\in \mathrm{Fin}\left|b\right|-\left|b\cap \bigcup x\right|=\sum _{s\in 𝒫x}{\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|\leftrightarrow \forall b\in \mathrm{Fin}\left|b\right|-\left|b\cap \left(\bigcup y\cup z\right)\right|=\sum _{s\in 𝒫\left(y\cup \left\{z\right\}\right)}{\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|\right)$$
39		unieq	$$⊢x=A\to \bigcup x=\bigcup A$$
40	39	ineq2d	$$⊢x=A\to b\cap \bigcup x=b\cap \bigcup A$$
41	40	fveq2d	$$⊢x=A\to \left|b\cap \bigcup x\right|=\left|b\cap \bigcup A\right|$$
42	41	oveq2d	$$⊢x=A\to \left|b\right|-\left|b\cap \bigcup x\right|=\left|b\right|-\left|b\cap \bigcup A\right|$$
43		pweq	$$⊢x=A\to 𝒫x=𝒫A$$
44	43	sumeq1d	$$⊢x=A\to \sum _{s\in 𝒫x}{\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|=\sum _{s\in 𝒫A}{\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|$$
45	42 44	eqeq12d	$$⊢x=A\to \left(\left|b\right|-\left|b\cap \bigcup x\right|=\sum _{s\in 𝒫x}{\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|\leftrightarrow \left|b\right|-\left|b\cap \bigcup A\right|=\sum _{s\in 𝒫A}{\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|\right)$$
46	45	ralbidv	$$⊢x=A\to \left(\forall b\in \mathrm{Fin}\left|b\right|-\left|b\cap \bigcup x\right|=\sum _{s\in 𝒫x}{\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|\leftrightarrow \forall b\in \mathrm{Fin}\left|b\right|-\left|b\cap \bigcup A\right|=\sum _{s\in 𝒫A}{\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|\right)$$
47		hashcl	$$⊢b\in \mathrm{Fin}\to \left|b\right|\in {\mathbb{N}}_0$$
48	47	nn0cnd	$$⊢b\in \mathrm{Fin}\to \left|b\right|\in ℂ$$
49	48	mulid2d	$$⊢b\in \mathrm{Fin}\to 1\left|b\right|=\left|b\right|$$
50		0ex	$$⊢\varnothing \in \mathrm{V}$$
51	49 48	eqeltrd	$$⊢b\in \mathrm{Fin}\to 1\left|b\right|\in ℂ$$
52		fveq2	$$⊢s=\varnothing \to \left|s\right|=\left|\varnothing \right|$$
53	52 8	eqtrdi	$$⊢s=\varnothing \to \left|s\right|=0$$
54	53	oveq2d	$$⊢s=\varnothing \to {\left(-1\right)}^{\left|s\right|}={\left(-1\right)}^0$$
55		neg1cn	$$⊢-1\in ℂ$$
56		exp0	$$⊢-1\in ℂ\to {\left(-1\right)}^0=1$$
57	55 56	ax-mp	$$⊢{\left(-1\right)}^0=1$$
58	54 57	eqtrdi	$$⊢s=\varnothing \to {\left(-1\right)}^{\left|s\right|}=1$$
59		rint0	$$⊢s=\varnothing \to b\cap \bigcap s=b$$
60	59	fveq2d	$$⊢s=\varnothing \to \left|b\cap \bigcap s\right|=\left|b\right|$$
61	58 60	oveq12d	$$⊢s=\varnothing \to {\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|=1\left|b\right|$$
62	61	sumsn	$$⊢\left(\varnothing \in \mathrm{V}\wedge 1\left|b\right|\in ℂ\right)\to \sum _{s\in \left\{\varnothing \right\}}{\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|=1\left|b\right|$$
63	50 51 62	sylancr	$$⊢b\in \mathrm{Fin}\to \sum _{s\in \left\{\varnothing \right\}}{\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|=1\left|b\right|$$
64	48	subid1d	$$⊢b\in \mathrm{Fin}\to \left|b\right|-0=\left|b\right|$$
65	49 63 64	3eqtr4rd	$$⊢b\in \mathrm{Fin}\to \left|b\right|-0=\sum _{s\in \left\{\varnothing \right\}}{\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|$$
66	65	rgen	$$⊢\forall b\in \mathrm{Fin}\left|b\right|-0=\sum _{s\in \left\{\varnothing \right\}}{\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|$$
67		fveq2	$$⊢b=x\to \left|b\right|=\left|x\right|$$
68		ineq1	$$⊢b=x\to b\cap \bigcup y=x\cap \bigcup y$$
69	68	fveq2d	$$⊢b=x\to \left|b\cap \bigcup y\right|=\left|x\cap \bigcup y\right|$$
70	67 69	oveq12d	$$⊢b=x\to \left|b\right|-\left|b\cap \bigcup y\right|=\left|x\right|-\left|x\cap \bigcup y\right|$$
71		simpl	$$⊢\left(b=x\wedge s\in 𝒫y\right)\to b=x$$
72	71	ineq1d	$$⊢\left(b=x\wedge s\in 𝒫y\right)\to b\cap \bigcap s=x\cap \bigcap s$$
73	72	fveq2d	$$⊢\left(b=x\wedge s\in 𝒫y\right)\to \left|b\cap \bigcap s\right|=\left|x\cap \bigcap s\right|$$
74	73	oveq2d	$$⊢\left(b=x\wedge s\in 𝒫y\right)\to {\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|={\left(-1\right)}^{\left|s\right|}\left|x\cap \bigcap s\right|$$
75	74	sumeq2dv	$$⊢b=x\to \sum _{s\in 𝒫y}{\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|=\sum _{s\in 𝒫y}{\left(-1\right)}^{\left|s\right|}\left|x\cap \bigcap s\right|$$
76	70 75	eqeq12d	$$⊢b=x\to \left(\left|b\right|-\left|b\cap \bigcup y\right|=\sum _{s\in 𝒫y}{\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|\leftrightarrow \left|x\right|-\left|x\cap \bigcup y\right|=\sum _{s\in 𝒫y}{\left(-1\right)}^{\left|s\right|}\left|x\cap \bigcap s\right|\right)$$
77	76	rspcva	$$⊢\left(x\in \mathrm{Fin}\wedge \forall b\in \mathrm{Fin}\left|b\right|-\left|b\cap \bigcup y\right|=\sum _{s\in 𝒫y}{\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|\right)\to \left|x\right|-\left|x\cap \bigcup y\right|=\sum _{s\in 𝒫y}{\left(-1\right)}^{\left|s\right|}\left|x\cap \bigcap s\right|$$
78	77	adantll	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge \forall b\in \mathrm{Fin}\left|b\right|-\left|b\cap \bigcup y\right|=\sum _{s\in 𝒫y}{\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|\right)\to \left|x\right|-\left|x\cap \bigcup y\right|=\sum _{s\in 𝒫y}{\left(-1\right)}^{\left|s\right|}\left|x\cap \bigcap s\right|$$
79		simpr	$$⊢\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\to x\in \mathrm{Fin}$$
80		inss1	$$⊢x\cap z\subseteq x$$
81		ssfi	$$⊢\left(x\in \mathrm{Fin}\wedge x\cap z\subseteq x\right)\to x\cap z\in \mathrm{Fin}$$
82	79 80 81	sylancl	$$⊢\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\to x\cap z\in \mathrm{Fin}$$
83		fveq2	$$⊢b=x\cap z\to \left|b\right|=\left|x\cap z\right|$$
84		ineq1	$$⊢b=x\cap z\to b\cap \bigcup y=\left(x\cap z\right)\cap \bigcup y$$
85		in32	$$⊢\left(x\cap z\right)\cap \bigcup y=\left(x\cap \bigcup y\right)\cap z$$
86		inass	$$⊢\left(x\cap \bigcup y\right)\cap z=x\cap \left(\bigcup y\cap z\right)$$
87	85 86	eqtri	$$⊢\left(x\cap z\right)\cap \bigcup y=x\cap \left(\bigcup y\cap z\right)$$
88	84 87	eqtrdi	$$⊢b=x\cap z\to b\cap \bigcup y=x\cap \left(\bigcup y\cap z\right)$$
89	88	fveq2d	$$⊢b=x\cap z\to \left|b\cap \bigcup y\right|=\left|x\cap \left(\bigcup y\cap z\right)\right|$$
90	83 89	oveq12d	$$⊢b=x\cap z\to \left|b\right|-\left|b\cap \bigcup y\right|=\left|x\cap z\right|-\left|x\cap \left(\bigcup y\cap z\right)\right|$$
91		ineq1	$$⊢b=x\cap z\to b\cap \bigcap s=\left(x\cap z\right)\cap \bigcap s$$
92		in32	$$⊢\left(x\cap z\right)\cap \bigcap s=\left(x\cap \bigcap s\right)\cap z$$
93		inass	$$⊢\left(x\cap \bigcap s\right)\cap z=x\cap \left(\bigcap s\cap z\right)$$
94	92 93	eqtri	$$⊢\left(x\cap z\right)\cap \bigcap s=x\cap \left(\bigcap s\cap z\right)$$
95	91 94	eqtrdi	$$⊢b=x\cap z\to b\cap \bigcap s=x\cap \left(\bigcap s\cap z\right)$$
96	95	fveq2d	$$⊢b=x\cap z\to \left|b\cap \bigcap s\right|=\left|x\cap \left(\bigcap s\cap z\right)\right|$$
97	96	oveq2d	$$⊢b=x\cap z\to {\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|={\left(-1\right)}^{\left|s\right|}\left|x\cap \left(\bigcap s\cap z\right)\right|$$
98	97	sumeq2sdv	$$⊢b=x\cap z\to \sum _{s\in 𝒫y}{\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|=\sum _{s\in 𝒫y}{\left(-1\right)}^{\left|s\right|}\left|x\cap \left(\bigcap s\cap z\right)\right|$$
99	90 98	eqeq12d	$$⊢b=x\cap z\to \left(\left|b\right|-\left|b\cap \bigcup y\right|=\sum _{s\in 𝒫y}{\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|\leftrightarrow \left|x\cap z\right|-\left|x\cap \left(\bigcup y\cap z\right)\right|=\sum _{s\in 𝒫y}{\left(-1\right)}^{\left|s\right|}\left|x\cap \left(\bigcap s\cap z\right)\right|\right)$$
100	99	rspcva	$$⊢\left(x\cap z\in \mathrm{Fin}\wedge \forall b\in \mathrm{Fin}\left|b\right|-\left|b\cap \bigcup y\right|=\sum _{s\in 𝒫y}{\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|\right)\to \left|x\cap z\right|-\left|x\cap \left(\bigcup y\cap z\right)\right|=\sum _{s\in 𝒫y}{\left(-1\right)}^{\left|s\right|}\left|x\cap \left(\bigcap s\cap z\right)\right|$$
101	82 100	sylan	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge \forall b\in \mathrm{Fin}\left|b\right|-\left|b\cap \bigcup y\right|=\sum _{s\in 𝒫y}{\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|\right)\to \left|x\cap z\right|-\left|x\cap \left(\bigcup y\cap z\right)\right|=\sum _{s\in 𝒫y}{\left(-1\right)}^{\left|s\right|}\left|x\cap \left(\bigcap s\cap z\right)\right|$$
102	78 101	oveq12d	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge \forall b\in \mathrm{Fin}\left|b\right|-\left|b\cap \bigcup y\right|=\sum _{s\in 𝒫y}{\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|\right)\to \left|x\right|-\left|x\cap \bigcup y\right|-\left(\left|x\cap z\right|-\left|x\cap \left(\bigcup y\cap z\right)\right|\right)=\sum _{s\in 𝒫y}{\left(-1\right)}^{\left|s\right|}\left|x\cap \bigcap s\right|-\sum _{s\in 𝒫y}{\left(-1\right)}^{\left|s\right|}\left|x\cap \left(\bigcap s\cap z\right)\right|$$
103		inss1	$$⊢x\cap \bigcup y\subseteq x$$
104		ssfi	$$⊢\left(x\in \mathrm{Fin}\wedge x\cap \bigcup y\subseteq x\right)\to x\cap \bigcup y\in \mathrm{Fin}$$
105	79 103 104	sylancl	$$⊢\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\to x\cap \bigcup y\in \mathrm{Fin}$$
106		hashcl	$$⊢x\cap \bigcup y\in \mathrm{Fin}\to \left|x\cap \bigcup y\right|\in {\mathbb{N}}_0$$
107	105 106	syl	$$⊢\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\to \left|x\cap \bigcup y\right|\in {\mathbb{N}}_0$$
108	107	nn0cnd	$$⊢\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\to \left|x\cap \bigcup y\right|\in ℂ$$
109		hashcl	$$⊢x\cap z\in \mathrm{Fin}\to \left|x\cap z\right|\in {\mathbb{N}}_0$$
110	82 109	syl	$$⊢\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\to \left|x\cap z\right|\in {\mathbb{N}}_0$$
111	110	nn0cnd	$$⊢\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\to \left|x\cap z\right|\in ℂ$$
112		inss1	$$⊢x\cap \left(\bigcup y\cap z\right)\subseteq x$$
113		ssfi	$$⊢\left(x\in \mathrm{Fin}\wedge x\cap \left(\bigcup y\cap z\right)\subseteq x\right)\to x\cap \left(\bigcup y\cap z\right)\in \mathrm{Fin}$$
114	79 112 113	sylancl	$$⊢\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\to x\cap \left(\bigcup y\cap z\right)\in \mathrm{Fin}$$
115		hashcl	$$⊢x\cap \left(\bigcup y\cap z\right)\in \mathrm{Fin}\to \left|x\cap \left(\bigcup y\cap z\right)\right|\in {\mathbb{N}}_0$$
116	114 115	syl	$$⊢\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\to \left|x\cap \left(\bigcup y\cap z\right)\right|\in {\mathbb{N}}_0$$
117	116	nn0cnd	$$⊢\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\to \left|x\cap \left(\bigcup y\cap z\right)\right|\in ℂ$$
118		hashun3	$$⊢\left(x\cap \bigcup y\in \mathrm{Fin}\wedge x\cap z\in \mathrm{Fin}\right)\to \left|\left(x\cap \bigcup y\right)\cup \left(x\cap z\right)\right|=\left|x\cap \bigcup y\right|+\left|x\cap z\right|-\left|\left(x\cap \bigcup y\right)\cap \left(x\cap z\right)\right|$$
119	105 82 118	syl2anc	$$⊢\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\to \left|\left(x\cap \bigcup y\right)\cup \left(x\cap z\right)\right|=\left|x\cap \bigcup y\right|+\left|x\cap z\right|-\left|\left(x\cap \bigcup y\right)\cap \left(x\cap z\right)\right|$$
120		indi	$$⊢x\cap \left(\bigcup y\cup z\right)=\left(x\cap \bigcup y\right)\cup \left(x\cap z\right)$$
121	120	fveq2i	$$⊢\left|x\cap \left(\bigcup y\cup z\right)\right|=\left|\left(x\cap \bigcup y\right)\cup \left(x\cap z\right)\right|$$
122		inindi	$$⊢x\cap \left(\bigcup y\cap z\right)=\left(x\cap \bigcup y\right)\cap \left(x\cap z\right)$$
123	122	fveq2i	$$⊢\left|x\cap \left(\bigcup y\cap z\right)\right|=\left|\left(x\cap \bigcup y\right)\cap \left(x\cap z\right)\right|$$
124	123	oveq2i	$$⊢\left|x\cap \bigcup y\right|+\left|x\cap z\right|-\left|x\cap \left(\bigcup y\cap z\right)\right|=\left|x\cap \bigcup y\right|+\left|x\cap z\right|-\left|\left(x\cap \bigcup y\right)\cap \left(x\cap z\right)\right|$$
125	119 121 124	3eqtr4g	$$⊢\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\to \left|x\cap \left(\bigcup y\cup z\right)\right|=\left|x\cap \bigcup y\right|+\left|x\cap z\right|-\left|x\cap \left(\bigcup y\cap z\right)\right|$$
126	108 111 117 125	assraddsubd	$$⊢\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\to \left|x\cap \left(\bigcup y\cup z\right)\right|=\left|x\cap \bigcup y\right|+\left|x\cap z\right|-\left|x\cap \left(\bigcup y\cap z\right)\right|$$
127	126	oveq2d	$$⊢\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\to \left|x\right|-\left|x\cap \left(\bigcup y\cup z\right)\right|=\left|x\right|-\left(\left|x\cap \bigcup y\right|+\left|x\cap z\right|-\left|x\cap \left(\bigcup y\cap z\right)\right|\right)$$
128		hashcl	$$⊢x\in \mathrm{Fin}\to \left|x\right|\in {\mathbb{N}}_0$$
129	128	adantl	$$⊢\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\to \left|x\right|\in {\mathbb{N}}_0$$
130	129	nn0cnd	$$⊢\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\to \left|x\right|\in ℂ$$
131	111 117	subcld	$$⊢\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\to \left|x\cap z\right|-\left|x\cap \left(\bigcup y\cap z\right)\right|\in ℂ$$
132	130 108 131	subsub4d	$$⊢\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\to \left|x\right|-\left|x\cap \bigcup y\right|-\left(\left|x\cap z\right|-\left|x\cap \left(\bigcup y\cap z\right)\right|\right)=\left|x\right|-\left(\left|x\cap \bigcup y\right|+\left|x\cap z\right|-\left|x\cap \left(\bigcup y\cap z\right)\right|\right)$$
133	127 132	eqtr4d	$$⊢\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\to \left|x\right|-\left|x\cap \left(\bigcup y\cup z\right)\right|=\left|x\right|-\left|x\cap \bigcup y\right|-\left(\left|x\cap z\right|-\left|x\cap \left(\bigcup y\cap z\right)\right|\right)$$
134	133	adantr	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge \forall b\in \mathrm{Fin}\left|b\right|-\left|b\cap \bigcup y\right|=\sum _{s\in 𝒫y}{\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|\right)\to \left|x\right|-\left|x\cap \left(\bigcup y\cup z\right)\right|=\left|x\right|-\left|x\cap \bigcup y\right|-\left(\left|x\cap z\right|-\left|x\cap \left(\bigcup y\cap z\right)\right|\right)$$
135		disjdif	$$⊢𝒫y\cap \left(𝒫\left(y\cup \left\{z\right\}\right)\setminus 𝒫y\right)=\varnothing$$
136	135	a1i	$$⊢\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\to 𝒫y\cap \left(𝒫\left(y\cup \left\{z\right\}\right)\setminus 𝒫y\right)=\varnothing$$
137		ssun1	$$⊢y\subseteq y\cup \left\{z\right\}$$
138	137	sspwi	$$⊢𝒫y\subseteq 𝒫\left(y\cup \left\{z\right\}\right)$$
139		undif	$$⊢𝒫y\subseteq 𝒫\left(y\cup \left\{z\right\}\right)\leftrightarrow 𝒫y\cup \left(𝒫\left(y\cup \left\{z\right\}\right)\setminus 𝒫y\right)=𝒫\left(y\cup \left\{z\right\}\right)$$
140	138 139	mpbi	$$⊢𝒫y\cup \left(𝒫\left(y\cup \left\{z\right\}\right)\setminus 𝒫y\right)=𝒫\left(y\cup \left\{z\right\}\right)$$
141	140	eqcomi	$$⊢𝒫\left(y\cup \left\{z\right\}\right)=𝒫y\cup \left(𝒫\left(y\cup \left\{z\right\}\right)\setminus 𝒫y\right)$$
142	141	a1i	$$⊢\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\to 𝒫\left(y\cup \left\{z\right\}\right)=𝒫y\cup \left(𝒫\left(y\cup \left\{z\right\}\right)\setminus 𝒫y\right)$$
143		simpll	$$⊢\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\to y\in \mathrm{Fin}$$
144		snfi	$$⊢\left\{z\right\}\in \mathrm{Fin}$$
145		unfi	$$⊢\left(y\in \mathrm{Fin}\wedge \left\{z\right\}\in \mathrm{Fin}\right)\to y\cup \left\{z\right\}\in \mathrm{Fin}$$
146	143 144 145	sylancl	$$⊢\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\to y\cup \left\{z\right\}\in \mathrm{Fin}$$
147		pwfi	$$⊢y\cup \left\{z\right\}\in \mathrm{Fin}\leftrightarrow 𝒫\left(y\cup \left\{z\right\}\right)\in \mathrm{Fin}$$
148	146 147	sylib	$$⊢\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\to 𝒫\left(y\cup \left\{z\right\}\right)\in \mathrm{Fin}$$
149	55	a1i	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge s\in 𝒫\left(y\cup \left\{z\right\}\right)\right)\to -1\in ℂ$$
150		elpwi	$$⊢s\in 𝒫\left(y\cup \left\{z\right\}\right)\to s\subseteq y\cup \left\{z\right\}$$
151		ssfi	$$⊢\left(y\cup \left\{z\right\}\in \mathrm{Fin}\wedge s\subseteq y\cup \left\{z\right\}\right)\to s\in \mathrm{Fin}$$
152	146 150 151	syl2an	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge s\in 𝒫\left(y\cup \left\{z\right\}\right)\right)\to s\in \mathrm{Fin}$$
153		hashcl	$$⊢s\in \mathrm{Fin}\to \left|s\right|\in {\mathbb{N}}_0$$
154	152 153	syl	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge s\in 𝒫\left(y\cup \left\{z\right\}\right)\right)\to \left|s\right|\in {\mathbb{N}}_0$$
155	149 154	expcld	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge s\in 𝒫\left(y\cup \left\{z\right\}\right)\right)\to {\left(-1\right)}^{\left|s\right|}\in ℂ$$
156		simplr	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge s\in 𝒫\left(y\cup \left\{z\right\}\right)\right)\to x\in \mathrm{Fin}$$
157		inss1	$$⊢x\cap \bigcap s\subseteq x$$
158		ssfi	$$⊢\left(x\in \mathrm{Fin}\wedge x\cap \bigcap s\subseteq x\right)\to x\cap \bigcap s\in \mathrm{Fin}$$
159	156 157 158	sylancl	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge s\in 𝒫\left(y\cup \left\{z\right\}\right)\right)\to x\cap \bigcap s\in \mathrm{Fin}$$
160		hashcl	$$⊢x\cap \bigcap s\in \mathrm{Fin}\to \left|x\cap \bigcap s\right|\in {\mathbb{N}}_0$$
161	159 160	syl	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge s\in 𝒫\left(y\cup \left\{z\right\}\right)\right)\to \left|x\cap \bigcap s\right|\in {\mathbb{N}}_0$$
162	161	nn0cnd	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge s\in 𝒫\left(y\cup \left\{z\right\}\right)\right)\to \left|x\cap \bigcap s\right|\in ℂ$$
163	155 162	mulcld	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge s\in 𝒫\left(y\cup \left\{z\right\}\right)\right)\to {\left(-1\right)}^{\left|s\right|}\left|x\cap \bigcap s\right|\in ℂ$$
164	136 142 148 163	fsumsplit	$$⊢\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\to \sum _{s\in 𝒫\left(y\cup \left\{z\right\}\right)}{\left(-1\right)}^{\left|s\right|}\left|x\cap \bigcap s\right|=\sum _{s\in 𝒫y}{\left(-1\right)}^{\left|s\right|}\left|x\cap \bigcap s\right|+\sum _{s\in 𝒫\left(y\cup \left\{z\right\}\right)\setminus 𝒫y}{\left(-1\right)}^{\left|s\right|}\left|x\cap \bigcap s\right|$$
165		fveq2	$$⊢s=t\cup \left\{z\right\}\to \left|s\right|=\left|t\cup \left\{z\right\}\right|$$
166	165	oveq2d	$$⊢s=t\cup \left\{z\right\}\to {\left(-1\right)}^{\left|s\right|}={\left(-1\right)}^{\left|t\cup \left\{z\right\}\right|}$$
167		inteq	$$⊢s=t\cup \left\{z\right\}\to \bigcap s=\bigcap \left(t\cup \left\{z\right\}\right)$$
168	27	intunsn	$$⊢\bigcap \left(t\cup \left\{z\right\}\right)=\bigcap t\cap z$$
169	167 168	eqtrdi	$$⊢s=t\cup \left\{z\right\}\to \bigcap s=\bigcap t\cap z$$
170	169	ineq2d	$$⊢s=t\cup \left\{z\right\}\to x\cap \bigcap s=x\cap \left(\bigcap t\cap z\right)$$
171	170	fveq2d	$$⊢s=t\cup \left\{z\right\}\to \left|x\cap \bigcap s\right|=\left|x\cap \left(\bigcap t\cap z\right)\right|$$
172	166 171	oveq12d	$$⊢s=t\cup \left\{z\right\}\to {\left(-1\right)}^{\left|s\right|}\left|x\cap \bigcap s\right|={\left(-1\right)}^{\left|t\cup \left\{z\right\}\right|}\left|x\cap \left(\bigcap t\cap z\right)\right|$$
173		pwfi	$$⊢y\in \mathrm{Fin}\leftrightarrow 𝒫y\in \mathrm{Fin}$$
174	143 173	sylib	$$⊢\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\to 𝒫y\in \mathrm{Fin}$$
175		eqid	$$⊢\left(u\in 𝒫y⟼u\cup \left\{z\right\}\right)=\left(u\in 𝒫y⟼u\cup \left\{z\right\}\right)$$
176		elpwi	$$⊢u\in 𝒫y\to u\subseteq y$$
177	176	adantl	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge u\in 𝒫y\right)\to u\subseteq y$$
178		unss1	$$⊢u\subseteq y\to u\cup \left\{z\right\}\subseteq y\cup \left\{z\right\}$$
179	177 178	syl	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge u\in 𝒫y\right)\to u\cup \left\{z\right\}\subseteq y\cup \left\{z\right\}$$
180		vex	$$⊢u\in \mathrm{V}$$
181		snex	$$⊢\left\{z\right\}\in \mathrm{V}$$
182	180 181	unex	$$⊢u\cup \left\{z\right\}\in \mathrm{V}$$
183	182	elpw	$$⊢u\cup \left\{z\right\}\in 𝒫\left(y\cup \left\{z\right\}\right)\leftrightarrow u\cup \left\{z\right\}\subseteq y\cup \left\{z\right\}$$
184	179 183	sylibr	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge u\in 𝒫y\right)\to u\cup \left\{z\right\}\in 𝒫\left(y\cup \left\{z\right\}\right)$$
185		simpllr	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge u\in 𝒫y\right)\to \neg z\in y$$
186		elpwi	$$⊢u\cup \left\{z\right\}\in 𝒫y\to u\cup \left\{z\right\}\subseteq y$$
187		ssun2	$$⊢\left\{z\right\}\subseteq u\cup \left\{z\right\}$$
188	27	snss	$$⊢z\in \left(u\cup \left\{z\right\}\right)\leftrightarrow \left\{z\right\}\subseteq u\cup \left\{z\right\}$$
189	187 188	mpbir	$$⊢z\in \left(u\cup \left\{z\right\}\right)$$
190	189	a1i	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge u\in 𝒫y\right)\to z\in \left(u\cup \left\{z\right\}\right)$$
191		ssel	$$⊢u\cup \left\{z\right\}\subseteq y\to \left(z\in \left(u\cup \left\{z\right\}\right)\to z\in y\right)$$
192	186 190 191	syl2imc	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge u\in 𝒫y\right)\to \left(u\cup \left\{z\right\}\in 𝒫y\to z\in y\right)$$
193	185 192	mtod	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge u\in 𝒫y\right)\to \neg u\cup \left\{z\right\}\in 𝒫y$$
194	184 193	eldifd	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge u\in 𝒫y\right)\to u\cup \left\{z\right\}\in \left(𝒫\left(y\cup \left\{z\right\}\right)\setminus 𝒫y\right)$$
195		eldifi	$$⊢s\in \left(𝒫\left(y\cup \left\{z\right\}\right)\setminus 𝒫y\right)\to s\in 𝒫\left(y\cup \left\{z\right\}\right)$$
196	195	adantl	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge s\in \left(𝒫\left(y\cup \left\{z\right\}\right)\setminus 𝒫y\right)\right)\to s\in 𝒫\left(y\cup \left\{z\right\}\right)$$
197	196	elpwid	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge s\in \left(𝒫\left(y\cup \left\{z\right\}\right)\setminus 𝒫y\right)\right)\to s\subseteq y\cup \left\{z\right\}$$
198		uncom	$$⊢y\cup \left\{z\right\}=\left\{z\right\}\cup y$$
199	197 198	sseqtrdi	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge s\in \left(𝒫\left(y\cup \left\{z\right\}\right)\setminus 𝒫y\right)\right)\to s\subseteq \left\{z\right\}\cup y$$
200		ssundif	$$⊢s\subseteq \left\{z\right\}\cup y\leftrightarrow s\setminus \left\{z\right\}\subseteq y$$
201	199 200	sylib	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge s\in \left(𝒫\left(y\cup \left\{z\right\}\right)\setminus 𝒫y\right)\right)\to s\setminus \left\{z\right\}\subseteq y$$
202		vex	$$⊢y\in \mathrm{V}$$
203	202	elpw2	$$⊢s\setminus \left\{z\right\}\in 𝒫y\leftrightarrow s\setminus \left\{z\right\}\subseteq y$$
204	201 203	sylibr	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge s\in \left(𝒫\left(y\cup \left\{z\right\}\right)\setminus 𝒫y\right)\right)\to s\setminus \left\{z\right\}\in 𝒫y$$
205		elpwunsn	$$⊢s\in \left(𝒫\left(y\cup \left\{z\right\}\right)\setminus 𝒫y\right)\to z\in s$$
206	205	ad2antll	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge \left(u\in 𝒫y\wedge s\in \left(𝒫\left(y\cup \left\{z\right\}\right)\setminus 𝒫y\right)\right)\right)\to z\in s$$
207	206	snssd	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge \left(u\in 𝒫y\wedge s\in \left(𝒫\left(y\cup \left\{z\right\}\right)\setminus 𝒫y\right)\right)\right)\to \left\{z\right\}\subseteq s$$
208		ssequn2	$$⊢\left\{z\right\}\subseteq s\leftrightarrow s\cup \left\{z\right\}=s$$
209	207 208	sylib	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge \left(u\in 𝒫y\wedge s\in \left(𝒫\left(y\cup \left\{z\right\}\right)\setminus 𝒫y\right)\right)\right)\to s\cup \left\{z\right\}=s$$
210	209	eqcomd	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge \left(u\in 𝒫y\wedge s\in \left(𝒫\left(y\cup \left\{z\right\}\right)\setminus 𝒫y\right)\right)\right)\to s=s\cup \left\{z\right\}$$
211		uneq1	$$⊢u=s\setminus \left\{z\right\}\to u\cup \left\{z\right\}=\left(s\setminus \left\{z\right\}\right)\cup \left\{z\right\}$$
212		undif1	$$⊢\left(s\setminus \left\{z\right\}\right)\cup \left\{z\right\}=s\cup \left\{z\right\}$$
213	211 212	eqtrdi	$$⊢u=s\setminus \left\{z\right\}\to u\cup \left\{z\right\}=s\cup \left\{z\right\}$$
214	213	eqeq2d	$$⊢u=s\setminus \left\{z\right\}\to \left(s=u\cup \left\{z\right\}\leftrightarrow s=s\cup \left\{z\right\}\right)$$
215	210 214	syl5ibrcom	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge \left(u\in 𝒫y\wedge s\in \left(𝒫\left(y\cup \left\{z\right\}\right)\setminus 𝒫y\right)\right)\right)\to \left(u=s\setminus \left\{z\right\}\to s=u\cup \left\{z\right\}\right)$$
216	176	ad2antrl	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge \left(u\in 𝒫y\wedge s\in \left(𝒫\left(y\cup \left\{z\right\}\right)\setminus 𝒫y\right)\right)\right)\to u\subseteq y$$
217		simpllr	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge \left(u\in 𝒫y\wedge s\in \left(𝒫\left(y\cup \left\{z\right\}\right)\setminus 𝒫y\right)\right)\right)\to \neg z\in y$$
218	216 217	ssneldd	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge \left(u\in 𝒫y\wedge s\in \left(𝒫\left(y\cup \left\{z\right\}\right)\setminus 𝒫y\right)\right)\right)\to \neg z\in u$$
219		difsnb	$$⊢\neg z\in u\leftrightarrow u\setminus \left\{z\right\}=u$$
220	218 219	sylib	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge \left(u\in 𝒫y\wedge s\in \left(𝒫\left(y\cup \left\{z\right\}\right)\setminus 𝒫y\right)\right)\right)\to u\setminus \left\{z\right\}=u$$
221	220	eqcomd	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge \left(u\in 𝒫y\wedge s\in \left(𝒫\left(y\cup \left\{z\right\}\right)\setminus 𝒫y\right)\right)\right)\to u=u\setminus \left\{z\right\}$$
222		difeq1	$$⊢s=u\cup \left\{z\right\}\to s\setminus \left\{z\right\}=\left(u\cup \left\{z\right\}\right)\setminus \left\{z\right\}$$
223		difun2	$$⊢\left(u\cup \left\{z\right\}\right)\setminus \left\{z\right\}=u\setminus \left\{z\right\}$$
224	222 223	eqtrdi	$$⊢s=u\cup \left\{z\right\}\to s\setminus \left\{z\right\}=u\setminus \left\{z\right\}$$
225	224	eqeq2d	$$⊢s=u\cup \left\{z\right\}\to \left(u=s\setminus \left\{z\right\}\leftrightarrow u=u\setminus \left\{z\right\}\right)$$
226	221 225	syl5ibrcom	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge \left(u\in 𝒫y\wedge s\in \left(𝒫\left(y\cup \left\{z\right\}\right)\setminus 𝒫y\right)\right)\right)\to \left(s=u\cup \left\{z\right\}\to u=s\setminus \left\{z\right\}\right)$$
227	215 226	impbid	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge \left(u\in 𝒫y\wedge s\in \left(𝒫\left(y\cup \left\{z\right\}\right)\setminus 𝒫y\right)\right)\right)\to \left(u=s\setminus \left\{z\right\}\leftrightarrow s=u\cup \left\{z\right\}\right)$$
228	175 194 204 227	f1o2d	$$⊢\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\to \left(u\in 𝒫y⟼u\cup \left\{z\right\}\right):𝒫y\underset{1-1\; onto}{⟶}𝒫\left(y\cup \left\{z\right\}\right)\setminus 𝒫y$$
229		uneq1	$$⊢u=t\to u\cup \left\{z\right\}=t\cup \left\{z\right\}$$
230		vex	$$⊢t\in \mathrm{V}$$
231	230 181	unex	$$⊢t\cup \left\{z\right\}\in \mathrm{V}$$
232	229 175 231	fvmpt	$$⊢t\in 𝒫y\to \left(u\in 𝒫y⟼u\cup \left\{z\right\}\right)\left(t\right)=t\cup \left\{z\right\}$$
233	232	adantl	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge t\in 𝒫y\right)\to \left(u\in 𝒫y⟼u\cup \left\{z\right\}\right)\left(t\right)=t\cup \left\{z\right\}$$
234	195 163	sylan2	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge s\in \left(𝒫\left(y\cup \left\{z\right\}\right)\setminus 𝒫y\right)\right)\to {\left(-1\right)}^{\left|s\right|}\left|x\cap \bigcap s\right|\in ℂ$$
235	172 174 228 233 234	fsumf1o	$$⊢\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\to \sum _{s\in 𝒫\left(y\cup \left\{z\right\}\right)\setminus 𝒫y}{\left(-1\right)}^{\left|s\right|}\left|x\cap \bigcap s\right|=\sum _{t\in 𝒫y}{\left(-1\right)}^{\left|t\cup \left\{z\right\}\right|}\left|x\cap \left(\bigcap t\cap z\right)\right|$$
236		uneq1	$$⊢t=s\to t\cup \left\{z\right\}=s\cup \left\{z\right\}$$
237	236	fveq2d	$$⊢t=s\to \left|t\cup \left\{z\right\}\right|=\left|s\cup \left\{z\right\}\right|$$
238	237	oveq2d	$$⊢t=s\to {\left(-1\right)}^{\left|t\cup \left\{z\right\}\right|}={\left(-1\right)}^{\left|s\cup \left\{z\right\}\right|}$$
239		inteq	$$⊢t=s\to \bigcap t=\bigcap s$$
240	239	ineq1d	$$⊢t=s\to \bigcap t\cap z=\bigcap s\cap z$$
241	240	ineq2d	$$⊢t=s\to x\cap \left(\bigcap t\cap z\right)=x\cap \left(\bigcap s\cap z\right)$$
242	241	fveq2d	$$⊢t=s\to \left|x\cap \left(\bigcap t\cap z\right)\right|=\left|x\cap \left(\bigcap s\cap z\right)\right|$$
243	238 242	oveq12d	$$⊢t=s\to {\left(-1\right)}^{\left|t\cup \left\{z\right\}\right|}\left|x\cap \left(\bigcap t\cap z\right)\right|={\left(-1\right)}^{\left|s\cup \left\{z\right\}\right|}\left|x\cap \left(\bigcap s\cap z\right)\right|$$
244	243	cbvsumv	$$⊢\sum _{t\in 𝒫y}{\left(-1\right)}^{\left|t\cup \left\{z\right\}\right|}\left|x\cap \left(\bigcap t\cap z\right)\right|=\sum _{s\in 𝒫y}{\left(-1\right)}^{\left|s\cup \left\{z\right\}\right|}\left|x\cap \left(\bigcap s\cap z\right)\right|$$
245	55	a1i	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge s\in 𝒫y\right)\to -1\in ℂ$$
246		elpwi	$$⊢s\in 𝒫y\to s\subseteq y$$
247		ssfi	$$⊢\left(y\in \mathrm{Fin}\wedge s\subseteq y\right)\to s\in \mathrm{Fin}$$
248	143 246 247	syl2an	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge s\in 𝒫y\right)\to s\in \mathrm{Fin}$$
249	248 153	syl	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge s\in 𝒫y\right)\to \left|s\right|\in {\mathbb{N}}_0$$
250	245 249	expp1d	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge s\in 𝒫y\right)\to {\left(-1\right)}^{\left|s\right|+1}={\left(-1\right)}^{\left|s\right|}-1$$
251	246	adantl	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge s\in 𝒫y\right)\to s\subseteq y$$
252		simpllr	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge s\in 𝒫y\right)\to \neg z\in y$$
253	251 252	ssneldd	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge s\in 𝒫y\right)\to \neg z\in s$$
254		hashunsng	$$⊢z\in \mathrm{V}\to \left(\left(s\in \mathrm{Fin}\wedge \neg z\in s\right)\to \left|s\cup \left\{z\right\}\right|=\left|s\right|+1\right)$$
255	254	elv	$$⊢\left(s\in \mathrm{Fin}\wedge \neg z\in s\right)\to \left|s\cup \left\{z\right\}\right|=\left|s\right|+1$$
256	248 253 255	syl2anc	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge s\in 𝒫y\right)\to \left|s\cup \left\{z\right\}\right|=\left|s\right|+1$$
257	256	oveq2d	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge s\in 𝒫y\right)\to {\left(-1\right)}^{\left|s\cup \left\{z\right\}\right|}={\left(-1\right)}^{\left|s\right|+1}$$
258	138	sseli	$$⊢s\in 𝒫y\to s\in 𝒫\left(y\cup \left\{z\right\}\right)$$
259	258 155	sylan2	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge s\in 𝒫y\right)\to {\left(-1\right)}^{\left|s\right|}\in ℂ$$
260	245 259	mulcomd	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge s\in 𝒫y\right)\to -1{\left(-1\right)}^{\left|s\right|}={\left(-1\right)}^{\left|s\right|}-1$$
261	250 257 260	3eqtr4d	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge s\in 𝒫y\right)\to {\left(-1\right)}^{\left|s\cup \left\{z\right\}\right|}=-1{\left(-1\right)}^{\left|s\right|}$$
262	259	mulm1d	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge s\in 𝒫y\right)\to -1{\left(-1\right)}^{\left|s\right|}=-{\left(-1\right)}^{\left|s\right|}$$
263	261 262	eqtrd	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge s\in 𝒫y\right)\to {\left(-1\right)}^{\left|s\cup \left\{z\right\}\right|}=-{\left(-1\right)}^{\left|s\right|}$$
264	263	oveq1d	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge s\in 𝒫y\right)\to {\left(-1\right)}^{\left|s\cup \left\{z\right\}\right|}\left|x\cap \left(\bigcap s\cap z\right)\right|=\left(-{\left(-1\right)}^{\left|s\right|}\right)\left|x\cap \left(\bigcap s\cap z\right)\right|$$
265		inss1	$$⊢x\cap \left(\bigcap s\cap z\right)\subseteq x$$
266		ssfi	$$⊢\left(x\in \mathrm{Fin}\wedge x\cap \left(\bigcap s\cap z\right)\subseteq x\right)\to x\cap \left(\bigcap s\cap z\right)\in \mathrm{Fin}$$
267	156 265 266	sylancl	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge s\in 𝒫\left(y\cup \left\{z\right\}\right)\right)\to x\cap \left(\bigcap s\cap z\right)\in \mathrm{Fin}$$
268		hashcl	$$⊢x\cap \left(\bigcap s\cap z\right)\in \mathrm{Fin}\to \left|x\cap \left(\bigcap s\cap z\right)\right|\in {\mathbb{N}}_0$$
269	267 268	syl	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge s\in 𝒫\left(y\cup \left\{z\right\}\right)\right)\to \left|x\cap \left(\bigcap s\cap z\right)\right|\in {\mathbb{N}}_0$$
270	269	nn0cnd	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge s\in 𝒫\left(y\cup \left\{z\right\}\right)\right)\to \left|x\cap \left(\bigcap s\cap z\right)\right|\in ℂ$$
271	258 270	sylan2	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge s\in 𝒫y\right)\to \left|x\cap \left(\bigcap s\cap z\right)\right|\in ℂ$$
272	259 271	mulneg1d	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge s\in 𝒫y\right)\to \left(-{\left(-1\right)}^{\left|s\right|}\right)\left|x\cap \left(\bigcap s\cap z\right)\right|=-{\left(-1\right)}^{\left|s\right|}\left|x\cap \left(\bigcap s\cap z\right)\right|$$
273	264 272	eqtrd	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge s\in 𝒫y\right)\to {\left(-1\right)}^{\left|s\cup \left\{z\right\}\right|}\left|x\cap \left(\bigcap s\cap z\right)\right|=-{\left(-1\right)}^{\left|s\right|}\left|x\cap \left(\bigcap s\cap z\right)\right|$$
274	273	sumeq2dv	$$⊢\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\to \sum _{s\in 𝒫y}{\left(-1\right)}^{\left|s\cup \left\{z\right\}\right|}\left|x\cap \left(\bigcap s\cap z\right)\right|=\sum _{s\in 𝒫y}\left(-{\left(-1\right)}^{\left|s\right|}\left|x\cap \left(\bigcap s\cap z\right)\right|\right)$$
275	244 274	syl5eq	$$⊢\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\to \sum _{t\in 𝒫y}{\left(-1\right)}^{\left|t\cup \left\{z\right\}\right|}\left|x\cap \left(\bigcap t\cap z\right)\right|=\sum _{s\in 𝒫y}\left(-{\left(-1\right)}^{\left|s\right|}\left|x\cap \left(\bigcap s\cap z\right)\right|\right)$$
276	155 270	mulcld	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge s\in 𝒫\left(y\cup \left\{z\right\}\right)\right)\to {\left(-1\right)}^{\left|s\right|}\left|x\cap \left(\bigcap s\cap z\right)\right|\in ℂ$$
277	258 276	sylan2	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge s\in 𝒫y\right)\to {\left(-1\right)}^{\left|s\right|}\left|x\cap \left(\bigcap s\cap z\right)\right|\in ℂ$$
278	174 277	fsumneg	$$⊢\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\to \sum _{s\in 𝒫y}\left(-{\left(-1\right)}^{\left|s\right|}\left|x\cap \left(\bigcap s\cap z\right)\right|\right)=-\sum _{s\in 𝒫y}{\left(-1\right)}^{\left|s\right|}\left|x\cap \left(\bigcap s\cap z\right)\right|$$
279	235 275 278	3eqtrd	$$⊢\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\to \sum _{s\in 𝒫\left(y\cup \left\{z\right\}\right)\setminus 𝒫y}{\left(-1\right)}^{\left|s\right|}\left|x\cap \bigcap s\right|=-\sum _{s\in 𝒫y}{\left(-1\right)}^{\left|s\right|}\left|x\cap \left(\bigcap s\cap z\right)\right|$$
280	279	oveq2d	$$⊢\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\to \sum _{s\in 𝒫y}{\left(-1\right)}^{\left|s\right|}\left|x\cap \bigcap s\right|+\sum _{s\in 𝒫\left(y\cup \left\{z\right\}\right)\setminus 𝒫y}{\left(-1\right)}^{\left|s\right|}\left|x\cap \bigcap s\right|=\sum _{s\in 𝒫y}{\left(-1\right)}^{\left|s\right|}\left|x\cap \bigcap s\right|+\left(-\sum _{s\in 𝒫y}{\left(-1\right)}^{\left|s\right|}\left|x\cap \left(\bigcap s\cap z\right)\right|\right)$$
281	138	a1i	$$⊢\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\to 𝒫y\subseteq 𝒫\left(y\cup \left\{z\right\}\right)$$
282	281	sselda	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge s\in 𝒫y\right)\to s\in 𝒫\left(y\cup \left\{z\right\}\right)$$
283	282 163	syldan	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge s\in 𝒫y\right)\to {\left(-1\right)}^{\left|s\right|}\left|x\cap \bigcap s\right|\in ℂ$$
284	174 283	fsumcl	$$⊢\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\to \sum _{s\in 𝒫y}{\left(-1\right)}^{\left|s\right|}\left|x\cap \bigcap s\right|\in ℂ$$
285	282 276	syldan	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge s\in 𝒫y\right)\to {\left(-1\right)}^{\left|s\right|}\left|x\cap \left(\bigcap s\cap z\right)\right|\in ℂ$$
286	174 285	fsumcl	$$⊢\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\to \sum _{s\in 𝒫y}{\left(-1\right)}^{\left|s\right|}\left|x\cap \left(\bigcap s\cap z\right)\right|\in ℂ$$
287	284 286	negsubd	$$⊢\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\to \sum _{s\in 𝒫y}{\left(-1\right)}^{\left|s\right|}\left|x\cap \bigcap s\right|+\left(-\sum _{s\in 𝒫y}{\left(-1\right)}^{\left|s\right|}\left|x\cap \left(\bigcap s\cap z\right)\right|\right)=\sum _{s\in 𝒫y}{\left(-1\right)}^{\left|s\right|}\left|x\cap \bigcap s\right|-\sum _{s\in 𝒫y}{\left(-1\right)}^{\left|s\right|}\left|x\cap \left(\bigcap s\cap z\right)\right|$$
288	164 280 287	3eqtrd	$$⊢\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\to \sum _{s\in 𝒫\left(y\cup \left\{z\right\}\right)}{\left(-1\right)}^{\left|s\right|}\left|x\cap \bigcap s\right|=\sum _{s\in 𝒫y}{\left(-1\right)}^{\left|s\right|}\left|x\cap \bigcap s\right|-\sum _{s\in 𝒫y}{\left(-1\right)}^{\left|s\right|}\left|x\cap \left(\bigcap s\cap z\right)\right|$$
289	288	adantr	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge \forall b\in \mathrm{Fin}\left|b\right|-\left|b\cap \bigcup y\right|=\sum _{s\in 𝒫y}{\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|\right)\to \sum _{s\in 𝒫\left(y\cup \left\{z\right\}\right)}{\left(-1\right)}^{\left|s\right|}\left|x\cap \bigcap s\right|=\sum _{s\in 𝒫y}{\left(-1\right)}^{\left|s\right|}\left|x\cap \bigcap s\right|-\sum _{s\in 𝒫y}{\left(-1\right)}^{\left|s\right|}\left|x\cap \left(\bigcap s\cap z\right)\right|$$
290	102 134 289	3eqtr4d	$$⊢\left(\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\wedge \forall b\in \mathrm{Fin}\left|b\right|-\left|b\cap \bigcup y\right|=\sum _{s\in 𝒫y}{\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|\right)\to \left|x\right|-\left|x\cap \left(\bigcup y\cup z\right)\right|=\sum _{s\in 𝒫\left(y\cup \left\{z\right\}\right)}{\left(-1\right)}^{\left|s\right|}\left|x\cap \bigcap s\right|$$
291	290	ex	$$⊢\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\to \left(\forall b\in \mathrm{Fin}\left|b\right|-\left|b\cap \bigcup y\right|=\sum _{s\in 𝒫y}{\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|\to \left|x\right|-\left|x\cap \left(\bigcup y\cup z\right)\right|=\sum _{s\in 𝒫\left(y\cup \left\{z\right\}\right)}{\left(-1\right)}^{\left|s\right|}\left|x\cap \bigcap s\right|\right)$$
292	291	ralrimdva	$$⊢\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\to \left(\forall b\in \mathrm{Fin}\left|b\right|-\left|b\cap \bigcup y\right|=\sum _{s\in 𝒫y}{\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|\to \forall x\in \mathrm{Fin}\left|x\right|-\left|x\cap \left(\bigcup y\cup z\right)\right|=\sum _{s\in 𝒫\left(y\cup \left\{z\right\}\right)}{\left(-1\right)}^{\left|s\right|}\left|x\cap \bigcap s\right|\right)$$
293		ineq1	$$⊢b=x\to b\cap \left(\bigcup y\cup z\right)=x\cap \left(\bigcup y\cup z\right)$$
294	293	fveq2d	$$⊢b=x\to \left|b\cap \left(\bigcup y\cup z\right)\right|=\left|x\cap \left(\bigcup y\cup z\right)\right|$$
295	67 294	oveq12d	$$⊢b=x\to \left|b\right|-\left|b\cap \left(\bigcup y\cup z\right)\right|=\left|x\right|-\left|x\cap \left(\bigcup y\cup z\right)\right|$$
296		ineq1	$$⊢b=x\to b\cap \bigcap s=x\cap \bigcap s$$
297	296	fveq2d	$$⊢b=x\to \left|b\cap \bigcap s\right|=\left|x\cap \bigcap s\right|$$
298	297	oveq2d	$$⊢b=x\to {\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|={\left(-1\right)}^{\left|s\right|}\left|x\cap \bigcap s\right|$$
299	298	sumeq2sdv	$$⊢b=x\to \sum _{s\in 𝒫\left(y\cup \left\{z\right\}\right)}{\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|=\sum _{s\in 𝒫\left(y\cup \left\{z\right\}\right)}{\left(-1\right)}^{\left|s\right|}\left|x\cap \bigcap s\right|$$
300	295 299	eqeq12d	$$⊢b=x\to \left(\left|b\right|-\left|b\cap \left(\bigcup y\cup z\right)\right|=\sum _{s\in 𝒫\left(y\cup \left\{z\right\}\right)}{\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|\leftrightarrow \left|x\right|-\left|x\cap \left(\bigcup y\cup z\right)\right|=\sum _{s\in 𝒫\left(y\cup \left\{z\right\}\right)}{\left(-1\right)}^{\left|s\right|}\left|x\cap \bigcap s\right|\right)$$
301	300	cbvralvw	$$⊢\forall b\in \mathrm{Fin}\left|b\right|-\left|b\cap \left(\bigcup y\cup z\right)\right|=\sum _{s\in 𝒫\left(y\cup \left\{z\right\}\right)}{\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|\leftrightarrow \forall x\in \mathrm{Fin}\left|x\right|-\left|x\cap \left(\bigcup y\cup z\right)\right|=\sum _{s\in 𝒫\left(y\cup \left\{z\right\}\right)}{\left(-1\right)}^{\left|s\right|}\left|x\cap \bigcap s\right|$$
302	292 301	syl6ibr	$$⊢\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\to \left(\forall b\in \mathrm{Fin}\left|b\right|-\left|b\cap \bigcup y\right|=\sum _{s\in 𝒫y}{\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|\to \forall b\in \mathrm{Fin}\left|b\right|-\left|b\cap \left(\bigcup y\cup z\right)\right|=\sum _{s\in 𝒫\left(y\cup \left\{z\right\}\right)}{\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|\right)$$
303	16 24 38 46 66 302	findcard2s	$$⊢A\in \mathrm{Fin}\to \forall b\in \mathrm{Fin}\left|b\right|-\left|b\cap \bigcup A\right|=\sum _{s\in 𝒫A}{\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|$$
304		fveq2	$$⊢b=B\to \left|b\right|=\left|B\right|$$
305		ineq1	$$⊢b=B\to b\cap \bigcup A=B\cap \bigcup A$$
306	305	fveq2d	$$⊢b=B\to \left|b\cap \bigcup A\right|=\left|B\cap \bigcup A\right|$$
307	304 306	oveq12d	$$⊢b=B\to \left|b\right|-\left|b\cap \bigcup A\right|=\left|B\right|-\left|B\cap \bigcup A\right|$$
308		simpl	$$⊢\left(b=B\wedge s\in 𝒫A\right)\to b=B$$
309	308	ineq1d	$$⊢\left(b=B\wedge s\in 𝒫A\right)\to b\cap \bigcap s=B\cap \bigcap s$$
310	309	fveq2d	$$⊢\left(b=B\wedge s\in 𝒫A\right)\to \left|b\cap \bigcap s\right|=\left|B\cap \bigcap s\right|$$
311	310	oveq2d	$$⊢\left(b=B\wedge s\in 𝒫A\right)\to {\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|={\left(-1\right)}^{\left|s\right|}\left|B\cap \bigcap s\right|$$
312	311	sumeq2dv	$$⊢b=B\to \sum _{s\in 𝒫A}{\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|=\sum _{s\in 𝒫A}{\left(-1\right)}^{\left|s\right|}\left|B\cap \bigcap s\right|$$
313	307 312	eqeq12d	$$⊢b=B\to \left(\left|b\right|-\left|b\cap \bigcup A\right|=\sum _{s\in 𝒫A}{\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|\leftrightarrow \left|B\right|-\left|B\cap \bigcup A\right|=\sum _{s\in 𝒫A}{\left(-1\right)}^{\left|s\right|}\left|B\cap \bigcap s\right|\right)$$
314	313	rspccva	$$⊢\left(\forall b\in \mathrm{Fin}\left|b\right|-\left|b\cap \bigcup A\right|=\sum _{s\in 𝒫A}{\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|\wedge B\in \mathrm{Fin}\right)\to \left|B\right|-\left|B\cap \bigcup A\right|=\sum _{s\in 𝒫A}{\left(-1\right)}^{\left|s\right|}\left|B\cap \bigcap s\right|$$
315	303 314	sylan	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left|B\right|-\left|B\cap \bigcup A\right|=\sum _{s\in 𝒫A}{\left(-1\right)}^{\left|s\right|}\left|B\cap \bigcap s\right|$$