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 )