Theorem smofvon

Description: If B is a strictly monotone ordinal function, and A is in the domain of B , then the value of the function at A is an ordinal. (Contributed by Andrew Salmon, 20-Nov-2011)

	Ref	Expression
Assertion	smofvon	|- ( ( Smo B /\ A e. dom B ) -> ( B ` A ) e. On )

Proof

Step	Hyp	Ref	Expression
1		df-smo	|- ( Smo B <-> ( B : dom B --> On /\ Ord dom B /\ A. x e. dom B A. y e. dom B ( x e. y -> ( B ` x ) e. ( B ` y ) ) ) )
2	1	simp1bi	|- ( Smo B -> B : dom B --> On )
3	2	ffvelrnda	|- ( ( Smo B /\ A e. dom B ) -> ( B ` A ) e. On )