Metamath Proof Explorer


Theorem rankuniss

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 )

Proof

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 )