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 AV
Assertion rankuniss rankArankA

Proof

Step Hyp Ref Expression
1 rankr1b.1 AV
2 rankuni rankA=rankA
3 rankon rankAOn
4 3 onordi OrdrankA
5 orduniss OrdrankArankArankA
6 4 5 ax-mp rankArankA
7 2 6 eqsstri rankArankA