Metamath Proof Explorer


Theorem cfub

Description: An upper bound on cofinality. (Contributed by NM, 25-Apr-2004) (Revised by Mario Carneiro, 15-Sep-2013)

Ref Expression
Assertion cfub
|- ( cf ` A ) C_ |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A C_ U. y ) ) }

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 dfss3
 |-  ( A C_ U. y <-> A. z e. A z e. U. y )
3 ssel
 |-  ( y C_ A -> ( w e. y -> w e. A ) )
4 onelon
 |-  ( ( A e. On /\ w e. A ) -> w e. On )
5 4 ex
 |-  ( A e. On -> ( w e. A -> w e. On ) )
6 3 5 sylan9r
 |-  ( ( A e. On /\ y C_ A ) -> ( w e. y -> w e. On ) )
7 onelss
 |-  ( w e. On -> ( z e. w -> z C_ w ) )
8 6 7 syl6
 |-  ( ( A e. On /\ y C_ A ) -> ( w e. y -> ( z e. w -> z C_ w ) ) )
9 8 imdistand
 |-  ( ( A e. On /\ y C_ A ) -> ( ( w e. y /\ z e. w ) -> ( w e. y /\ z C_ w ) ) )
10 9 ancomsd
 |-  ( ( A e. On /\ y C_ A ) -> ( ( z e. w /\ w e. y ) -> ( w e. y /\ z C_ w ) ) )
11 10 eximdv
 |-  ( ( A e. On /\ y C_ A ) -> ( E. w ( z e. w /\ w e. y ) -> E. w ( w e. y /\ z C_ w ) ) )
12 eluni
 |-  ( z e. U. y <-> E. w ( z e. w /\ w e. y ) )
13 df-rex
 |-  ( E. w e. y z C_ w <-> E. w ( w e. y /\ z C_ w ) )
14 11 12 13 3imtr4g
 |-  ( ( A e. On /\ y C_ A ) -> ( z e. U. y -> E. w e. y z C_ w ) )
15 14 ralimdv
 |-  ( ( A e. On /\ y C_ A ) -> ( A. z e. A z e. U. y -> A. z e. A E. w e. y z C_ w ) )
16 2 15 syl5bi
 |-  ( ( A e. On /\ y C_ A ) -> ( A C_ U. y -> A. z e. A E. w e. y z C_ w ) )
17 16 imdistanda
 |-  ( A e. On -> ( ( y C_ A /\ A C_ U. y ) -> ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) )
18 17 anim2d
 |-  ( A e. On -> ( ( x = ( card ` y ) /\ ( y C_ A /\ A C_ U. y ) ) -> ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) ) )
19 18 eximdv
 |-  ( A e. On -> ( E. y ( x = ( card ` y ) /\ ( y C_ A /\ A C_ U. y ) ) -> E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) ) )
20 19 ss2abdv
 |-  ( A e. On -> { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A C_ U. y ) ) } C_ { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } )
21 intss
 |-  ( { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A C_ U. y ) ) } 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_ |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A C_ U. y ) ) } )
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_ |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A C_ U. y ) ) } )
23 1 22 eqsstrd
 |-  ( A e. On -> ( cf ` A ) C_ |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A C_ U. y ) ) } )
24 cff
 |-  cf : On --> On
25 24 fdmi
 |-  dom cf = On
26 25 eleq2i
 |-  ( A e. dom cf <-> A e. On )
27 ndmfv
 |-  ( -. A e. dom cf -> ( cf ` A ) = (/) )
28 26 27 sylnbir
 |-  ( -. A e. On -> ( cf ` A ) = (/) )
29 0ss
 |-  (/) C_ |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A C_ U. y ) ) }
30 28 29 eqsstrdi
 |-  ( -. A e. On -> ( cf ` A ) C_ |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A C_ U. y ) ) } )
31 23 30 pm2.61i
 |-  ( cf ` A ) C_ |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A C_ U. y ) ) }