Metamath Proof Explorer


Theorem rankdmr1

Description: A rank is a member of the cumulative hierarchy. (Contributed by Mario Carneiro, 17-Nov-2014)

Ref Expression
Assertion rankdmr1 rankAdomR1

Proof

Step Hyp Ref Expression
1 rankidb AR1OnAR1sucrankA
2 elfvdm AR1sucrankAsucrankAdomR1
3 1 2 syl AR1OnsucrankAdomR1
4 r1funlim FunR1LimdomR1
5 4 simpri LimdomR1
6 limsuc LimdomR1rankAdomR1sucrankAdomR1
7 5 6 ax-mp rankAdomR1sucrankAdomR1
8 3 7 sylibr AR1OnrankAdomR1
9 rankvaln ¬AR1OnrankA=
10 limomss LimdomR1ωdomR1
11 5 10 ax-mp ωdomR1
12 peano1 ω
13 11 12 sselii domR1
14 9 13 eqeltrdi ¬AR1OnrankAdomR1
15 8 14 pm2.61i rankAdomR1