Theorem cover2 33508

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 3687	. . . 4 ⊢ {𝑦 ∈ 𝐵 ∣ 𝜑} ⊆ 𝐵
2		cover2.1	. . . . 5 ⊢ 𝐵 ∈ V
3	2	elpw2 4828	. . . 4 ⊢ ({𝑦 ∈ 𝐵 ∣ 𝜑} ∈ 𝒫 𝐵 ↔ {𝑦 ∈ 𝐵 ∣ 𝜑} ⊆ 𝐵)
4	1, 3	mpbir 221	. . 3 ⊢ {𝑦 ∈ 𝐵 ∣ 𝜑} ∈ 𝒫 𝐵
5		nfra1 2941	. . . . 5 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑)
6	1	unissi 4461	. . . . . . . 8 ⊢ ∪ {𝑦 ∈ 𝐵 ∣ 𝜑} ⊆ ∪ 𝐵
7	6	sseli 3599	. . . . . . 7 ⊢ (𝑥 ∈ ∪ {𝑦 ∈ 𝐵 ∣ 𝜑} → 𝑥 ∈ ∪ 𝐵)
8		cover2.2	. . . . . . 7 ⊢ 𝐴 = ∪ 𝐵
9	7, 8	syl6eleqr 2712	. . . . . 6 ⊢ (𝑥 ∈ ∪ {𝑦 ∈ 𝐵 ∣ 𝜑} → 𝑥 ∈ 𝐴)
10		rsp 2929	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑) → (𝑥 ∈ 𝐴 → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑)))
11		elunirab 4448	. . . . . . 7 ⊢ (𝑥 ∈ ∪ {𝑦 ∈ 𝐵 ∣ 𝜑} ↔ ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑))
12	10, 11	syl6ibr 242	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑) → (𝑥 ∈ 𝐴 → 𝑥 ∈ ∪ {𝑦 ∈ 𝐵 ∣ 𝜑}))
13	9, 12	impbid2 216	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑) → (𝑥 ∈ ∪ {𝑦 ∈ 𝐵 ∣ 𝜑} ↔ 𝑥 ∈ 𝐴))
14	5, 13	alrimi 2082	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑) → ∀𝑥(𝑥 ∈ ∪ {𝑦 ∈ 𝐵 ∣ 𝜑} ↔ 𝑥 ∈ 𝐴))
15		dfcleq 2616	. . . 4 ⊢ (∪ {𝑦 ∈ 𝐵 ∣ 𝜑} = 𝐴 ↔ ∀𝑥(𝑥 ∈ ∪ {𝑦 ∈ 𝐵 ∣ 𝜑} ↔ 𝑥 ∈ 𝐴))
16	14, 15	sylibr 224	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑) → ∪ {𝑦 ∈ 𝐵 ∣ 𝜑} = 𝐴)
17		unieq 4444	. . . . . . 7 ⊢ (𝑧 = {𝑦 ∈ 𝐵 ∣ 𝜑} → ∪ 𝑧 = ∪ {𝑦 ∈ 𝐵 ∣ 𝜑})
18	17	eqeq1d 2624	. . . . . 6 ⊢ (𝑧 = {𝑦 ∈ 𝐵 ∣ 𝜑} → (∪ 𝑧 = 𝐴 ↔ ∪ {𝑦 ∈ 𝐵 ∣ 𝜑} = 𝐴))
19	18	anbi1d 741	. . . . 5 ⊢ (𝑧 = {𝑦 ∈ 𝐵 ∣ 𝜑} → ((∪ 𝑧 = 𝐴 ∧ ∀𝑦 ∈ 𝑧 𝜑) ↔ (∪ {𝑦 ∈ 𝐵 ∣ 𝜑} = 𝐴 ∧ ∀𝑦 ∈ 𝑧 𝜑)))
20		nfrab1 3122	. . . . . . . 8 ⊢ Ⅎ𝑦{𝑦 ∈ 𝐵 ∣ 𝜑}
21	20	nfeq2 2780	. . . . . . 7 ⊢ Ⅎ𝑦 𝑧 = {𝑦 ∈ 𝐵 ∣ 𝜑}
22		eleq2 2690	. . . . . . . 8 ⊢ (𝑧 = {𝑦 ∈ 𝐵 ∣ 𝜑} → (𝑦 ∈ 𝑧 ↔ 𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}))
23		rabid 3116	. . . . . . . . 9 ⊢ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑} ↔ (𝑦 ∈ 𝐵 ∧ 𝜑))
24	23	simprbi 480	. . . . . . . 8 ⊢ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑} → 𝜑)
25	22, 24	syl6bi 243	. . . . . . 7 ⊢ (𝑧 = {𝑦 ∈ 𝐵 ∣ 𝜑} → (𝑦 ∈ 𝑧 → 𝜑))
26	21, 25	ralrimi 2957	. . . . . 6 ⊢ (𝑧 = {𝑦 ∈ 𝐵 ∣ 𝜑} → ∀𝑦 ∈ 𝑧 𝜑)
27	26	biantrud 528	. . . . 5 ⊢ (𝑧 = {𝑦 ∈ 𝐵 ∣ 𝜑} → (∪ {𝑦 ∈ 𝐵 ∣ 𝜑} = 𝐴 ↔ (∪ {𝑦 ∈ 𝐵 ∣ 𝜑} = 𝐴 ∧ ∀𝑦 ∈ 𝑧 𝜑)))
28	19, 27	bitr4d 271	. . . 4 ⊢ (𝑧 = {𝑦 ∈ 𝐵 ∣ 𝜑} → ((∪ 𝑧 = 𝐴 ∧ ∀𝑦 ∈ 𝑧 𝜑) ↔ ∪ {𝑦 ∈ 𝐵 ∣ 𝜑} = 𝐴))
29	28	rspcev 3309	. . 3 ⊢ (({𝑦 ∈ 𝐵 ∣ 𝜑} ∈ 𝒫 𝐵 ∧ ∪ {𝑦 ∈ 𝐵 ∣ 𝜑} = 𝐴) → ∃𝑧 ∈ 𝒫 𝐵(∪ 𝑧 = 𝐴 ∧ ∀𝑦 ∈ 𝑧 𝜑))
30	4, 16, 29	sylancr 695	. 2 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑) → ∃𝑧 ∈ 𝒫 𝐵(∪ 𝑧 = 𝐴 ∧ ∀𝑦 ∈ 𝑧 𝜑))
31		elpwi 4168	. . . . . . . . 9 ⊢ (𝑧 ∈ 𝒫 𝐵 → 𝑧 ⊆ 𝐵)
32		r19.29r 3073	. . . . . . . . . . 11 ⊢ ((∃𝑦 ∈ 𝑧 𝑥 ∈ 𝑦 ∧ ∀𝑦 ∈ 𝑧 𝜑) → ∃𝑦 ∈ 𝑧 (𝑥 ∈ 𝑦 ∧ 𝜑))
33	32	expcom 451	. . . . . . . . . 10 ⊢ (∀𝑦 ∈ 𝑧 𝜑 → (∃𝑦 ∈ 𝑧 𝑥 ∈ 𝑦 → ∃𝑦 ∈ 𝑧 (𝑥 ∈ 𝑦 ∧ 𝜑)))
34		ssrexv 3667	. . . . . . . . . 10 ⊢ (𝑧 ⊆ 𝐵 → (∃𝑦 ∈ 𝑧 (𝑥 ∈ 𝑦 ∧ 𝜑) → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑)))
35	33, 34	sylan9r 690	. . . . . . . . 9 ⊢ ((𝑧 ⊆ 𝐵 ∧ ∀𝑦 ∈ 𝑧 𝜑) → (∃𝑦 ∈ 𝑧 𝑥 ∈ 𝑦 → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑)))
36	31, 35	sylan 488	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝒫 𝐵 ∧ ∀𝑦 ∈ 𝑧 𝜑) → (∃𝑦 ∈ 𝑧 𝑥 ∈ 𝑦 → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑)))
37		eleq2 2690	. . . . . . . . . 10 ⊢ (∪ 𝑧 = 𝐴 → (𝑥 ∈ ∪ 𝑧 ↔ 𝑥 ∈ 𝐴))
38	37	biimpar 502	. . . . . . . . 9 ⊢ ((∪ 𝑧 = 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ∪ 𝑧)
39		eluni2 4440	. . . . . . . . 9 ⊢ (𝑥 ∈ ∪ 𝑧 ↔ ∃𝑦 ∈ 𝑧 𝑥 ∈ 𝑦)
40	38, 39	sylib 208	. . . . . . . 8 ⊢ ((∪ 𝑧 = 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ 𝑧 𝑥 ∈ 𝑦)
41	36, 40	impel 485	. . . . . . 7 ⊢ (((𝑧 ∈ 𝒫 𝐵 ∧ ∀𝑦 ∈ 𝑧 𝜑) ∧ (∪ 𝑧 = 𝐴 ∧ 𝑥 ∈ 𝐴)) → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑))
42	41	anassrs 680	. . . . . 6 ⊢ ((((𝑧 ∈ 𝒫 𝐵 ∧ ∀𝑦 ∈ 𝑧 𝜑) ∧ ∪ 𝑧 = 𝐴) ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑))
43	42	ralrimiva 2966	. . . . 5 ⊢ (((𝑧 ∈ 𝒫 𝐵 ∧ ∀𝑦 ∈ 𝑧 𝜑) ∧ ∪ 𝑧 = 𝐴) → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑))
44	43	anasss 679	. . . 4 ⊢ ((𝑧 ∈ 𝒫 𝐵 ∧ (∀𝑦 ∈ 𝑧 𝜑 ∧ ∪ 𝑧 = 𝐴)) → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑))
45	44	ancom2s 844	. . 3 ⊢ ((𝑧 ∈ 𝒫 𝐵 ∧ (∪ 𝑧 = 𝐴 ∧ ∀𝑦 ∈ 𝑧 𝜑)) → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑))
46	45	rexlimiva 3028	. 2 ⊢ (∃𝑧 ∈ 𝒫 𝐵(∪ 𝑧 = 𝐴 ∧ ∀𝑦 ∈ 𝑧 𝜑) → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑))
47	30, 46	impbii 199	1 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑) ↔ ∃𝑧 ∈ 𝒫 𝐵(∪ 𝑧 = 𝐴 ∧ ∀𝑦 ∈ 𝑧 𝜑))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384  ∀wal 1481   = wceq 1483   ∈ wcel 1990  ∀wral 2912  ∃wrex 2913  {crab 2916  Vcvv 3200   ⊆ wss 3574  𝒫 cpw 4158  ∪ cuni 4436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-in 3581  df-ss 3588  df-pw 4160  df-uni 4437

This theorem is referenced by:  cover2g  33509