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 cfcfA=cfA

Proof

Step Hyp Ref Expression
1 cfle cfcfAcfA
2 1 a1i AOncfcfAcfA
3 cfsmo AOnff:cfAASmofxAycfAxfy
4 cfon cfAOn
5 cfcoflem AOncfAOnff:cfAASmofxAycfAxfycfAcfcfA
6 4 5 mpan2 AOnff:cfAASmofxAycfAxfycfAcfcfA
7 3 6 mpd AOncfAcfcfA
8 2 7 eqssd AOncfcfA=cfA
9 cf0 cf=
10 cff cf:OnOn
11 10 fdmi domcf=On
12 11 eleq2i AdomcfAOn
13 ndmfv ¬AdomcfcfA=
14 12 13 sylnbir ¬AOncfA=
15 14 fveq2d ¬AOncfcfA=cf
16 9 15 14 3eqtr4a ¬AOncfcfA=cfA
17 8 16 pm2.61i cfcfA=cfA