This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cflecard

Description: Cofinality is bounded by the cardinality of its argument. (Contributed by NM, 24-Apr-2004) (Revised by Mario Carneiro, 15-Sep-2013)

Ref Expression
Assertion cflecard 
|- ( cf ` A ) C_ ( card ` 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 df-sn 
 |-  { ( card ` A ) } = { x | x = ( card ` A ) }
3 ssid 
 |-  A C_ A
4 ssid 
 |-  z C_ z
5 sseq2 
 |-  ( w = z -> ( z C_ w <-> z C_ z ) )
6 5 rspcev 
 |-  ( ( z e. A /\ z C_ z ) -> E. w e. A z C_ w )
7 4 6 mpan2 
 |-  ( z e. A -> E. w e. A z C_ w )
8 7 rgen 
 |-  A. z e. A E. w e. A z C_ w
9 3 8 pm3.2i 
 |-  ( A C_ A /\ A. z e. A E. w e. A z C_ w )
10 fveq2 
 |-  ( y = A -> ( card ` y ) = ( card ` A ) )
11 10 eqeq2d 
 |-  ( y = A -> ( x = ( card ` y ) <-> x = ( card ` A ) ) )
12 sseq1 
 |-  ( y = A -> ( y C_ A <-> A C_ A ) )
13 rexeq 
 |-  ( y = A -> ( E. w e. y z C_ w <-> E. w e. A z C_ w ) )
14 13 ralbidv 
 |-  ( y = A -> ( A. z e. A E. w e. y z C_ w <-> A. z e. A E. w e. A z C_ w ) )
15 12 14 anbi12d 
 |-  ( y = A -> ( ( y C_ A /\ A. z e. A E. w e. y z C_ w ) <-> ( A C_ A /\ A. z e. A E. w e. A z C_ w ) ) )
16 11 15 anbi12d 
 |-  ( y = A -> ( ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) <-> ( x = ( card ` A ) /\ ( A C_ A /\ A. z e. A E. w e. A z C_ w ) ) ) )
17 16 spcegv 
 |-  ( A e. On -> ( ( x = ( card ` A ) /\ ( A C_ A /\ A. z e. A E. w e. A z C_ w ) ) -> E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) ) )
18 9 17 mpan2i 
 |-  ( A e. On -> ( x = ( card ` A ) -> E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) ) )
19 18 ss2abdv 
 |-  ( A e. On -> { x | x = ( card ` A ) } C_ { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } )
20 2 19 eqsstrid 
 |-  ( A e. On -> { ( card ` A ) } C_ { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } )
21 intss 
 |-  ( { ( card ` A ) } C_ { 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 ) ) } C_ |^| { ( card ` A ) } )
22 20 21 syl 
 |-  ( A e. On -> |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } C_ |^| { ( card ` A ) } )
23 fvex 
 |-  ( card ` A ) e. _V
24 23 intsn 
 |-  |^| { ( card ` A ) } = ( card ` A )
25 22 24 sseqtrdi 
 |-  ( A e. On -> |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } C_ ( card ` A ) )
26 1 25 eqsstrd 
 |-  ( A e. On -> ( cf ` A ) C_ ( card ` A ) )
27 cff 
 |-  cf : On --> On
28 27 fdmi 
 |-  dom cf = On
29 28 eleq2i 
 |-  ( A e. dom cf <-> A e. On )
30 ndmfv 
 |-  ( -. A e. dom cf -> ( cf ` A ) = (/) )
31 29 30 sylnbir 
 |-  ( -. A e. On -> ( cf ` A ) = (/) )
32 0ss 
 |-  (/) C_ ( card ` A )
33 31 32 eqsstrdi 
 |-  ( -. A e. On -> ( cf ` A ) C_ ( card ` A ) )
34 26 33 pm2.61i 
 |-  ( cf ` A ) C_ ( card ` A )