Metamath Proof Explorer

Theorem 0elsuc

Description: The successor of an ordinal class contains the empty set. (Contributed by NM, 4-Apr-1995)

Ref Expression
Assertion 0elsuc ⊢ Ord ⁡ A → ∅ ∈ suc ⁡ A

Proof

Step Hyp Ref Expression
1 ordsuc ⊢ Ord ⁡ A ↔ Ord ⁡ suc ⁡ A
2 nsuceq0 ⊢ suc ⁡ A ≠ ∅
3 ord0eln0 ⊢ Ord ⁡ suc ⁡ A → ∅ ∈ suc ⁡ A ↔ suc ⁡ A ≠ ∅
4 2 3 mpbiri ⊢ Ord ⁡ suc ⁡ A → ∅ ∈ suc ⁡ A
5 1 4 sylbi ⊢ Ord ⁡ A → ∅ ∈ suc ⁡ A