Definition df-lim 6367

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 6421, dflim3 7858, and dflim4 7859 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 6363	. 2 wff Lim 𝐴
3	1	word 6361	. . 3 wff Ord 𝐴
4		c0 4278	. . . 4 class ∅
5	1, 4	wne 2955	. . 3 wff 𝐴 ≠ ∅
6	1	cuni 4866	. . . 4 class ∪ 𝐴
7	1, 6	wceq 1569	. . 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  6374  dflim2  6421  limord  6424  limuni  6425  unizlim  6487  limon  7847  dflim3  7858  nnsuc  7895  onfununi  8349  nlim1  8497  nlim2  8498  dfrdg2  36599  ellimits  36714  onsucuni3  38333  omlimcl2  44286  dflim5  44373