Definition df-lim 6353

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 6406, dflim3 7829, 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 6349	. 2 wff Lim 𝐴
3	1	word 6347	. . 3 wff Ord 𝐴
4		c0 4287	. . . 4 class ∅
5	1, 4	wne 2959	. . 3 wff 𝐴 ≠ ∅
6	1	cuni 4867	. . . 4 class ∪ 𝐴
7	1, 6	wceq 1562	. . 3 wff 𝐴 = ∪ 𝐴
8	3, 5, 7	w3a 1099	. 2 wff (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴)
9	2, 8	wb 208	1 wff (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴))

This definition is referenced by:  limeq  6360  dflim2  6406  limord  6409  limuni  6410  unizlim  6472  limon  7818  dflim3  7829  nnsuc  7866  onfununi  8314  nlim1  8460  nlim2  8461  dfrdg2  36148  ellimits  36263  onsucuni3  37866  omlimcl2  43824  dflim5  43911