Description: Any class whose elements have bounded rank is a set. Proposition 9.19 of TakeutiZaring p. 80. (Contributed by NM, 13-Oct-2003)
Ref | Expression | ||
---|---|---|---|
Assertion | bndrank | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rankon | |
|
2 | 1 | onordi | |
3 | eloni | |
|
4 | ordsucsssuc | |
|
5 | 2 3 4 | sylancr | |
6 | 1 | onsuci | |
7 | onsuc | |
|
8 | r1ord3 | |
|
9 | 6 7 8 | sylancr | |
10 | 5 9 | sylbid | |
11 | vex | |
|
12 | 11 | rankid | |
13 | ssel | |
|
14 | 10 12 13 | syl6mpi | |
15 | 14 | ralimdv | |
16 | dfss3 | |
|
17 | fvex | |
|
18 | 17 | ssex | |
19 | 16 18 | sylbir | |
20 | 15 19 | syl6 | |
21 | 20 | rexlimiv | |