This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑥 )