Definition df-lim 6356

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 7841, and dflim4 7842 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 6352	. 2 wff Lim 𝐴
3	1	word 6350	. . 3 wff Ord 𝐴
4		c0 4278	. . . 4 class ∅
5	1, 4	wne 2955	. . 3 wff 𝐴 ≠ ∅
6	1	cuni 4866	. . . 4 class ∪ 𝐴
7	1, 6	wceq 1570	. . 3 wff 𝐴 = ∪ 𝐴
8	3, 5, 7	w3a 1103	. 2 wff (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴)
9	2, 8	wb 209	1 wff (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴))

This definition is used by:  limeq  6363  dflim2  6410  limord  6413  limuni  6414  unizlim  6476  limon  7830  dflim3  7841  nnsuc  7878  onfununi  8327  nlim1  8475  nlim2  8476  dfrdg2  36479  ellimits  36594  onsucuni3  38210  omlimcl2  44187  dflim5  44274