Theorem kmlem9

Description: Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. (Contributed by NM, 25-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	kmlem9	$$⊢\forall z\in A\forall w\in A\left(z\ne w\to z\cap w=\varnothing \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		vex	$$⊢z\in \mathrm{V}$$
3		eqeq1	$$⊢u=z\to \left(u=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\leftrightarrow z=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)$$
4	3	rexbidv	$$⊢u=z\to \left(\exists t\in xu=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\leftrightarrow \exists t\in xz=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)$$
5	2 4 1	elab2	$$⊢z\in A\leftrightarrow \exists t\in xz=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)$$
6		vex	$$⊢w\in \mathrm{V}$$
7		eqeq1	$$⊢u=w\to \left(u=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\leftrightarrow w=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)$$
8	7	rexbidv	$$⊢u=w\to \left(\exists t\in xu=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\leftrightarrow \exists t\in xw=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)$$
9	6 8 1	elab2	$$⊢w\in A\leftrightarrow \exists t\in xw=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)$$
10		difeq1	$$⊢t=h\to t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)=h\setminus \bigcup \left(x\setminus \left\{t\right\}\right)$$
11		sneq	$$⊢t=h\to \left\{t\right\}=\left\{h\right\}$$
12	11	difeq2d	$$⊢t=h\to x\setminus \left\{t\right\}=x\setminus \left\{h\right\}$$
13	12	unieqd	$$⊢t=h\to \bigcup \left(x\setminus \left\{t\right\}\right)=\bigcup \left(x\setminus \left\{h\right\}\right)$$
14	13	difeq2d	$$⊢t=h\to h\setminus \bigcup \left(x\setminus \left\{t\right\}\right)=h\setminus \bigcup \left(x\setminus \left\{h\right\}\right)$$
15	10 14	eqtrd	$$⊢t=h\to t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)=h\setminus \bigcup \left(x\setminus \left\{h\right\}\right)$$
16	15	eqeq2d	$$⊢t=h\to \left(w=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\leftrightarrow w=h\setminus \bigcup \left(x\setminus \left\{h\right\}\right)\right)$$
17	16	cbvrexvw	$$⊢\exists t\in xw=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\leftrightarrow \exists h\in xw=h\setminus \bigcup \left(x\setminus \left\{h\right\}\right)$$
18	9 17	bitri	$$⊢w\in A\leftrightarrow \exists h\in xw=h\setminus \bigcup \left(x\setminus \left\{h\right\}\right)$$
19		reeanv	$$⊢\exists t\in x\exists h\in x\left(z=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\wedge w=h\setminus \bigcup \left(x\setminus \left\{h\right\}\right)\right)\leftrightarrow \left(\exists t\in xz=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\wedge \exists h\in xw=h\setminus \bigcup \left(x\setminus \left\{h\right\}\right)\right)$$
20		eqeq12	$$⊢\left(z=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\wedge w=h\setminus \bigcup \left(x\setminus \left\{h\right\}\right)\right)\to \left(z=w\leftrightarrow t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)=h\setminus \bigcup \left(x\setminus \left\{h\right\}\right)\right)$$
21	15 20	syl5ibr	$$⊢\left(z=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\wedge w=h\setminus \bigcup \left(x\setminus \left\{h\right\}\right)\right)\to \left(t=h\to z=w\right)$$
22	21	necon3d	$$⊢\left(z=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\wedge w=h\setminus \bigcup \left(x\setminus \left\{h\right\}\right)\right)\to \left(z\ne w\to t\ne h\right)$$
23		kmlem5	$$⊢\left(h\in x\wedge t\ne h\right)\to \left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)\cap \left(h\setminus \bigcup \left(x\setminus \left\{h\right\}\right)\right)=\varnothing$$
24		ineq12	$$⊢\left(z=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\wedge w=h\setminus \bigcup \left(x\setminus \left\{h\right\}\right)\right)\to z\cap w=\left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)\cap \left(h\setminus \bigcup \left(x\setminus \left\{h\right\}\right)\right)$$
25	24	eqeq1d	$$⊢\left(z=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\wedge w=h\setminus \bigcup \left(x\setminus \left\{h\right\}\right)\right)\to \left(z\cap w=\varnothing \leftrightarrow \left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)\cap \left(h\setminus \bigcup \left(x\setminus \left\{h\right\}\right)\right)=\varnothing \right)$$
26	23 25	syl5ibr	$$⊢\left(z=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\wedge w=h\setminus \bigcup \left(x\setminus \left\{h\right\}\right)\right)\to \left(\left(h\in x\wedge t\ne h\right)\to z\cap w=\varnothing \right)$$
27	26	expd	$$⊢\left(z=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\wedge w=h\setminus \bigcup \left(x\setminus \left\{h\right\}\right)\right)\to \left(h\in x\to \left(t\ne h\to z\cap w=\varnothing \right)\right)$$
28	22 27	syl5d	$$⊢\left(z=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\wedge w=h\setminus \bigcup \left(x\setminus \left\{h\right\}\right)\right)\to \left(h\in x\to \left(z\ne w\to z\cap w=\varnothing \right)\right)$$
29	28	com12	$$⊢h\in x\to \left(\left(z=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\wedge w=h\setminus \bigcup \left(x\setminus \left\{h\right\}\right)\right)\to \left(z\ne w\to z\cap w=\varnothing \right)\right)$$
30	29	adantl	$$⊢\left(t\in x\wedge h\in x\right)\to \left(\left(z=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\wedge w=h\setminus \bigcup \left(x\setminus \left\{h\right\}\right)\right)\to \left(z\ne w\to z\cap w=\varnothing \right)\right)$$
31	30	rexlimivv	$$⊢\exists t\in x\exists h\in x\left(z=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\wedge w=h\setminus \bigcup \left(x\setminus \left\{h\right\}\right)\right)\to \left(z\ne w\to z\cap w=\varnothing \right)$$
32	19 31	sylbir	$$⊢\left(\exists t\in xz=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\wedge \exists h\in xw=h\setminus \bigcup \left(x\setminus \left\{h\right\}\right)\right)\to \left(z\ne w\to z\cap w=\varnothing \right)$$
33	5 18 32	syl2anb	$$⊢\left(z\in A\wedge w\in A\right)\to \left(z\ne w\to z\cap w=\varnothing \right)$$
34	33	rgen2	$$⊢\forall z\in A\forall w\in A\left(z\ne w\to z\cap w=\varnothing \right)$$