Theorem rankbnd2

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

	Ref	Expression
Hypothesis	rankr1b.1	⊢ 𝐴 ∈ V
Assertion	rankbnd2	⊢ ( 𝐵 ∈ On → ( ∀ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ 𝐵 ↔ ( rank ‘ 𝐴 ) ⊆ suc 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		rankr1b.1	⊢ 𝐴 ∈ V
2		rankuni	⊢ ( rank ‘ ∪ 𝐴 ) = ∪ ( rank ‘ 𝐴 )
3	1	rankuni2	⊢ ( rank ‘ ∪ 𝐴 ) = ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 )
4	2 3	eqtr3i	⊢ ∪ ( rank ‘ 𝐴 ) = ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 )
5	4	sseq1i	⊢ ( ∪ ( rank ‘ 𝐴 ) ⊆ 𝐵 ↔ ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ 𝐵 )
6		iunss	⊢ ( ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ 𝐵 )
7	5 6	bitr2i	⊢ ( ∀ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ 𝐵 ↔ ∪ ( rank ‘ 𝐴 ) ⊆ 𝐵 )
8		rankon	⊢ ( rank ‘ 𝐴 ) ∈ On
9	8	onssi	⊢ ( rank ‘ 𝐴 ) ⊆ On
10		eloni	⊢ ( 𝐵 ∈ On → Ord 𝐵 )
11		ordunisssuc	⊢ ( ( ( rank ‘ 𝐴 ) ⊆ On ∧ Ord 𝐵 ) → ( ∪ ( rank ‘ 𝐴 ) ⊆ 𝐵 ↔ ( rank ‘ 𝐴 ) ⊆ suc 𝐵 ) )
12	9 10 11	sylancr	⊢ ( 𝐵 ∈ On → ( ∪ ( rank ‘ 𝐴 ) ⊆ 𝐵 ↔ ( rank ‘ 𝐴 ) ⊆ suc 𝐵 ) )
13	7 12	bitrid	⊢ ( 𝐵 ∈ On → ( ∀ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ 𝐵 ↔ ( rank ‘ 𝐴 ) ⊆ suc 𝐵 ) )