Metamath Proof Explorer

Theorem ordge1n0

Description: An ordinal greater than or equal to 1 is nonzero. (Contributed by NM, 21-Dec-2004)

Ref Expression
Assertion ordge1n0 
|- ( Ord A -> ( 1o C_ A <-> A =/= (/) ) )

Proof

Step Hyp Ref Expression
1 ordgt0ge1 
 |-  ( Ord A -> ( (/) e. A <-> 1o C_ A ) )
2 ord0eln0 
 |-  ( Ord A -> ( (/) e. A <-> A =/= (/) ) )
3 1 2 bitr3d 
 |-  ( Ord A -> ( 1o C_ A <-> A =/= (/) ) )