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 )