Definition df-lim 2980

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 3029, dflim3 3201, 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 2976	. 2 wff Lim A
3	1	word 2974	. . 3 wff Ord A
4		c0 2332	. . . 4 class (/)
5	1, 4	wne 1628	. . 3 wff A =/= (/)
6	1	cuni 2569	. . . 4 class U.A
7	1, 6	wceq 992	. . 3 wff A = U.A
8	3, 5, 7	w3a 781	. 2 wff (Ord A /\ A =/= (/) /\ A = U.A)
9	2, 8	wb 144	1 wff (Lim A <-> (Ord A /\ A =/= (/) /\ A = U.A))

This definition is referenced by:  limeq 2987  dflim2 3029  nlim0 3031  limord 3032  limuni 3033  unizlim 3086  limon 3190  nlimsucg 3196  tfinds 3212  nnsuc 3235  onfununi 4209  abianfplem 4262

Copyright terms: Public domain