Description: A strictly monotone ordinal function preserves strict ordering. (Contributed by Mario Carneiro, 4-Mar-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | smoord | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | smodm2 | |
|
2 | simprl | |
|
3 | ordelord | |
|
4 | 1 2 3 | syl2an2r | |
5 | simprr | |
|
6 | ordelord | |
|
7 | 1 5 6 | syl2an2r | |
8 | ordtri3or | |
|
9 | simp3 | |
|
10 | smoel2 | |
|
11 | 10 | expr | |
12 | 11 | adantrl | |
13 | 12 | 3impia | |
14 | 9 13 | 2thd | |
15 | 14 | 3expia | |
16 | ordirr | |
|
17 | 4 16 | syl | |
18 | 17 | 3adant3 | |
19 | simp3 | |
|
20 | 18 19 | neleqtrd | |
21 | smofvon2 | |
|
22 | 21 | ad2antlr | |
23 | eloni | |
|
24 | ordirr | |
|
25 | 22 23 24 | 3syl | |
26 | 25 | 3adant3 | |
27 | 19 | fveq2d | |
28 | 26 27 | neleqtrd | |
29 | 20 28 | 2falsed | |
30 | 29 | 3expia | |
31 | 7 | 3adant3 | |
32 | ordn2lp | |
|
33 | 31 32 | syl | |
34 | pm3.2 | |
|
35 | 34 | 3ad2ant3 | |
36 | 33 35 | mtod | |
37 | 22 23 | syl | |
38 | 37 | 3adant3 | |
39 | ordn2lp | |
|
40 | 38 39 | syl | |
41 | smoel2 | |
|
42 | 41 | adantrlr | |
43 | 42 | 3impb | |
44 | pm3.21 | |
|
45 | 43 44 | syl | |
46 | 40 45 | mtod | |
47 | 36 46 | 2falsed | |
48 | 47 | 3expia | |
49 | 15 30 48 | 3jaod | |
50 | 8 49 | syl5 | |
51 | 4 7 50 | mp2and | |