This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ffvelcdm 
 |-  ( ( 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 )