Description: Cofinality is bounded by the cardinality of its argument. (Contributed by NM, 24-Apr-2004) (Revised by Mario Carneiro, 15-Sep-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | cflecard | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cfval | |
|
2 | df-sn | |
|
3 | ssid | |
|
4 | ssid | |
|
5 | sseq2 | |
|
6 | 5 | rspcev | |
7 | 4 6 | mpan2 | |
8 | 7 | rgen | |
9 | 3 8 | pm3.2i | |
10 | fveq2 | |
|
11 | 10 | eqeq2d | |
12 | sseq1 | |
|
13 | rexeq | |
|
14 | 13 | ralbidv | |
15 | 12 14 | anbi12d | |
16 | 11 15 | anbi12d | |
17 | 16 | spcegv | |
18 | 9 17 | mpan2i | |
19 | 18 | ss2abdv | |
20 | 2 19 | eqsstrid | |
21 | intss | |
|
22 | 20 21 | syl | |
23 | fvex | |
|
24 | 23 | intsn | |
25 | 22 24 | sseqtrdi | |
26 | 1 25 | eqsstrd | |
27 | cff | |
|
28 | 27 | fdmi | |
29 | 28 | eleq2i | |
30 | ndmfv | |
|
31 | 29 30 | sylnbir | |
32 | 0ss | |
|
33 | 31 32 | eqsstrdi | |
34 | 26 33 | pm2.61i | |