Definition df-lim 6400

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 6452, dflim3 7884, 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 6396	. 2 wff Lim 𝐴
3	1	word 6394	. . 3 wff Ord 𝐴
4		c0 4352	. . . 4 class ∅
5	1, 4	wne 2946	. . 3 wff 𝐴 ≠ ∅
6	1	cuni 4931	. . . 4 class ∪ 𝐴
7	1, 6	wceq 1537	. . 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  6407  dflim2  6452  limord  6455  limuni  6456  unizlim  6518  limon  7872  dflim3  7884  nnsuc  7921  onfununi  8397  nlim1  8545  nlim2  8546  dfrdg2  35759  ellimits  35874  onsucuni3  37333  omlimcl2  43203  dflim5  43291