Metamath Proof Explorer

Theorem onnbtwn

Description: There is no set between an ordinal number and its successor. Proposition 7.25 of TakeutiZaring p. 41. Lemma 1.15 of Schloeder p. 2. (Contributed by NM, 9-Jun-1994)

Ref Expression
Assertion onnbtwn ⊢ A ∈ On → ¬ A ∈ B ∧ B ∈ suc ⁡ A

Proof

Step Hyp Ref Expression
1 eloni ⊢ A ∈ On → Ord ⁡ A
2 ordnbtwn ⊢ Ord ⁡ A → ¬ A ∈ B ∧ B ∈ suc ⁡ A
3 1 2 syl ⊢ A ∈ On → ¬ A ∈ B ∧ B ∈ suc ⁡ A