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 )