Definition df-lim 6365

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 6419, dflim3 7842, 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 6361	. 2 wff Lim 𝐴
3	1	word 6359	. . 3 wff Ord 𝐴
4		c0 4285	. . . 4 class ∅
5	1, 4	wne 2956	. . 3 wff 𝐴 ≠ ∅
6	1	cuni 4871	. . . 4 class ∪ 𝐴
7	1, 6	wceq 1568	. . 3 wff 𝐴 = ∪ 𝐴
8	3, 5, 7	w3a 1101	. 2 wff (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴)
9	2, 8	wb 209	1 wff (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴))

This definition is referenced by:  limeq  6372  dflim2  6419  limord  6422  limuni  6423  unizlim  6485  limon  7831  dflim3  7842  nnsuc  7879  onfununi  8327  nlim1  8473  nlim2  8474  dfrdg2  36239  ellimits  36354  onsucuni3  37957  omlimcl2  43917  dflim5  44004