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 ⊆ 𝐴 ) )