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	⊢ ( ∀ 𝑥 ∈ 𝐵 ( ∪ 𝑥 ∈ 𝐵 ∧ 𝒫 𝑥 ∈ 𝐵 ) → ( 𝐴 ∈ 𝐵 ↔ 𝒫 𝐴 ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		simpr	⊢ ( ( ∪ 𝑥 ∈ 𝐵 ∧ 𝒫 𝑥 ∈ 𝐵 ) → 𝒫 𝑥 ∈ 𝐵 )
2	1	ralimi	⊢ ( ∀ 𝑥 ∈ 𝐵 ( ∪ 𝑥 ∈ 𝐵 ∧ 𝒫 𝑥 ∈ 𝐵 ) → ∀ 𝑥 ∈ 𝐵 𝒫 𝑥 ∈ 𝐵 )
3		pweq	⊢ ( 𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴 )
4	3	eleq1d	⊢ ( 𝑥 = 𝐴 → ( 𝒫 𝑥 ∈ 𝐵 ↔ 𝒫 𝐴 ∈ 𝐵 ) )
5	4	rspccv	⊢ ( ∀ 𝑥 ∈ 𝐵 𝒫 𝑥 ∈ 𝐵 → ( 𝐴 ∈ 𝐵 → 𝒫 𝐴 ∈ 𝐵 ) )
6	2 5	syl	⊢ ( ∀ 𝑥 ∈ 𝐵 ( ∪ 𝑥 ∈ 𝐵 ∧ 𝒫 𝑥 ∈ 𝐵 ) → ( 𝐴 ∈ 𝐵 → 𝒫 𝐴 ∈ 𝐵 ) )
7		simpl	⊢ ( ( ∪ 𝑥 ∈ 𝐵 ∧ 𝒫 𝑥 ∈ 𝐵 ) → ∪ 𝑥 ∈ 𝐵 )
8	7	ralimi	⊢ ( ∀ 𝑥 ∈ 𝐵 ( ∪ 𝑥 ∈ 𝐵 ∧ 𝒫 𝑥 ∈ 𝐵 ) → ∀ 𝑥 ∈ 𝐵 ∪ 𝑥 ∈ 𝐵 )
9		unieq	⊢ ( 𝑥 = 𝒫 𝐴 → ∪ 𝑥 = ∪ 𝒫 𝐴 )
10		unipw	⊢ ∪ 𝒫 𝐴 = 𝐴
11	9 10	eqtrdi	⊢ ( 𝑥 = 𝒫 𝐴 → ∪ 𝑥 = 𝐴 )
12	11	eleq1d	⊢ ( 𝑥 = 𝒫 𝐴 → ( ∪ 𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵 ) )
13	12	rspccv	⊢ ( ∀ 𝑥 ∈ 𝐵 ∪ 𝑥 ∈ 𝐵 → ( 𝒫 𝐴 ∈ 𝐵 → 𝐴 ∈ 𝐵 ) )
14	8 13	syl	⊢ ( ∀ 𝑥 ∈ 𝐵 ( ∪ 𝑥 ∈ 𝐵 ∧ 𝒫 𝑥 ∈ 𝐵 ) → ( 𝒫 𝐴 ∈ 𝐵 → 𝐴 ∈ 𝐵 ) )
15	6 14	impbid	⊢ ( ∀ 𝑥 ∈ 𝐵 ( ∪ 𝑥 ∈ 𝐵 ∧ 𝒫 𝑥 ∈ 𝐵 ) → ( 𝐴 ∈ 𝐵 ↔ 𝒫 𝐴 ∈ 𝐵 ) )