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