Description: Value of the cofinality function at 0. Exercise 2 of TakeutiZaring p. 102. (Contributed by NM, 16-Apr-2004)
Ref | Expression | ||
---|---|---|---|
Assertion | cf0 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cfub | |
|
2 | 0ss | |
|
3 | 2 | biantru | |
4 | ss0b | |
|
5 | 3 4 | bitr3i | |
6 | 5 | anbi1ci | |
7 | 6 | exbii | |
8 | 0ex | |
|
9 | fveq2 | |
|
10 | 9 | eqeq2d | |
11 | 8 10 | ceqsexv | |
12 | card0 | |
|
13 | 12 | eqeq2i | |
14 | 7 11 13 | 3bitri | |
15 | 14 | abbii | |
16 | df-sn | |
|
17 | 15 16 | eqtr4i | |
18 | 17 | inteqi | |
19 | 8 | intsn | |
20 | 18 19 | eqtri | |
21 | 1 20 | sseqtri | |
22 | ss0b | |
|
23 | 21 22 | mpbi | |