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 7841, 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 2957	. . 3 wff 𝐴 ≠ ∅
6	1	cuni 4871	. . . 4 class ∪ 𝐴
7	1, 6	wceq 1569	. . 3 wff 𝐴 = ∪ 𝐴
8	3, 5, 7	w3a 1102	. 2 wff (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴)
9	2, 8	wb 209	1 wff (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴))

This definition is used by:  limeq  6372  dflim2  6419  limord  6422  limuni  6423  unizlim  6485  limon  7830  dflim3  7841  nnsuc  7878  onfununi  8326  nlim1  8472  nlim2  8473  dfrdg2  36293  ellimits  36408  onsucuni3  38041  omlimcl2  43997  dflim5  44084