# Metamath Proof Explorer

## Theorem ord0eln0

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

Ref Expression
Assertion ord0eln0 ${⊢}\mathrm{Ord}{A}\to \left(\varnothing \in {A}↔{A}\ne \varnothing \right)$

### Proof

Step Hyp Ref Expression
1 ne0i ${⊢}\varnothing \in {A}\to {A}\ne \varnothing$
2 ord0 ${⊢}\mathrm{Ord}\varnothing$
3 noel ${⊢}¬{A}\in \varnothing$
4 ordtri2 ${⊢}\left(\mathrm{Ord}{A}\wedge \mathrm{Ord}\varnothing \right)\to \left({A}\in \varnothing ↔¬\left({A}=\varnothing \vee \varnothing \in {A}\right)\right)$
5 4 con2bid ${⊢}\left(\mathrm{Ord}{A}\wedge \mathrm{Ord}\varnothing \right)\to \left(\left({A}=\varnothing \vee \varnothing \in {A}\right)↔¬{A}\in \varnothing \right)$
6 3 5 mpbiri ${⊢}\left(\mathrm{Ord}{A}\wedge \mathrm{Ord}\varnothing \right)\to \left({A}=\varnothing \vee \varnothing \in {A}\right)$
7 2 6 mpan2 ${⊢}\mathrm{Ord}{A}\to \left({A}=\varnothing \vee \varnothing \in {A}\right)$
8 neor ${⊢}\left({A}=\varnothing \vee \varnothing \in {A}\right)↔\left({A}\ne \varnothing \to \varnothing \in {A}\right)$
9 7 8 sylib ${⊢}\mathrm{Ord}{A}\to \left({A}\ne \varnothing \to \varnothing \in {A}\right)$
10 1 9 impbid2 ${⊢}\mathrm{Ord}{A}\to \left(\varnothing \in {A}↔{A}\ne \varnothing \right)$