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

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 biimtrid 
 |-  ( ( 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 ) ) }