Metamath Proof Explorer

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 \in On \| (x = \emptyset \lor \exists y \in On x = suc y)\} = \{x \in On \| \neg Lim x\}$

Proof

Step	Hyp	Ref	Expression
1		eloni	$⊢ x \in On \to Ord x$
2		dflim3	$⊢ Lim x \leftrightarrow (Ord x \land \neg (x = \emptyset \lor \exists y \in On x = suc y))$
3	2	baib	$⊢ Ord x \to (Lim x \leftrightarrow \neg (x = \emptyset \lor \exists y \in On x = suc y))$
4	3	con2bid	$⊢ Ord x \to ((x = \emptyset \lor \exists y \in On x = suc y) \leftrightarrow \neg Lim x)$
5	1 4	syl	$⊢ x \in On \to ((x = \emptyset \lor \exists y \in On x = suc y) \leftrightarrow \neg Lim x)$
6	5	rabbiia	$⊢ \{x \in On \| (x = \emptyset \lor \exists y \in On x = suc y)\} = \{x \in On \| \neg Lim x\}$