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