Metamath Proof Explorer

Theorem cfss

Description: There is a cofinal subset of A of cardinality ( cfA ) . (Contributed by Mario Carneiro, 24-Jun-2013)

Ref Expression
Hypothesis cfss.1 
|- A e. _V
Assertion cfss 
|- ( Lim A -> E. x ( x C_ A /\ x ~~ ( cf ` A ) /\ U. x = A ) )

Proof

Step Hyp Ref Expression
1 cfss.1 
 |-  A e. _V
2 1 cflim3 
 |-  ( Lim A -> ( cf ` A ) = |^|_ x e. { x e. ~P A | U. x = A } ( card ` x ) )
3 fvex 
 |-  ( card ` x ) e. _V
4 3 dfiin2 
 |-  |^|_ x e. { x e. ~P A | U. x = A } ( card ` x ) = |^| { y | E. x e. { x e. ~P A | U. x = A } y = ( card ` x ) }
5 cardon 
 |-  ( card ` x ) e. On
6 eleq1 
 |-  ( y = ( card ` x ) -> ( y e. On <-> ( card ` x ) e. On ) )
7 5 6 mpbiri 
 |-  ( y = ( card ` x ) -> y e. On )
8 7 rexlimivw 
 |-  ( E. x e. { x e. ~P A | U. x = A } y = ( card ` x ) -> y e. On )
9 8 abssi 
 |-  { y | E. x e. { x e. ~P A | U. x = A } y = ( card ` x ) } C_ On
10 limuni 
 |-  ( Lim A -> A = U. A )
11 10 eqcomd 
 |-  ( Lim A -> U. A = A )
12 fveq2 
 |-  ( x = A -> ( card ` x ) = ( card ` A ) )
13 12 eqcomd 
 |-  ( x = A -> ( card ` A ) = ( card ` x ) )
14 13 biantrud 
 |-  ( x = A -> ( U. A = A <-> ( U. A = A /\ ( card ` A ) = ( card ` x ) ) ) )
15 unieq 
 |-  ( x = A -> U. x = U. A )
16 15 eqeq1d 
 |-  ( x = A -> ( U. x = A <-> U. A = A ) )
17 1 pwid 
 |-  A e. ~P A
18 eleq1 
 |-  ( x = A -> ( x e. ~P A <-> A e. ~P A ) )
19 17 18 mpbiri 
 |-  ( x = A -> x e. ~P A )
20 19 biantrurd 
 |-  ( x = A -> ( U. x = A <-> ( x e. ~P A /\ U. x = A ) ) )
21 16 20 bitr3d 
 |-  ( x = A -> ( U. A = A <-> ( x e. ~P A /\ U. x = A ) ) )
22 21 anbi1d 
 |-  ( x = A -> ( ( U. A = A /\ ( card ` A ) = ( card ` x ) ) <-> ( ( x e. ~P A /\ U. x = A ) /\ ( card ` A ) = ( card ` x ) ) ) )
23 14 22 bitr2d 
 |-  ( x = A -> ( ( ( x e. ~P A /\ U. x = A ) /\ ( card ` A ) = ( card ` x ) ) <-> U. A = A ) )
24 1 23 spcev 
 |-  ( U. A = A -> E. x ( ( x e. ~P A /\ U. x = A ) /\ ( card ` A ) = ( card ` x ) ) )
25 11 24 syl 
 |-  ( Lim A -> E. x ( ( x e. ~P A /\ U. x = A ) /\ ( card ` A ) = ( card ` x ) ) )
26 df-rex 
 |-  ( E. x e. { x e. ~P A | U. x = A } ( card ` A ) = ( card ` x ) <-> E. x ( x e. { x e. ~P A | U. x = A } /\ ( card ` A ) = ( card ` x ) ) )
27 rabid 
 |-  ( x e. { x e. ~P A | U. x = A } <-> ( x e. ~P A /\ U. x = A ) )
28 27 anbi1i 
 |-  ( ( x e. { x e. ~P A | U. x = A } /\ ( card ` A ) = ( card ` x ) ) <-> ( ( x e. ~P A /\ U. x = A ) /\ ( card ` A ) = ( card ` x ) ) )
29 28 exbii 
 |-  ( E. x ( x e. { x e. ~P A | U. x = A } /\ ( card ` A ) = ( card ` x ) ) <-> E. x ( ( x e. ~P A /\ U. x = A ) /\ ( card ` A ) = ( card ` x ) ) )
30 26 29 bitri 
 |-  ( E. x e. { x e. ~P A | U. x = A } ( card ` A ) = ( card ` x ) <-> E. x ( ( x e. ~P A /\ U. x = A ) /\ ( card ` A ) = ( card ` x ) ) )
31 25 30 sylibr 
 |-  ( Lim A -> E. x e. { x e. ~P A | U. x = A } ( card ` A ) = ( card ` x ) )
32 fvex 
 |-  ( card ` A ) e. _V
33 eqeq1 
 |-  ( y = ( card ` A ) -> ( y = ( card ` x ) <-> ( card ` A ) = ( card ` x ) ) )
34 33 rexbidv 
 |-  ( y = ( card ` A ) -> ( E. x e. { x e. ~P A | U. x = A } y = ( card ` x ) <-> E. x e. { x e. ~P A | U. x = A } ( card ` A ) = ( card ` x ) ) )
35 32 34 spcev 
 |-  ( E. x e. { x e. ~P A | U. x = A } ( card ` A ) = ( card ` x ) -> E. y E. x e. { x e. ~P A | U. x = A } y = ( card ` x ) )
36 31 35 syl 
 |-  ( Lim A -> E. y E. x e. { x e. ~P A | U. x = A } y = ( card ` x ) )
37 abn0 
 |-  ( { y | E. x e. { x e. ~P A | U. x = A } y = ( card ` x ) } =/= (/) <-> E. y E. x e. { x e. ~P A | U. x = A } y = ( card ` x ) )
38 36 37 sylibr 
 |-  ( Lim A -> { y | E. x e. { x e. ~P A | U. x = A } y = ( card ` x ) } =/= (/) )
