Definition df-lim 6326

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 6379, dflim3 7795, 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 6322	. 2 wff Lim 𝐴
3	1	word 6320	. . 3 wff Ord 𝐴
4		c0 4274	. . . 4 class ∅
5	1, 4	wne 2933	. . 3 wff 𝐴 ≠ ∅
6	1	cuni 4851	. . . 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  6333  dflim2  6379  limord  6382  limuni  6383  unizlim  6445  limon  7784  dflim3  7795  nnsuc  7832  onfununi  8278  nlim1  8421  nlim2  8422  dfrdg2  35972  ellimits  36087  onsucuni3  37680  omlimcl2  43667  dflim5  43754