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 = U. B
Assertion	cover2g	|- ( B e. C -> ( A. x e. A E. y e. B ( x e. y /\ ph ) <-> E. z e. ~P B ( U. z = A /\ A. y e. z ph ) ) )

Proof

Step	Hyp	Ref	Expression
1		cover2g.1	|- A = U. B
2		unieq	|- ( b = B -> U. b = U. B )
3	2 1	eqtr4di	|- ( b = B -> U. b = A )
4		rexeq	|- ( b = B -> ( E. y e. b ( x e. y /\ ph ) <-> E. y e. B ( x e. y /\ ph ) ) )
5	3 4	raleqbidv	|- ( b = B -> ( A. x e. U. b E. y e. b ( x e. y /\ ph ) <-> A. x e. A E. y e. B ( x e. y /\ ph ) ) )
6		pweq	|- ( b = B -> ~P b = ~P B )
7	3	eqeq2d	|- ( b = B -> ( U. z = U. b <-> U. z = A ) )
8	7	anbi1d	|- ( b = B -> ( ( U. z = U. b /\ A. y e. z ph ) <-> ( U. z = A /\ A. y e. z ph ) ) )
9	6 8	rexeqbidv	|- ( b = B -> ( E. z e. ~P b ( U. z = U. b /\ A. y e. z ph ) <-> E. z e. ~P B ( U. z = A /\ A. y e. z ph ) ) )
10		vex	|- b e. _V
11		eqid	|- U. b = U. b
12	10 11	cover2	|- ( A. x e. U. b E. y e. b ( x e. y /\ ph ) <-> E. z e. ~P b ( U. z = U. b /\ A. y e. z ph ) )
13	5 9 12	vtoclbg	|- ( B e. C -> ( A. x e. A E. y e. B ( x e. y /\ ph ) <-> E. z e. ~P B ( U. z = A /\ A. y e. z ph ) ) )