Definition df-lim 2943

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 3015, dflim3 3108, 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 2939	. 2 wff Lim A
3	1	word 2937	. . 3 wff Ord A
4		c0 2270	. . . 4 class (/)
5	1, 4	wne 1577	. . 3 wff A =/= (/)
6	1	cuni 2493	. . . 4 class U.A
7	1, 6	wceq 953	. . 3 wff A = U.A
8	3, 5, 7	w3a 773	. 2 wff (Ord A /\ A =/= (/) /\ A = U.A)
9	2, 8	wb 146	1 wff (Lim A <-> (Ord A /\ A =/= (/) /\ A = U.A))

This definition is referenced by:  limeq 2950  dflim2 3015  nlim0 3017  limord 3018  limuni 3019  limon 3084  nlimsucg 3102  unizlim 3103  nnsuc 3138  tfinds 3151  abianfplem 3946

Copyright terms: Public domain