Metamath Proof Explorer

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 ⊢ A = ⋃ B
Assertion cover2g ⊢ B ∈ C → ∀ x ∈ A ∃ y ∈ B x ∈ y ∧ φ ↔ ∃ z ∈ 𝒫 B ⋃ z = A ∧ ∀ y ∈ z φ

Proof

Step Hyp Ref Expression
1 cover2g.1 ⊢ A = ⋃ B
2 unieq ⊢ b = B → ⋃ b = ⋃ B
3 2 1 eqtr4di ⊢ b = B → ⋃ b = A
4 rexeq ⊢ b = B → ∃ y ∈ b x ∈ y ∧ φ ↔ ∃ y ∈ B x ∈ y ∧ φ
5 3 4 raleqbidv ⊢ b = B → ∀ x ∈ ⋃ b ∃ y ∈ b x ∈ y ∧ φ ↔ ∀ x ∈ A ∃ y ∈ B x ∈ y ∧ φ
6 pweq ⊢ b = B → 𝒫 b = 𝒫 B
7 3 eqeq2d ⊢ b = B → ⋃ z = ⋃ b ↔ ⋃ z = A
8 7 anbi1d ⊢ b = B → ⋃ z = ⋃ b ∧ ∀ y ∈ z φ ↔ ⋃ z = A ∧ ∀ y ∈ z φ
9 6 8 rexeqbidv ⊢ b = B → ∃ z ∈ 𝒫 b ⋃ z = ⋃ b ∧ ∀ y ∈ z φ ↔ ∃ z ∈ 𝒫 B ⋃ z = A ∧ ∀ y ∈ z φ
10 vex ⊢ b ∈ V
11 eqid ⊢ ⋃ b = ⋃ b
12 10 11 cover2 ⊢ ∀ x ∈ ⋃ b ∃ y ∈ b x ∈ y ∧ φ ↔ ∃ z ∈ 𝒫 b ⋃ z = ⋃ b ∧ ∀ y ∈ z φ
13 5 9 12 vtoclbg ⊢ B ∈ C → ∀ x ∈ A ∃ y ∈ B x ∈ y ∧ φ ↔ ∃ z ∈ 𝒫 B ⋃ z = A ∧ ∀ y ∈ z φ