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\in \mathrm{V}$$
Assertion	rankuniss	$$⊢\mathrm{rank}\left(\bigcup A\right)\subseteq \mathrm{rank}\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		rankr1b.1	$$⊢A\in \mathrm{V}$$
2		rankuni	$$⊢\mathrm{rank}\left(\bigcup A\right)=\bigcup \mathrm{rank}\left(A\right)$$
3		rankon	$$⊢\mathrm{rank}\left(A\right)\in \mathrm{On}$$
4	3	onordi	$$⊢\mathrm{Ord}\mathrm{rank}\left(A\right)$$
5		orduniss	$$⊢\mathrm{Ord}\mathrm{rank}\left(A\right)\to \bigcup \mathrm{rank}\left(A\right)\subseteq \mathrm{rank}\left(A\right)$$
6	4 5	ax-mp	$$⊢\bigcup \mathrm{rank}\left(A\right)\subseteq \mathrm{rank}\left(A\right)$$
7	2 6	eqsstri	$$⊢\mathrm{rank}\left(\bigcup A\right)\subseteq \mathrm{rank}\left(A\right)$$