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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssiun | |
|
2 | eliun | |
|
3 | velpw | |
|
4 | 3 | rexbii | |
5 | 2 4 | bitri | |
6 | velpw | |
|
7 | uniiun | |
|
8 | 7 | sseq2i | |
9 | 6 8 | bitri | |
10 | 1 5 9 | 3imtr4i | |
11 | 10 | ssriv | |