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 e. _V
Assertion	rankbnd	|- ( A. x e. A suc ( rank ` x ) C_ B <-> ( rank ` A ) C_ B )

Proof

Step	Hyp	Ref	Expression
1		rankr1b.1	|- A e. _V
2	1	rankval4	|- ( rank ` A ) = U_ x e. A suc ( rank ` x )
3	2	sseq1i	|- ( ( rank ` A ) C_ B <-> U_ x e. A suc ( rank ` x ) C_ B )
4		iunss	|- ( U_ x e. A suc ( rank ` x ) C_ B <-> A. x e. A suc ( rank ` x ) C_ B )
5	3 4	bitr2i	|- ( A. x e. A suc ( rank ` x ) C_ B <-> ( rank ` A ) C_ B )