nnsuc

Description: A nonzero natural number is a successor. (Contributed by NM, 18-Feb-2004)

		Ref	Expression
	Assertion	nnsuc	$⊢ (A \in ω \land A \neq \emptyset) \to \exists x \in ω A = suc x$

Proof

Step	Hyp	Ref	Expression
1		nnlim	$⊢ A \in ω \to \neg Lim A$
2	1	adantr	$⊢ (A \in ω \land A \neq \emptyset) \to \neg Lim A$
3		nnord	$⊢ A \in ω \to Ord A$
4		orduninsuc	$⊢ Ord A \to (A = ⋃ A \leftrightarrow \neg \exists x \in On A = suc x)$
5	4	adantr	$⊢ (Ord A \land A \neq \emptyset) \to (A = ⋃ A \leftrightarrow \neg \exists x \in On A = suc x)$
6		df-lim	$⊢ Lim A \leftrightarrow (Ord A \land A \neq \emptyset \land A = ⋃ A)$
7	6	biimpri	$⊢ (Ord A \land A \neq \emptyset \land A = ⋃ A) \to Lim A$
8	7	3expia	$⊢ (Ord A \land A \neq \emptyset) \to (A = ⋃ A \to Lim A)$
9	5 8	sylbird	$⊢ (Ord A \land A \neq \emptyset) \to (\neg \exists x \in On A = suc x \to Lim A)$
10	3 9	sylan	$⊢ (A \in ω \land A \neq \emptyset) \to (\neg \exists x \in On A = suc x \to Lim A)$
11	2 10	mt3d	$⊢ (A \in ω \land A \neq \emptyset) \to \exists x \in On A = suc x$
12		eleq1	$⊢ A = suc x \to (A \in ω \leftrightarrow suc x \in ω)$
13	12	biimpcd	$⊢ A \in ω \to (A = suc x \to suc x \in ω)$
14		peano2b	$⊢ x \in ω \leftrightarrow suc x \in ω$
15	13 14	imbitrrdi	$⊢ A \in ω \to (A = suc x \to x \in ω)$
16	15	ancrd	$⊢ A \in ω \to (A = suc x \to (x \in ω \land A = suc x))$
17	16	adantld	$⊢ A \in ω \to ((x \in On \land A = suc x) \to (x \in ω \land A = suc x))$
18	17	reximdv2	$⊢ A \in ω \to (\exists x \in On A = suc x \to \exists x \in ω A = suc x)$
19	18	adantr	$⊢ (A \in ω \land A \neq \emptyset) \to (\exists x \in On A = suc x \to \exists x \in ω A = suc x)$
20	11 19	mpd	$⊢ (A \in ω \land A \neq \emptyset) \to \exists x \in ω A = suc x$

Metamath Proof Explorer

Theorem nnsuc

Proof