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 F Fn A Smo F Ord A

Proof

Step Hyp Ref Expression
1 smodm Smo F Ord dom F
2 fndm F Fn A dom F = A
3 ordeq dom F = A Ord dom F Ord A
4 2 3 syl F Fn A Ord dom F Ord A
5 4 biimpa F Fn A Ord dom F Ord A
6 1 5 sylan2 F Fn A Smo F Ord A