Definition df-lim 6317

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 6370, dflim3 7787, and dflim4 for alternate definitions. (Contributed by NM, 22-Apr-1994.)

Assertion

Ref	Expression
df-lim	⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴))

Detailed syntax breakdown of Definition df-lim

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2	1	wlim 6313	. 2 wff Lim 𝐴
3	1	word 6311	. . 3 wff Ord 𝐴
4		c0 4263	. . . 4 class ∅
5	1, 4	wne 2930	. . 3 wff 𝐴 ≠ ∅
6	1	cuni 4840	. . . 4 class ∪ 𝐴
7	1, 6	wceq 1542	. . 3 wff 𝐴 = ∪ 𝐴
8	3, 5, 7	w3a 1087	. 2 wff (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴)
9	2, 8	wb 206	1 wff (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴))

This definition is referenced by:  limeq  6324  dflim2  6370  limord  6373  limuni  6374  unizlim  6436  limon  7776  dflim3  7787  nnsuc  7824  onfununi  8270  nlim1  8413  nlim2  8414  dfrdg2  35963  ellimits  36078  onsucuni3  37671  omlimcl2  43658  dflim5  43745