Description: Cofinality is bounded by its argument. Exercise 1 of TakeutiZaring p. 102. (Contributed by NM, 26-Apr-2004) (Revised by Mario Carneiro, 15-Sep-2013)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | cfle | |- ( cf ` A ) C_ A |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cflecard | |- ( cf ` A ) C_ ( card ` A ) |
|
| 2 | cardonle | |- ( A e. On -> ( card ` A ) C_ A ) |
|
| 3 | 1 2 | sstrid | |- ( A e. On -> ( cf ` A ) C_ A ) |
| 4 | cff | |- cf : On --> On |
|
| 5 | 4 | fdmi | |- dom cf = On |
| 6 | 5 | eleq2i | |- ( A e. dom cf <-> A e. On ) |
| 7 | ndmfv | |- ( -. A e. dom cf -> ( cf ` A ) = (/) ) |
|
| 8 | 6 7 | sylnbir | |- ( -. A e. On -> ( cf ` A ) = (/) ) |
| 9 | 0ss | |- (/) C_ A |
|
| 10 | 8 9 | eqsstrdi | |- ( -. A e. On -> ( cf ` A ) C_ A ) |
| 11 | 3 10 | pm2.61i | |- ( cf ` A ) C_ A |