Metamath Proof Explorer


Theorem iunpwss

Description: Inclusion of an indexed union of a power class in the power class of the union of its index. Part of Exercise 24(b) of Enderton p. 33. (Contributed by NM, 25-Nov-2003)

Ref Expression
Assertion iunpwss xA𝒫x𝒫A

Proof

Step Hyp Ref Expression
1 ssiun xAyxyxAx
2 eliun yxA𝒫xxAy𝒫x
3 velpw y𝒫xyx
4 3 rexbii xAy𝒫xxAyx
5 2 4 bitri yxA𝒫xxAyx
6 velpw y𝒫AyA
7 uniiun A=xAx
8 7 sseq2i yAyxAx
9 6 8 bitri y𝒫AyxAx
10 1 5 9 3imtr4i yxA𝒫xy𝒫A
11 10 ssriv xA𝒫x𝒫A