Metamath Proof Explorer


Theorem rankc1

Description: A relationship that can be used for computation of rank. (Contributed by NM, 16-Sep-2006)

Ref Expression
Hypothesis rankr1b.1 AV
Assertion rankc1 xArankxrankArankA=rankA

Proof

Step Hyp Ref Expression
1 rankr1b.1 AV
2 1 rankuniss rankArankA
3 2 biantru rankArankArankArankArankArankA
4 iunss xAsucrankxrankAxAsucrankxrankA
5 1 rankval4 rankA=xAsucrankx
6 5 sseq1i rankArankAxAsucrankxrankA
7 rankon rankxOn
8 rankon rankAOn
9 7 8 onsucssi rankxrankAsucrankxrankA
10 9 ralbii xArankxrankAxAsucrankxrankA
11 4 6 10 3bitr4ri xArankxrankArankArankA
12 eqss rankA=rankArankArankArankArankA
13 3 11 12 3bitr4i xArankxrankArankA=rankA