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