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 ) → ∅ ∈ 𝐴 )