Description: The class of ordinals dominated by a given set is an ordinal. Theorem 56 of Suppes p. 227. This theorem can be proved without the axiom of choice, see hartogs . (Contributed by NM, 7-Nov-2003) (Proof modification is discouraged.) Use hartogs instead. (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | ondomon | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | onelon | |
|
2 | vex | |
|
3 | onelss | |
|
4 | 3 | imp | |
5 | ssdomg | |
|
6 | 2 4 5 | mpsyl | |
7 | 1 6 | jca | |
8 | domtr | |
|
9 | 8 | anim2i | |
10 | 9 | anassrs | |
11 | 7 10 | sylan | |
12 | 11 | exp31 | |
13 | 12 | com12 | |
14 | 13 | impd | |
15 | breq1 | |
|
16 | 15 | elrab | |
17 | breq1 | |
|
18 | 17 | elrab | |
19 | 14 16 18 | 3imtr4g | |
20 | 19 | imp | |
21 | 20 | gen2 | |
22 | dftr2 | |
|
23 | 21 22 | mpbir | |
24 | ssrab2 | |
|
25 | ordon | |
|
26 | trssord | |
|
27 | 23 24 25 26 | mp3an | |
28 | elex | |
|
29 | canth2g | |
|
30 | domsdomtr | |
|
31 | 29 30 | sylan2 | |
32 | 31 | expcom | |
33 | 32 | ralrimivw | |
34 | 28 33 | syl | |
35 | ss2rab | |
|
36 | 34 35 | sylibr | |
37 | pwexg | |
|
38 | numth3 | |
|
39 | cardval2 | |
|
40 | 37 38 39 | 3syl | |
41 | fvex | |
|
42 | 40 41 | eqeltrrdi | |
43 | ssexg | |
|
44 | 36 42 43 | syl2anc | |
45 | elong | |
|
46 | 44 45 | syl | |
47 | 27 46 | mpbiri | |