Metamath Proof Explorer

Theorem omsmo

Description: A strictly monotonic ordinal function on the set of natural numbers is one-to-one. (Contributed by NM, 30-Nov-2003) (Revised by David Abernethy, 1-Jan-2014)

Ref Expression
Assertion omsmo 
|- ( ( ( A C_ On /\ F : _om --> A ) /\ A. x e. _om ( F ` x ) e. ( F ` suc x ) ) -> F : _om -1-1-> A )

Proof

Step Hyp Ref Expression
1 simplr 
 |-  ( ( ( A C_ On /\ F : _om --> A ) /\ A. x e. _om ( F ` x ) e. ( F ` suc x ) ) -> F : _om --> A )
2 omsmolem 
 |-  ( z e. _om -> ( ( ( A C_ On /\ F : _om --> A ) /\ A. x e. _om ( F ` x ) e. ( F ` suc x ) ) -> ( y e. z -> ( F ` y ) e. ( F ` z ) ) ) )
3 2 adantl 
 |-  ( ( y e. _om /\ z e. _om ) -> ( ( ( A C_ On /\ F : _om --> A ) /\ A. x e. _om ( F ` x ) e. ( F ` suc x ) ) -> ( y e. z -> ( F ` y ) e. ( F ` z ) ) ) )
4 3 imp 
 |-  ( ( ( y e. _om /\ z e. _om ) /\ ( ( A C_ On /\ F : _om --> A ) /\ A. x e. _om ( F ` x ) e. ( F ` suc x ) ) ) -> ( y e. z -> ( F ` y ) e. ( F ` z ) ) )
5 omsmolem 
 |-  ( y e. _om -> ( ( ( A C_ On /\ F : _om --> A ) /\ A. x e. _om ( F ` x ) e. ( F ` suc x ) ) -> ( z e. y -> ( F ` z ) e. ( F ` y ) ) ) )
6 5 adantr 
 |-  ( ( y e. _om /\ z e. _om ) -> ( ( ( A C_ On /\ F : _om --> A ) /\ A. x e. _om ( F ` x ) e. ( F ` suc x ) ) -> ( z e. y -> ( F ` z ) e. ( F ` y ) ) ) )
7 6 imp 
 |-  ( ( ( y e. _om /\ z e. _om ) /\ ( ( A C_ On /\ F : _om --> A ) /\ A. x e. _om ( F ` x ) e. ( F ` suc x ) ) ) -> ( z e. y -> ( F ` z ) e. ( F ` y ) ) )
8 4 7 orim12d 
 |-  ( ( ( y e. _om /\ z e. _om ) /\ ( ( A C_ On /\ F : _om --> A ) /\ A. x e. _om ( F ` x ) e. ( F ` suc x ) ) ) -> ( ( y e. z \/ z e. y ) -> ( ( F ` y ) e. ( F ` z ) \/ ( F ` z ) e. ( F ` y ) ) ) )
9 8 ancoms 
 |-  ( ( ( ( A C_ On /\ F : _om --> A ) /\ A. x e. _om ( F ` x ) e. ( F ` suc x ) ) /\ ( y e. _om /\ z e. _om ) ) -> ( ( y e. z \/ z e. y ) -> ( ( F ` y ) e. ( F ` z ) \/ ( F ` z ) e. ( F ` y ) ) ) )
10 9 con3d 
 |-  ( ( ( ( A C_ On /\ F : _om --> A ) /\ A. x e. _om ( F ` x ) e. ( F ` suc x ) ) /\ ( y e. _om /\ z e. _om ) ) -> ( -. ( ( F ` y ) e. ( F ` z ) \/ ( F ` z ) e. ( F ` y ) ) -> -. ( y e. z \/ z e. y ) ) )
11 ffvelcdm 
 |-  ( ( F : _om --> A /\ y e. _om ) -> ( F ` y ) e. A )
12 ssel 
 |-  ( A C_ On -> ( ( F ` y ) e. A -> ( F ` y ) e. On ) )
13 11 12 syl5 
 |-  ( A C_ On -> ( ( F : _om --> A /\ y e. _om ) -> ( F ` y ) e. On ) )
