Definition df-lim 6322

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 6375, dflim3 7789, 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 6318	. 2 wff Lim 𝐴
3	1	word 6316	. . 3 wff Ord 𝐴
4		c0 4285	. . . 4 class ∅
5	1, 4	wne 2932	. . 3 wff 𝐴 ≠ ∅
6	1	cuni 4863	. . . 4 class ∪ 𝐴
7	1, 6	wceq 1541	. . 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  6329  dflim2  6375  limord  6378  limuni  6379  unizlim  6441  limon  7778  dflim3  7789  nnsuc  7826  onfununi  8273  nlim1  8416  nlim2  8417  dfrdg2  35987  ellimits  36102  onsucuni3  37568  omlimcl2  43480  dflim5  43567