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

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 𝐴 → ∅ ∈ suc 𝐴 )

Proof

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