Theorem ordne0gt0

Description: Ordinal zero is less than every non-zero ordinal. Theorem 1.10 of Schloeder p. 2. Closely related to ord0eln0 . (Contributed by RP, 16-Jan-2025)

	Ref	Expression
Assertion	ordne0gt0	⊢ ( ( Ord 𝐴 ∧ 𝐴 ≠ ∅ ) → ∅ ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		ord0eln0	⊢ ( Ord 𝐴 → ( ∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅ ) )
2	1	biimpar	⊢ ( ( Ord 𝐴 ∧ 𝐴 ≠ ∅ ) → ∅ ∈ 𝐴 )