Metamath Proof Explorer

Theorem limnsuc

Description: A limit ordinal is not an element of the class of successor ordinals. Definition 1.11 of Schloeder p. 2. (Contributed by RP, 16-Jan-2025)

Ref Expression
Assertion limnsuc ⊢ Lim ⁡ A → ¬ A ∈ a ∈ On | ∃ b ∈ On a = suc ⁡ b

Proof

Step Hyp Ref Expression
1 dflim6 ⊢ Lim ⁡ A ↔ Ord ⁡ A ∧ A ≠ ∅ ∧ ¬ ∃ b ∈ On A = suc ⁡ b
2 simp3 ⊢ Ord ⁡ A ∧ A ≠ ∅ ∧ ¬ ∃ b ∈ On A = suc ⁡ b → ¬ ∃ b ∈ On A = suc ⁡ b
3 eqeq1 ⊢ a = A → a = suc ⁡ b ↔ A = suc ⁡ b
4 3 rexbidv ⊢ a = A → ∃ b ∈ On a = suc ⁡ b ↔ ∃ b ∈ On A = suc ⁡ b
5 4 elrab ⊢ A ∈ a ∈ On | ∃ b ∈ On a = suc ⁡ b ↔ A ∈ On ∧ ∃ b ∈ On A = suc ⁡ b
6 5 simprbi ⊢ A ∈ a ∈ On | ∃ b ∈ On a = suc ⁡ b → ∃ b ∈ On A = suc ⁡ b
7 2 6 nsyl ⊢ Ord ⁡ A ∧ A ≠ ∅ ∧ ¬ ∃ b ∈ On A = suc ⁡ b → ¬ A ∈ a ∈ On | ∃ b ∈ On a = suc ⁡ b
8 1 7 sylbi ⊢ Lim ⁡ A → ¬ A ∈ a ∈ On | ∃ b ∈ On a = suc ⁡ b