Definition df-lim 6332

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 6385, dflim3 7801, 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 6328	. 2 wff Lim 𝐴
3	1	word 6326	. . 3 wff Ord 𝐴
4		c0 4287	. . . 4 class ∅
5	1, 4	wne 2933	. . 3 wff 𝐴 ≠ ∅
6	1	cuni 4865	. . . 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  6339  dflim2  6385  limord  6388  limuni  6389  unizlim  6451  limon  7790  dflim3  7801  nnsuc  7838  onfununi  8285  nlim1  8428  nlim2  8429  dfrdg2  36015  ellimits  36130  onsucuni3  37649  omlimcl2  43628  dflim5  43715