Metamath Proof Explorer

Theorem ordgt0ge1

Description: Two ways to express that an ordinal class is positive. (Contributed by NM, 21-Dec-2004)

Ref Expression
Assertion ordgt0ge1 
|- ( Ord A -> ( (/) e. A <-> 1o C_ A ) )

Proof

Step Hyp Ref Expression
1 0elon 
 |-  (/) e. On
2 ordelsuc 
 |-  ( ( (/) e. On /\ Ord A ) -> ( (/) e. A <-> suc (/) C_ A ) )
3 1 2 mpan 
 |-  ( Ord A -> ( (/) e. A <-> suc (/) C_ A ) )
4 df-1o 
 |-  1o = suc (/)
5 4 sseq1i 
 |-  ( 1o C_ A <-> suc (/) C_ A )
6 3 5 bitr4di 
 |-  ( Ord A -> ( (/) e. A <-> 1o C_ A ) )