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

Theorem smoiso 6379
 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
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isof1o 5822 . . . 4
2 f1of 5472 . . . 4
31, 2syl 15 . . 3
4 ffdm 5403 . . . . . 6
54simpld 445 . . . . 5
6 fss 5397 . . . . 5
75, 6sylan 457 . . . 4
93, 8syl3an1 1215 . 2
10 fdm 5393 . . . . . . 7
1110eqcomd 2288 . . . . . 6
121, 2, 113syl 18 . . . . 5
13 ordeq 4399 . . . . 5
1412, 13syl 15 . . . 4
1514biimpa 470 . . 3
1710eleq2d 2350 . . . . . . 7
1810eleq2d 2350 . . . . . . 7
1917, 18anbi12d 691 . . . . . 6
201, 2, 193syl 18 . . . . 5
21 isorel 5823 . . . . . . . 8
22 epel 4308 . . . . . . . 8
23 fvex 5539 . . . . . . . . 9
2423epelc 4307 . . . . . . . 8
2521, 22, 243bitr3g 278 . . . . . . 7
2625biimpd 198 . . . . . 6
2726ex 423 . . . . 5
2820, 27sylbid 206 . . . 4
2928ralrimivv 2634 . . 3