Description: Alternate definition of a strictly monotone ordinal function. (Contributed by Mario Carneiro, 4-Mar-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | dfsmo2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-smo | |
|
2 | ralcom | |
|
3 | impexp | |
|
4 | simpr | |
|
5 | ordtr1 | |
|
6 | 5 | 3impib | |
7 | 6 | 3com23 | |
8 | simp3 | |
|
9 | 7 8 | jca | |
10 | 9 | 3expia | |
11 | 4 10 | impbid2 | |
12 | 11 | imbi1d | |
13 | 3 12 | bitr3id | |
14 | 13 | ralbidv2 | |
15 | 14 | ralbidva | |
16 | 2 15 | bitrid | |
17 | 16 | pm5.32i | |
18 | 17 | anbi2i | |
19 | 3anass | |
|
20 | 3anass | |
|
21 | 18 19 20 | 3bitr4i | |
22 | 1 21 | bitri | |