Definition df-lim 6382

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 6436, dflim3 7879, and dflim4 7880 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 6378	. 2 wff Lim 𝐴
3	1	word 6376	. . 3 wff Ord 𝐴
4		c0 4281	. . . 4 class ∅
5	1, 4	wne 2959	. . 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  6389  dflim2  6436  limord  6439  limuni  6440  unizlim  6502  limon  7868  dflim3  7879  nnsuc  7916  onfununi  8374  nlim1  8522  nlim2  8523  dfrdg2  36734  ellimits  36849  onsucuni3  38481  omlimcl2  44434  dflim5  44521