Definition df-lim 6323

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 6376, dflim3 7791, 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 6319	. 2 wff Lim 𝐴
3	1	word 6317	. . 3 wff Ord 𝐴
4		c0 4286	. . . 4 class ∅
5	1, 4	wne 2933	. . 3 wff 𝐴 ≠ ∅
6	1	cuni 4864	. . . 4 class ∪ 𝐴
7	1, 6	wceq 1542	. . 3 wff 𝐴 = ∪ 𝐴
8	3, 5, 7	w3a 1087	. 2 wff (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴)
9	2, 8	wb 206	1 wff (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴))

This definition is referenced by:  limeq  6330  dflim2  6376  limord  6379  limuni  6380  unizlim  6442  limon  7780  dflim3  7791  nnsuc  7828  onfununi  8275  nlim1  8418  nlim2  8419  dfrdg2  35989  ellimits  36104  onsucuni3  37574  omlimcl2  43551  dflim5  43638