Metamath Proof Explorer


Theorem dflim3

Description: An alternate definition of a limit ordinal, which is any ordinal that is neither zero nor a successor. (Contributed by NM, 1-Nov-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011)

Ref Expression
Assertion dflim3 LimAOrdA¬A=xOnA=sucx

Proof

Step Hyp Ref Expression
1 df-lim LimAOrdAAA=A
2 3anass OrdAAA=AOrdAAA=A
3 df-ne A¬A=
4 3 a1i OrdAA¬A=
5 orduninsuc OrdAA=A¬xOnA=sucx
6 4 5 anbi12d OrdAAA=A¬A=¬xOnA=sucx
7 ioran ¬A=xOnA=sucx¬A=¬xOnA=sucx
8 6 7 bitr4di OrdAAA=A¬A=xOnA=sucx
9 8 pm5.32i OrdAAA=AOrdA¬A=xOnA=sucx
10 1 2 9 3bitri LimAOrdA¬A=xOnA=sucx