Definition df-lim 5728

Description: Define the limit ordinal predicate, which is true for a nonempty ordinal that is not a successor (i.e. that is the union of itself). Our definition combines the definition of Lim of [BellMachover] p. 471 and Exercise 1 of [TakeutiZaring] p. 42. See dflim2 5781, dflim3 7047, and dflim4 for alternate definitions. (Contributed by NM, 22-Apr-1994.)

Assertion

Ref	Expression
df-lim	|- ( Lim A <-> ( Ord A /\ A =/= (/) /\ A = U. A ) )

Detailed syntax breakdown of Definition df-lim

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	wlim 5724	. 2 wff Lim A
3	1	word 5722	. . 3 wff Ord A
4		c0 3915	. . . 4 class (/)
5	1, 4	wne 2794	. . 3 wff A =/= (/)
6	1	cuni 4436	. . . 4 class U. A
7	1, 6	wceq 1483	. . 3 wff A = U. A
8	3, 5, 7	w3a 1037	. 2 wff ( Ord A /\ A =/= (/) /\ A = U. A )
9	2, 8	wb 196	1 wff ( Lim A <-> ( Ord A /\ A =/= (/) /\ A = U. A ) )

This definition is referenced by:  limeq  5735  dflim2  5781  limord  5784  limuni  5785  unizlim  5844  limon  7036  dflim3  7047  nnsuc  7082  onfununi  7438  dfrdg2  31701  ellimits  32017  onsucuni3  33215