Theorem cover2g

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, 21-Jun-2010)

	Ref	Expression
Hypothesis	cover2g.1	$$⊢A=\bigcup B$$
Assertion	cover2g	$$⊢B\in C\to \left(\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)\right)$$

Proof

Step	Hyp	Ref	Expression
1		cover2g.1	$$⊢A=\bigcup B$$
2		unieq	$$⊢b=B\to \bigcup b=\bigcup B$$
3	2 1	eqtr4di	$$⊢b=B\to \bigcup b=A$$
4		rexeq	$$⊢b=B\to \left(\exists y\in b\left(x\in y\wedge \phi \right)\leftrightarrow \exists y\in B\left(x\in y\wedge \phi \right)\right)$$
5	3 4	raleqbidv	$$⊢b=B\to \left(\forall x\in \bigcup b\exists y\in b\left(x\in y\wedge \phi \right)\leftrightarrow \forall x\in A\exists y\in B\left(x\in y\wedge \phi \right)\right)$$
6		pweq	$$⊢b=B\to 𝒫b=𝒫B$$
7	3	eqeq2d	$$⊢b=B\to \left(\bigcup z=\bigcup b\leftrightarrow \bigcup z=A\right)$$
8	7	anbi1d	$$⊢b=B\to \left(\left(\bigcup z=\bigcup b\wedge \forall y\in z\phi \right)\leftrightarrow \left(\bigcup z=A\wedge \forall y\in z\phi \right)\right)$$
9	6 8	rexeqbidv	$$⊢b=B\to \left(\exists z\in 𝒫b\left(\bigcup z=\bigcup b\wedge \forall y\in z\phi \right)\leftrightarrow \exists z\in 𝒫B\left(\bigcup z=A\wedge \forall y\in z\phi \right)\right)$$
10		vex	$$⊢b\in \mathrm{V}$$
11		eqid	$$⊢\bigcup b=\bigcup b$$
12	10 11	cover2	$$⊢\forall x\in \bigcup b\exists y\in b\left(x\in y\wedge \phi \right)\leftrightarrow \exists z\in 𝒫b\left(\bigcup z=\bigcup b\wedge \forall y\in z\phi \right)$$
13	5 9 12	vtoclbg	$$⊢B\in C\to \left(\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)\right)$$