Metamath Proof Explorer

Theorem nlimsuc

Description: A successor is not a limit ordinal. (Contributed by RP, 13-Dec-2024)

Ref Expression
Assertion nlimsuc ⊢ A ∈ On → ¬ Lim ⁡ suc ⁡ A

Proof

Step Hyp Ref Expression
1 sucidg ⊢ A ∈ On → A ∈ suc ⁡ A
2 eloni ⊢ A ∈ On → Ord ⁡ A
3 ordirr ⊢ Ord ⁡ A → ¬ A ∈ A
4 2 3 syl ⊢ A ∈ On → ¬ A ∈ A
5 eleq2 ⊢ suc ⁡ A = A → A ∈ suc ⁡ A ↔ A ∈ A
6 5 notbid ⊢ suc ⁡ A = A → ¬ A ∈ suc ⁡ A ↔ ¬ A ∈ A
7 4 6 syl5ibrcom ⊢ A ∈ On → suc ⁡ A = A → ¬ A ∈ suc ⁡ A
8 1 7 mt2d ⊢ A ∈ On → ¬ suc ⁡ A = A
9 8 neqned ⊢ A ∈ On → suc ⁡ A ≠ A
10 onunisuc ⊢ A ∈ On → ⋃ suc ⁡ A = A
11 9 10 neeqtrrd ⊢ A ∈ On → suc ⁡ A ≠ ⋃ suc ⁡ A
12 11 neneqd ⊢ A ∈ On → ¬ suc ⁡ A = ⋃ suc ⁡ A
13 12 intn3an3d ⊢ A ∈ On → ¬ Ord ⁡ suc ⁡ A ∧ ∅ ∈ suc ⁡ A ∧ suc ⁡ A = ⋃ suc ⁡ A
14 dflim2 ⊢ Lim ⁡ suc ⁡ A ↔ Ord ⁡ suc ⁡ A ∧ ∅ ∈ suc ⁡ A ∧ suc ⁡ A = ⋃ suc ⁡ A
15 13 14 sylnibr ⊢ A ∈ On → ¬ Lim ⁡ suc ⁡ A