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 -> ( (/) e. A <-> A =/= (/) ) )

Proof

Step Hyp Ref Expression
1 ne0i 
 |-  ( (/) e. A -> A =/= (/) )
2 ord0 
 |-  Ord (/)
3 noel 
 |-  -. A e. (/)
4 ordtri2 
 |-  ( ( Ord A /\ Ord (/) ) -> ( A e. (/) <-> -. ( A = (/) \/ (/) e. A ) ) )
5 4 con2bid 
 |-  ( ( Ord A /\ Ord (/) ) -> ( ( A = (/) \/ (/) e. A ) <-> -. A e. (/) ) )
6 3 5 mpbiri 
 |-  ( ( Ord A /\ Ord (/) ) -> ( A = (/) \/ (/) e. A ) )
7 2 6 mpan2 
 |-  ( Ord A -> ( A = (/) \/ (/) e. A ) )
8 neor 
 |-  ( ( A = (/) \/ (/) e. A ) <-> ( A =/= (/) -> (/) e. A ) )
9 7 8 sylib 
 |-  ( Ord A -> ( A =/= (/) -> (/) e. A ) )
10 1 9 impbid2 
 |-  ( Ord A -> ( (/) e. A <-> A =/= (/) ) )