Definition df-lim 6337

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 6390, dflim3 7823, 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 6333	. 2 wff Lim 𝐴
3	1	word 6331	. . 3 wff Ord 𝐴
4		c0 4296	. . . 4 class ∅
5	1, 4	wne 2925	. . 3 wff 𝐴 ≠ ∅
6	1	cuni 4871	. . . 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  6344  dflim2  6390  limord  6393  limuni  6394  unizlim  6457  limon  7811  dflim3  7823  nnsuc  7860  onfununi  8310  nlim1  8453  nlim2  8454  dfrdg2  35783  ellimits  35898  onsucuni3  37355  omlimcl2  43231  dflim5  43318