Theorem smofvon2

Description: The function values of a strictly monotone ordinal function are ordinals. (Contributed by Mario Carneiro, 12-Mar-2013)

	Ref	Expression
Assertion	smofvon2	|- ( Smo F -> ( F ` B ) e. On )

Proof

Step	Hyp	Ref	Expression
1		dfsmo2	|- ( Smo F <-> ( F : dom F --> On /\ Ord dom F /\ A. x e. dom F A. y e. x ( F ` y ) e. ( F ` x ) ) )
2	1	simp1bi	|- ( Smo F -> F : dom F --> On )
3		ffvelrn	|- ( ( F : dom F --> On /\ B e. dom F ) -> ( F ` B ) e. On )
4	3	expcom	|- ( B e. dom F -> ( F : dom F --> On -> ( F ` B ) e. On ) )
5	2 4	syl5	|- ( B e. dom F -> ( Smo F -> ( F ` B ) e. On ) )
6		ndmfv	|- ( -. B e. dom F -> ( F ` B ) = (/) )
7		0elon	|- (/) e. On
8	6 7	eqeltrdi	|- ( -. B e. dom F -> ( F ` B ) e. On )
9	8	a1d	|- ( -. B e. dom F -> ( Smo F -> ( F ` B ) e. On ) )
10	5 9	pm2.61i	|- ( Smo F -> ( F ` B ) e. On )