Definition df-lim 3848

Description: Define the limit ordinal predicate, which is true for a non-empty 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 3898, dflim3 4100, and dflim4 for alternate definitions.

Assertion

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

Detailed syntax breakdown of Definition df-lim

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	wlim 3844	. 2 wff Lim A
3	1	word 3842	. . 3 wff Ord A
4		c0 3114	. . . 4 class (/)
5	1, 4	wne 2295	. . 3 wff A =/= (/)
6	1	cuni 3398	. . . 4 class U.A
7	1, 6	wceq 1615	. . 3 wff A = U.A
8	3, 5, 7	w3a 1130	. 2 wff (Ord A /\ A =/= (/) /\ A = U.A)
9	2, 8	wb 231	1 wff (Lim A <-> (Ord A /\ A =/= (/) /\ A = U.A))

This definition is referenced by:  limeq 3855  dflim2 3898  limord 3901  limuni 3902  unizlim 3958  limon 4089  nlimsucg 4095  dflim3 4100  nnsuc 4135  onfununi 5293  abianfplem 5377  ellimits 15018

Copyright terms: Public domain