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∈On∖2𝑜→∅∈A

Proof

Step Hyp Ref Expression
1 ondif2 ⊢A∈On∖2𝑜↔A∈On∧1𝑜∈A
2 1 simprbi ⊢A∈On∖2𝑜→1𝑜∈A
3 0lt1o ⊢∅∈1𝑜
4 eldifi ⊢A∈On∖2𝑜→A∈On
5 ontr1 ⊢A∈On→∅∈1𝑜∧1𝑜∈A→∅∈A
6 4 5 syl ⊢A∈On∖2𝑜→∅∈1𝑜∧1𝑜∈A→∅∈A
7 3 6 mpani ⊢A∈On∖2𝑜→1𝑜∈A→∅∈A
8 2 7 mpd ⊢A∈On∖2𝑜→∅∈A