Metamath Proof Explorer


Theorem ondif2

Description: Two ways to say that A is an ordinal greater than one. (Contributed by Mario Carneiro, 21-May-2015)

Ref Expression
Assertion ondif2
|- ( A e. ( On \ 2o ) <-> ( A e. On /\ 1o e. A ) )

Proof

Step Hyp Ref Expression
1 eldif
 |-  ( A e. ( On \ 2o ) <-> ( A e. On /\ -. A e. 2o ) )
2 1on
 |-  1o e. On
3 ontri1
 |-  ( ( A e. On /\ 1o e. On ) -> ( A C_ 1o <-> -. 1o e. A ) )
4 onsssuc
 |-  ( ( A e. On /\ 1o e. On ) -> ( A C_ 1o <-> A e. suc 1o ) )
5 df-2o
 |-  2o = suc 1o
6 5 eleq2i
 |-  ( A e. 2o <-> A e. suc 1o )
7 4 6 bitr4di
 |-  ( ( A e. On /\ 1o e. On ) -> ( A C_ 1o <-> A e. 2o ) )
8 3 7 bitr3d
 |-  ( ( A e. On /\ 1o e. On ) -> ( -. 1o e. A <-> A e. 2o ) )
9 2 8 mpan2
 |-  ( A e. On -> ( -. 1o e. A <-> A e. 2o ) )
10 9 con1bid
 |-  ( A e. On -> ( -. A e. 2o <-> 1o e. A ) )
11 10 pm5.32i
 |-  ( ( A e. On /\ -. A e. 2o ) <-> ( A e. On /\ 1o e. A ) )
12 1 11 bitri
 |-  ( A e. ( On \ 2o ) <-> ( A e. On /\ 1o e. A ) )