Theorem cover2 15673

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.

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

Proof of Theorem cover2

Step	Hyp	Ref	Expression
1		unieq 3185	. . . . . . 7 |- (z = {y e. B | ph} -> U.z = U.{y e. B | ph})
2	1	eqeq1d 1892	. . . . . 6 |- (z = {y e. B | ph} -> (U.z = A <-> U.{y e. B | ph} = A))
3	2	anbi1d 679	. . . . 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)))
4		ax-17 1317	. . . . . . . 8 |- (x e. z -> A.y x e. z)
5		hbrab1 2257	. . . . . . . 8 |- (x e. {y e. B | ph} -> A.y x e. {y e. B | ph})
6	4, 5	hbeq 1995	. . . . . . 7 |- (z = {y e. B | ph} -> A.y z = {y e. B | ph})
7		eleq2 1958	. . . . . . . 8 |- (z = {y e. B | ph} -> (y e. z <-> y e. {y e. B | ph}))
8		rabid 2253	. . . . . . . . 9 |- (y e. {y e. B | ph} <-> (y e. B /\ ph))
9	8	simprbi 353	. . . . . . . 8 |- (y e. {y e. B | ph} -> ph)
10	7, 9	syl6bi 231	. . . . . . 7 |- (z = {y e. B | ph} -> (y e. z -> ph))
11	6, 10	r19.21ai 2174	. . . . . 6 |- (z = {y e. B | ph} -> A.y e. z ph)
12	11	biantrud 795	. . . . 5 |- (z = {y e. B | ph} -> (U.{y e. B | ph} = A <-> (U.{y e. B | ph} = A /\ A.y e. z ph)))
13	3, 12	bitr4d 590	. . . 4 |- (z = {y e. B | ph} -> ((U.z = A /\ A.y e. z ph) <-> U.{y e. B | ph} = A))
14	13	rcla4ev 2381	. . 3 |- (({y e. B | ph} e. ~PB /\ U.{y e. B | ph} = A) -> E.z e. ~P B(U.z = A /\ A.y e. z ph))
15		ssrab2 2692	. . . 4 |- {y e. B | ph} C_ B
16		cover2.1	. . . . 5 |- B e. _V
17	16	elpw2 3464	. . . 4 |- ({y e. B | ph} e. ~PB <-> {y e. B | ph} C_ B)
18	15, 17	mpbir 207	. . 3 |- {y e. B | ph} e. ~PB
19		hbra1 2147	. . . . 5 |- (A.x e. A E.y e. B (x e. y /\ ph) -> A.xA.x e. A E.y e. B (x e. y /\ ph))
20		uniss 3199	. . . . . . . . 9 |- ({y e. B | ph} C_ B -> U.{y e. B | ph} C_ U.B)
21	15, 20	ax-mp 7	. . . . . . . 8 |- U.{y e. B | ph} C_ U.B
22	21	sseli 2617	. . . . . . 7 |- (x e. U.{y e. B | ph} -> x e. U.B)
23		cover2.2	. . . . . . 7 |- A = U.B
24	22, 23	syl6eleqr 1982	. . . . . 6 |- (x e. U.{y e. B | ph} -> x e. A)
25		ra4 2155	. . . . . . 7 |- (A.x e. A E.y e. B (x e. y /\ ph) -> (x e. A -> E.y e. B (x e. y /\ ph)))
26		elunirab 3190	. . . . . . 7 |- (x e. U.{y e. B | ph} <-> E.y e. B (x e. y /\ ph))
27	25, 26	syl6ibr 230	. . . . . 6 |- (A.x e. A E.y e. B (x e. y /\ ph) -> (x e. A -> x e. U.{y e. B | ph}))
28	24, 27	impbid2 576	. . . . 5 |- (A.x e. A E.y e. B (x e. y /\ ph) -> (x e. U.{y e. B | ph} <-> x e. A))
29	19, 28	19.21ai 1345	. . . 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))
30		dfcleq 1878	. . . 4 |- (U.{y e. B | ph} = A <-> A.x(x e. U.{y e. B | ph} <-> x e. A))
31	29, 30	sylibr 217	. . 3 |- (A.x e. A E.y e. B (x e. y /\ ph) -> U.{y e. B | ph} = A)
32	14, 18, 31	sylancr 526	. 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))
33		r19.29r 2229	. . . . . . . . . . . 12 |- ((E.y e. z x e. y /\ A.y e. z ph) -> E.y e. z (x e. y /\ ph))
34	33	expcom 403	. . . . . . . . . . 11 |- (A.y e. z ph -> (E.y e. z x e. y -> E.y e. z (x e. y /\ ph)))
35		ssrexv 2673	. . . . . . . . . . 11 |- (z C_ B -> (E.y e. z (x e. y /\ ph) -> E.y e. B (x e. y /\ ph)))
36	34, 35	sylan9r 519	. . . . . . . . . 10 |- ((z C_ B /\ A.y e. z ph) -> (E.y e. z x e. y -> E.y e. B (x e. y /\ ph)))
37		elpwi 3039	. . . . . . . . . 10 |- (z e. ~PB -> z C_ B)
38	36, 37	sylan 497	. . . . . . . . 9 |- ((z e. ~PB /\ A.y e. z ph) -> (E.y e. z x e. y -> E.y e. B (x e. y /\ ph)))
39	38	imp 377	. . . . . . . 8 |- (((z e. ~PB /\ A.y e. z ph) /\ E.y e. z x e. y) -> E.y e. B (x e. y /\ ph))
40		eleq2 1958	. . . . . . . . . 10 |- (U.z = A -> (x e. U.z <-> x e. A))
41	40	biimpar 461	. . . . . . . . 9 |- ((U.z = A /\ x e. A) -> x e. U.z)
42		eluni2 3181	. . . . . . . . 9 |- (x e. U.z <-> E.y e. z x e. y)
43	41, 42	sylib 215	. . . . . . . 8 |- ((U.z = A /\ x e. A) -> E.y e. z x e. y)
44	39, 43	sylan2 500	. . . . . . 7 |- (((z e. ~PB /\ A.y e. z ph) /\ (U.z = A /\ x e. A)) -> E.y e. B (x e. y /\ ph))
45	44	anassrs 489	. . . . . 6 |- ((((z e. ~PB /\ A.y e. z ph) /\ U.z = A) /\ x e. A) -> E.y e. B (x e. y /\ ph))
46	45	r19.21aiva 2176	. . . . 5 |- (((z e. ~PB /\ A.y e. z ph) /\ U.z = A) -> A.x e. A E.y e. B (x e. y /\ ph))
47	46	anasss 488	. . . 4 |- ((z e. ~PB /\ (A.y e. z ph /\ U.z = A)) -> A.x e. A E.y e. B (x e. y /\ ph))
48	47	ancom2s 545	. . 3 |- ((z e. ~PB /\ (U.z = A /\ A.y e. z ph)) -> A.x e. A E.y e. B (x e. y /\ ph))
49	48	r19.23aiva 2212	. 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))
50	32, 49	impbii 174	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 3   <-> wb 163   /\ wa 240  A.wal 1296   = wceq 1298   e. wcel 1300  A.wral 2105  E.wrex 2106  {crab 2108  _Vcvv 2292   C_ wss 2593  ~Pcpw 3032  U.cuni 3177

This theorem is referenced by:  cover2g 15674

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-ral 2109  df-rex 2110  df-rab 2112  df-v 2294  df-in 2603  df-ss 2605  df-pw 3035  df-uni 3178

Copyright terms: Public domain