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

Theorem smoiso 6375
 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
Dummy variables are mutually distinct and distinct from all other variables.

Proof of Theorem smoiso
StepHypRef Expression
1 isof1o 5784 . . . 4
2 f1of 5438 . . . 4
31, 2syl 17 . . 3
4 ffdm 5369 . . . . . 6
54simpld 447 . . . . 5
6 fss 5363 . . . . 5
75, 6sylan 459 . . . 4
93, 8syl3an1 1217 . 2
10 fdm 5359 . . . . . . 7
1110eqcomd 2290 . . . . . 6
121, 2, 113syl 20 . . . . 5
13 ordeq 4399 . . . . 5
1412, 13syl 17 . . . 4
1514biimpa 472 . . 3
1710eleq2d 2352 . . . . . . 7
1810eleq2d 2352 . . . . . . 7
1917, 18anbi12d 693 . . . . . 6
201, 2, 193syl 20 . . . . 5
21 isorel 5785 . . . . . . . 8
22 epel 4308 . . . . . . . 8
23 fvex 5500 . . . . . . . . 9
2423epelc 4307 . . . . . . . 8
2521, 22, 243bitr3g 280 . . . . . . 7
2625biimpd 200 . . . . . 6
2726ex 425 . . . . 5
2820, 27sylbid 208 . . . 4
2928ralrimivv 2636 . . 3