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 ) ) C_ ( cf ` A )
2 1 a1i 
 |-  ( A e. On -> ( cf ` ( cf ` A ) ) C_ ( cf ` A ) )
3 cfsmo 
 |-  ( A e. On -> E. f ( f : ( cf ` A ) --> A /\ Smo f /\ A. x e. A E. y e. ( cf ` A ) x C_ ( f ` y ) ) )
4 cfon 
 |-  ( cf ` A ) e. On
5 cfcoflem 
 |-  ( ( A e. On /\ ( cf ` A ) e. On ) -> ( E. f ( f : ( cf ` A ) --> A /\ Smo f /\ A. x e. A E. y e. ( cf ` A ) x C_ ( f ` y ) ) -> ( cf ` A ) C_ ( cf ` ( cf ` A ) ) ) )
6 4 5 mpan2 
 |-  ( A e. On -> ( E. f ( f : ( cf ` A ) --> A /\ Smo f /\ A. x e. A E. y e. ( cf ` A ) x C_ ( f ` y ) ) -> ( cf ` A ) C_ ( cf ` ( cf ` A ) ) ) )
7 3 6 mpd 
 |-  ( A e. On -> ( cf ` A ) C_ ( cf ` ( cf ` A ) ) )
8 2 7 eqssd 
 |-  ( A e. On -> ( cf ` ( cf ` A ) ) = ( cf ` A ) )
9 cf0 
 |-  ( cf ` (/) ) = (/)
10 cff 
 |-  cf : On --> On
11 10 fdmi 
 |-  dom cf = On
12 11 eleq2i 
 |-  ( A e. dom cf <-> A e. On )
13 ndmfv 
 |-  ( -. A e. dom cf -> ( cf ` A ) = (/) )
14 12 13 sylnbir 
 |-  ( -. A e. On -> ( cf ` A ) = (/) )
15 14 fveq2d 
 |-  ( -. A e. On -> ( cf ` ( cf ` A ) ) = ( cf ` (/) ) )
16 9 15 14 3eqtr4a 
 |-  ( -. A e. On -> ( cf ` ( cf ` A ) ) = ( cf ` A ) )
17 8 16 pm2.61i 
 |-  ( cf ` ( cf ` A ) ) = ( cf ` A )