Theorem cover2g

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, 21-Jun-2010)

	Ref	Expression
Hypothesis	cover2g.1	⊢ 𝐴 = ∪ 𝐵
Assertion	cover2g	⊢ ( 𝐵 ∈ 𝐶 → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ↔ ∃ 𝑧 ∈ 𝒫 𝐵 ( ∪ 𝑧 = 𝐴 ∧ ∀ 𝑦 ∈ 𝑧 𝜑 ) ) )

Proof

Step	Hyp	Ref	Expression
1		cover2g.1	⊢ 𝐴 = ∪ 𝐵
2		unieq	⊢ ( 𝑏 = 𝐵 → ∪ 𝑏 = ∪ 𝐵 )
3	2 1	eqtr4di	⊢ ( 𝑏 = 𝐵 → ∪ 𝑏 = 𝐴 )
4		rexeq	⊢ ( 𝑏 = 𝐵 → ( ∃ 𝑦 ∈ 𝑏 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ↔ ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ) )
5	3 4	raleqbidv	⊢ ( 𝑏 = 𝐵 → ( ∀ 𝑥 ∈ ∪ 𝑏 ∃ 𝑦 ∈ 𝑏 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ) )
6		pweq	⊢ ( 𝑏 = 𝐵 → 𝒫 𝑏 = 𝒫 𝐵 )
7	3	eqeq2d	⊢ ( 𝑏 = 𝐵 → ( ∪ 𝑧 = ∪ 𝑏 ↔ ∪ 𝑧 = 𝐴 ) )
8	7	anbi1d	⊢ ( 𝑏 = 𝐵 → ( ( ∪ 𝑧 = ∪ 𝑏 ∧ ∀ 𝑦 ∈ 𝑧 𝜑 ) ↔ ( ∪ 𝑧 = 𝐴 ∧ ∀ 𝑦 ∈ 𝑧 𝜑 ) ) )
9	6 8	rexeqbidv	⊢ ( 𝑏 = 𝐵 → ( ∃ 𝑧 ∈ 𝒫 𝑏 ( ∪ 𝑧 = ∪ 𝑏 ∧ ∀ 𝑦 ∈ 𝑧 𝜑 ) ↔ ∃ 𝑧 ∈ 𝒫 𝐵 ( ∪ 𝑧 = 𝐴 ∧ ∀ 𝑦 ∈ 𝑧 𝜑 ) ) )
10		vex	⊢ 𝑏 ∈ V
11		eqid	⊢ ∪ 𝑏 = ∪ 𝑏
12	10 11	cover2	⊢ ( ∀ 𝑥 ∈ ∪ 𝑏 ∃ 𝑦 ∈ 𝑏 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ↔ ∃ 𝑧 ∈ 𝒫 𝑏 ( ∪ 𝑧 = ∪ 𝑏 ∧ ∀ 𝑦 ∈ 𝑧 𝜑 ) )
13	5 9 12	vtoclbg	⊢ ( 𝐵 ∈ 𝐶 → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ↔ ∃ 𝑧 ∈ 𝒫 𝐵 ( ∪ 𝑧 = 𝐴 ∧ ∀ 𝑦 ∈ 𝑧 𝜑 ) ) )