Theorem nlimon

Description: Two ways to express the class of non-limit ordinal numbers. Part of Definition 7.27 of TakeutiZaring p. 42, who use the symbol K_I for this class. (Contributed by NM, 1-Nov-2004)

	Ref	Expression
Assertion	nlimon	|- { x e. On | ( x = (/) \/ E. y e. On x = suc y ) } = { x e. On | -. Lim x }

Proof

Step	Hyp	Ref	Expression
1		eloni	|- ( x e. On -> Ord x )
2		dflim3	|- ( Lim x <-> ( Ord x /\ -. ( x = (/) \/ E. y e. On x = suc y ) ) )
3	2	baib	|- ( Ord x -> ( Lim x <-> -. ( x = (/) \/ E. y e. On x = suc y ) ) )
4	3	con2bid	|- ( Ord x -> ( ( x = (/) \/ E. y e. On x = suc y ) <-> -. Lim x ) )
5	1 4	syl	|- ( x e. On -> ( ( x = (/) \/ E. y e. On x = suc y ) <-> -. Lim x ) )
6	5	rabbiia	|- { x e. On | ( x = (/) \/ E. y e. On x = suc y ) } = { x e. On | -. Lim x }