Theorem kmlem11

Description: Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. (Contributed by NM, 26-Mar-2004)

	Ref	Expression
Hypothesis	kmlem9.1	$$⊢A=\left\{u|\exists t\in xu=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right\}$$
Assertion	kmlem11	$$⊢z\in x\to z\cap \bigcup A=z\setminus \bigcup \left(x\setminus \left\{z\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		kmlem9.1	$$⊢A=\left\{u|\exists t\in xu=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right\}$$
2	1	unieqi	$$⊢\bigcup A=\bigcup \left\{u|\exists t\in xu=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right\}$$
3		vex	$$⊢t\in \mathrm{V}$$
4	3	difexi	$$⊢t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\in \mathrm{V}$$
5	4	dfiun2	$$⊢\bigcup _{t\in x}\left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)=\bigcup \left\{u|\exists t\in xu=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right\}$$
6	2 5	eqtr4i	$$⊢\bigcup A=\bigcup _{t\in x}\left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)$$
7	6	ineq2i	$$⊢z\cap \bigcup A=z\cap \bigcup _{t\in x}\left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)$$
8		iunin2	$$⊢\bigcup _{t\in x}\left(z\cap \left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)\right)=z\cap \bigcup _{t\in x}\left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)$$
9	7 8	eqtr4i	$$⊢z\cap \bigcup A=\bigcup _{t\in x}\left(z\cap \left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)\right)$$
10		undif2	$$⊢\left\{z\right\}\cup \left(x\setminus \left\{z\right\}\right)=\left\{z\right\}\cup x$$
11		snssi	$$⊢z\in x\to \left\{z\right\}\subseteq x$$
12		ssequn1	$$⊢\left\{z\right\}\subseteq x\leftrightarrow \left\{z\right\}\cup x=x$$
13	11 12	sylib	$$⊢z\in x\to \left\{z\right\}\cup x=x$$
14	10 13	syl5req	$$⊢z\in x\to x=\left\{z\right\}\cup \left(x\setminus \left\{z\right\}\right)$$
15	14	iuneq1d	$$⊢z\in x\to \bigcup _{t\in x}\left(z\cap \left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)\right)=\bigcup _{t\in \left\{z\right\}\cup \left(x\setminus \left\{z\right\}\right)}\left(z\cap \left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)\right)$$
16		iunxun	$$⊢\bigcup _{t\in \left\{z\right\}\cup \left(x\setminus \left\{z\right\}\right)}\left(z\cap \left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)\right)=\bigcup _{t\in \left\{z\right\}}\left(z\cap \left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)\right)\cup \bigcup _{t\in x\setminus \left\{z\right\}}\left(z\cap \left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)\right)$$
17		vex	$$⊢z\in \mathrm{V}$$
18		difeq1	$$⊢t=z\to t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)=z\setminus \bigcup \left(x\setminus \left\{t\right\}\right)$$
19		sneq	$$⊢t=z\to \left\{t\right\}=\left\{z\right\}$$
20	19	difeq2d	$$⊢t=z\to x\setminus \left\{t\right\}=x\setminus \left\{z\right\}$$
21	20	unieqd	$$⊢t=z\to \bigcup \left(x\setminus \left\{t\right\}\right)=\bigcup \left(x\setminus \left\{z\right\}\right)$$
22	21	difeq2d	$$⊢t=z\to z\setminus \bigcup \left(x\setminus \left\{t\right\}\right)=z\setminus \bigcup \left(x\setminus \left\{z\right\}\right)$$
23	18 22	eqtrd	$$⊢t=z\to t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)=z\setminus \bigcup \left(x\setminus \left\{z\right\}\right)$$
24	23	ineq2d	$$⊢t=z\to z\cap \left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)=z\cap \left(z\setminus \bigcup \left(x\setminus \left\{z\right\}\right)\right)$$
25	17 24	iunxsn	$$⊢\bigcup _{t\in \left\{z\right\}}\left(z\cap \left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)\right)=z\cap \left(z\setminus \bigcup \left(x\setminus \left\{z\right\}\right)\right)$$
26	25	uneq1i	$$⊢\bigcup _{t\in \left\{z\right\}}\left(z\cap \left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)\right)\cup \bigcup _{t\in x\setminus \left\{z\right\}}\left(z\cap \left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)\right)=\left(z\cap \left(z\setminus \bigcup \left(x\setminus \left\{z\right\}\right)\right)\right)\cup \bigcup _{t\in x\setminus \left\{z\right\}}\left(z\cap \left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)\right)$$
27	16 26	eqtri	$$⊢\bigcup _{t\in \left\{z\right\}\cup \left(x\setminus \left\{z\right\}\right)}\left(z\cap \left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)\right)=\left(z\cap \left(z\setminus \bigcup \left(x\setminus \left\{z\right\}\right)\right)\right)\cup \bigcup _{t\in x\setminus \left\{z\right\}}\left(z\cap \left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)\right)$$
28		eldifsni	$$⊢t\in \left(x\setminus \left\{z\right\}\right)\to t\ne z$$
29		incom	$$⊢z\cap \left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)=\left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)\cap z$$
30		kmlem4	$$⊢\left(z\in x\wedge t\ne z\right)\to \left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)\cap z=\varnothing$$
31	29 30	syl5eq	$$⊢\left(z\in x\wedge t\ne z\right)\to z\cap \left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)=\varnothing$$
32	31	ex	$$⊢z\in x\to \left(t\ne z\to z\cap \left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)=\varnothing \right)$$
33	28 32	syl5	$$⊢z\in x\to \left(t\in \left(x\setminus \left\{z\right\}\right)\to z\cap \left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)=\varnothing \right)$$
34	33	ralrimiv	$$⊢z\in x\to \forall t\in \left(x\setminus \left\{z\right\}\right)z\cap \left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)=\varnothing$$
35		iuneq2	$$⊢\forall t\in \left(x\setminus \left\{z\right\}\right)z\cap \left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)=\varnothing \to \bigcup _{t\in x\setminus \left\{z\right\}}\left(z\cap \left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)\right)=\bigcup _{t\in x\setminus \left\{z\right\}}\varnothing$$
36	34 35	syl	$$⊢z\in x\to \bigcup _{t\in x\setminus \left\{z\right\}}\left(z\cap \left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)\right)=\bigcup _{t\in x\setminus \left\{z\right\}}\varnothing$$
37		iun0	$$⊢\bigcup _{t\in x\setminus \left\{z\right\}}\varnothing =\varnothing$$
38	36 37	eqtrdi	$$⊢z\in x\to \bigcup _{t\in x\setminus \left\{z\right\}}\left(z\cap \left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)\right)=\varnothing$$
39	38	uneq2d	$$⊢z\in x\to \left(z\cap \left(z\setminus \bigcup \left(x\setminus \left\{z\right\}\right)\right)\right)\cup \bigcup _{t\in x\setminus \left\{z\right\}}\left(z\cap \left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)\right)=\left(z\cap \left(z\setminus \bigcup \left(x\setminus \left\{z\right\}\right)\right)\right)\cup \varnothing$$
40	27 39	syl5eq	$$⊢z\in x\to \bigcup _{t\in \left\{z\right\}\cup \left(x\setminus \left\{z\right\}\right)}\left(z\cap \left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)\right)=\left(z\cap \left(z\setminus \bigcup \left(x\setminus \left\{z\right\}\right)\right)\right)\cup \varnothing$$
41	15 40	eqtrd	$$⊢z\in x\to \bigcup _{t\in x}\left(z\cap \left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)\right)=\left(z\cap \left(z\setminus \bigcup \left(x\setminus \left\{z\right\}\right)\right)\right)\cup \varnothing$$
42		un0	$$⊢\left(z\cap \left(z\setminus \bigcup \left(x\setminus \left\{z\right\}\right)\right)\right)\cup \varnothing =z\cap \left(z\setminus \bigcup \left(x\setminus \left\{z\right\}\right)\right)$$
43		indif	$$⊢z\cap \left(z\setminus \bigcup \left(x\setminus \left\{z\right\}\right)\right)=z\setminus \bigcup \left(x\setminus \left\{z\right\}\right)$$
44	42 43	eqtri	$$⊢\left(z\cap \left(z\setminus \bigcup \left(x\setminus \left\{z\right\}\right)\right)\right)\cup \varnothing =z\setminus \bigcup \left(x\setminus \left\{z\right\}\right)$$
45	41 44	eqtrdi	$$⊢z\in x\to \bigcup _{t\in x}\left(z\cap \left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)\right)=z\setminus \bigcup \left(x\setminus \left\{z\right\}\right)$$
46	9 45	syl5eq	$$⊢z\in x\to z\cap \bigcup A=z\setminus \bigcup \left(x\setminus \left\{z\right\}\right)$$