Theorem kmlem12

Description: Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. (Contributed by NM, 27-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	kmlem12	$$⊢\forall z\in xz\setminus \bigcup \left(x\setminus \left\{z\right\}\right)\ne \varnothing \to \left(\forall z\in A\left(z\ne \varnothing \to \exists !vv\in \left(z\cap y\right)\right)\to \forall z\in x\left(z\ne \varnothing \to \exists !vv\in \left(z\cap \left(y\cap \bigcup A\right)\right)\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		difeq1	$$⊢t=z\to t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)=z\setminus \bigcup \left(x\setminus \left\{t\right\}\right)$$
3		sneq	$$⊢t=z\to \left\{t\right\}=\left\{z\right\}$$
4	3	difeq2d	$$⊢t=z\to x\setminus \left\{t\right\}=x\setminus \left\{z\right\}$$
5	4	unieqd	$$⊢t=z\to \bigcup \left(x\setminus \left\{t\right\}\right)=\bigcup \left(x\setminus \left\{z\right\}\right)$$
6	5	difeq2d	$$⊢t=z\to z\setminus \bigcup \left(x\setminus \left\{t\right\}\right)=z\setminus \bigcup \left(x\setminus \left\{z\right\}\right)$$
7	2 6	eqtrd	$$⊢t=z\to t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)=z\setminus \bigcup \left(x\setminus \left\{z\right\}\right)$$
8	7	neeq1d	$$⊢t=z\to \left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\ne \varnothing \leftrightarrow z\setminus \bigcup \left(x\setminus \left\{z\right\}\right)\ne \varnothing \right)$$
9	8	cbvralvw	$$⊢\forall t\in xt\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\ne \varnothing \leftrightarrow \forall z\in xz\setminus \bigcup \left(x\setminus \left\{z\right\}\right)\ne \varnothing$$
10	7	ineq1d	$$⊢t=z\to \left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)\cap y=\left(z\setminus \bigcup \left(x\setminus \left\{z\right\}\right)\right)\cap y$$
11	10	eleq2d	$$⊢t=z\to \left(v\in \left(\left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)\cap y\right)\leftrightarrow v\in \left(\left(z\setminus \bigcup \left(x\setminus \left\{z\right\}\right)\right)\cap y\right)\right)$$
12	11	eubidv	$$⊢t=z\to \left(\exists !vv\in \left(\left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)\cap y\right)\leftrightarrow \exists !vv\in \left(\left(z\setminus \bigcup \left(x\setminus \left\{z\right\}\right)\right)\cap y\right)\right)$$
13	12	cbvralvw	$$⊢\forall t\in x\exists !vv\in \left(\left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)\cap y\right)\leftrightarrow \forall z\in x\exists !vv\in \left(\left(z\setminus \bigcup \left(x\setminus \left\{z\right\}\right)\right)\cap y\right)$$
14	9 13	imbi12i	$$⊢\left(\forall t\in xt\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\ne \varnothing \to \forall t\in x\exists !vv\in \left(\left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)\cap y\right)\right)\leftrightarrow \left(\forall z\in xz\setminus \bigcup \left(x\setminus \left\{z\right\}\right)\ne \varnothing \to \forall z\in x\exists !vv\in \left(\left(z\setminus \bigcup \left(x\setminus \left\{z\right\}\right)\right)\cap y\right)\right)$$
15		in12	$$⊢z\cap \left(y\cap \bigcup A\right)=y\cap \left(z\cap \bigcup A\right)$$
16		incom	$$⊢y\cap \left(z\cap \bigcup A\right)=\left(z\cap \bigcup A\right)\cap y$$
17	15 16	eqtri	$$⊢z\cap \left(y\cap \bigcup A\right)=\left(z\cap \bigcup A\right)\cap y$$
18	1	kmlem11	$$⊢z\in x\to z\cap \bigcup A=z\setminus \bigcup \left(x\setminus \left\{z\right\}\right)$$
19	18	ineq1d	$$⊢z\in x\to \left(z\cap \bigcup A\right)\cap y=\left(z\setminus \bigcup \left(x\setminus \left\{z\right\}\right)\right)\cap y$$
20	17 19	eqtr2id	$$⊢z\in x\to \left(z\setminus \bigcup \left(x\setminus \left\{z\right\}\right)\right)\cap y=z\cap \left(y\cap \bigcup A\right)$$
21	20	eleq2d	$$⊢z\in x\to \left(v\in \left(\left(z\setminus \bigcup \left(x\setminus \left\{z\right\}\right)\right)\cap y\right)\leftrightarrow v\in \left(z\cap \left(y\cap \bigcup A\right)\right)\right)$$
22	21	eubidv	$$⊢z\in x\to \left(\exists !vv\in \left(\left(z\setminus \bigcup \left(x\setminus \left\{z\right\}\right)\right)\cap y\right)\leftrightarrow \exists !vv\in \left(z\cap \left(y\cap \bigcup A\right)\right)\right)$$
23		ax-1	$$⊢\exists !vv\in \left(z\cap \left(y\cap \bigcup A\right)\right)\to \left(z\ne \varnothing \to \exists !vv\in \left(z\cap \left(y\cap \bigcup A\right)\right)\right)$$
24	22 23	syl6bi	$$⊢z\in x\to \left(\exists !vv\in \left(\left(z\setminus \bigcup \left(x\setminus \left\{z\right\}\right)\right)\cap y\right)\to \left(z\ne \varnothing \to \exists !vv\in \left(z\cap \left(y\cap \bigcup A\right)\right)\right)\right)$$
25	24	ralimia	$$⊢\forall z\in x\exists !vv\in \left(\left(z\setminus \bigcup \left(x\setminus \left\{z\right\}\right)\right)\cap y\right)\to \forall z\in x\left(z\ne \varnothing \to \exists !vv\in \left(z\cap \left(y\cap \bigcup A\right)\right)\right)$$
26	25	imim2i	$$⊢\left(\forall z\in xz\setminus \bigcup \left(x\setminus \left\{z\right\}\right)\ne \varnothing \to \forall z\in x\exists !vv\in \left(\left(z\setminus \bigcup \left(x\setminus \left\{z\right\}\right)\right)\cap y\right)\right)\to \left(\forall z\in xz\setminus \bigcup \left(x\setminus \left\{z\right\}\right)\ne \varnothing \to \forall z\in x\left(z\ne \varnothing \to \exists !vv\in \left(z\cap \left(y\cap \bigcup A\right)\right)\right)\right)$$
27	14 26	sylbi	$$⊢\left(\forall t\in xt\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\ne \varnothing \to \forall t\in x\exists !vv\in \left(\left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)\cap y\right)\right)\to \left(\forall z\in xz\setminus \bigcup \left(x\setminus \left\{z\right\}\right)\ne \varnothing \to \forall z\in x\left(z\ne \varnothing \to \exists !vv\in \left(z\cap \left(y\cap \bigcup A\right)\right)\right)\right)$$
28	1	raleqi	$$⊢\forall z\in A\left(z\ne \varnothing \to \exists !vv\in \left(z\cap y\right)\right)\leftrightarrow \forall z\in \left\{u|\exists t\in xu=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right\}\left(z\ne \varnothing \to \exists !vv\in \left(z\cap y\right)\right)$$
29		df-ral	$$⊢\forall z\in \left\{u|\exists t\in xu=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right\}\left(z\ne \varnothing \to \exists !vv\in \left(z\cap y\right)\right)\leftrightarrow \forall z\left(z\in \left\{u|\exists t\in xu=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right\}\to \left(z\ne \varnothing \to \exists !vv\in \left(z\cap y\right)\right)\right)$$
30		vex	$$⊢z\in \mathrm{V}$$
31		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)$$
32	31	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)$$
33	30 32	elab	$$⊢z\in \left\{u|\exists t\in xu=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right\}\leftrightarrow \exists t\in xz=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)$$
34	33	imbi1i	$$⊢\left(z\in \left\{u|\exists t\in xu=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right\}\to \left(z\ne \varnothing \to \exists !vv\in \left(z\cap y\right)\right)\right)\leftrightarrow \left(\exists t\in xz=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\to \left(z\ne \varnothing \to \exists !vv\in \left(z\cap y\right)\right)\right)$$
35		r19.23v	$$⊢\forall t\in x\left(z=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\to \left(z\ne \varnothing \to \exists !vv\in \left(z\cap y\right)\right)\right)\leftrightarrow \left(\exists t\in xz=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\to \left(z\ne \varnothing \to \exists !vv\in \left(z\cap y\right)\right)\right)$$
36	34 35	bitr4i	$$⊢\left(z\in \left\{u|\exists t\in xu=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right\}\to \left(z\ne \varnothing \to \exists !vv\in \left(z\cap y\right)\right)\right)\leftrightarrow \forall t\in x\left(z=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\to \left(z\ne \varnothing \to \exists !vv\in \left(z\cap y\right)\right)\right)$$
37	36	albii	$$⊢\forall z\left(z\in \left\{u|\exists t\in xu=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right\}\to \left(z\ne \varnothing \to \exists !vv\in \left(z\cap y\right)\right)\right)\leftrightarrow \forall z\forall t\in x\left(z=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\to \left(z\ne \varnothing \to \exists !vv\in \left(z\cap y\right)\right)\right)$$
38		ralcom4	$$⊢\forall t\in x\forall z\left(z=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\to \left(z\ne \varnothing \to \exists !vv\in \left(z\cap y\right)\right)\right)\leftrightarrow \forall z\forall t\in x\left(z=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\to \left(z\ne \varnothing \to \exists !vv\in \left(z\cap y\right)\right)\right)$$
39		vex	$$⊢t\in \mathrm{V}$$
40	39	difexi	$$⊢t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\in \mathrm{V}$$
41		neeq1	$$⊢z=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\to \left(z\ne \varnothing \leftrightarrow t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\ne \varnothing \right)$$
42		ineq1	$$⊢z=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\to z\cap y=\left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)\cap y$$
43	42	eleq2d	$$⊢z=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\to \left(v\in \left(z\cap y\right)\leftrightarrow v\in \left(\left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)\cap y\right)\right)$$
44	43	eubidv	$$⊢z=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\to \left(\exists !vv\in \left(z\cap y\right)\leftrightarrow \exists !vv\in \left(\left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)\cap y\right)\right)$$
45	41 44	imbi12d	$$⊢z=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\to \left(\left(z\ne \varnothing \to \exists !vv\in \left(z\cap y\right)\right)\leftrightarrow \left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\ne \varnothing \to \exists !vv\in \left(\left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)\cap y\right)\right)\right)$$
46	40 45	ceqsalv	$$⊢\forall z\left(z=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\to \left(z\ne \varnothing \to \exists !vv\in \left(z\cap y\right)\right)\right)\leftrightarrow \left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\ne \varnothing \to \exists !vv\in \left(\left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)\cap y\right)\right)$$
47	46	ralbii	$$⊢\forall t\in x\forall z\left(z=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\to \left(z\ne \varnothing \to \exists !vv\in \left(z\cap y\right)\right)\right)\leftrightarrow \forall t\in x\left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\ne \varnothing \to \exists !vv\in \left(\left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)\cap y\right)\right)$$
48	37 38 47	3bitr2i	$$⊢\forall z\left(z\in \left\{u|\exists t\in xu=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right\}\to \left(z\ne \varnothing \to \exists !vv\in \left(z\cap y\right)\right)\right)\leftrightarrow \forall t\in x\left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\ne \varnothing \to \exists !vv\in \left(\left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)\cap y\right)\right)$$
49	28 29 48	3bitri	$$⊢\forall z\in A\left(z\ne \varnothing \to \exists !vv\in \left(z\cap y\right)\right)\leftrightarrow \forall t\in x\left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\ne \varnothing \to \exists !vv\in \left(\left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)\cap y\right)\right)$$
50		ralim	$$⊢\forall t\in x\left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\ne \varnothing \to \exists !vv\in \left(\left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)\cap y\right)\right)\to \left(\forall t\in xt\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\ne \varnothing \to \forall t\in x\exists !vv\in \left(\left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)\cap y\right)\right)$$
51	49 50	sylbi	$$⊢\forall z\in A\left(z\ne \varnothing \to \exists !vv\in \left(z\cap y\right)\right)\to \left(\forall t\in xt\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\ne \varnothing \to \forall t\in x\exists !vv\in \left(\left(t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right)\cap y\right)\right)$$
52	27 51	syl11	$$⊢\forall z\in xz\setminus \bigcup \left(x\setminus \left\{z\right\}\right)\ne \varnothing \to \left(\forall z\in A\left(z\ne \varnothing \to \exists !vv\in \left(z\cap y\right)\right)\to \forall z\in x\left(z\ne \varnothing \to \exists !vv\in \left(z\cap \left(y\cap \bigcup A\right)\right)\right)\right)$$