Metamath Proof Explorer

Theorem pwelg

Description: The powerclass is an element of a class closed under union and powerclass operations iff the element is a member of that class. (Contributed by RP, 21-Mar-2020)

Ref Expression
Assertion pwelg ⊢ ∀ x ∈ B ⋃ x ∈ B ∧ 𝒫 x ∈ B → A ∈ B ↔ 𝒫 A ∈ B

Proof

Step Hyp Ref Expression
1 simpr ⊢ ⋃ x ∈ B ∧ 𝒫 x ∈ B → 𝒫 x ∈ B
2 1 ralimi ⊢ ∀ x ∈ B ⋃ x ∈ B ∧ 𝒫 x ∈ B → ∀ x ∈ B 𝒫 x ∈ B
3 pweq ⊢ x = A → 𝒫 x = 𝒫 A
4 3 eleq1d ⊢ x = A → 𝒫 x ∈ B ↔ 𝒫 A ∈ B
5 4 rspccv ⊢ ∀ x ∈ B 𝒫 x ∈ B → A ∈ B → 𝒫 A ∈ B
6 2 5 syl ⊢ ∀ x ∈ B ⋃ x ∈ B ∧ 𝒫 x ∈ B → A ∈ B → 𝒫 A ∈ B
7 simpl ⊢ ⋃ x ∈ B ∧ 𝒫 x ∈ B → ⋃ x ∈ B
8 7 ralimi ⊢ ∀ x ∈ B ⋃ x ∈ B ∧ 𝒫 x ∈ B → ∀ x ∈ B ⋃ x ∈ B
9 unieq ⊢ x = 𝒫 A → ⋃ x = ⋃ 𝒫 A
10 unipw ⊢ ⋃ 𝒫 A = A
11 9 10 eqtrdi ⊢ x = 𝒫 A → ⋃ x = A
12 11 eleq1d ⊢ x = 𝒫 A → ⋃ x ∈ B ↔ A ∈ B
13 12 rspccv ⊢ ∀ x ∈ B ⋃ x ∈ B → 𝒫 A ∈ B → A ∈ B
14 8 13 syl ⊢ ∀ x ∈ B ⋃ x ∈ B ∧ 𝒫 x ∈ B → 𝒫 A ∈ B → A ∈ B
15 6 14 impbid ⊢ ∀ x ∈ B ⋃ x ∈ B ∧ 𝒫 x ∈ B → A ∈ B ↔ 𝒫 A ∈ B