Theorem cover2

Description: Two ways of expressing the statement "there is a cover of A by elements of B such that for each set in the cover, ph ". Note that ph and x must be distinct. (Contributed by Jeff Madsen, 20-Jun-2010)

	Ref	Expression
Hypotheses	cover2.1	$$⊢B\in \mathrm{V}$$
	cover2.2	$$⊢A=\bigcup B$$
Assertion	cover2	$$⊢\forall x\in A\exists y\in B\left(x\in y\wedge \phi \right)\leftrightarrow \exists z\in 𝒫B\left(\bigcup z=A\wedge \forall y\in z\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		cover2.1	$$⊢B\in \mathrm{V}$$
2		cover2.2	$$⊢A=\bigcup B$$
3		ssrab2	$$⊢\left\{y\in B|\phi \right\}\subseteq B$$
4	1 3	elpwi2	$$⊢\left\{y\in B|\phi \right\}\in 𝒫B$$
5		nfra1	$$⊢Ⅎx\forall x\in A\exists y\in B\left(x\in y\wedge \phi \right)$$
6	3	unissi	$$⊢\bigcup \left\{y\in B|\phi \right\}\subseteq \bigcup B$$
7	6	sseli	$$⊢x\in \bigcup \left\{y\in B|\phi \right\}\to x\in \bigcup B$$
8	7 2	eleqtrrdi	$$⊢x\in \bigcup \left\{y\in B|\phi \right\}\to x\in A$$
9		rsp	$$⊢\forall x\in A\exists y\in B\left(x\in y\wedge \phi \right)\to \left(x\in A\to \exists y\in B\left(x\in y\wedge \phi \right)\right)$$
10		elunirab	$$⊢x\in \bigcup \left\{y\in B|\phi \right\}\leftrightarrow \exists y\in B\left(x\in y\wedge \phi \right)$$
11	9 10	syl6ibr	$$⊢\forall x\in A\exists y\in B\left(x\in y\wedge \phi \right)\to \left(x\in A\to x\in \bigcup \left\{y\in B|\phi \right\}\right)$$
12	8 11	impbid2	$$⊢\forall x\in A\exists y\in B\left(x\in y\wedge \phi \right)\to \left(x\in \bigcup \left\{y\in B|\phi \right\}\leftrightarrow x\in A\right)$$
13	5 12	alrimi	$$⊢\forall x\in A\exists y\in B\left(x\in y\wedge \phi \right)\to \forall x\left(x\in \bigcup \left\{y\in B|\phi \right\}\leftrightarrow x\in A\right)$$
14		dfcleq	$$⊢\bigcup \left\{y\in B|\phi \right\}=A\leftrightarrow \forall x\left(x\in \bigcup \left\{y\in B|\phi \right\}\leftrightarrow x\in A\right)$$
15	13 14	sylibr	$$⊢\forall x\in A\exists y\in B\left(x\in y\wedge \phi \right)\to \bigcup \left\{y\in B|\phi \right\}=A$$
16		nfrab1	$$⊢\underset{\_}{Ⅎ}y\left\{y\in B|\phi \right\}$$
17	16	nfeq2	$$⊢Ⅎyz=\left\{y\in B|\phi \right\}$$
18		eleq2	$$⊢z=\left\{y\in B|\phi \right\}\to \left(y\in z\leftrightarrow y\in \left\{y\in B|\phi \right\}\right)$$
19		rabid	$$⊢y\in \left\{y\in B|\phi \right\}\leftrightarrow \left(y\in B\wedge \phi \right)$$
20	19	simprbi	$$⊢y\in \left\{y\in B|\phi \right\}\to \phi$$
21	18 20	syl6bi	$$⊢z=\left\{y\in B|\phi \right\}\to \left(y\in z\to \phi \right)$$
22	17 21	ralrimi	$$⊢z=\left\{y\in B|\phi \right\}\to \forall y\in z\phi$$
23		unieq	$$⊢z=\left\{y\in B|\phi \right\}\to \bigcup z=\bigcup \left\{y\in B|\phi \right\}$$
24	23	eqeq1d	$$⊢z=\left\{y\in B|\phi \right\}\to \left(\bigcup z=A\leftrightarrow \bigcup \left\{y\in B|\phi \right\}=A\right)$$
25	24	anbi1d	$$⊢z=\left\{y\in B|\phi \right\}\to \left(\left(\bigcup z=A\wedge \forall y\in z\phi \right)\leftrightarrow \left(\bigcup \left\{y\in B|\phi \right\}=A\wedge \forall y\in z\phi \right)\right)$$
26	22 25	mpbiran2d	$$⊢z=\left\{y\in B|\phi \right\}\to \left(\left(\bigcup z=A\wedge \forall y\in z\phi \right)\leftrightarrow \bigcup \left\{y\in B|\phi \right\}=A\right)$$
27	26	rspcev	$$⊢\left(\left\{y\in B|\phi \right\}\in 𝒫B\wedge \bigcup \left\{y\in B|\phi \right\}=A\right)\to \exists z\in 𝒫B\left(\bigcup z=A\wedge \forall y\in z\phi \right)$$
28	4 15 27	sylancr	$$⊢\forall x\in A\exists y\in B\left(x\in y\wedge \phi \right)\to \exists z\in 𝒫B\left(\bigcup z=A\wedge \forall y\in z\phi \right)$$
29		elpwi	$$⊢z\in 𝒫B\to z\subseteq B$$
30		r19.29r	$$⊢\left(\exists y\in zx\in y\wedge \forall y\in z\phi \right)\to \exists y\in z\left(x\in y\wedge \phi \right)$$
31	30	expcom	$$⊢\forall y\in z\phi \to \left(\exists y\in zx\in y\to \exists y\in z\left(x\in y\wedge \phi \right)\right)$$
32		ssrexv	$$⊢z\subseteq B\to \left(\exists y\in z\left(x\in y\wedge \phi \right)\to \exists y\in B\left(x\in y\wedge \phi \right)\right)$$
33	31 32	sylan9r	$$⊢\left(z\subseteq B\wedge \forall y\in z\phi \right)\to \left(\exists y\in zx\in y\to \exists y\in B\left(x\in y\wedge \phi \right)\right)$$
34	29 33	sylan	$$⊢\left(z\in 𝒫B\wedge \forall y\in z\phi \right)\to \left(\exists y\in zx\in y\to \exists y\in B\left(x\in y\wedge \phi \right)\right)$$
35		eleq2	$$⊢\bigcup z=A\to \left(x\in \bigcup z\leftrightarrow x\in A\right)$$
36	35	biimpar	$$⊢\left(\bigcup z=A\wedge x\in A\right)\to x\in \bigcup z$$
37		eluni2	$$⊢x\in \bigcup z\leftrightarrow \exists y\in zx\in y$$
38	36 37	sylib	$$⊢\left(\bigcup z=A\wedge x\in A\right)\to \exists y\in zx\in y$$
39	34 38	impel	$$⊢\left(\left(z\in 𝒫B\wedge \forall y\in z\phi \right)\wedge \left(\bigcup z=A\wedge x\in A\right)\right)\to \exists y\in B\left(x\in y\wedge \phi \right)$$
40	39	anassrs	$$⊢\left(\left(\left(z\in 𝒫B\wedge \forall y\in z\phi \right)\wedge \bigcup z=A\right)\wedge x\in A\right)\to \exists y\in B\left(x\in y\wedge \phi \right)$$
41	40	ralrimiva	$$⊢\left(\left(z\in 𝒫B\wedge \forall y\in z\phi \right)\wedge \bigcup z=A\right)\to \forall x\in A\exists y\in B\left(x\in y\wedge \phi \right)$$
42	41	anasss	$$⊢\left(z\in 𝒫B\wedge \left(\forall y\in z\phi \wedge \bigcup z=A\right)\right)\to \forall x\in A\exists y\in B\left(x\in y\wedge \phi \right)$$
43	42	ancom2s	$$⊢\left(z\in 𝒫B\wedge \left(\bigcup z=A\wedge \forall y\in z\phi \right)\right)\to \forall x\in A\exists y\in B\left(x\in y\wedge \phi \right)$$
44	43	rexlimiva	$$⊢\exists z\in 𝒫B\left(\bigcup z=A\wedge \forall y\in z\phi \right)\to \forall x\in A\exists y\in B\left(x\in y\wedge \phi \right)$$
45	28 44	impbii	$$⊢\forall x\in A\exists y\in B\left(x\in y\wedge \phi \right)\leftrightarrow \exists z\in 𝒫B\left(\bigcup z=A\wedge \forall y\in z\phi \right)$$