Description: Relationship between power class and union. (Contributed by Glauco Siliprandi, 17-Aug-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | pwpwuni | ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ 𝒫 𝒫 𝐵 ↔ ∪ 𝐴 ∈ 𝒫 𝐵 ) ) |
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 | ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ 𝒫 𝒫 𝐵 ↔ ∪ 𝐴 ∈ 𝒫 𝐵 ) ) |