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 )