Metamath Proof Explorer


Theorem dflim2

Description: An alternate definition of a limit ordinal. (Contributed by NM, 4-Nov-2004)

Ref Expression
Assertion dflim2 LimAOrdAAA=A

Proof

Step Hyp Ref Expression
1 df-lim LimAOrdAAA=A
2 ord0eln0 OrdAAA
3 2 anbi1d OrdAAA=AAA=A
4 3 pm5.32i OrdAAA=AOrdAAA=A
5 3anass OrdAAA=AOrdAAA=A
6 3anass OrdAAA=AOrdAAA=A
7 4 5 6 3bitr4i OrdAAA=AOrdAAA=A
8 1 7 bitr4i LimAOrdAAA=A