Description: The cofinality function is idempotent. (Contributed by Mario Carneiro, 7-Mar-2013) (Revised by Mario Carneiro, 15-Sep-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | cfidm | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cfle | |
|
2 | 1 | a1i | |
3 | cfsmo | |
|
4 | cfon | |
|
5 | cfcoflem | |
|
6 | 4 5 | mpan2 | |
7 | 3 6 | mpd | |
8 | 2 7 | eqssd | |
9 | cf0 | |
|
10 | cff | |
|
11 | 10 | fdmi | |
12 | 11 | eleq2i | |
13 | ndmfv | |
|
14 | 12 13 | sylnbir | |
15 | 14 | fveq2d | |
16 | 9 15 14 | 3eqtr4a | |
17 | 8 16 | pm2.61i | |