Definition df-lim 6357

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 6410, dflim3 7840, 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 6353	. 2 wff Lim 𝐴
3	1	word 6351	. . 3 wff Ord 𝐴
4		c0 4308	. . . 4 class ∅
5	1, 4	wne 2932	. . 3 wff 𝐴 ≠ ∅
6	1	cuni 4883	. . . 4 class ∪ 𝐴
7	1, 6	wceq 1540	. . 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  6364  dflim2  6410  limord  6413  limuni  6414  unizlim  6476  limon  7828  dflim3  7840  nnsuc  7877  onfununi  8353  nlim1  8499  nlim2  8500  dfrdg2  35759  ellimits  35874  onsucuni3  37331  omlimcl2  43213  dflim5  43300