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 )