Metamath Proof Explorer

Theorem smodm

Description: The domain of a strictly monotone function is an ordinal. (Contributed by Andrew Salmon, 16-Nov-2011)

Ref Expression
Assertion smodm ⊢ Smo ⁡ A → Ord ⁡ dom ⁡ A

Proof

Step Hyp Ref Expression
1 df-smo ⊢ Smo ⁡ A ↔ A : dom ⁡ A ⟶ On ∧ Ord ⁡ dom ⁡ A ∧ ∀ x ∈ dom ⁡ A ∀ y ∈ dom ⁡ A x ∈ y → A ⁡ x ∈ A ⁡ y
2 1 simp2bi ⊢ Smo ⁡ A → Ord ⁡ dom ⁡ A