Metamath Proof Explorer

Theorem ordne0gt0

Description: Ordinal zero is less than every nonzero ordinal. Theorem 1.10 of Schloeder p. 2. Closely related to ord0eln0 . (Contributed by RP, 16-Jan-2025)

Ref Expression
Assertion ordne0gt0 ⊢ Ord ⁡ A ∧ A ≠ ∅ → ∅ ∈ A

Proof

Step Hyp Ref Expression
1 ord0eln0 ⊢ Ord ⁡ A → ∅ ∈ A ↔ A ≠ ∅
2 1 biimpar ⊢ Ord ⁡ A ∧ A ≠ ∅ → ∅ ∈ A