Definition df-lim 3662

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 3719, dflim3 3930, 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 3658	. 2 wff Lim A
3	1	word 3656	. . 3 wff Ord A
4		c0 2875	. . . 4 class (/)
5	1, 4	wne 2017	. . 3 wff A =/= (/)
6	1	cuni 3177	. . . 4 class U.A
7	1, 6	wceq 1298	. . 3 wff A = U.A
8	3, 5, 7	w3a 858	. 2 wff (Ord A /\ A =/= (/) /\ A = U.A)
9	2, 8	wb 163	1 wff (Lim A <-> (Ord A /\ A =/= (/) /\ A = U.A))

This definition is referenced by:  limeq 3669  limeqOLD 3670  dflim2 3719  nlim0OLD 3722  limord 3723  limuni 3724  unizlim 3786  limon 3917  nlimsucg 3923  nlimsucgOLD 3924  dflim3 3930  tfindsOLD 3943  nnsuc 3969  onfununi 5116  abianfplem 5170  ellimits 14079

Copyright terms: Public domain