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 
|- U_ x e. A ~P x C_ ~P U. A

Proof

Step Hyp Ref Expression
1 ssiun 
 |-  ( E. x e. A y C_ x -> y C_ U_ x e. A x )
2 eliun 
 |-  ( y e. U_ x e. A ~P x <-> E. x e. A y e. ~P x )
3 velpw 
 |-  ( y e. ~P x <-> y C_ x )
4 3 rexbii 
 |-  ( E. x e. A y e. ~P x <-> E. x e. A y C_ x )
5 2 4 bitri 
 |-  ( y e. U_ x e. A ~P x <-> E. x e. A y C_ x )
6 velpw 
 |-  ( y e. ~P U. A <-> y C_ U. A )
7 uniiun 
 |-  U. A = U_ x e. A x
8 7 sseq2i 
 |-  ( y C_ U. A <-> y C_ U_ x e. A x )
9 6 8 bitri 
 |-  ( y e. ~P U. A <-> y C_ U_ x e. A x )
10 1 5 9 3imtr4i 
 |-  ( y e. U_ x e. A ~P x -> y e. ~P U. A )
11 10 ssriv 
 |-  U_ x e. A ~P x C_ ~P U. A