Metamath Proof Explorer


Theorem rankun

Description: The rank of the union of two sets. Theorem 15.17(iii) of Monk1 p. 112. (Contributed by NM, 26-Nov-2003) (Revised by Mario Carneiro, 17-Nov-2014)

Ref Expression
Hypotheses ranksn.1 AV
rankun.2 BV
Assertion rankun rankAB=rankArankB

Proof

Step Hyp Ref Expression
1 ranksn.1 AV
2 rankun.2 BV
3 unir1 R1On=V
4 1 3 eleqtrri AR1On
5 2 3 eleqtrri BR1On
6 rankunb AR1OnBR1OnrankAB=rankArankB
7 4 5 6 mp2an rankAB=rankArankB