Theorem cover2 33863

Description: Two ways of expressing the statement "there is a cover of 𝐴 by elements of 𝐵 such that for each set in the cover, 𝜑". Note that 𝜑 and 𝑥 must be distinct. (Contributed by Jeff Madsen, 20-Jun-2010.)

Hypotheses

Ref	Expression
cover2.1	⊢ 𝐵 ∈ V
cover2.2	⊢ 𝐴 = ∪ 𝐵

Assertion

Ref	Expression
cover2	⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑) ↔ ∃𝑧 ∈ 𝒫 𝐵(∪ 𝑧 = 𝐴 ∧ ∀𝑦 ∈ 𝑧 𝜑))

Distinct variable groups:   𝜑,𝑥,𝑧   𝑥,𝐵,𝑦,𝑧   𝑥,𝐴,𝑧

Allowed substitution hints:   𝜑(𝑦)   𝐴(𝑦)

Proof of Theorem cover2

Step	Hyp	Ref	Expression
1		ssrab2 3846	. . . 4 ⊢ {𝑦 ∈ 𝐵 ∣ 𝜑} ⊆ 𝐵
2		cover2.1	. . . . 5 ⊢ 𝐵 ∈ V
3	2	elpw2 4985	. . . 4 ⊢ ({𝑦 ∈ 𝐵 ∣ 𝜑} ∈ 𝒫 𝐵 ↔ {𝑦 ∈ 𝐵 ∣ 𝜑} ⊆ 𝐵)
4	1, 3	mpbir 222	. . 3 ⊢ {𝑦 ∈ 𝐵 ∣ 𝜑} ∈ 𝒫 𝐵
5		nfra1 3087	. . . . 5 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑)
6	1	unissi 4618	. . . . . . . 8 ⊢ ∪ {𝑦 ∈ 𝐵 ∣ 𝜑} ⊆ ∪ 𝐵
7	6	sseli 3756	. . . . . . 7 ⊢ (𝑥 ∈ ∪ {𝑦 ∈ 𝐵 ∣ 𝜑} → 𝑥 ∈ ∪ 𝐵)
8		cover2.2	. . . . . . 7 ⊢ 𝐴 = ∪ 𝐵
9	7, 8	syl6eleqr 2854	. . . . . 6 ⊢ (𝑥 ∈ ∪ {𝑦 ∈ 𝐵 ∣ 𝜑} → 𝑥 ∈ 𝐴)
10		rsp 3075	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑) → (𝑥 ∈ 𝐴 → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑)))
11		elunirab 4605	. . . . . . 7 ⊢ (𝑥 ∈ ∪ {𝑦 ∈ 𝐵 ∣ 𝜑} ↔ ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑))
12	10, 11	syl6ibr 243	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑) → (𝑥 ∈ 𝐴 → 𝑥 ∈ ∪ {𝑦 ∈ 𝐵 ∣ 𝜑}))
13	9, 12	impbid2 217	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑) → (𝑥 ∈ ∪ {𝑦 ∈ 𝐵 ∣ 𝜑} ↔ 𝑥 ∈ 𝐴))
14	5, 13	alrimi 2246	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑) → ∀𝑥(𝑥 ∈ ∪ {𝑦 ∈ 𝐵 ∣ 𝜑} ↔ 𝑥 ∈ 𝐴))
15		dfcleq 2758	. . . 4 ⊢ (∪ {𝑦 ∈ 𝐵 ∣ 𝜑} = 𝐴 ↔ ∀𝑥(𝑥 ∈ ∪ {𝑦 ∈ 𝐵 ∣ 𝜑} ↔ 𝑥 ∈ 𝐴))
16	14, 15	sylibr 225	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑) → ∪ {𝑦 ∈ 𝐵 ∣ 𝜑} = 𝐴)
17		unieq 4601	. . . . . . 7 ⊢ (𝑧 = {𝑦 ∈ 𝐵 ∣ 𝜑} → ∪ 𝑧 = ∪ {𝑦 ∈ 𝐵 ∣ 𝜑})
18	17	eqeq1d 2766	. . . . . 6 ⊢ (𝑧 = {𝑦 ∈ 𝐵 ∣ 𝜑} → (∪ 𝑧 = 𝐴 ↔ ∪ {𝑦 ∈ 𝐵 ∣ 𝜑} = 𝐴))
19	18	anbi1d 623	. . . . 5 ⊢ (𝑧 = {𝑦 ∈ 𝐵 ∣ 𝜑} → ((∪ 𝑧 = 𝐴 ∧ ∀𝑦 ∈ 𝑧 𝜑) ↔ (∪ {𝑦 ∈ 𝐵 ∣ 𝜑} = 𝐴 ∧ ∀𝑦 ∈ 𝑧 𝜑)))
20		nfrab1 3269	. . . . . . . 8 ⊢ Ⅎ𝑦{𝑦 ∈ 𝐵 ∣ 𝜑}
21	20	nfeq2 2922	. . . . . . 7 ⊢ Ⅎ𝑦 𝑧 = {𝑦 ∈ 𝐵 ∣ 𝜑}
22		eleq2 2832	. . . . . . . 8 ⊢ (𝑧 = {𝑦 ∈ 𝐵 ∣ 𝜑} → (𝑦 ∈ 𝑧 ↔ 𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}))
23		rabid 3262	. . . . . . . . 9 ⊢ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑} ↔ (𝑦 ∈ 𝐵 ∧ 𝜑))
24	23	simprbi 490	. . . . . . . 8 ⊢ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑} → 𝜑)
25	22, 24	syl6bi 244	. . . . . . 7 ⊢ (𝑧 = {𝑦 ∈ 𝐵 ∣ 𝜑} → (𝑦 ∈ 𝑧 → 𝜑))
26	21, 25	ralrimi 3103	. . . . . 6 ⊢ (𝑧 = {𝑦 ∈ 𝐵 ∣ 𝜑} → ∀𝑦 ∈ 𝑧 𝜑)
27	26	biantrud 527	. . . . 5 ⊢ (𝑧 = {𝑦 ∈ 𝐵 ∣ 𝜑} → (∪ {𝑦 ∈ 𝐵 ∣ 𝜑} = 𝐴 ↔ (∪ {𝑦 ∈ 𝐵 ∣ 𝜑} = 𝐴 ∧ ∀𝑦 ∈ 𝑧 𝜑)))
28	19, 27	bitr4d 273	. . . 4 ⊢ (𝑧 = {𝑦 ∈ 𝐵 ∣ 𝜑} → ((∪ 𝑧 = 𝐴 ∧ ∀𝑦 ∈ 𝑧 𝜑) ↔ ∪ {𝑦 ∈ 𝐵 ∣ 𝜑} = 𝐴))
29	28	rspcev 3460	. . 3 ⊢ (({𝑦 ∈ 𝐵 ∣ 𝜑} ∈ 𝒫 𝐵 ∧ ∪ {𝑦 ∈ 𝐵 ∣ 𝜑} = 𝐴) → ∃𝑧 ∈ 𝒫 𝐵(∪ 𝑧 = 𝐴 ∧ ∀𝑦 ∈ 𝑧 𝜑))
30	4, 16, 29	sylancr 581	. 2 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑) → ∃𝑧 ∈ 𝒫 𝐵(∪ 𝑧 = 𝐴 ∧ ∀𝑦 ∈ 𝑧 𝜑))
31		elpwi 4324	. . . . . . . . 9 ⊢ (𝑧 ∈ 𝒫 𝐵 → 𝑧 ⊆ 𝐵)
32		r19.29r 3219	. . . . . . . . . . 11 ⊢ ((∃𝑦 ∈ 𝑧 𝑥 ∈ 𝑦 ∧ ∀𝑦 ∈ 𝑧 𝜑) → ∃𝑦 ∈ 𝑧 (𝑥 ∈ 𝑦 ∧ 𝜑))
33	32	expcom 402	. . . . . . . . . 10 ⊢ (∀𝑦 ∈ 𝑧 𝜑 → (∃𝑦 ∈ 𝑧 𝑥 ∈ 𝑦 → ∃𝑦 ∈ 𝑧 (𝑥 ∈ 𝑦 ∧ 𝜑)))
34		ssrexv 3826	. . . . . . . . . 10 ⊢ (𝑧 ⊆ 𝐵 → (∃𝑦 ∈ 𝑧 (𝑥 ∈ 𝑦 ∧ 𝜑) → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑)))
35	33, 34	sylan9r 504	. . . . . . . . 9 ⊢ ((𝑧 ⊆ 𝐵 ∧ ∀𝑦 ∈ 𝑧 𝜑) → (∃𝑦 ∈ 𝑧 𝑥 ∈ 𝑦 → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑)))
36	31, 35	sylan 575	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝒫 𝐵 ∧ ∀𝑦 ∈ 𝑧 𝜑) → (∃𝑦 ∈ 𝑧 𝑥 ∈ 𝑦 → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑)))
37		eleq2 2832	. . . . . . . . . 10 ⊢ (∪ 𝑧 = 𝐴 → (𝑥 ∈ ∪ 𝑧 ↔ 𝑥 ∈ 𝐴))
38	37	biimpar 469	. . . . . . . . 9 ⊢ ((∪ 𝑧 = 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ∪ 𝑧)
39		eluni2 4597	. . . . . . . . 9 ⊢ (𝑥 ∈ ∪ 𝑧 ↔ ∃𝑦 ∈ 𝑧 𝑥 ∈ 𝑦)
40	38, 39	sylib 209	. . . . . . . 8 ⊢ ((∪ 𝑧 = 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ 𝑧 𝑥 ∈ 𝑦)
41	36, 40	impel 501	. . . . . . 7 ⊢ (((𝑧 ∈ 𝒫 𝐵 ∧ ∀𝑦 ∈ 𝑧 𝜑) ∧ (∪ 𝑧 = 𝐴 ∧ 𝑥 ∈ 𝐴)) → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑))
42	41	anassrs 459	. . . . . 6 ⊢ ((((𝑧 ∈ 𝒫 𝐵 ∧ ∀𝑦 ∈ 𝑧 𝜑) ∧ ∪ 𝑧 = 𝐴) ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑))
43	42	ralrimiva 3112	. . . . 5 ⊢ (((𝑧 ∈ 𝒫 𝐵 ∧ ∀𝑦 ∈ 𝑧 𝜑) ∧ ∪ 𝑧 = 𝐴) → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑))
44	43	anasss 458	. . . 4 ⊢ ((𝑧 ∈ 𝒫 𝐵 ∧ (∀𝑦 ∈ 𝑧 𝜑 ∧ ∪ 𝑧 = 𝐴)) → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑))
45	44	ancom2s 640	. . 3 ⊢ ((𝑧 ∈ 𝒫 𝐵 ∧ (∪ 𝑧 = 𝐴 ∧ ∀𝑦 ∈ 𝑧 𝜑)) → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑))
46	45	rexlimiva 3174	. 2 ⊢ (∃𝑧 ∈ 𝒫 𝐵(∪ 𝑧 = 𝐴 ∧ ∀𝑦 ∈ 𝑧 𝜑) → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑))
47	30, 46	impbii 200	1 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑) ↔ ∃𝑧 ∈ 𝒫 𝐵(∪ 𝑧 = 𝐴 ∧ ∀𝑦 ∈ 𝑧 𝜑))

Syntax hints:   → wi 4   ↔ wb 197   ∧ wa 384  ∀wal 1650   = wceq 1652   ∈ wcel 2155  ∀wral 3054  ∃wrex 3055  {crab 3058  Vcvv 3349   ⊆ wss 3731  𝒫 cpw 4314  ∪ cuni 4593

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742  ax-sep 4940

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-ral 3059  df-rex 3060  df-rab 3063  df-v 3351  df-in 3738  df-ss 3745  df-pw 4316  df-uni 4594

This theorem is referenced by:  cover2g  33864