Description: Upper bound of the rank of a union. Part of Exercise 30 of Enderton p. 207. (Contributed by NM, 30-Nov-2003)
Ref | Expression | ||
---|---|---|---|
Hypothesis | rankr1b.1 | |- A e. _V |
|
Assertion | rankuniss | |- ( rank ` U. A ) C_ ( rank ` A ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rankr1b.1 | |- A e. _V |
|
2 | rankuni | |- ( rank ` U. A ) = U. ( rank ` A ) |
|
3 | rankon | |- ( rank ` A ) e. On |
|
4 | 3 | onordi | |- Ord ( rank ` A ) |
5 | orduniss | |- ( Ord ( rank ` A ) -> U. ( rank ` A ) C_ ( rank ` A ) ) |
|
6 | 4 5 | ax-mp | |- U. ( rank ` A ) C_ ( rank ` A ) |
7 | 2 6 | eqsstri | |- ( rank ` U. A ) C_ ( rank ` A ) |