Definition df-lim 6366

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 6420, dflim3 7846, and dflim4 7847 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 6362	. 2 wff Lim 𝐴
3	1	word 6360	. . 3 wff Ord 𝐴
4		c0 4282	. . . 4 class ∅
5	1, 4	wne 2957	. . 3 wff 𝐴 ≠ ∅
6	1	cuni 4870	. . . 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  6373  dflim2  6420  limord  6423  limuni  6424  unizlim  6486  limon  7835  dflim3  7846  nnsuc  7883  onfununi  8333  nlim1  8479  nlim2  8480  dfrdg2  36359  ellimits  36474  onsucuni3  38108  omlimcl2  44070  dflim5  44157