Metamath Proof Explorer


Theorem cardcf

Description: Cofinality is a cardinal number. Proposition 11.11 of TakeutiZaring p. 103. (Contributed by NM, 24-Apr-2004) (Revised by Mario Carneiro, 15-Sep-2013)

Ref Expression
Assertion cardcf
|- ( card ` ( cf ` A ) ) = ( cf ` A )

Proof

Step Hyp Ref Expression
1 cfval
 |-  ( A e. On -> ( cf ` A ) = |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } )
2 vex
 |-  v e. _V
3 eqeq1
 |-  ( x = v -> ( x = ( card ` y ) <-> v = ( card ` y ) ) )
4 3 anbi1d
 |-  ( x = v -> ( ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) <-> ( v = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) ) )
5 4 exbidv
 |-  ( x = v -> ( E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) <-> E. y ( v = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) ) )
6 2 5 elab
 |-  ( v e. { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } <-> E. y ( v = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) )
7 fveq2
 |-  ( v = ( card ` y ) -> ( card ` v ) = ( card ` ( card ` y ) ) )
8 cardidm
 |-  ( card ` ( card ` y ) ) = ( card ` y )
9 7 8 eqtrdi
 |-  ( v = ( card ` y ) -> ( card ` v ) = ( card ` y ) )
10 eqeq2
 |-  ( v = ( card ` y ) -> ( ( card ` v ) = v <-> ( card ` v ) = ( card ` y ) ) )
11 9 10 mpbird
 |-  ( v = ( card ` y ) -> ( card ` v ) = v )
12 11 adantr
 |-  ( ( v = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) -> ( card ` v ) = v )
13 12 exlimiv
 |-  ( E. y ( v = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) -> ( card ` v ) = v )
14 6 13 sylbi
 |-  ( v e. { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } -> ( card ` v ) = v )
15 cardon
 |-  ( card ` v ) e. On
16 14 15 eqeltrrdi
 |-  ( v e. { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } -> v e. On )
17 16 ssriv
 |-  { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } C_ On
18 fvex
 |-  ( cf ` A ) e. _V
19 1 18 eqeltrrdi
 |-  ( A e. On -> |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } e. _V )
20 intex
 |-  ( { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } =/= (/) <-> |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } e. _V )
21 19 20 sylibr
 |-  ( A e. On -> { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } =/= (/) )
22 onint
 |-  ( ( { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } C_ On /\ { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } =/= (/) ) -> |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } e. { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } )
23 17 21 22 sylancr
 |-  ( A e. On -> |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } e. { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } )
24 1 23 eqeltrd
 |-  ( A e. On -> ( cf ` A ) e. { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } )
25 fveq2
 |-  ( v = ( cf ` A ) -> ( card ` v ) = ( card ` ( cf ` A ) ) )
26 id
 |-  ( v = ( cf ` A ) -> v = ( cf ` A ) )
27 25 26 eqeq12d
 |-  ( v = ( cf ` A ) -> ( ( card ` v ) = v <-> ( card ` ( cf ` A ) ) = ( cf ` A ) ) )
28 27 14 vtoclga
 |-  ( ( cf ` A ) e. { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } -> ( card ` ( cf ` A ) ) = ( cf ` A ) )
29 24 28 syl
 |-  ( A e. On -> ( card ` ( cf ` A ) ) = ( cf ` A ) )
30 cff
 |-  cf : On --> On
31 30 fdmi
 |-  dom cf = On
32 31 eleq2i
 |-  ( A e. dom cf <-> A e. On )
33 ndmfv
 |-  ( -. A e. dom cf -> ( cf ` A ) = (/) )
34 32 33 sylnbir
 |-  ( -. A e. On -> ( cf ` A ) = (/) )
35 card0
 |-  ( card ` (/) ) = (/)
36 fveq2
 |-  ( ( cf ` A ) = (/) -> ( card ` ( cf ` A ) ) = ( card ` (/) ) )
37 id
 |-  ( ( cf ` A ) = (/) -> ( cf ` A ) = (/) )
38 35 36 37 3eqtr4a
 |-  ( ( cf ` A ) = (/) -> ( card ` ( cf ` A ) ) = ( cf ` A ) )
39 34 38 syl
 |-  ( -. A e. On -> ( card ` ( cf ` A ) ) = ( cf ` A ) )
40 29 39 pm2.61i
 |-  ( card ` ( cf ` A ) ) = ( cf ` A )