Theorem pwpwuni

Description: Relationship between power class and union. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Assertion	pwpwuni	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ 𝒫 𝒫 𝐵 ↔ ∪ 𝐴 ∈ 𝒫 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		elpwg	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ 𝒫 𝒫 𝐵 ↔ 𝐴 ⊆ 𝒫 𝐵 ) )
2		sspwuni	⊢ ( 𝐴 ⊆ 𝒫 𝐵 ↔ ∪ 𝐴 ⊆ 𝐵 )
3	2	a1i	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ⊆ 𝒫 𝐵 ↔ ∪ 𝐴 ⊆ 𝐵 ) )
4		uniexg	⊢ ( 𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V )
5		elpwg	⊢ ( ∪ 𝐴 ∈ V → ( ∪ 𝐴 ∈ 𝒫 𝐵 ↔ ∪ 𝐴 ⊆ 𝐵 ) )
6	4 5	syl	⊢ ( 𝐴 ∈ 𝑉 → ( ∪ 𝐴 ∈ 𝒫 𝐵 ↔ ∪ 𝐴 ⊆ 𝐵 ) )
7	6	bicomd	⊢ ( 𝐴 ∈ 𝑉 → ( ∪ 𝐴 ⊆ 𝐵 ↔ ∪ 𝐴 ∈ 𝒫 𝐵 ) )
8	1 3 7	3bitrd	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ 𝒫 𝒫 𝐵 ↔ ∪ 𝐴 ∈ 𝒫 𝐵 ) )