This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ) )