Theorem pwun

Description: The power class of the union of two classes equals the union of their power classes, iff one class is a subclass of the other. Part of Exercise 7(b) of Enderton p. 28. (Contributed by NM, 23-Nov-2003)

	Ref	Expression
Assertion	pwun	⊢ ( ( 𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴 ) ↔ 𝒫 ( 𝐴 ∪ 𝐵 ) = ( 𝒫 𝐴 ∪ 𝒫 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		pwunss	⊢ ( 𝒫 𝐴 ∪ 𝒫 𝐵 ) ⊆ 𝒫 ( 𝐴 ∪ 𝐵 )
2	1	biantru	⊢ ( 𝒫 ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝒫 𝐴 ∪ 𝒫 𝐵 ) ↔ ( 𝒫 ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝒫 𝐴 ∪ 𝒫 𝐵 ) ∧ ( 𝒫 𝐴 ∪ 𝒫 𝐵 ) ⊆ 𝒫 ( 𝐴 ∪ 𝐵 ) ) )
3		pwssun	⊢ ( ( 𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴 ) ↔ 𝒫 ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝒫 𝐴 ∪ 𝒫 𝐵 ) )
4		eqss	⊢ ( 𝒫 ( 𝐴 ∪ 𝐵 ) = ( 𝒫 𝐴 ∪ 𝒫 𝐵 ) ↔ ( 𝒫 ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝒫 𝐴 ∪ 𝒫 𝐵 ) ∧ ( 𝒫 𝐴 ∪ 𝒫 𝐵 ) ⊆ 𝒫 ( 𝐴 ∪ 𝐵 ) ) )
5	2 3 4	3bitr4i	⊢ ( ( 𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴 ) ↔ 𝒫 ( 𝐴 ∪ 𝐵 ) = ( 𝒫 𝐴 ∪ 𝒫 𝐵 ) )