14 13 expdimp 
 |-  ( ( A C_ On /\ F : _om --> A ) -> ( y e. _om -> ( F ` y ) e. On ) )
15 eloni 
 |-  ( ( F ` y ) e. On -> Ord ( F ` y ) )
16 14 15 syl6 
 |-  ( ( A C_ On /\ F : _om --> A ) -> ( y e. _om -> Ord ( F ` y ) ) )
17 ffvelcdm 
 |-  ( ( F : _om --> A /\ z e. _om ) -> ( F ` z ) e. A )
18 ssel 
 |-  ( A C_ On -> ( ( F ` z ) e. A -> ( F ` z ) e. On ) )
19 17 18 syl5 
 |-  ( A C_ On -> ( ( F : _om --> A /\ z e. _om ) -> ( F ` z ) e. On ) )
20 19 expdimp 
 |-  ( ( A C_ On /\ F : _om --> A ) -> ( z e. _om -> ( F ` z ) e. On ) )
21 eloni 
 |-  ( ( F ` z ) e. On -> Ord ( F ` z ) )
22 20 21 syl6 
 |-  ( ( A C_ On /\ F : _om --> A ) -> ( z e. _om -> Ord ( F ` z ) ) )
23 16 22 anim12d 
 |-  ( ( A C_ On /\ F : _om --> A ) -> ( ( y e. _om /\ z e. _om ) -> ( Ord ( F ` y ) /\ Ord ( F ` z ) ) ) )
24 23 imp 
 |-  ( ( ( A C_ On /\ F : _om --> A ) /\ ( y e. _om /\ z e. _om ) ) -> ( Ord ( F ` y ) /\ Ord ( F ` z ) ) )
25 ordtri3 
 |-  ( ( Ord ( F ` y ) /\ Ord ( F ` z ) ) -> ( ( F ` y ) = ( F ` z ) <-> -. ( ( F ` y ) e. ( F ` z ) \/ ( F ` z ) e. ( F ` y ) ) ) )
26 24 25 syl 
 |-  ( ( ( A C_ On /\ F : _om --> A ) /\ ( y e. _om /\ z e. _om ) ) -> ( ( F ` y ) = ( F ` z ) <-> -. ( ( F ` y ) e. ( F ` z ) \/ ( F ` z ) e. ( F ` y ) ) ) )
27 26 adantlr 
 |-  ( ( ( ( A C_ On /\ F : _om --> A ) /\ A. x e. _om ( F ` x ) e. ( F ` suc x ) ) /\ ( y e. _om /\ z e. _om ) ) -> ( ( F ` y ) = ( F ` z ) <-> -. ( ( F ` y ) e. ( F ` z ) \/ ( F ` z ) e. ( F ` y ) ) ) )
28 nnord 
 |-  ( y e. _om -> Ord y )
29 nnord 
 |-  ( z e. _om -> Ord z )
30 ordtri3 
 |-  ( ( Ord y /\ Ord z ) -> ( y = z <-> -. ( y e. z \/ z e. y ) ) )
31 28 29 30 syl2an 
 |-  ( ( y e. _om /\ z e. _om ) -> ( y = z <-> -. ( y e. z \/ z e. y ) ) )
32 31 adantl 
 |-  ( ( ( ( A C_ On /\ F : _om --> A ) /\ A. x e. _om ( F ` x ) e. ( F ` suc x ) ) /\ ( y e. _om /\ z e. _om ) ) -> ( y = z <-> -. ( y e. z \/ z e. y ) ) )
33 10 27 32 3imtr4d 
 |-  ( ( ( ( A C_ On /\ F : _om --> A ) /\ A. x e. _om ( F ` x ) e. ( F ` suc x ) ) /\ ( y e. _om /\ z e. _om ) ) -> ( ( F ` y ) = ( F ` z ) -> y = z ) )
34 33 ralrimivva 
 |-  ( ( ( A C_ On /\ F : _om --> A ) /\ A. x e. _om ( F ` x ) e. ( F ` suc x ) ) -> A. y e. _om A. z e. _om ( ( F ` y ) = ( F ` z ) -> y = z ) )
35 dff13 
 |-  ( F : _om -1-1-> A <-> ( F : _om --> A /\ A. y e. _om A. z e. _om ( ( F ` y ) = ( F ` z ) -> y = z ) ) )
36 1 34 35 sylanbrc 
 |-  ( ( ( A C_ On /\ F : _om --> A ) /\ A. x e. _om ( F ` x ) e. ( F ` suc x ) ) -> F : _om -1-1-> A )