This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐵 ) )