Theorem rankbnd

Description: The rank of a set is bounded by a bound for the successor of its members. (Contributed by NM, 18-Sep-2006)

	Ref	Expression
Hypothesis	rankr1b.1	$$⊢A\in \mathrm{V}$$
Assertion	rankbnd	$$⊢\forall x\in A\mathrm{suc}\mathrm{rank}\left(x\right)\subseteq B\leftrightarrow \mathrm{rank}\left(A\right)\subseteq B$$

Proof

Step	Hyp	Ref	Expression
1		rankr1b.1	$$⊢A\in \mathrm{V}$$
2	1	rankval4	$$⊢\mathrm{rank}\left(A\right)=\bigcup _{x\in A}\mathrm{suc}\mathrm{rank}\left(x\right)$$
3	2	sseq1i	$$⊢\mathrm{rank}\left(A\right)\subseteq B\leftrightarrow \bigcup _{x\in A}\mathrm{suc}\mathrm{rank}\left(x\right)\subseteq B$$
4		iunss	$$⊢\bigcup _{x\in A}\mathrm{suc}\mathrm{rank}\left(x\right)\subseteq B\leftrightarrow \forall x\in A\mathrm{suc}\mathrm{rank}\left(x\right)\subseteq B$$
5	3 4	bitr2i	$$⊢\forall x\in A\mathrm{suc}\mathrm{rank}\left(x\right)\subseteq B\leftrightarrow \mathrm{rank}\left(A\right)\subseteq B$$