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 ) )