This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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