Theorem cover2 30179

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.)

Hypotheses

Ref	Expression
cover2.1	|- B e. _V
cover2.2	|- A = U. B

Assertion

Ref	Expression
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 ) )

Distinct variable groups:   ph, x, z   x, B, y, z   x, A, z

Allowed substitution hints:   ph( y)   A( y)

Proof of Theorem cover2

Step	Hyp	Ref	Expression
1		ssrab2 3570	. . . 4 |- { y e. B | ph } C_ B
2		cover2.1	. . . . 5 |- B e. _V
3	2	elpw2 4601	. . . 4 |- ( { y e. B | ph } e. ~P B <-> { y e. B | ph } C_ B )
4	1, 3	mpbir 209	. . 3 |- { y e. B | ph } e. ~P B
5		nfra1 2824	. . . . 5 |- F/ x A. x e. A E. y e. B ( x e. y /\ ph )
6	1	unissi 4257	. . . . . . . 8 |- U. { y e. B | ph } C_ U. B
7	6	sseli 3485	. . . . . . 7 |- ( x e. U. { y e. B | ph } -> x e. U. B )
8		cover2.2	. . . . . . 7 |- A = U. B
9	7, 8	syl6eleqr 2542	. . . . . 6 |- ( x e. U. { y e. B | ph } -> x e. A )
10		rsp 2809	. . . . . . 7 |- ( A. x e. A E. y e. B ( x e. y /\ ph ) -> ( x e. A -> E. y e. B ( x e. y /\ ph ) ) )
11		elunirab 4246	. . . . . . 7 |- ( x e. U. { y e. B | ph } <-> E. y e. B ( x e. y /\ ph ) )
12	10, 11	syl6ibr 227	. . . . . 6 |- ( A. x e. A E. y e. B ( x e. y /\ ph ) -> ( x e. A -> x e. U. { y e. B | ph } ) )
13	9, 12	impbid2 204	. . . . 5 |- ( A. x e. A E. y e. B ( x e. y /\ ph ) -> ( x e. U. { y e. B | ph } <-> x e. A ) )
14	5, 13	alrimi 1863	. . . 4 |- ( A. x e. A E. y e. B ( x e. y /\ ph ) -> A. x ( x e. U. { y e. B | ph } <-> x e. A ) )
15		dfcleq 2436	. . . 4 |- ( U. { y e. B | ph } = A <-> A. x ( x e. U. { y e. B | ph } <-> x e. A ) )
16	14, 15	sylibr 212	. . 3 |- ( A. x e. A E. y e. B ( x e. y /\ ph ) -> U. { y e. B | ph } = A )
17		unieq 4242	. . . . . . 7 |- ( z = { y e. B | ph } -> U. z = U. { y e. B | ph } )
18	17	eqeq1d 2445	. . . . . 6 |- ( z = { y e. B | ph } -> ( U. z = A <-> U. { y e. B | ph } = A ) )
19	18	anbi1d 704	. . . . 5 |- ( z = { y e. B | ph } -> ( ( U. z = A /\ A. y e. z ph ) <-> ( U. { y e. B | ph } = A /\ A. y e. z ph ) ) )
20		nfrab1 3024	. . . . . . . 8 |- F/_ y { y e. B | ph }
21	20	nfeq2 2622	. . . . . . 7 |- F/ y z = { y e. B | ph }
22		eleq2 2516	. . . . . . . 8 |- ( z = { y e. B | ph } -> ( y e. z <-> y e. { y e. B | ph } ) )
23		rabid 3020	. . . . . . . . 9 |- ( y e. { y e. B | ph } <-> ( y e. B /\ ph ) )
24	23	simprbi 464	. . . . . . . 8 |- ( y e. { y e. B | ph } -> ph )
25	22, 24	syl6bi 228	. . . . . . 7 |- ( z = { y e. B | ph } -> ( y e. z -> ph ) )
26	21, 25	ralrimi 2843	. . . . . 6 |- ( z = { y e. B | ph } -> A. y e. z ph )
27	26	biantrud 507	. . . . 5 |- ( z = { y e. B | ph } -> ( U. { y e. B | ph } = A <-> ( U. { y e. B | ph } = A /\ A. y e. z ph ) ) )
28	19, 27	bitr4d 256	. . . 4 |- ( z = { y e. B | ph } -> ( ( U. z = A /\ A. y e. z ph ) <-> U. { y e. B | ph } = A ) )
29	28	rspcev 3196	. . 3 |- ( ( { 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 ) )
30	4, 16, 29	sylancr 663	. 2 |- ( 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 ) )
31		eleq2 2516	. . . . . . . . . 10 |- ( U. z = A -> ( x e. U. z <-> x e. A ) )
32	31	biimpar 485	. . . . . . . . 9 |- ( ( U. z = A /\ x e. A ) -> x e. U. z )
33		eluni2 4238	. . . . . . . . 9 |- ( x e. U. z <-> E. y e. z x e. y )
34	32, 33	sylib 196	. . . . . . . 8 |- ( ( U. z = A /\ x e. A ) -> E. y e. z x e. y )
35		elpwi 4006	. . . . . . . . . 10 |- ( z e. ~P B -> z C_ B )
36		r19.29r 2979	. . . . . . . . . . . 12 |- ( ( E. y e. z x e. y /\ A. y e. z ph ) -> E. y e. z ( x e. y /\ ph ) )
37	36	expcom 435	. . . . . . . . . . 11 |- ( A. y e. z ph -> ( E. y e. z x e. y -> E. y e. z ( x e. y /\ ph ) ) )
38		ssrexv 3550	. . . . . . . . . . 11 |- ( z C_ B -> ( E. y e. z ( x e. y /\ ph ) -> E. y e. B ( x e. y /\ ph ) ) )
39	37, 38	sylan9r 658	. . . . . . . . . 10 |- ( ( z C_ B /\ A. y e. z ph ) -> ( E. y e. z x e. y -> E. y e. B ( x e. y /\ ph ) ) )
40	35, 39	sylan 471	. . . . . . . . 9 |- ( ( z e. ~P B /\ A. y e. z ph ) -> ( E. y e. z x e. y -> E. y e. B ( x e. y /\ ph ) ) )
41	40	imp 429	. . . . . . . 8 |- ( ( ( z e. ~P B /\ A. y e. z ph ) /\ E. y e. z x e. y ) -> E. y e. B ( x e. y /\ ph ) )
42	34, 41	sylan2 474	. . . . . . 7 |- ( ( ( z e. ~P B /\ A. y e. z ph ) /\ ( U. z = A /\ x e. A ) ) -> E. y e. B ( x e. y /\ ph ) )
43	42	anassrs 648	. . . . . 6 |- ( ( ( ( z e. ~P B /\ A. y e. z ph ) /\ U. z = A ) /\ x e. A ) -> E. y e. B ( x e. y /\ ph ) )
44	43	ralrimiva 2857	. . . . 5 |- ( ( ( z e. ~P B /\ A. y e. z ph ) /\ U. z = A ) -> A. x e. A E. y e. B ( x e. y /\ ph ) )
45	44	anasss 647	. . . 4 |- ( ( z e. ~P B /\ ( A. y e. z ph /\ U. z = A ) ) -> A. x e. A E. y e. B ( x e. y /\ ph ) )
46	45	ancom2s 802	. . 3 |- ( ( z e. ~P B /\ ( U. z = A /\ A. y e. z ph ) ) -> A. x e. A E. y e. B ( x e. y /\ ph ) )
47	46	rexlimiva 2931	. 2 |- ( 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 ) )
48	30, 47	impbii 188	1 |- ( 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 ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   A.wal 1381   = wceq 1383   e. wcel 1804   A.wral 2793   E.wrex 2794   {crab 2797   _Vcvv 3095   C_ wss 3461   ~Pcpw 3997   U.cuni 4234

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-in 3468  df-ss 3475  df-pw 3999  df-uni 4235

This theorem is referenced by:  cover2g  30180