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 𝐴 ∈ V
Assertion rankuniss ( rank ‘ 𝐴 ) ⊆ ( rank ‘ 𝐴 )

Proof

Step Hyp Ref Expression
1 rankr1b.1 𝐴 ∈ V
2 rankuni ( rank ‘ 𝐴 ) = ( rank ‘ 𝐴 )
3 rankon ( rank ‘ 𝐴 ) ∈ On
4 3 onordi Ord ( rank ‘ 𝐴 )
5 orduniss ( Ord ( rank ‘ 𝐴 ) → ( rank ‘ 𝐴 ) ⊆ ( rank ‘ 𝐴 ) )
6 4 5 ax-mp ( rank ‘ 𝐴 ) ⊆ ( rank ‘ 𝐴 )
7 2 6 eqsstri ( rank ‘ 𝐴 ) ⊆ ( rank ‘ 𝐴 )