Definition df-ilim 4347

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 (/) e. 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 4348 instead for naming consistency with set.mm. (New usage is discouraged.)

Assertion

Ref	Expression
df-ilim	|- ( Lim A <-> ( Ord A /\ (/) e. A /\ A = U. A ) )

Detailed syntax breakdown of Definition df-ilim

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	wlim 4342	. 2 wff Lim A
3	1	word 4340	. . 3 wff Ord A
4		c0 3409	. . . 4 class (/)
5	4, 1	wcel 2136	. . 3 wff (/) e. A
6	1	cuni 3789	. . . 4 class U. A
7	1, 6	wceq 1343	. . 3 wff A = U. A
8	3, 5, 7	w3a 968	. 2 wff ( Ord A /\ (/) e. A /\ A = U. A )
9	2, 8	wb 104	1 wff ( Lim A <-> ( Ord A /\ (/) e. A /\ A = U. A ) )

This definition is referenced by:  dflim2  4348