Definition df-lim 2204

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 2280 and dflim3 2368 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 2200	. 2 wff Lim A
3	1	word 2198	. . 3 wff Ord A
4		c0 1707	. . . . 5 class (/)
5	1, 4	wceq 1091	. . . 4 wff A = (/)
6	5	wn 1	. . 3 wff -. A = (/)
7	1	cuni 1919	. . . 4 class U.A
8	1, 7	wceq 1091	. . 3 wff A = U.A
9	3, 6, 8	w3a 581	. 2 wff (Ord A /\ -. A = (/) /\ A = U.A)
10	2, 9	wb 127	1 wff (Lim A <-> (Ord A /\ -. A = (/) /\ A = U.A))

This definition is referenced by:  limeq 2211  dflim2 2280  nlim0 2282  limord 2283  limuni 2284  limon 2342  nlimsuc 2363  unizlim 2364  nnsuc 2389  tfinds 2401  abianfplem 2999

metamath.org