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