Definition df-ilim 4106

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 𝐴 ≠ ∅ to ∅ ∈ 𝐴 (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 4107 instead for naming consistency with set.mm. (New usage is discouraged.)

Assertion

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

Detailed syntax breakdown of Definition df-ilim

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2	1	wlim 4101	. 2 wff Lim 𝐴
3	1	word 4099	. . 3 wff Ord 𝐴
4		c0 3224	. . . 4 class ∅
5	4, 1	wcel 1393	. . 3 wff ∅ ∈ 𝐴
6	1	cuni 3580	. . . 4 class ∪ 𝐴
7	1, 6	wceq 1243	. . 3 wff 𝐴 = ∪ 𝐴
8	3, 5, 7	w3a 885	. 2 wff (Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ 𝐴 = ∪ 𝐴)
9	2, 8	wb 98	1 wff (Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ 𝐴 = ∪ 𝐴))

This definition is referenced by:  dflim2  4107