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		unisnv	$$⊢\bigcup \left\{z\right\}=z$$
28	27	uneq2i	$$⊢\bigcup y\cup \bigcup \left\{z\right\}=\bigcup y\cup z$$
29	26 28	eqtri	$$⊢\bigcup \left(y\cup \left\{z\right\}\right)=\bigcup y\cup z$$
30	25 29	eqtrdi	$$⊢x=y\cup \left\{z\right\}\to \bigcup x=\bigcup y\cup z$$
31	30	ineq2d	$$⊢x=y\cup \left\{z\right\}\to b\cap \bigcup x=b\cap \left(\bigcup y\cup z\right)$$
32	31	fveq2d	$$⊢x=y\cup \left\{z\right\}\to \left|b\cap \bigcup x\right|=\left|b\cap \left(\bigcup y\cup z\right)\right|$$
33	32	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|$$
34		pweq	$$⊢x=y\cup \left\{z\right\}\to 𝒫x=𝒫\left(y\cup \left\{z\right\}\right)$$
35	34	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|$$
36	33 35	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)$$
37	36	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)$$
38		unieq	$$⊢x=A\to \bigcup x=\bigcup A$$
39	38	ineq2d	$$⊢x=A\to b\cap \bigcup x=b\cap \bigcup A$$
40	39	fveq2d	$$⊢x=A\to \left|b\cap \bigcup x\right|=\left|b\cap \bigcup A\right|$$
41	40	oveq2d	$$⊢x=A\to \left|b\right|-\left|b\cap \bigcup x\right|=\left|b\right|-\left|b\cap \bigcup A\right|$$
42		pweq	$$⊢x=A\to 𝒫x=𝒫A$$
43	42	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|$$
44	41 43	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)$$
45	44	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)$$
46		hashcl	$$⊢b\in \mathrm{Fin}\to \left|b\right|\in {\mathbb{N}}_0$$
47	46	nn0cnd	$$⊢b\in \mathrm{Fin}\to \left|b\right|\in ℂ$$
48	47	mullidd	$$⊢b\in \mathrm{Fin}\to 1\left|b\right|=\left|b\right|$$
49		0ex	$$⊢\varnothing \in \mathrm{V}$$
50	48 47	eqeltrd	$$⊢b\in \mathrm{Fin}\to 1\left|b\right|\in ℂ$$
51		fveq2	$$⊢s=\varnothing \to \left|s\right|=\left|\varnothing \right|$$
52	51 8	eqtrdi	$$⊢s=\varnothing \to \left|s\right|=0$$
53	52	oveq2d	$$⊢s=\varnothing \to {\left(-1\right)}^{\left|s\right|}={\left(-1\right)}^0$$
54		neg1cn	$$⊢-1\in ℂ$$
55		exp0	$$⊢-1\in ℂ\to {\left(-1\right)}^0=1$$
56	54 55	ax-mp	$$⊢{\left(-1\right)}^0=1$$
57	53 56	eqtrdi	$$⊢s=\varnothing \to {\left(-1\right)}^{\left|s\right|}=1$$
58		rint0	$$⊢s=\varnothing \to b\cap \bigcap s=b$$
59	58	fveq2d	$$⊢s=\varnothing \to \left|b\cap \bigcap s\right|=\left|b\right|$$
60	57 59	oveq12d	$$⊢s=\varnothing \to {\left(-1\right)}^{\left|s\right|}\left|b\cap \bigcap s\right|=1\left|b\right|$$
61	60	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|$$
62	49 50 61	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|$$
63	47	subid1d	$$⊢b\in \mathrm{Fin}\to \left|b\right|-0=\left|b\right|$$
64	48 62 63	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|$$
65	64	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|$$
66		fveq2	$$⊢b=x\to \left|b\right|=\left|x\right|$$
67		ineq1	$$⊢b=x\to b\cap \bigcup y=x\cap \bigcup y$$
68	67	fveq2d	$$⊢b=x\to \left|b\cap \bigcup y\right|=\left|x\cap \bigcup y\right|$$
69	66 68	oveq12d	$$⊢b=x\to \left|b\right|-\left|b\cap \bigcup y\right|=\left|x\right|-\left|x\cap \bigcup y\right|$$
70		simpl	$$⊢\left(b=x\wedge s\in 𝒫y\right)\to b=x$$
71	70	ineq1d	$$⊢\left(b=x\wedge s\in 𝒫y\right)\to b\cap \bigcap s=x\cap \bigcap s$$
72	71	fveq2d	$$⊢\left(b=x\wedge s\in 𝒫y\right)\to \left|b\cap \bigcap s\right|=\left|x\cap \bigcap s\right|$$
73	72	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|$$
74	73	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|$$
75	69 74	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)$$
76	75	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|$$
77	76	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|$$
78		simpr	$$⊢\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\to x\in \mathrm{Fin}$$
79		inss1	$$⊢x\cap z\subseteq x$$
80		ssfi	$$⊢\left(x\in \mathrm{Fin}\wedge x\cap z\subseteq x\right)\to x\cap z\in \mathrm{Fin}$$
81	78 79 80	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}$$
82		fveq2	$$⊢b=x\cap z\to \left|b\right|=\left|x\cap z\right|$$
83		ineq1	$$⊢b=x\cap z\to b\cap \bigcup y=\left(x\cap z\right)\cap \bigcup y$$
84		in32	$$⊢\left(x\cap z\right)\cap \bigcup y=\left(x\cap \bigcup y\right)\cap z$$
85		inass	$$⊢\left(x\cap \bigcup y\right)\cap z=x\cap \left(\bigcup y\cap z\right)$$
86	84 85	eqtri	$$⊢\left(x\cap z\right)\cap \bigcup y=x\cap \left(\bigcup y\cap z\right)$$
87	83 86	eqtrdi	$$⊢b=x\cap z\to b\cap \bigcup y=x\cap \left(\bigcup y\cap z\right)$$
88	87	fveq2d	$$⊢b=x\cap z\to \left|b\cap \bigcup y\right|=\left|x\cap \left(\bigcup y\cap z\right)\right|$$
89	82 88	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|$$
90		ineq1	$$⊢b=x\cap z\to b\cap \bigcap s=\left(x\cap z\right)\cap \bigcap s$$
91		in32	$$⊢\left(x\cap z\right)\cap \bigcap s=\left(x\cap \bigcap s\right)\cap z$$
92		inass	$$⊢\left(x\cap \bigcap s\right)\cap z=x\cap \left(\bigcap s\cap z\right)$$
93	91 92	eqtri	$$⊢\left(x\cap z\right)\cap \bigcap s=x\cap \left(\bigcap s\cap z\right)$$
94	90 93	eqtrdi	$$⊢b=x\cap z\to b\cap \bigcap s=x\cap \left(\bigcap s\cap z\right)$$
95	94	fveq2d	$$⊢b=x\cap z\to \left|b\cap \bigcap s\right|=\left|x\cap \left(\bigcap s\cap z\right)\right|$$
96	95	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|$$
97	96	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|$$
98	89 97	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)$$
99	98	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|$$
100	81 99	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|$$
101	77 100	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|$$
102		inss1	$$⊢x\cap \bigcup y\subseteq x$$
103		ssfi	$$⊢\left(x\in \mathrm{Fin}\wedge x\cap \bigcup y\subseteq x\right)\to x\cap \bigcup y\in \mathrm{Fin}$$
104	78 102 103	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}$$
105		hashcl	$$⊢x\cap \bigcup y\in \mathrm{Fin}\to \left|x\cap \bigcup y\right|\in {\mathbb{N}}_0$$
106	104 105	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$$
107	106	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 ℂ$$
108		hashcl	$$⊢x\cap z\in \mathrm{Fin}\to \left|x\cap z\right|\in {\mathbb{N}}_0$$
109	81 108	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$$
110	109	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 ℂ$$
111		inss1	$$⊢x\cap \left(\bigcup y\cap z\right)\subseteq x$$
112		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}$$
113	78 111 112	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}$$
114		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$$
115	113 114	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$$
116	115	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 ℂ$$
117		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|$$
118	104 81 117	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|$$
119		indi	$$⊢x\cap \left(\bigcup y\cup z\right)=\left(x\cap \bigcup y\right)\cup \left(x\cap z\right)$$
120	119	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|$$
121		inindi	$$⊢x\cap \left(\bigcup y\cap z\right)=\left(x\cap \bigcup y\right)\cap \left(x\cap z\right)$$
122	121	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|$$
123	122	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|$$
124	118 120 123	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|$$
125	107 110 116 124	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|$$
126	125	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)$$
127		hashcl	$$⊢x\in \mathrm{Fin}\to \left|x\right|\in {\mathbb{N}}_0$$
128	127	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$$
129	128	nn0cnd	$$⊢\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\to \left|x\right|\in ℂ$$
130	110 116	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 ℂ$$
131	129 107 130	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)$$
132	126 131	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)$$
133	132	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)$$
134		disjdif	$$⊢𝒫y\cap \left(𝒫\left(y\cup \left\{z\right\}\right)\setminus 𝒫y\right)=\varnothing$$
135	134	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$$
136		ssun1	$$⊢y\subseteq y\cup \left\{z\right\}$$
137	136	sspwi	$$⊢𝒫y\subseteq 𝒫\left(y\cup \left\{z\right\}\right)$$
138		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)$$
139	137 138	mpbi	$$⊢𝒫y\cup \left(𝒫\left(y\cup \left\{z\right\}\right)\setminus 𝒫y\right)=𝒫\left(y\cup \left\{z\right\}\right)$$
140	139	eqcomi	$$⊢𝒫\left(y\cup \left\{z\right\}\right)=𝒫y\cup \left(𝒫\left(y\cup \left\{z\right\}\right)\setminus 𝒫y\right)$$
141	140	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)$$
142		simpll	$$⊢\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge x\in \mathrm{Fin}\right)\to y\in \mathrm{Fin}$$
143		snfi	$$⊢\left\{z\right\}\in \mathrm{Fin}$$
144		unfi	$$⊢\left(y\in \mathrm{Fin}\wedge \left\{z\right\}\in \mathrm{Fin}\right)\to y\cup \left\{z\right\}\in \mathrm{Fin}$$
145	142 143 144	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}$$
146		pwfi	$$⊢y\cup \left\{z\right\}\in \mathrm{Fin}\leftrightarrow 𝒫\left(y\cup \left\{z\right\}\right)\in \mathrm{Fin}$$
147	145 146	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}$$
148	54	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 ℂ$$
149		elpwi	$$⊢s\in 𝒫\left(y\cup \left\{z\right\}\right)\to s\subseteq y\cup \left\{z\right\}$$
150		ssfi	$$⊢\left(y\cup \left\{z\right\}\in \mathrm{Fin}\wedge s\subseteq y\cup \left\{z\right\}\right)\to s\in \mathrm{Fin}$$
151	145 149 150	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}$$
152		hashcl	$$⊢s\in \mathrm{Fin}\to \left|s\right|\in {\mathbb{N}}_0$$
153	151 152	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$$
154	148 153	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 ℂ$$
155		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}$$
156		inss1	$$⊢x\cap \bigcap s\subseteq x$$
157		ssfi	$$⊢\left(x\in \mathrm{Fin}\wedge x\cap \bigcap s\subseteq x\right)\to x\cap \bigcap s\in \mathrm{Fin}$$
158	155 156 157	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}$$
159		hashcl	$$⊢x\cap \bigcap s\in \mathrm{Fin}\to \left|x\cap \bigcap s\right|\in {\mathbb{N}}_0$$
160	158 159	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$$
161	160	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 ℂ$$
162	154 161	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 ℂ$$
163	135 141 147 162	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|$$
164		fveq2	$$⊢s=t\cup \left\{z\right\}\to \left|s\right|=\left|t\cup \left\{z\right\}\right|$$
165	164	oveq2d	$$⊢s=t\cup \left\{z\right\}\to {\left(-1\right)}^{\left|s\right|}={\left(-1\right)}^{\left|t\cup \left\{z\right\}\right|}$$
166		inteq	$$⊢s=t\cup \left\{z\right\}\to \bigcap s=\bigcap \left(t\cup \left\{z\right\}\right)$$
167		vex	$$⊢z\in \mathrm{V}$$
168	167	intunsn	$$⊢\bigcap \left(t\cup \left\{z\right\}\right)=\bigcap t\cap z$$
169	166 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	165 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	142 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		vsnex	$$⊢\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	167	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 162	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	54	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	142 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 152	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	137	sseli	$$⊢s\in 𝒫y\to s\in 𝒫\left(y\cup \left\{z\right\}\right)$$
259	258 154	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	155 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	eqtrid	$$⊢\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	154 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	137	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 162	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	163 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	101 133 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	66 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 37 45 65 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|$$