Definition df-lim 6320

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 6373, 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 6316	. 2 wff Lim 𝐴
3	1	word 6314	. . 3 wff Ord 𝐴
4		c0 4283	. . . 4 class ∅
5	1, 4	wne 2930	. . 3 wff 𝐴 ≠ ∅
6	1	cuni 4861	. . . 4 class ∪ 𝐴
7	1, 6	wceq 1541	. . 3 wff 𝐴 = ∪ 𝐴
8	3, 5, 7	w3a 1086	. 2 wff (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴)
9	2, 8	wb 206	1 wff (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴))

This definition is referenced by:  limeq  6327  dflim2  6373  limord  6376  limuni  6377  unizlim  6439  limon  7776  dflim3  7787  nnsuc  7824  onfununi  8271  nlim1  8414  nlim2  8415  dfrdg2  35936  ellimits  36051  onsucuni3  37511  omlimcl2  43426  dflim5  43513