Definition df-lim 6318

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 6371, dflim3 7790, 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 6314	. 2 wff Lim 𝐴
3	1	word 6312	. . 3 wff Ord 𝐴
4		c0 4263	. . . 4 class ∅
5	1, 4	wne 2936	. . 3 wff 𝐴 ≠ ∅
6	1	cuni 4840	. . . 4 class ∪ 𝐴
7	1, 6	wceq 1548	. . 3 wff 𝐴 = ∪ 𝐴
8	3, 5, 7	w3a 1093	. 2 wff (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴)
9	2, 8	wb 208	1 wff (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴))

This definition is referenced by:  limeq  6325  dflim2  6371  limord  6374  limuni  6375  unizlim  6437  limon  7779  dflim3  7790  nnsuc  7827  onfununi  8274  nlim1  8418  nlim2  8419  dfrdg2  36034  ellimits  36149  onsucuni3  37742  omlimcl2  43700  dflim5  43787