Metamath Proof Explorer


Theorem smodm2

Description: The domain of a strictly monotone ordinal function is an ordinal. (Contributed by Mario Carneiro, 12-Mar-2013)

Ref Expression
Assertion smodm2 FFnASmoFOrdA

Proof

Step Hyp Ref Expression
1 smodm SmoFOrddomF
2 fndm FFnAdomF=A
3 ordeq domF=AOrddomFOrdA
4 2 3 syl FFnAOrddomFOrdA
5 4 biimpa FFnAOrddomFOrdA
6 1 5 sylan2 FFnASmoFOrdA