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
|- ( Lim A <-> ( Ord A /\ -. ( A = (/) \/ E. x e. On A = suc x ) ) )

Proof

Step Hyp Ref Expression
1 df-lim
 |-  ( Lim A <-> ( Ord A /\ A =/= (/) /\ A = U. A ) )
2 3anass
 |-  ( ( Ord A /\ A =/= (/) /\ A = U. A ) <-> ( Ord A /\ ( A =/= (/) /\ A = U. A ) ) )
3 df-ne
 |-  ( A =/= (/) <-> -. A = (/) )
4 3 a1i
 |-  ( Ord A -> ( A =/= (/) <-> -. A = (/) ) )
5 orduninsuc
 |-  ( Ord A -> ( A = U. A <-> -. E. x e. On A = suc x ) )
6 4 5 anbi12d
 |-  ( Ord A -> ( ( A =/= (/) /\ A = U. A ) <-> ( -. A = (/) /\ -. E. x e. On A = suc x ) ) )
7 ioran
 |-  ( -. ( A = (/) \/ E. x e. On A = suc x ) <-> ( -. A = (/) /\ -. E. x e. On A = suc x ) )
8 6 7 bitr4di
 |-  ( Ord A -> ( ( A =/= (/) /\ A = U. A ) <-> -. ( A = (/) \/ E. x e. On A = suc x ) ) )
9 8 pm5.32i
 |-  ( ( Ord A /\ ( A =/= (/) /\ A = U. A ) ) <-> ( Ord A /\ -. ( A = (/) \/ E. x e. On A = suc x ) ) )
10 1 2 9 3bitri
 |-  ( Lim A <-> ( Ord A /\ -. ( A = (/) \/ E. x e. On A = suc x ) ) )