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 ‘ 𝐴 ) ⊆ 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cflecard | ⊢ ( cf ‘ 𝐴 ) ⊆ ( card ‘ 𝐴 ) | |
2 | cardonle | ⊢ ( 𝐴 ∈ On → ( card ‘ 𝐴 ) ⊆ 𝐴 ) | |
3 | 1 2 | sstrid | ⊢ ( 𝐴 ∈ On → ( cf ‘ 𝐴 ) ⊆ 𝐴 ) |
4 | cff | ⊢ cf : On ⟶ On | |
5 | 4 | fdmi | ⊢ dom cf = On |
6 | 5 | eleq2i | ⊢ ( 𝐴 ∈ dom cf ↔ 𝐴 ∈ On ) |
7 | ndmfv | ⊢ ( ¬ 𝐴 ∈ dom cf → ( cf ‘ 𝐴 ) = ∅ ) | |
8 | 6 7 | sylnbir | ⊢ ( ¬ 𝐴 ∈ On → ( cf ‘ 𝐴 ) = ∅ ) |
9 | 0ss | ⊢ ∅ ⊆ 𝐴 | |
10 | 8 9 | eqsstrdi | ⊢ ( ¬ 𝐴 ∈ On → ( cf ‘ 𝐴 ) ⊆ 𝐴 ) |
11 | 3 10 | pm2.61i | ⊢ ( cf ‘ 𝐴 ) ⊆ 𝐴 |