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

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 ‘ 𝐴 ) ) = ( cf ‘ 𝐴 )

Proof

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