Metamath Proof Explorer

Theorem cfslb

Description: Any cofinal subset of A is at least as large as ( cfA ) . (Contributed by Mario Carneiro, 24-Jun-2013)

Ref Expression
Hypothesis cfslb.1 
|- A e. _V
Assertion cfslb 
|- ( ( Lim A /\ B C_ A /\ U. B = A ) -> ( cf ` A ) ~<_ B )

Proof

Step Hyp Ref Expression
1 cfslb.1 
 |-  A e. _V
2 fvex 
 |-  ( card ` B ) e. _V
3 ssid 
 |-  ( card ` B ) C_ ( card ` B )
4 1 ssex 
 |-  ( B C_ A -> B e. _V )
5 4 ad2antrr 
 |-  ( ( ( B C_ A /\ U. B = A ) /\ ( card ` B ) C_ ( card ` B ) ) -> B e. _V )
6 velpw 
 |-  ( x e. ~P A <-> x C_ A )
7 sseq1 
 |-  ( x = B -> ( x C_ A <-> B C_ A ) )
8 6 7 syl5bb 
 |-  ( x = B -> ( x e. ~P A <-> B C_ A ) )
9 unieq 
 |-  ( x = B -> U. x = U. B )
10 9 eqeq1d 
 |-  ( x = B -> ( U. x = A <-> U. B = A ) )
11 8 10 anbi12d 
 |-  ( x = B -> ( ( x e. ~P A /\ U. x = A ) <-> ( B C_ A /\ U. B = A ) ) )
12 fveq2 
 |-  ( x = B -> ( card ` x ) = ( card ` B ) )
13 12 sseq1d 
 |-  ( x = B -> ( ( card ` x ) C_ ( card ` B ) <-> ( card ` B ) C_ ( card ` B ) ) )
14 11 13 anbi12d 
 |-  ( x = B -> ( ( ( x e. ~P A /\ U. x = A ) /\ ( card ` x ) C_ ( card ` B ) ) <-> ( ( B C_ A /\ U. B = A ) /\ ( card ` B ) C_ ( card ` B ) ) ) )
15 14 spcegv 
 |-  ( B e. _V -> ( ( ( B C_ A /\ U. B = A ) /\ ( card ` B ) C_ ( card ` B ) ) -> E. x ( ( x e. ~P A /\ U. x = A ) /\ ( card ` x ) C_ ( card ` B ) ) ) )
16 5 15 mpcom 
 |-  ( ( ( B C_ A /\ U. B = A ) /\ ( card ` B ) C_ ( card ` B ) ) -> E. x ( ( x e. ~P A /\ U. x = A ) /\ ( card ` x ) C_ ( card ` B ) ) )
17 df-rex 
 |-  ( E. x e. { x e. ~P A | U. x = A } ( card ` x ) C_ ( card ` B ) <-> E. x ( x e. { x e. ~P A | U. x = A } /\ ( card ` x ) C_ ( card ` B ) ) )
18 rabid 
 |-  ( x e. { x e. ~P A | U. x = A } <-> ( x e. ~P A /\ U. x = A ) )
19 18 anbi1i 
 |-  ( ( x e. { x e. ~P A | U. x = A } /\ ( card ` x ) C_ ( card ` B ) ) <-> ( ( x e. ~P A /\ U. x = A ) /\ ( card ` x ) C_ ( card ` B ) ) )
20 19 exbii 
 |-  ( E. x ( x e. { x e. ~P A | U. x = A } /\ ( card ` x ) C_ ( card ` B ) ) <-> E. x ( ( x e. ~P A /\ U. x = A ) /\ ( card ` x ) C_ ( card ` B ) ) )
21 17 20 bitri 
 |-  ( E. x e. { x e. ~P A | U. x = A } ( card ` x ) C_ ( card ` B ) <-> E. x ( ( x e. ~P A /\ U. x = A ) /\ ( card ` x ) C_ ( card ` B ) ) )
22 16 21 sylibr 
 |-  ( ( ( B C_ A /\ U. B = A ) /\ ( card ` B ) C_ ( card ` B ) ) -> E. x e. { x e. ~P A | U. x = A } ( card ` x ) C_ ( card ` B ) )
23 3 22 mpan2 
 |-  ( ( B C_ A /\ U. B = A ) -> E. x e. { x e. ~P A | U. x = A } ( card ` x ) C_ ( card ` B ) )
24 iinss 
 |-  ( E. x e. { x e. ~P A | U. x = A } ( card ` x ) C_ ( card ` B ) -> |^|_ x e. { x e. ~P A | U. x = A } ( card ` x ) C_ ( card ` B ) )
25 23 24 syl 
 |-  ( ( B C_ A /\ U. B = A ) -> |^|_ x e. { x e. ~P A | U. x = A } ( card ` x ) C_ ( card ` B ) )
26 1 cflim3 
 |-  ( Lim A -> ( cf ` A ) = |^|_ x e. { x e. ~P A | U. x = A } ( card ` x ) )
27 26 sseq1d 
 |-  ( Lim A -> ( ( cf ` A ) C_ ( card ` B ) <-> |^|_ x e. { x e. ~P A | U. x = A } ( card ` x ) C_ ( card ` B ) ) )
28 25 27 syl5ibr 
 |-  ( Lim A -> ( ( B C_ A /\ U. B = A ) -> ( cf ` A ) C_ ( card ` B ) ) )
29 28 3impib 
 |-  ( ( Lim A /\ B C_ A /\ U. B = A ) -> ( cf ` A ) C_ ( card ` B ) )
30 ssdomg 
 |-  ( ( card ` B ) e. _V -> ( ( cf ` A ) C_ ( card ` B ) -> ( cf ` A ) ~<_ ( card ` B ) ) )
31 2 29 30 mpsyl 
 |-  ( ( Lim A /\ B C_ A /\ U. B = A ) -> ( cf ` A ) ~<_ ( card ` B ) )
32 limord 
 |-  ( Lim A -> Ord A )
33 ordsson 
 |-  ( Ord A -> A C_ On )
34 32 33 syl 
 |-  ( Lim A -> A C_ On )
35 sstr2 
 |-  ( B C_ A -> ( A C_ On -> B C_ On ) )
36 34 35 mpan9 
 |-  ( ( Lim A /\ B C_ A ) -> B C_ On )
37 onssnum 
 |-  ( ( B e. _V /\ B C_ On ) -> B e. dom card )
38 4 36 37 syl2an2 
 |-  ( ( Lim A /\ B C_ A ) -> B e. dom card )
39 cardid2 
 |-  ( B e. dom card -> ( card ` B ) ~~ B )
40 38 39 syl 
 |-  ( ( Lim A /\ B C_ A ) -> ( card ` B ) ~~ B )
41 40 3adant3 
 |-  ( ( Lim A /\ B C_ A /\ U. B = A ) -> ( card ` B ) ~~ B )
42 domentr 
 |-  ( ( ( cf ` A ) ~<_ ( card ` B ) /\ ( card ` B ) ~~ B ) -> ( cf ` A ) ~<_ B )
43 31 41 42 syl2anc 
 |-  ( ( Lim A /\ B C_ A /\ U. B = A ) -> ( cf ` A ) ~<_ B )