Metamath Proof Explorer


Theorem ordgt0ge1

Description: Two ways to express that an ordinal class is positive. (Contributed by NM, 21-Dec-2004)

Ref Expression
Assertion ordgt0ge1 ( Ord 𝐴 → ( ∅ ∈ 𝐴 ↔ 1o𝐴 ) )

Proof

Step Hyp Ref Expression
1 0elon ∅ ∈ On
2 ordelsuc ( ( ∅ ∈ On ∧ Ord 𝐴 ) → ( ∅ ∈ 𝐴 ↔ suc ∅ ⊆ 𝐴 ) )
3 1 2 mpan ( Ord 𝐴 → ( ∅ ∈ 𝐴 ↔ suc ∅ ⊆ 𝐴 ) )
4 df-1o 1o = suc ∅
5 4 sseq1i ( 1o𝐴 ↔ suc ∅ ⊆ 𝐴 )
6 3 5 bitr4di ( Ord 𝐴 → ( ∅ ∈ 𝐴 ↔ 1o𝐴 ) )