Metamath Proof Explorer

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 e. _V
cover2.2 
|- A = U. B
Assertion cover2 
|- ( 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 cover2.1 
 |-  B e. _V
2 cover2.2 
 |-  A = U. B
3 ssrab2 
 |-  { y e. B | ph } C_ B
4 1 3 elpwi2 
 |-  { y e. B | ph } e. ~P B
5 nfra1 
 |-  F/ x A. x e. A E. y e. B ( x e. y /\ ph )
6 3 unissi 
 |-  U. { y e. B | ph } C_ U. B
7 6 sseli 
 |-  ( x e. U. { y e. B | ph } -> x e. U. B )
8 7 2 eleqtrrdi 
 |-  ( x e. U. { y e. B | ph } -> x e. A )
9 rsp 
 |-  ( A. x e. A E. y e. B ( x e. y /\ ph ) -> ( x e. A -> E. y e. B ( x e. y /\ ph ) ) )
10 elunirab 
 |-  ( x e. U. { y e. B | ph } <-> E. y e. B ( x e. y /\ ph ) )
11 9 10 syl6ibr 
 |-  ( A. x e. A E. y e. B ( x e. y /\ ph ) -> ( x e. A -> x e. U. { y e. B | ph } ) )
12 8 11 impbid2 
 |-  ( A. x e. A E. y e. B ( x e. y /\ ph ) -> ( x e. U. { y e. B | ph } <-> x e. A ) )
13 5 12 alrimi 
 |-  ( A. x e. A E. y e. B ( x e. y /\ ph ) -> A. x ( x e. U. { y e. B | ph } <-> x e. A ) )
14 dfcleq 
 |-  ( U. { y e. B | ph } = A <-> A. x ( x e. U. { y e. B | ph } <-> x e. A ) )
15 13 14 sylibr 
 |-  ( A. x e. A E. y e. B ( x e. y /\ ph ) -> U. { y e. B | ph } = A )
16 nfrab1 
 |-  F/_ y { y e. B | ph }
17 16 nfeq2 
 |-  F/ y z = { y e. B | ph }
18 eleq2 
 |-  ( z = { y e. B | ph } -> ( y e. z <-> y e. { y e. B | ph } ) )
19 rabid 
 |-  ( y e. { y e. B | ph } <-> ( y e. B /\ ph ) )
20 19 simprbi 
 |-  ( y e. { y e. B | ph } -> ph )
21 18 20 syl6bi 
 |-  ( z = { y e. B | ph } -> ( y e. z -> ph ) )
22 17 21 ralrimi 
 |-  ( z = { y e. B | ph } -> A. y e. z ph )
23 unieq 
 |-  ( z = { y e. B | ph } -> U. z = U. { y e. B | ph } )
24 23 eqeq1d 
 |-  ( z = { y e. B | ph } -> ( U. z = A <-> U. { y e. B | ph } = A ) )
25 24 anbi1d 
 |-  ( z = { y e. B | ph } -> ( ( U. z = A /\ A. y e. z ph ) <-> ( U. { y e. B | ph } = A /\ A. y e. z ph ) ) )
26 22 25 mpbiran2d 
 |-  ( z = { y e. B | ph } -> ( ( U. z = A /\ A. y e. z ph ) <-> U. { y e. B | ph } = A ) )
27 26 rspcev 
 |-  ( ( { y e. B | ph } e. ~P B /\ U. { y e. B | ph } = A ) -> E. z e. ~P B ( U. z = A /\ A. y e. z ph ) )
28 4 15 27 sylancr 
 |-  ( 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 ) )
29 elpwi 
 |-  ( z e. ~P B -> z C_ B )
30 r19.29r 
 |-  ( ( E. y e. z x e. y /\ A. y e. z ph ) -> E. y e. z ( x e. y /\ ph ) )
31 30 expcom 
 |-  ( A. y e. z ph -> ( E. y e. z x e. y -> E. y e. z ( x e. y /\ ph ) ) )
32 ssrexv 
 |-  ( z C_ B -> ( E. y e. z ( x e. y /\ ph ) -> E. y e. B ( x e. y /\ ph ) ) )
33 31 32 sylan9r 
 |-  ( ( z C_ B /\ A. y e. z ph ) -> ( E. y e. z x e. y -> E. y e. B ( x e. y /\ ph ) ) )
34 29 33 sylan 
 |-  ( ( z e. ~P B /\ A. y e. z ph ) -> ( E. y e. z x e. y -> E. y e. B ( x e. y /\ ph ) ) )
35 eleq2 
 |-  ( U. z = A -> ( x e. U. z <-> x e. A ) )
36 35 biimpar 
 |-  ( ( U. z = A /\ x e. A ) -> x e. U. z )
37 eluni2 
 |-  ( x e. U. z <-> E. y e. z x e. y )
38 36 37 sylib 
 |-  ( ( U. z = A /\ x e. A ) -> E. y e. z x e. y )
39 34 38 impel 
 |-  ( ( ( z e. ~P B /\ A. y e. z ph ) /\ ( U. z = A /\ x e. A ) ) -> E. y e. B ( x e. y /\ ph ) )
40 39 anassrs 
 |-  ( ( ( ( z e. ~P B /\ A. y e. z ph ) /\ U. z = A ) /\ x e. A ) -> E. y e. B ( x e. y /\ ph ) )
41 40 ralrimiva 
 |-  ( ( ( z e. ~P B /\ A. y e. z ph ) /\ U. z = A ) -> A. x e. A E. y e. B ( x e. y /\ ph ) )
42 41 anasss 
 |-  ( ( z e. ~P B /\ ( A. y e. z ph /\ U. z = A ) ) -> A. x e. A E. y e. B ( x e. y /\ ph ) )
43 42 ancom2s 
 |-  ( ( z e. ~P B /\ ( U. z = A /\ A. y e. z ph ) ) -> A. x e. A E. y e. B ( x e. y /\ ph ) )
44 43 rexlimiva 
 |-  ( E. z e. ~P B ( U. z = A /\ A. y e. z ph ) -> A. x e. A E. y e. B ( x e. y /\ ph ) )
45 28 44 impbii 
 |-  ( 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 ) )