Definition df-ilim 4072

Description: Define the limit ordinal predicate, which is true for an ordinal that has the empty set as an element and 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, and then changes A ≠ ∅ to ∅ ∈ A (which would be equivalent given the law of the excluded middle, but which is not for us). (Contributed by Jim Kingdon, 11-Nov-2018.) Use its alias dflim2 4073 instead for naming consistency with set.mm. (New usage is discouraged.)

Assertion

Ref	Expression
df-ilim	⊢ (Lim A ↔ (Ord A ∧ ∅ ∈ A ∧ A = ∪ A))

Detailed syntax breakdown of Definition df-ilim

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	wlim 4067	. 2 wff Lim A
3	1	word 4065	. . 3 wff Ord A
4		c0 3218	. . . 4 class ∅
5	4, 1	wcel 1390	. . 3 wff ∅ ∈ A
6	1	cuni 3571	. . . 4 class ∪ A
7	1, 6	wceq 1242	. . 3 wff A = ∪ A
8	3, 5, 7	w3a 884	. 2 wff (Ord A ∧ ∅ ∈ A ∧ A = ∪ A)
9	2, 8	wb 98	1 wff (Lim A ↔ (Ord A ∧ ∅ ∈ A ∧ A = ∪ A))

This definition is referenced by:  dflim2  4073