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