Metamath Proof Explorer

Theorem ord0eln0

Description: A nonempty ordinal contains the empty set. (Contributed by NM, 25-Nov-1995)

Ref Expression
Assertion ord0eln0 ⊢ Ord ⁡ A → ∅ ∈ A ↔ A ≠ ∅

Proof

Step Hyp Ref Expression
1 ne0i ⊢ ∅ ∈ A → A ≠ ∅
2 ord0 ⊢ Ord ⁡ ∅
3 noel ⊢ ¬ A ∈ ∅
4 ordtri2 ⊢ Ord ⁡ A ∧ Ord ⁡ ∅ → A ∈ ∅ ↔ ¬ A = ∅ ∨ ∅ ∈ A
5 4 con2bid ⊢ Ord ⁡ A ∧ Ord ⁡ ∅ → A = ∅ ∨ ∅ ∈ A ↔ ¬ A ∈ ∅
6 3 5 mpbiri ⊢ Ord ⁡ A ∧ Ord ⁡ ∅ → A = ∅ ∨ ∅ ∈ A
7 2 6 mpan2 ⊢ Ord ⁡ A → A = ∅ ∨ ∅ ∈ A
8 neor ⊢ A = ∅ ∨ ∅ ∈ A ↔ A ≠ ∅ → ∅ ∈ A
9 7 8 sylib ⊢ Ord ⁡ A → A ≠ ∅ → ∅ ∈ A
10 1 9 impbid2 ⊢ Ord ⁡ A → ∅ ∈ A ↔ A ≠ ∅