Definition df-lim 6325

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 6378, dflim3 7803, 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 6321	. 2 wff Lim 𝐴
3	1	word 6319	. . 3 wff Ord 𝐴
4		c0 4292	. . . 4 class ∅
5	1, 4	wne 2925	. . 3 wff 𝐴 ≠ ∅
6	1	cuni 4867	. . . 4 class ∪ 𝐴
7	1, 6	wceq 1540	. . 3 wff 𝐴 = ∪ 𝐴
8	3, 5, 7	w3a 1086	. 2 wff (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴)
9	2, 8	wb 206	1 wff (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴))

This definition is referenced by:  limeq  6332  dflim2  6378  limord  6381  limuni  6382  unizlim  6445  limon  7791  dflim3  7803  nnsuc  7840  onfununi  8287  nlim1  8430  nlim2  8431  dfrdg2  35756  ellimits  35871  onsucuni3  37328  omlimcl2  43204  dflim5  43291