Definition df-lim 6366

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 6418, dflim3 7831, 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 6362	. 2 wff Lim 𝐴
3	1	word 6360	. . 3 wff Ord 𝐴
4		c0 4321	. . . 4 class ∅
5	1, 4	wne 2941	. . 3 wff 𝐴 ≠ ∅
6	1	cuni 4907	. . . 4 class ∪ 𝐴
7	1, 6	wceq 1542	. . 3 wff 𝐴 = ∪ 𝐴
8	3, 5, 7	w3a 1088	. 2 wff (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴)
9	2, 8	wb 205	1 wff (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴))

This definition is referenced by:  limeq  6373  dflim2  6418  limord  6421  limuni  6422  unizlim  6484  limon  7819  dflim3  7831  nnsuc  7868  onfununi  8336  nlim1  8484  nlim2  8485  dfrdg2  34705  ellimits  34820  onsucuni3  36186  omlimcl2  41924  dflim5  42012