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 On
5 1 4 ax-mp A On
6 3 5 eqsstri ran I A On
7 df-f I A : A On I A Fn A ran I A On
8 2 6 7 mpbir2an I A : A On
9 fvresi x A I A x = x
10 9 adantr x A y A I A x = x
11 fvresi y A I A y = y
12 11 adantl x A y A I A y = y
13 10 12 eleq12d x A y A I A x I A y x y
14 13 biimprd x A y A x y I A x I A y
15 dmresi dom I A = A
16 8 1 14 15 issmo Smo I A