Theorem nnsuc

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

	Ref	Expression
Assertion	nnsuc	⊢ ( ( 𝐴 ∈ ω ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ ω 𝐴 = suc 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		nnlim	⊢ ( 𝐴 ∈ ω → ¬ Lim 𝐴 )
2	1	adantr	⊢ ( ( 𝐴 ∈ ω ∧ 𝐴 ≠ ∅ ) → ¬ Lim 𝐴 )
3		nnord	⊢ ( 𝐴 ∈ ω → Ord 𝐴 )
4		orduninsuc	⊢ ( Ord 𝐴 → ( 𝐴 = ∪ 𝐴 ↔ ¬ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) )
5	4	adantr	⊢ ( ( Ord 𝐴 ∧ 𝐴 ≠ ∅ ) → ( 𝐴 = ∪ 𝐴 ↔ ¬ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) )
6		df-lim	⊢ ( Lim 𝐴 ↔ ( Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴 ) )
7	6	biimpri	⊢ ( ( Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴 ) → Lim 𝐴 )
8	7	3expia	⊢ ( ( Ord 𝐴 ∧ 𝐴 ≠ ∅ ) → ( 𝐴 = ∪ 𝐴 → Lim 𝐴 ) )
9	5 8	sylbird	⊢ ( ( Ord 𝐴 ∧ 𝐴 ≠ ∅ ) → ( ¬ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 → Lim 𝐴 ) )
10	3 9	sylan	⊢ ( ( 𝐴 ∈ ω ∧ 𝐴 ≠ ∅ ) → ( ¬ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 → Lim 𝐴 ) )
11	2 10	mt3d	⊢ ( ( 𝐴 ∈ ω ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 )
12		eleq1	⊢ ( 𝐴 = suc 𝑥 → ( 𝐴 ∈ ω ↔ suc 𝑥 ∈ ω ) )
13	12	biimpcd	⊢ ( 𝐴 ∈ ω → ( 𝐴 = suc 𝑥 → suc 𝑥 ∈ ω ) )
14		peano2b	⊢ ( 𝑥 ∈ ω ↔ suc 𝑥 ∈ ω )
15	13 14	imbitrrdi	⊢ ( 𝐴 ∈ ω → ( 𝐴 = suc 𝑥 → 𝑥 ∈ ω ) )
16	15	ancrd	⊢ ( 𝐴 ∈ ω → ( 𝐴 = suc 𝑥 → ( 𝑥 ∈ ω ∧ 𝐴 = suc 𝑥 ) ) )
17	16	adantld	⊢ ( 𝐴 ∈ ω → ( ( 𝑥 ∈ On ∧ 𝐴 = suc 𝑥 ) → ( 𝑥 ∈ ω ∧ 𝐴 = suc 𝑥 ) ) )
18	17	reximdv2	⊢ ( 𝐴 ∈ ω → ( ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 → ∃ 𝑥 ∈ ω 𝐴 = suc 𝑥 ) )
19	18	adantr	⊢ ( ( 𝐴 ∈ ω ∧ 𝐴 ≠ ∅ ) → ( ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 → ∃ 𝑥 ∈ ω 𝐴 = suc 𝑥 ) )
20	11 19	mpd	⊢ ( ( 𝐴 ∈ ω ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ ω 𝐴 = suc 𝑥 )