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

Metamath Proof Explorer

Theorem rankuniss

Description: Upper bound of the rank of a union. Part of Exercise 30 of Enderton p. 207. (Contributed by NM, 30-Nov-2003)

Ref Expression
Hypothesis rankr1b.1 ⊢ A ∈ V
Assertion rankuniss ⊢ rank ⁡ ⋃ A ⊆ rank ⁡ A

Proof

Step Hyp Ref Expression
1 rankr1b.1 ⊢ A ∈ V
2 rankuni ⊢ rank ⁡ ⋃ A = ⋃ rank ⁡ A
3 rankon ⊢ rank ⁡ A ∈ On
4 3 onordi ⊢ Ord ⁡ rank ⁡ A
5 orduniss ⊢ Ord ⁡ rank ⁡ A → ⋃ rank ⁡ A ⊆ rank ⁡ A
6 4 5 ax-mp ⊢ ⋃ rank ⁡ A ⊆ rank ⁡ A
7 2 6 eqsstri ⊢ rank ⁡ ⋃ A ⊆ rank ⁡ A