Description: If F is an isomorphism from an ordinal A onto B , which is a subset of the ordinals, then F is a strictly monotonic function. Exercise 3 in TakeutiZaring p. 50. (Contributed by Andrew Salmon, 24-Nov-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | smoiso | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isof1o | |
|
2 | f1of | |
|
3 | 1 2 | syl | |
4 | ffdm | |
|
5 | 4 | simpld | |
6 | fss | |
|
7 | 5 6 | sylan | |
8 | 7 | 3adant2 | |
9 | 3 8 | syl3an1 | |
10 | fdm | |
|
11 | 10 | eqcomd | |
12 | ordeq | |
|
13 | 1 2 11 12 | 4syl | |
14 | 13 | biimpa | |
15 | 14 | 3adant3 | |
16 | 10 | eleq2d | |
17 | 10 | eleq2d | |
18 | 16 17 | anbi12d | |
19 | 1 2 18 | 3syl | |
20 | isorel | |
|
21 | epel | |
|
22 | fvex | |
|
23 | 22 | epeli | |
24 | 20 21 23 | 3bitr3g | |
25 | 24 | biimpd | |
26 | 25 | ex | |
27 | 19 26 | sylbid | |
28 | 27 | ralrimivv | |
29 | 28 | 3ad2ant1 | |
30 | df-smo | |
|
31 | 9 15 29 30 | syl3anbrc | |