# Metamath Proof Explorer

## Theorem dif20el

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

Ref Expression
Assertion dif20el ${⊢}{A}\in \left(\mathrm{On}\setminus {2}_{𝑜}\right)\to \varnothing \in {A}$

### Proof

Step Hyp Ref Expression
1 ondif2 ${⊢}{A}\in \left(\mathrm{On}\setminus {2}_{𝑜}\right)↔\left({A}\in \mathrm{On}\wedge {1}_{𝑜}\in {A}\right)$
2 1 simprbi ${⊢}{A}\in \left(\mathrm{On}\setminus {2}_{𝑜}\right)\to {1}_{𝑜}\in {A}$
3 0lt1o ${⊢}\varnothing \in {1}_{𝑜}$
4 eldifi ${⊢}{A}\in \left(\mathrm{On}\setminus {2}_{𝑜}\right)\to {A}\in \mathrm{On}$
5 ontr1 ${⊢}{A}\in \mathrm{On}\to \left(\left(\varnothing \in {1}_{𝑜}\wedge {1}_{𝑜}\in {A}\right)\to \varnothing \in {A}\right)$
6 4 5 syl ${⊢}{A}\in \left(\mathrm{On}\setminus {2}_{𝑜}\right)\to \left(\left(\varnothing \in {1}_{𝑜}\wedge {1}_{𝑜}\in {A}\right)\to \varnothing \in {A}\right)$
7 3 6 mpani ${⊢}{A}\in \left(\mathrm{On}\setminus {2}_{𝑜}\right)\to \left({1}_{𝑜}\in {A}\to \varnothing \in {A}\right)$
8 2 7 mpd ${⊢}{A}\in \left(\mathrm{On}\setminus {2}_{𝑜}\right)\to \varnothing \in {A}$