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

Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 rankr1b.1 ⊢ A ∈ V
2 1 rankval4 ⊢ rank ⁡ A = ⋃ x ∈ A suc ⁡ rank ⁡ x
3 2 sseq1i ⊢ rank ⁡ A ⊆ B ↔ ⋃ x ∈ A suc ⁡ rank ⁡ x ⊆ B
4 iunss ⊢ ⋃ x ∈ A suc ⁡ rank ⁡ x ⊆ B ↔ ∀ x ∈ A suc ⁡ rank ⁡ x ⊆ B
5 3 4 bitr2i ⊢ ∀ x ∈ A suc ⁡ rank ⁡ x ⊆ B ↔ rank ⁡ A ⊆ B