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	⊢ 𝐴 ∈ V
Assertion	rankbnd	⊢ ( ∀ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ⊆ 𝐵 ↔ ( rank ‘ 𝐴 ) ⊆ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		rankr1b.1	⊢ 𝐴 ∈ V
2	1	rankval4	⊢ ( rank ‘ 𝐴 ) = ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 )
3	2	sseq1i	⊢ ( ( rank ‘ 𝐴 ) ⊆ 𝐵 ↔ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ⊆ 𝐵 )
4		iunss	⊢ ( ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ⊆ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ⊆ 𝐵 )
5	3 4	bitr2i	⊢ ( ∀ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ⊆ 𝐵 ↔ ( rank ‘ 𝐴 ) ⊆ 𝐵 )