39 onint 
 |-  ( ( { y | E. x e. { x e. ~P A | U. x = A } y = ( card ` x ) } C_ On /\ { y | E. x e. { x e. ~P A | U. x = A } y = ( card ` x ) } =/= (/) ) -> |^| { y | E. x e. { x e. ~P A | U. x = A } y = ( card ` x ) } e. { y | E. x e. { x e. ~P A | U. x = A } y = ( card ` x ) } )
40 9 38 39 sylancr 
 |-  ( Lim A -> |^| { y | E. x e. { x e. ~P A | U. x = A } y = ( card ` x ) } e. { y | E. x e. { x e. ~P A | U. x = A } y = ( card ` x ) } )
41 4 40 eqeltrid 
 |-  ( Lim A -> |^|_ x e. { x e. ~P A | U. x = A } ( card ` x ) e. { y | E. x e. { x e. ~P A | U. x = A } y = ( card ` x ) } )
42 2 41 eqeltrd 
 |-  ( Lim A -> ( cf ` A ) e. { y | E. x e. { x e. ~P A | U. x = A } y = ( card ` x ) } )
43 fvex 
 |-  ( cf ` A ) e. _V
44 eqeq1 
 |-  ( y = ( cf ` A ) -> ( y = ( card ` x ) <-> ( cf ` A ) = ( card ` x ) ) )
45 44 rexbidv 
 |-  ( y = ( cf ` A ) -> ( E. x e. { x e. ~P A | U. x = A } y = ( card ` x ) <-> E. x e. { x e. ~P A | U. x = A } ( cf ` A ) = ( card ` x ) ) )
46 43 45 elab 
 |-  ( ( cf ` A ) e. { y | E. x e. { x e. ~P A | U. x = A } y = ( card ` x ) } <-> E. x e. { x e. ~P A | U. x = A } ( cf ` A ) = ( card ` x ) )
47 42 46 sylib 
 |-  ( Lim A -> E. x e. { x e. ~P A | U. x = A } ( cf ` A ) = ( card ` x ) )
48 df-rex 
 |-  ( E. x e. { x e. ~P A | U. x = A } ( cf ` A ) = ( card ` x ) <-> E. x ( x e. { x e. ~P A | U. x = A } /\ ( cf ` A ) = ( card ` x ) ) )
49 47 48 sylib 
 |-  ( Lim A -> E. x ( x e. { x e. ~P A | U. x = A } /\ ( cf ` A ) = ( card ` x ) ) )
50 simprl 
 |-  ( ( Lim A /\ ( x e. { x e. ~P A | U. x = A } /\ ( cf ` A ) = ( card ` x ) ) ) -> x e. { x e. ~P A | U. x = A } )
51 50 27 sylib 
 |-  ( ( Lim A /\ ( x e. { x e. ~P A | U. x = A } /\ ( cf ` A ) = ( card ` x ) ) ) -> ( x e. ~P A /\ U. x = A ) )
52 51 simpld 
 |-  ( ( Lim A /\ ( x e. { x e. ~P A | U. x = A } /\ ( cf ` A ) = ( card ` x ) ) ) -> x e. ~P A )
53 52 elpwid 
 |-  ( ( Lim A /\ ( x e. { x e. ~P A | U. x = A } /\ ( cf ` A ) = ( card ` x ) ) ) -> x C_ A )
54 simpl 
 |-  ( ( Lim A /\ ( x e. { x e. ~P A | U. x = A } /\ ( cf ` A ) = ( card ` x ) ) ) -> Lim A )
55 vex 
 |-  x e. _V
56 limord 
 |-  ( Lim A -> Ord A )
57 ordsson 
 |-  ( Ord A -> A C_ On )
58 56 57 syl 
 |-  ( Lim A -> A C_ On )
59 sstr 
 |-  ( ( x C_ A /\ A C_ On ) -> x C_ On )
60 58 59 sylan2 
 |-  ( ( x C_ A /\ Lim A ) -> x C_ On )
61 onssnum 
 |-  ( ( x e. _V /\ x C_ On ) -> x e. dom card )
62 55 60 61 sylancr 
 |-  ( ( x C_ A /\ Lim A ) -> x e. dom card )
63 cardid2 
 |-  ( x e. dom card -> ( card ` x ) ~~ x )
64 62 63 syl 
 |-  ( ( x C_ A /\ Lim A ) -> ( card ` x ) ~~ x )
65 64 ensymd 
 |-  ( ( x C_ A /\ Lim A ) -> x ~~ ( card ` x ) )
66 53 54 65 syl2anc 
 |-  ( ( Lim A /\ ( x e. { x e. ~P A | U. x = A } /\ ( cf ` A ) = ( card ` x ) ) ) -> x ~~ ( card ` x ) )
67 simprr 
 |-  ( ( Lim A /\ ( x e. { x e. ~P A | U. x = A } /\ ( cf ` A ) = ( card ` x ) ) ) -> ( cf ` A ) = ( card ` x ) )
68 66 67 breqtrrd 
 |-  ( ( Lim A /\ ( x e. { x e. ~P A | U. x = A } /\ ( cf ` A ) = ( card ` x ) ) ) -> x ~~ ( cf ` A ) )
69 51 simprd 
 |-  ( ( Lim A /\ ( x e. { x e. ~P A | U. x = A } /\ ( cf ` A ) = ( card ` x ) ) ) -> U. x = A )
70 53 68 69 3jca 
 |-  ( ( Lim A /\ ( x e. { x e. ~P A | U. x = A } /\ ( cf ` A ) = ( card ` x ) ) ) -> ( x C_ A /\ x ~~ ( cf ` A ) /\ U. x = A ) )
71 70 ex 
 |-  ( Lim A -> ( ( x e. { x e. ~P A | U. x = A } /\ ( cf ` A ) = ( card ` x ) ) -> ( x C_ A /\ x ~~ ( cf ` A ) /\ U. x = A ) ) )
72 71 eximdv 
 |-  ( Lim A -> ( E. x ( x e. { x e. ~P A | U. x = A } /\ ( cf ` A ) = ( card ` x ) ) -> E. x ( x C_ A /\ x ~~ ( cf ` A ) /\ U. x = A ) ) )
73 49 72 mpd 
 |-  ( Lim A -> E. x ( x C_ A /\ x ~~ ( cf ` A ) /\ U. x = A ) )