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	⊢ 𝐵 ∈ V
	cover2.2	⊢ 𝐴 = ∪ 𝐵
Assertion	cover2	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ↔ ∃ 𝑧 ∈ 𝒫 𝐵 ( ∪ 𝑧 = 𝐴 ∧ ∀ 𝑦 ∈ 𝑧 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		cover2.1	⊢ 𝐵 ∈ V
2		cover2.2	⊢ 𝐴 = ∪ 𝐵
3		ssrab2	⊢ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ⊆ 𝐵
4	1 3	elpwi2	⊢ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∈ 𝒫 𝐵
5		nfra1	⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝜑 )
6	3	unissi	⊢ ∪ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ⊆ ∪ 𝐵
7	6	sseli	⊢ ( 𝑥 ∈ ∪ { 𝑦 ∈ 𝐵 ∣ 𝜑 } → 𝑥 ∈ ∪ 𝐵 )
8	7 2	eleqtrrdi	⊢ ( 𝑥 ∈ ∪ { 𝑦 ∈ 𝐵 ∣ 𝜑 } → 𝑥 ∈ 𝐴 )
9		rsp	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) → ( 𝑥 ∈ 𝐴 → ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ) )
10		elunirab	⊢ ( 𝑥 ∈ ∪ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ↔ ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) )
11	9 10	imbitrrdi	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ∪ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) )
12	8 11	impbid2	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) → ( 𝑥 ∈ ∪ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ↔ 𝑥 ∈ 𝐴 ) )
13	5 12	alrimi	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) → ∀ 𝑥 ( 𝑥 ∈ ∪ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ↔ 𝑥 ∈ 𝐴 ) )
14		dfcleq	⊢ ( ∪ { 𝑦 ∈ 𝐵 ∣ 𝜑 } = 𝐴 ↔ ∀ 𝑥 ( 𝑥 ∈ ∪ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ↔ 𝑥 ∈ 𝐴 ) )
15	13 14	sylibr	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) → ∪ { 𝑦 ∈ 𝐵 ∣ 𝜑 } = 𝐴 )
16		nfrab1	⊢ Ⅎ 𝑦 { 𝑦 ∈ 𝐵 ∣ 𝜑 }
17	16	nfeq2	⊢ Ⅎ 𝑦 𝑧 = { 𝑦 ∈ 𝐵 ∣ 𝜑 }
18		eleq2	⊢ ( 𝑧 = { 𝑦 ∈ 𝐵 ∣ 𝜑 } → ( 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) )
19		rabid	⊢ ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ↔ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) )
20	19	simprbi	⊢ ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } → 𝜑 )
21	18 20	biimtrdi	⊢ ( 𝑧 = { 𝑦 ∈ 𝐵 ∣ 𝜑 } → ( 𝑦 ∈ 𝑧 → 𝜑 ) )
22	17 21	ralrimi	⊢ ( 𝑧 = { 𝑦 ∈ 𝐵 ∣ 𝜑 } → ∀ 𝑦 ∈ 𝑧 𝜑 )
23		unieq	⊢ ( 𝑧 = { 𝑦 ∈ 𝐵 ∣ 𝜑 } → ∪ 𝑧 = ∪ { 𝑦 ∈ 𝐵 ∣ 𝜑 } )
24	23	eqeq1d	⊢ ( 𝑧 = { 𝑦 ∈ 𝐵 ∣ 𝜑 } → ( ∪ 𝑧 = 𝐴 ↔ ∪ { 𝑦 ∈ 𝐵 ∣ 𝜑 } = 𝐴 ) )
25	24	anbi1d	⊢ ( 𝑧 = { 𝑦 ∈ 𝐵 ∣ 𝜑 } → ( ( ∪ 𝑧 = 𝐴 ∧ ∀ 𝑦 ∈ 𝑧 𝜑 ) ↔ ( ∪ { 𝑦 ∈ 𝐵 ∣ 𝜑 } = 𝐴 ∧ ∀ 𝑦 ∈ 𝑧 𝜑 ) ) )
26	22 25	mpbiran2d	⊢ ( 𝑧 = { 𝑦 ∈ 𝐵 ∣ 𝜑 } → ( ( ∪ 𝑧 = 𝐴 ∧ ∀ 𝑦 ∈ 𝑧 𝜑 ) ↔ ∪ { 𝑦 ∈ 𝐵 ∣ 𝜑 } = 𝐴 ) )
27	26	rspcev	⊢ ( ( { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∈ 𝒫 𝐵 ∧ ∪ { 𝑦 ∈ 𝐵 ∣ 𝜑 } = 𝐴 ) → ∃ 𝑧 ∈ 𝒫 𝐵 ( ∪ 𝑧 = 𝐴 ∧ ∀ 𝑦 ∈ 𝑧 𝜑 ) )
28	4 15 27	sylancr	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) → ∃ 𝑧 ∈ 𝒫 𝐵 ( ∪ 𝑧 = 𝐴 ∧ ∀ 𝑦 ∈ 𝑧 𝜑 ) )
29		elpwi	⊢ ( 𝑧 ∈ 𝒫 𝐵 → 𝑧 ⊆ 𝐵 )
30		r19.29r	⊢ ( ( ∃ 𝑦 ∈ 𝑧 𝑥 ∈ 𝑦 ∧ ∀ 𝑦 ∈ 𝑧 𝜑 ) → ∃ 𝑦 ∈ 𝑧 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) )
31	30	expcom	⊢ ( ∀ 𝑦 ∈ 𝑧 𝜑 → ( ∃ 𝑦 ∈ 𝑧 𝑥 ∈ 𝑦 → ∃ 𝑦 ∈ 𝑧 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ) )
32		ssrexv	⊢ ( 𝑧 ⊆ 𝐵 → ( ∃ 𝑦 ∈ 𝑧 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) → ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ) )
33	31 32	sylan9r	⊢ ( ( 𝑧 ⊆ 𝐵 ∧ ∀ 𝑦 ∈ 𝑧 𝜑 ) → ( ∃ 𝑦 ∈ 𝑧 𝑥 ∈ 𝑦 → ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ) )
34	29 33	sylan	⊢ ( ( 𝑧 ∈ 𝒫 𝐵 ∧ ∀ 𝑦 ∈ 𝑧 𝜑 ) → ( ∃ 𝑦 ∈ 𝑧 𝑥 ∈ 𝑦 → ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ) )
35		eleq2	⊢ ( ∪ 𝑧 = 𝐴 → ( 𝑥 ∈ ∪ 𝑧 ↔ 𝑥 ∈ 𝐴 ) )
36	35	biimpar	⊢ ( ( ∪ 𝑧 = 𝐴 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ∪ 𝑧 )
37		eluni2	⊢ ( 𝑥 ∈ ∪ 𝑧 ↔ ∃ 𝑦 ∈ 𝑧 𝑥 ∈ 𝑦 )
38	36 37	sylib	⊢ ( ( ∪ 𝑧 = 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ∈ 𝑧 𝑥 ∈ 𝑦 )
39	34 38	impel	⊢ ( ( ( 𝑧 ∈ 𝒫 𝐵 ∧ ∀ 𝑦 ∈ 𝑧 𝜑 ) ∧ ( ∪ 𝑧 = 𝐴 ∧ 𝑥 ∈ 𝐴 ) ) → ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) )
40	39	anassrs	⊢ ( ( ( ( 𝑧 ∈ 𝒫 𝐵 ∧ ∀ 𝑦 ∈ 𝑧 𝜑 ) ∧ ∪ 𝑧 = 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) )
41	40	ralrimiva	⊢ ( ( ( 𝑧 ∈ 𝒫 𝐵 ∧ ∀ 𝑦 ∈ 𝑧 𝜑 ) ∧ ∪ 𝑧 = 𝐴 ) → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) )
42	41	anasss	⊢ ( ( 𝑧 ∈ 𝒫 𝐵 ∧ ( ∀ 𝑦 ∈ 𝑧 𝜑 ∧ ∪ 𝑧 = 𝐴 ) ) → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) )
43	42	ancom2s	⊢ ( ( 𝑧 ∈ 𝒫 𝐵 ∧ ( ∪ 𝑧 = 𝐴 ∧ ∀ 𝑦 ∈ 𝑧 𝜑 ) ) → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) )
44	43	rexlimiva	⊢ ( ∃ 𝑧 ∈ 𝒫 𝐵 ( ∪ 𝑧 = 𝐴 ∧ ∀ 𝑦 ∈ 𝑧 𝜑 ) → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) )
45	28 44	impbii	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ↔ ∃ 𝑧 ∈ 𝒫 𝐵 ( ∪ 𝑧 = 𝐴 ∧ ∀ 𝑦 ∈ 𝑧 𝜑 ) )