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 ⊢ A ∈ V
Assertion rankbnd2 ⊢ B ∈ On → ∀ x ∈ A rank ⁡ x ⊆ B ↔ rank ⁡ A ⊆ suc ⁡ B

Proof

Step Hyp Ref Expression
1 rankr1b.1 ⊢ A ∈ V
2 rankuni ⊢ rank ⁡ ⋃ A = ⋃ rank ⁡ A
3 1 rankuni2 ⊢ rank ⁡ ⋃ A = ⋃ x ∈ A rank ⁡ x
4 2 3 eqtr3i ⊢ ⋃ rank ⁡ A = ⋃ x ∈ A rank ⁡ x
5 4 sseq1i ⊢ ⋃ rank ⁡ A ⊆ B ↔ ⋃ x ∈ A rank ⁡ x ⊆ B
6 iunss ⊢ ⋃ x ∈ A rank ⁡ x ⊆ B ↔ ∀ x ∈ A rank ⁡ x ⊆ B
7 5 6 bitr2i ⊢ ∀ x ∈ A rank ⁡ x ⊆ B ↔ ⋃ rank ⁡ A ⊆ B
8 rankon ⊢ rank ⁡ A ∈ On
9 8 onssi ⊢ rank ⁡ A ⊆ On
10 eloni ⊢ B ∈ On → Ord ⁡ B
11 ordunisssuc ⊢ rank ⁡ A ⊆ On ∧ Ord ⁡ B → ⋃ rank ⁡ A ⊆ B ↔ rank ⁡ A ⊆ suc ⁡ B
12 9 10 11 sylancr ⊢ B ∈ On → ⋃ rank ⁡ A ⊆ B ↔ rank ⁡ A ⊆ suc ⁡ B
13 7 12 bitrid ⊢ B ∈ On → ∀ x ∈ A rank ⁡ x ⊆ B ↔ rank ⁡ A ⊆ suc ⁡ B