Theorem dif20el

Description: An ordinal greater than one is greater than zero. (Contributed by Mario Carneiro, 25-May-2015)

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

Proof

Step	Hyp	Ref	Expression
1		ondif2	|- ( A e. ( On \ 2o ) <-> ( A e. On /\ 1o e. A ) )
2	1	simprbi	|- ( A e. ( On \ 2o ) -> 1o e. A )
3		0lt1o	|- (/) e. 1o
4		eldifi	|- ( A e. ( On \ 2o ) -> A e. On )
5		ontr1	|- ( A e. On -> ( ( (/) e. 1o /\ 1o e. A ) -> (/) e. A ) )
6	4 5	syl	|- ( A e. ( On \ 2o ) -> ( ( (/) e. 1o /\ 1o e. A ) -> (/) e. A ) )
7	3 6	mpani	|- ( A e. ( On \ 2o ) -> ( 1o e. A -> (/) e. A ) )
8	2 7	mpd	|- ( A e. ( On \ 2o ) -> (/) e. A )