Metamath Proof Explorer


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 ( 𝐴𝑉 → ( 𝐴 ∈ 𝒫 𝒫 𝐵 𝐴 ∈ 𝒫 𝐵 ) )