Theorem cp

Description: Collection Principle. This remarkable theorem scheme is in effect a very strong generalization of the Axiom of Replacement. The proof makes use of Scott's trick df-scott to collapse a proper class into a set of minimum rank. The wff ph can be thought of as ph ( x , y ) . Scheme "Collection Principle" of Jech p. 72. (Contributed by NM, 17-Oct-2003)

	Ref	Expression
Assertion	cp	$$⊢\exists w\forall x\in z\left(\exists y\phi \to \exists y\in w\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢z\in \mathrm{V}$$
2	1	cplem2	$$⊢\exists w\forall x\in z\left(\left\{y|\phi \right\}\ne \varnothing \to \left\{y|\phi \right\}\cap w\ne \varnothing \right)$$
3		abn0	$$⊢\left\{y|\phi \right\}\ne \varnothing \leftrightarrow \exists y\phi$$
4		elin	$$⊢y\in \left(\left\{y|\phi \right\}\cap w\right)\leftrightarrow \left(y\in \left\{y|\phi \right\}\wedge y\in w\right)$$
5		abid	$$⊢y\in \left\{y|\phi \right\}\leftrightarrow \phi$$
6	5	anbi1i	$$⊢\left(y\in \left\{y|\phi \right\}\wedge y\in w\right)\leftrightarrow \left(\phi \wedge y\in w\right)$$
7		ancom	$$⊢\left(\phi \wedge y\in w\right)\leftrightarrow \left(y\in w\wedge \phi \right)$$
8	4 6 7	3bitri	$$⊢y\in \left(\left\{y|\phi \right\}\cap w\right)\leftrightarrow \left(y\in w\wedge \phi \right)$$
9	8	exbii	$$⊢\exists yy\in \left(\left\{y|\phi \right\}\cap w\right)\leftrightarrow \exists y\left(y\in w\wedge \phi \right)$$
10		nfab1	$$⊢\underset{\_}{Ⅎ}y\left\{y|\phi \right\}$$
11		nfcv	$$⊢\underset{\_}{Ⅎ}yw$$
12	10 11	nfin	$$⊢\underset{\_}{Ⅎ}y\left(\left\{y|\phi \right\}\cap w\right)$$
13	12	n0f	$$⊢\left\{y|\phi \right\}\cap w\ne \varnothing \leftrightarrow \exists yy\in \left(\left\{y|\phi \right\}\cap w\right)$$
14		df-rex	$$⊢\exists y\in w\phi \leftrightarrow \exists y\left(y\in w\wedge \phi \right)$$
15	9 13 14	3bitr4i	$$⊢\left\{y|\phi \right\}\cap w\ne \varnothing \leftrightarrow \exists y\in w\phi$$
16	3 15	imbi12i	$$⊢\left(\left\{y|\phi \right\}\ne \varnothing \to \left\{y|\phi \right\}\cap w\ne \varnothing \right)\leftrightarrow \left(\exists y\phi \to \exists y\in w\phi \right)$$
17	16	ralbii	$$⊢\forall x\in z\left(\left\{y|\phi \right\}\ne \varnothing \to \left\{y|\phi \right\}\cap w\ne \varnothing \right)\leftrightarrow \forall x\in z\left(\exists y\phi \to \exists y\in w\phi \right)$$
18	17	exbii	$$⊢\exists w\forall x\in z\left(\left\{y|\phi \right\}\ne \varnothing \to \left\{y|\phi \right\}\cap w\ne \varnothing \right)\leftrightarrow \exists w\forall x\in z\left(\exists y\phi \to \exists y\in w\phi \right)$$
19	2 18	mpbi	$$⊢\exists w\forall x\in z\left(\exists y\phi \to \exists y\in w\phi \right)$$