Metamath Proof Explorer


Theorem limensuc

Description: A limit ordinal is equinumerous to its successor. (Contributed by NM, 30-Oct-2003)

Ref Expression
Assertion limensuc AVLimAAsucA

Proof

Step Hyp Ref Expression
1 eleq1 A=ifLimAAOnAVifLimAAOnV
2 id A=ifLimAAOnA=ifLimAAOn
3 suceq A=ifLimAAOnsucA=sucifLimAAOn
4 2 3 breq12d A=ifLimAAOnAsucAifLimAAOnsucifLimAAOn
5 1 4 imbi12d A=ifLimAAOnAVAsucAifLimAAOnVifLimAAOnsucifLimAAOn
6 limeq A=ifLimAAOnLimALimifLimAAOn
7 limeq On=ifLimAAOnLimOnLimifLimAAOn
8 limon LimOn
9 6 7 8 elimhyp LimifLimAAOn
10 9 limensuci ifLimAAOnVifLimAAOnsucifLimAAOn
11 5 10 dedth LimAAVAsucA
12 11 impcom AVLimAAsucA