Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  smoiso Unicode version

Theorem smoiso 6265
 Description: If is an isomorphism from an ordinal onto , which is a subset of the ordinals, then is a strictly monotonic function. Exercise 3 in [TakeutiZaring] p. 50. (Contributed by Andrew Salmon, 24-Nov-2011.)
Assertion
Ref Expression
smoiso

Proof of Theorem smoiso
StepHypRef Expression
1 isof1o 5674 . . . 4
2 f1of 5329 . . . 4
31, 2syl 17 . . 3
4 ffdm 5260 . . . . . 6
54simpld 447 . . . . 5
6 fss 5254 . . . . 5
75, 6sylan 459 . . . 4
93, 8syl3an1 1220 . 2
10 fdm 5250 . . . . . . 7
1110eqcomd 2258 . . . . . 6
121, 2, 113syl 20 . . . . 5
13 ordeq 4292 . . . . 5
1412, 13syl 17 . . . 4
1514biimpa 472 . . 3
1710eleq2d 2320 . . . . . . 7
1810eleq2d 2320 . . . . . . 7
1917, 18anbi12d 694 . . . . . 6
201, 2, 193syl 20 . . . . 5
21 isorel 5675 . . . . . . . 8
22 epel 4201 . . . . . . . 8
23 fvex 5391 . . . . . . . . 9
2423epelc 4200 . . . . . . . 8
2521, 22, 243bitr3g 280 . . . . . . 7
2625biimpd 200 . . . . . 6
2726ex 425 . . . . 5
2820, 27sylbid 208 . . . 4
2928ralrimivv 2596 . . 3