Theorem pwunss

Description: The power class of the union of two classes includes the union of their power classes. Exercise 4.12(k) of Mendelson p. 235. (Contributed by NM, 23-Nov-2003) Remove use of ax-sep , ax-nul , ax-pr and shorten proof. (Revised by BJ, 13-Apr-2024)

	Ref	Expression
Assertion	pwunss	|- ( ~P A u. ~P B ) C_ ~P ( A u. B )

Proof

Step	Hyp	Ref	Expression
1		ssun1	|- A C_ ( A u. B )
2	1	sspwi	|- ~P A C_ ~P ( A u. B )
3		ssun2	|- B C_ ( A u. B )
4	3	sspwi	|- ~P B C_ ~P ( A u. B )
5	2 4	unssi	|- ( ~P A u. ~P B ) C_ ~P ( A u. B )