Theorem kmlem10

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	kmlem10	$$⊢\forall h\left(\forall z\in h\forall w\in h\left(z\ne w\to z\cap w=\varnothing \right)\to \exists y\forall z\in h\phi \right)\to \exists y\forall z\in A\phi$$

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	kmlem9	$$⊢\forall z\in A\forall w\in A\left(z\ne w\to z\cap w=\varnothing \right)$$
3		vex	$$⊢x\in \mathrm{V}$$
4	3	abrexex	$$⊢\left\{u|\exists t\in xu=t\setminus \bigcup \left(x\setminus \left\{t\right\}\right)\right\}\in \mathrm{V}$$
5	1 4	eqeltri	$$⊢A\in \mathrm{V}$$
6		raleq	$$⊢h=A\to \left(\forall w\in h\left(z\ne w\to z\cap w=\varnothing \right)\leftrightarrow \forall w\in A\left(z\ne w\to z\cap w=\varnothing \right)\right)$$
7	6	raleqbi1dv	$$⊢h=A\to \left(\forall z\in h\forall w\in h\left(z\ne w\to z\cap w=\varnothing \right)\leftrightarrow \forall z\in A\forall w\in A\left(z\ne w\to z\cap w=\varnothing \right)\right)$$
8		raleq	$$⊢h=A\to \left(\forall z\in h\phi \leftrightarrow \forall z\in A\phi \right)$$
9	8	exbidv	$$⊢h=A\to \left(\exists y\forall z\in h\phi \leftrightarrow \exists y\forall z\in A\phi \right)$$
10	7 9	imbi12d	$$⊢h=A\to \left(\left(\forall z\in h\forall w\in h\left(z\ne w\to z\cap w=\varnothing \right)\to \exists y\forall z\in h\phi \right)\leftrightarrow \left(\forall z\in A\forall w\in A\left(z\ne w\to z\cap w=\varnothing \right)\to \exists y\forall z\in A\phi \right)\right)$$
11	5 10	spcv	$$⊢\forall h\left(\forall z\in h\forall w\in h\left(z\ne w\to z\cap w=\varnothing \right)\to \exists y\forall z\in h\phi \right)\to \left(\forall z\in A\forall w\in A\left(z\ne w\to z\cap w=\varnothing \right)\to \exists y\forall z\in A\phi \right)$$
12	2 11	mpi	$$⊢\forall h\left(\forall z\in h\forall w\in h\left(z\ne w\to z\cap w=\varnothing \right)\to \exists y\forall z\in h\phi \right)\to \exists y\forall z\in A\phi$$