This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pwundif

Description: Break up the power class of a union into a union of smaller classes. (Contributed by NM, 25-Mar-2007) (Proof shortened by Thierry Arnoux, 20-Dec-2016) Remove use of ax-sep , ax-nul , ax-pr and shorten proof. (Revised by BJ, 14-Apr-2024)

Ref Expression
Assertion pwundif 𝒫 ( 𝐴 ∪ 𝐵 ) = ( ( 𝒫 ( 𝐴 ∪ 𝐵 ) ∖ 𝒫 𝐴 ) ∪ 𝒫 𝐴 )

Proof

Step Hyp Ref Expression
1 ssun1 ⊢ 𝐴 ⊆ ( 𝐴 ∪ 𝐵 )
2 1 sspwi ⊢ 𝒫 𝐴 ⊆ 𝒫 ( 𝐴 ∪ 𝐵 )
3 undif ⊢ ( 𝒫 𝐴 ⊆ 𝒫 ( 𝐴 ∪ 𝐵 ) ↔ ( 𝒫 𝐴 ∪ ( 𝒫 ( 𝐴 ∪ 𝐵 ) ∖ 𝒫 𝐴 ) ) = 𝒫 ( 𝐴 ∪ 𝐵 ) )
4 2 3 mpbi ⊢ ( 𝒫 𝐴 ∪ ( 𝒫 ( 𝐴 ∪ 𝐵 ) ∖ 𝒫 𝐴 ) ) = 𝒫 ( 𝐴 ∪ 𝐵 )
5 uncom ⊢ ( 𝒫 𝐴 ∪ ( 𝒫 ( 𝐴 ∪ 𝐵 ) ∖ 𝒫 𝐴 ) ) = ( ( 𝒫 ( 𝐴 ∪ 𝐵 ) ∖ 𝒫 𝐴 ) ∪ 𝒫 𝐴 )
6 4 5 eqtr3i ⊢ 𝒫 ( 𝐴 ∪ 𝐵 ) = ( ( 𝒫 ( 𝐴 ∪ 𝐵 ) ∖ 𝒫 𝐴 ) ∪ 𝒫 𝐴 )