Metamath Proof Explorer


Theorem rankop

Description: The rank of an ordered pair. Part of Exercise 4 of Kunen p. 107. (Contributed by NM, 13-Sep-2006) (Revised by Mario Carneiro, 17-Nov-2014)

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

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 rankopb AR1OnBR1OnrankAB=sucsucrankArankB
7 4 5 6 mp2an rankAB=sucsucrankArankB