Description: The smallest ordinal that strictly dominates a set is a cardinal. (Contributed by NM, 28-Oct-2003) (Revised by Mario Carneiro, 20-Sep-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | cardmin | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | numthcor | |
|
2 | onintrab2 | |
|
3 | 1 2 | sylib | |
4 | onelon | |
|
5 | 4 | ex | |
6 | 3 5 | syl | |
7 | breq2 | |
|
8 | 7 | onnminsb | |
9 | 6 8 | syli | |
10 | vex | |
|
11 | domtri | |
|
12 | 10 11 | mpan | |
13 | 9 12 | sylibrd | |
14 | nfcv | |
|
15 | nfcv | |
|
16 | nfrab1 | |
|
17 | 16 | nfint | |
18 | 14 15 17 | nfbr | |
19 | breq2 | |
|
20 | 18 19 | onminsb | |
21 | 1 20 | syl | |
22 | 13 21 | jctird | |
23 | domsdomtr | |
|
24 | 22 23 | syl6 | |
25 | 24 | ralrimiv | |
26 | iscard | |
|
27 | 3 25 26 | sylanbrc | |