Metamath Proof Explorer

Theorem on0eqel

Description: An ordinal number either equals zero or contains zero. (Contributed by NM, 1-Jun-2004)

Ref Expression
Assertion on0eqel ⊢ A ∈ On → A = ∅ ∨ ∅ ∈ A

Proof

Step Hyp Ref Expression
1 0ss ⊢ ∅ ⊆ A
2 0elon ⊢ ∅ ∈ On
3 onsseleq ⊢ ∅ ∈ On ∧ A ∈ On → ∅ ⊆ A ↔ ∅ ∈ A ∨ ∅ = A
4 2 3 mpan ⊢ A ∈ On → ∅ ⊆ A ↔ ∅ ∈ A ∨ ∅ = A
5 1 4 mpbii ⊢ A ∈ On → ∅ ∈ A ∨ ∅ = A
6 eqcom ⊢ ∅ = A ↔ A = ∅
7 6 orbi2i ⊢ ∅ ∈ A ∨ ∅ = A ↔ ∅ ∈ A ∨ A = ∅
8 orcom ⊢ ∅ ∈ A ∨ A = ∅ ↔ A = ∅ ∨ ∅ ∈ A
9 7 8 bitri ⊢ ∅ ∈ A ∨ ∅ = A ↔ A = ∅ ∨ ∅ ∈ A
10 5 9 sylib ⊢ A ∈ On → A = ∅ ∨ ∅ ∈ A