Metamath Proof Explorer

Theorem cfidm

Description: The cofinality function is idempotent. (Contributed by Mario Carneiro, 7-Mar-2013) (Revised by Mario Carneiro, 15-Sep-2013)

Ref Expression
Assertion cfidm ⊢ cf ⁡ cf ⁡ A = cf ⁡ A

Proof

Step Hyp Ref Expression
1 cfle ⊢ cf ⁡ cf ⁡ A ⊆ cf ⁡ A
2 1 a1i ⊢ A ∈ On → cf ⁡ cf ⁡ A ⊆ cf ⁡ A
3 cfsmo ⊢ A ∈ On → ∃ f f : cf ⁡ A ⟶ A ∧ Smo ⁡ f ∧ ∀ x ∈ A ∃ y ∈ cf ⁡ A x ⊆ f ⁡ y
4 cfon ⊢ cf ⁡ A ∈ On
5 cfcoflem ⊢ A ∈ On ∧ cf ⁡ A ∈ On → ∃ f f : cf ⁡ A ⟶ A ∧ Smo ⁡ f ∧ ∀ x ∈ A ∃ y ∈ cf ⁡ A x ⊆ f ⁡ y → cf ⁡ A ⊆ cf ⁡ cf ⁡ A
6 4 5 mpan2 ⊢ A ∈ On → ∃ f f : cf ⁡ A ⟶ A ∧ Smo ⁡ f ∧ ∀ x ∈ A ∃ y ∈ cf ⁡ A x ⊆ f ⁡ y → cf ⁡ A ⊆ cf ⁡ cf ⁡ A
7 3 6 mpd ⊢ A ∈ On → cf ⁡ A ⊆ cf ⁡ cf ⁡ A
8 2 7 eqssd ⊢ A ∈ On → cf ⁡ cf ⁡ A = cf ⁡ A
9 cf0 ⊢ cf ⁡ ∅ = ∅
10 cff ⊢ cf : On ⟶ On
11 10 fdmi ⊢ dom ⁡ cf = On
12 11 eleq2i ⊢ A ∈ dom ⁡ cf ↔ A ∈ On
13 ndmfv ⊢ ¬ A ∈ dom ⁡ cf → cf ⁡ A = ∅
14 12 13 sylnbir ⊢ ¬ A ∈ On → cf ⁡ A = ∅
15 14 fveq2d ⊢ ¬ A ∈ On → cf ⁡ cf ⁡ A = cf ⁡ ∅
16 9 15 14 3eqtr4a ⊢ ¬ A ∈ On → cf ⁡ cf ⁡ A = cf ⁡ A
17 8 16 pm2.61i ⊢ cf ⁡ cf ⁡ A = cf ⁡ A