Metamath Proof Explorer

Theorem cflm

Description: Value of the cofinality function at a limit ordinal. Part of Definition of cofinality of Enderton p. 257. (Contributed by NM, 26-Apr-2004)

Ref Expression
Assertion cflm 
|- ( ( A e. B /\ Lim A ) -> ( cf ` A ) = |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) } )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( A e. B -> A e. _V )
2 limsuc 
 |-  ( Lim A -> ( v e. A <-> suc v e. A ) )
3 2 biimpd 
 |-  ( Lim A -> ( v e. A -> suc v e. A ) )
4 sseq1 
 |-  ( z = suc v -> ( z C_ w <-> suc v C_ w ) )
5 4 rexbidv 
 |-  ( z = suc v -> ( E. w e. y z C_ w <-> E. w e. y suc v C_ w ) )
6 5 rspcv 
 |-  ( suc v e. A -> ( A. z e. A E. w e. y z C_ w -> E. w e. y suc v C_ w ) )
7 sucssel 
 |-  ( v e. _V -> ( suc v C_ w -> v e. w ) )
8 7 elv 
 |-  ( suc v C_ w -> v e. w )
9 8 reximi 
 |-  ( E. w e. y suc v C_ w -> E. w e. y v e. w )
10 eluni2 
 |-  ( v e. U. y <-> E. w e. y v e. w )
11 9 10 sylibr 
 |-  ( E. w e. y suc v C_ w -> v e. U. y )
12 6 11 syl6com 
 |-  ( A. z e. A E. w e. y z C_ w -> ( suc v e. A -> v e. U. y ) )
13 3 12 syl9 
 |-  ( Lim A -> ( A. z e. A E. w e. y z C_ w -> ( v e. A -> v e. U. y ) ) )
14 13 ralrimdv 
 |-  ( Lim A -> ( A. z e. A E. w e. y z C_ w -> A. v e. A v e. U. y ) )
15 dfss3 
 |-  ( A C_ U. y <-> A. v e. A v e. U. y )
16 14 15 syl6ibr 
 |-  ( Lim A -> ( A. z e. A E. w e. y z C_ w -> A C_ U. y ) )
17 16 adantr 
 |-  ( ( Lim A /\ y C_ A ) -> ( A. z e. A E. w e. y z C_ w -> A C_ U. y ) )
18 uniss 
 |-  ( y C_ A -> U. y C_ U. A )
19 limuni 
 |-  ( Lim A -> A = U. A )
20 19 sseq2d 
 |-  ( Lim A -> ( U. y C_ A <-> U. y C_ U. A ) )
21 18 20 syl5ibr 
 |-  ( Lim A -> ( y C_ A -> U. y C_ A ) )
22 21 imp 
 |-  ( ( Lim A /\ y C_ A ) -> U. y C_ A )
23 17 22 jctird 
 |-  ( ( Lim A /\ y C_ A ) -> ( A. z e. A E. w e. y z C_ w -> ( A C_ U. y /\ U. y C_ A ) ) )
24 eqss 
 |-  ( A = U. y <-> ( A C_ U. y /\ U. y C_ A ) )
25 23 24 syl6ibr 
 |-  ( ( Lim A /\ y C_ A ) -> ( A. z e. A E. w e. y z C_ w -> A = U. y ) )
26 25 imdistanda 
 |-  ( Lim A -> ( ( y C_ A /\ A. z e. A E. w e. y z C_ w ) -> ( y C_ A /\ A = U. y ) ) )
27 26 anim2d 
 |-  ( Lim A -> ( ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) -> ( x = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) ) )
28 27 eximdv 
 |-  ( Lim A -> ( E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) -> E. y ( x = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) ) )
29 28 ss2abdv 
 |-  ( Lim A -> { 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 = U. y ) ) } )
30 intss 
 |-  ( { 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 = U. y ) ) } -> |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) } C_ |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } )
31 29 30 syl 
 |-  ( Lim A -> |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) } C_ |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } )
32 31 adantl 
 |-  ( ( A e. _V /\ Lim A ) -> |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) } C_ |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } )
33 limelon 
 |-  ( ( A e. _V /\ Lim A ) -> A e. On )
34 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 ) ) } )
35 33 34 syl 
 |-  ( ( A e. _V /\ Lim A ) -> ( cf ` A ) = |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. w e. y z C_ w ) ) } )
36 32 35 sseqtrrd 
 |-  ( ( A e. _V /\ Lim A ) -> |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) } C_ ( cf ` A ) )
37 cfub 
 |-  ( cf ` A ) C_ |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A C_ U. y ) ) }
38 eqimss 
 |-  ( A = U. y -> A C_ U. y )
39 38 anim2i 
 |-  ( ( y C_ A /\ A = U. y ) -> ( y C_ A /\ A C_ U. y ) )
40 39 anim2i 
 |-  ( ( x = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) -> ( x = ( card ` y ) /\ ( y C_ A /\ A C_ U. y ) ) )
41 40 eximi 
 |-  ( E. y ( x = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) -> E. y ( x = ( card ` y ) /\ ( y C_ A /\ A C_ U. y ) ) )
42 41 ss2abi 
 |-  { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) } C_ { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A C_ U. y ) ) }
43 intss 
 |-  ( { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) } C_ { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A C_ U. y ) ) } -> |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A C_ U. y ) ) } C_ |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) } )
44 42 43 ax-mp 
 |-  |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A C_ U. y ) ) } C_ |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) }
45 37 44 sstri 
 |-  ( cf ` A ) C_ |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) }
46 36 45 jctil 
 |-  ( ( A e. _V /\ Lim A ) -> ( ( cf ` A ) C_ |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) } /\ |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) } C_ ( cf ` A ) ) )
47 eqss 
 |-  ( ( cf ` A ) = |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) } <-> ( ( cf ` A ) C_ |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) } /\ |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) } C_ ( cf ` A ) ) )
48 46 47 sylibr 
 |-  ( ( A e. _V /\ Lim A ) -> ( cf ` A ) = |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) } )
49 1 48 sylan 
 |-  ( ( A e. B /\ Lim A ) -> ( cf ` A ) = |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) } )