Definition df-lim 6316

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 6369, dflim3 7787, 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 6312	. 2 wff Lim 𝐴
3	1	word 6310	. . 3 wff Ord 𝐴
4		c0 4286	. . . 4 class ∅
5	1, 4	wne 2925	. . 3 wff 𝐴 ≠ ∅
6	1	cuni 4861	. . . 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  6323  dflim2  6369  limord  6372  limuni  6373  unizlim  6435  limon  7775  dflim3  7787  nnsuc  7824  onfununi  8271  nlim1  8414  nlim2  8415  dfrdg2  35788  ellimits  35903  onsucuni3  37360  omlimcl2  43235  dflim5  43322