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 ( 𝐴 ∈ ( On ∖ 2o ) → ∅ ∈ 𝐴 )

Proof

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