Theorem ordge1n0

Description: An ordinal greater than or equal to 1 is nonzero. (Contributed by NM, 21-Dec-2004)

	Ref	Expression
Assertion	ordge1n0	⊢ ( Ord 𝐴 → ( 1o ⊆ 𝐴 ↔ 𝐴 ≠ ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		ordgt0ge1	⊢ ( Ord 𝐴 → ( ∅ ∈ 𝐴 ↔ 1o ⊆ 𝐴 ) )
2		ord0eln0	⊢ ( Ord 𝐴 → ( ∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅ ) )
3	1 2	bitr3d	⊢ ( Ord 𝐴 → ( 1o ⊆ 𝐴 ↔ 𝐴 ≠ ∅ ) )