Definition df-lim 2948

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 3020, dflim3 3113, 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 2944	. 2 wff Lim A
3	1	word 2942	. . 3 wff Ord A
4		c0 2276	. . . 4 class (/)
5	1, 4	wne 1582	. . 3 wff A =/= (/)
6	1	cuni 2498	. . . 4 class U.A
7	1, 6	wceq 954	. . 3 wff A = U.A
8	3, 5, 7	w3a 774	. 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 2955  dflim2 3020  nlim0 3022  limord 3023  limuni 3024  limon 3089  nlimsucg 3107  unizlim 3108  nnsuc 3143  tfinds 3156  abianfplem 3952

Copyright terms: Public domain