This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cfle

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 ⊆ A

Proof

Step Hyp Ref Expression
1 cflecard ⊢ cf ⁡ A ⊆ card ⁡ A
2 cardonle ⊢ A ∈ On → card ⁡ A ⊆ A
3 1 2 sstrid ⊢ A ∈ On → cf ⁡ A ⊆ A
4 cff ⊢ cf : On ⟶ On
5 4 fdmi ⊢ dom ⁡ cf = On
6 5 eleq2i ⊢ A ∈ dom ⁡ cf ↔ A ∈ On
7 ndmfv ⊢ ¬ A ∈ dom ⁡ cf → cf ⁡ A = ∅
8 6 7 sylnbir ⊢ ¬ A ∈ On → cf ⁡ A = ∅
9 0ss ⊢ ∅ ⊆ A
10 8 9 eqsstrdi ⊢ ¬ A ∈ On → cf ⁡ A ⊆ A
11 3 10 pm2.61i ⊢ cf ⁡ A ⊆ A