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 ‘ 𝐴 )