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

Metamath Proof Explorer

Theorem iordsmo

Description: The identity relation restricted to the ordinals is a strictly monotone function. (Contributed by Andrew Salmon, 16-Nov-2011)

Ref Expression
Hypothesis iordsmo.1 
|- Ord A
Assertion iordsmo 
|- Smo ( _I |` A )

Proof

Step Hyp Ref Expression
1 iordsmo.1 
 |-  Ord A
2 fnresi 
 |-  ( _I |` A ) Fn A
3 rnresi 
 |-  ran ( _I |` A ) = A
4 ordsson 
 |-  ( Ord A -> A C_ On )
5 1 4 ax-mp 
 |-  A C_ On
6 3 5 eqsstri 
 |-  ran ( _I |` A ) C_ On
7 df-f 
 |-  ( ( _I |` A ) : A --> On <-> ( ( _I |` A ) Fn A /\ ran ( _I |` A ) C_ On ) )
8 2 6 7 mpbir2an 
 |-  ( _I |` A ) : A --> On
9 fvresi 
 |-  ( x e. A -> ( ( _I |` A ) ` x ) = x )
10 9 adantr 
 |-  ( ( x e. A /\ y e. A ) -> ( ( _I |` A ) ` x ) = x )
11 fvresi 
 |-  ( y e. A -> ( ( _I |` A ) ` y ) = y )
12 11 adantl 
 |-  ( ( x e. A /\ y e. A ) -> ( ( _I |` A ) ` y ) = y )
13 10 12 eleq12d 
 |-  ( ( x e. A /\ y e. A ) -> ( ( ( _I |` A ) ` x ) e. ( ( _I |` A ) ` y ) <-> x e. y ) )
14 13 biimprd 
 |-  ( ( x e. A /\ y e. A ) -> ( x e. y -> ( ( _I |` A ) ` x ) e. ( ( _I |` A ) ` y ) ) )
15 dmresi 
 |-  dom ( _I |` A ) = A
16 8 1 14 15 issmo 
 |-  Smo ( _I |` A )