Description: Obsolete proof of pwundif as of 26-Dec-2023. (Contributed by NM, 25-Mar-2007) (Proof shortened by Thierry Arnoux, 20-Dec-2016) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | pwundifOLD | ⊢ 𝒫 ( 𝐴 ∪ 𝐵 ) = ( ( 𝒫 ( 𝐴 ∪ 𝐵 ) ∖ 𝒫 𝐴 ) ∪ 𝒫 𝐴 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | undif1 | ⊢ ( ( 𝒫 ( 𝐴 ∪ 𝐵 ) ∖ 𝒫 𝐴 ) ∪ 𝒫 𝐴 ) = ( 𝒫 ( 𝐴 ∪ 𝐵 ) ∪ 𝒫 𝐴 ) | |
| 2 | pwunss | ⊢ ( 𝒫 𝐴 ∪ 𝒫 𝐵 ) ⊆ 𝒫 ( 𝐴 ∪ 𝐵 ) | |
| 3 | unss | ⊢ ( ( 𝒫 𝐴 ⊆ 𝒫 ( 𝐴 ∪ 𝐵 ) ∧ 𝒫 𝐵 ⊆ 𝒫 ( 𝐴 ∪ 𝐵 ) ) ↔ ( 𝒫 𝐴 ∪ 𝒫 𝐵 ) ⊆ 𝒫 ( 𝐴 ∪ 𝐵 ) ) | |
| 4 | 2 3 | mpbir | ⊢ ( 𝒫 𝐴 ⊆ 𝒫 ( 𝐴 ∪ 𝐵 ) ∧ 𝒫 𝐵 ⊆ 𝒫 ( 𝐴 ∪ 𝐵 ) ) |
| 5 | 4 | simpli | ⊢ 𝒫 𝐴 ⊆ 𝒫 ( 𝐴 ∪ 𝐵 ) |
| 6 | ssequn2 | ⊢ ( 𝒫 𝐴 ⊆ 𝒫 ( 𝐴 ∪ 𝐵 ) ↔ ( 𝒫 ( 𝐴 ∪ 𝐵 ) ∪ 𝒫 𝐴 ) = 𝒫 ( 𝐴 ∪ 𝐵 ) ) | |
| 7 | 5 6 | mpbi | ⊢ ( 𝒫 ( 𝐴 ∪ 𝐵 ) ∪ 𝒫 𝐴 ) = 𝒫 ( 𝐴 ∪ 𝐵 ) |
| 8 | 1 7 | eqtr2i | ⊢ 𝒫 ( 𝐴 ∪ 𝐵 ) = ( ( 𝒫 ( 𝐴 ∪ 𝐵 ) ∖ 𝒫 𝐴 ) ∪ 𝒫 𝐴 ) |