nnlim

Description: A natural number is not a limit ordinal. (Contributed by NM, 18-Oct-1995)

		Ref	Expression
	Assertion	nnlim	$⊢ A \in ω \to \neg Lim A$

Step	Hyp	Ref	Expression
1		nnord	$⊢ A \in ω \to Ord A$
2		ordirr	$⊢ Ord A \to \neg A \in A$
3	1 2	syl	$⊢ A \in ω \to \neg A \in A$
4		elom	$⊢ A \in ω \leftrightarrow (A \in On \land \forall x (Lim x \to A \in x))$
5	4	simprbi	$⊢ A \in ω \to \forall x (Lim x \to A \in x)$
6		limeq	$⊢ x = A \to (Lim x \leftrightarrow Lim A)$
7		eleq2	$⊢ x = A \to (A \in x \leftrightarrow A \in A)$
8	6 7	imbi12d	$⊢ x = A \to ((Lim x \to A \in x) \leftrightarrow (Lim A \to A \in A))$
9	8	spcgv	$⊢ A \in ω \to (\forall x (Lim x \to A \in x) \to (Lim A \to A \in A))$
10	5 9	mpd	$⊢ A \in ω \to (Lim A \to A \in A)$
11	3 10	mtod	$⊢ A \in ω \to \neg Lim A$

Metamath Proof Explorer