Definition df-lim 6271

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 6322, dflim3 7694, 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 6267	. 2 wff Lim 𝐴
3	1	word 6265	. . 3 wff Ord 𝐴
4		c0 4256	. . . 4 class ∅
5	1, 4	wne 2943	. . 3 wff 𝐴 ≠ ∅
6	1	cuni 4839	. . . 4 class ∪ 𝐴
7	1, 6	wceq 1539	. . 3 wff 𝐴 = ∪ 𝐴
8	3, 5, 7	w3a 1086	. 2 wff (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴)
9	2, 8	wb 205	1 wff (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴))

This definition is referenced by:  limeq  6278  dflim2  6322  limord  6325  limuni  6326  unizlim  6383  limon  7683  dflim3  7694  nnsuc  7730  onfununi  8172  nlim1  8319  nlim2  8320  dfrdg2  33771  ellimits  34212  onsucuni3  35538