This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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