Definition df-lim 6311

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 6364, dflim3 7777, 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 6307	. 2 wff Lim 𝐴
3	1	word 6305	. . 3 wff Ord 𝐴
4		c0 4280	. . . 4 class ∅
5	1, 4	wne 2928	. . 3 wff 𝐴 ≠ ∅
6	1	cuni 4856	. . . 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  6318  dflim2  6364  limord  6367  limuni  6368  unizlim  6430  limon  7766  dflim3  7777  nnsuc  7814  onfununi  8261  nlim1  8404  nlim2  8405  dfrdg2  35837  ellimits  35952  onsucuni3  37409  omlimcl2  43283  dflim5  43370