Metamath Proof Explorer

Theorem cfslb2n

Description: Any small collection of small subsets of A cannot have union A , where "small" means smaller than the cofinality. This is a stronger version of cfslb . This is a common application of cofinality: under AC, ( aleph1 ) is regular, so it is not a countable union of countable sets. (Contributed by Mario Carneiro, 24-Jun-2013)

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

Proof

Step Hyp Ref Expression
1 cfslb.1 
 |-  A e. _V
2 limord 
 |-  ( Lim A -> Ord A )
3 ordsson 
 |-  ( Ord A -> A C_ On )
4 sstr 
 |-  ( ( x C_ A /\ A C_ On ) -> x C_ On )
5 4 expcom 
 |-  ( A C_ On -> ( x C_ A -> x C_ On ) )
6 2 3 5 3syl 
 |-  ( Lim A -> ( x C_ A -> x C_ On ) )
7 onsucuni 
 |-  ( x C_ On -> x C_ suc U. x )
8 6 7 syl6 
 |-  ( Lim A -> ( x C_ A -> x C_ suc U. x ) )
9 8 adantrd 
 |-  ( Lim A -> ( ( x C_ A /\ x ~< ( cf ` A ) ) -> x C_ suc U. x ) )
10 9 ralimdv 
 |-  ( Lim A -> ( A. x e. B ( x C_ A /\ x ~< ( cf ` A ) ) -> A. x e. B x C_ suc U. x ) )
11 uniiun 
 |-  U. B = U_ x e. B x
12 ss2iun 
 |-  ( A. x e. B x C_ suc U. x -> U_ x e. B x C_ U_ x e. B suc U. x )
13 11 12 eqsstrid 
 |-  ( A. x e. B x C_ suc U. x -> U. B C_ U_ x e. B suc U. x )
14 10 13 syl6 
 |-  ( Lim A -> ( A. x e. B ( x C_ A /\ x ~< ( cf ` A ) ) -> U. B C_ U_ x e. B suc U. x ) )
15 14 imp 
 |-  ( ( Lim A /\ A. x e. B ( x C_ A /\ x ~< ( cf ` A ) ) ) -> U. B C_ U_ x e. B suc U. x )
16 1 cfslbn 
 |-  ( ( Lim A /\ x C_ A /\ x ~< ( cf ` A ) ) -> U. x e. A )
17 16 3expib 
 |-  ( Lim A -> ( ( x C_ A /\ x ~< ( cf ` A ) ) -> U. x e. A ) )
18 ordsucss 
 |-  ( Ord A -> ( U. x e. A -> suc U. x C_ A ) )
19 2 17 18 sylsyld 
 |-  ( Lim A -> ( ( x C_ A /\ x ~< ( cf ` A ) ) -> suc U. x C_ A ) )
20 19 ralimdv 
 |-  ( Lim A -> ( A. x e. B ( x C_ A /\ x ~< ( cf ` A ) ) -> A. x e. B suc U. x C_ A ) )
21 iunss 
 |-  ( U_ x e. B suc U. x C_ A <-> A. x e. B suc U. x C_ A )
22 20 21 imbitrrdi 
 |-  ( Lim A -> ( A. x e. B ( x C_ A /\ x ~< ( cf ` A ) ) -> U_ x e. B suc U. x C_ A ) )
23 22 imp 
 |-  ( ( Lim A /\ A. x e. B ( x C_ A /\ x ~< ( cf ` A ) ) ) -> U_ x e. B suc U. x C_ A )
24 sseq1 
 |-  ( U. B = A -> ( U. B C_ U_ x e. B suc U. x <-> A C_ U_ x e. B suc U. x ) )
25 eqss 
 |-  ( U_ x e. B suc U. x = A <-> ( U_ x e. B suc U. x C_ A /\ A C_ U_ x e. B suc U. x ) )
26 25 simplbi2com 
 |-  ( A C_ U_ x e. B suc U. x -> ( U_ x e. B suc U. x C_ A -> U_ x e. B suc U. x = A ) )
27 24 26 biimtrdi 
 |-  ( U. B = A -> ( U. B C_ U_ x e. B suc U. x -> ( U_ x e. B suc U. x C_ A -> U_ x e. B suc U. x = A ) ) )
28 27 com3l 
 |-  ( U. B C_ U_ x e. B suc U. x -> ( U_ x e. B suc U. x C_ A -> ( U. B = A -> U_ x e. B suc U. x = A ) ) )
29 15 23 28 sylc 
 |-  ( ( Lim A /\ A. x e. B ( x C_ A /\ x ~< ( cf ` A ) ) ) -> ( U. B = A -> U_ x e. B suc U. x = A ) )
30 limsuc 
 |-  ( Lim A -> ( U. x e. A <-> suc U. x e. A ) )
31 17 30 sylibd 
 |-  ( Lim A -> ( ( x C_ A /\ x ~< ( cf ` A ) ) -> suc U. x e. A ) )
32 31 ralimdv 
 |-  ( Lim A -> ( A. x e. B ( x C_ A /\ x ~< ( cf ` A ) ) -> A. x e. B suc U. x e. A ) )
33 32 imp 
 |-  ( ( Lim A /\ A. x e. B ( x C_ A /\ x ~< ( cf ` A ) ) ) -> A. x e. B suc U. x e. A )
34 r19.29 
 |-  ( ( A. x e. B suc U. x e. A /\ E. x e. B y = suc U. x ) -> E. x e. B ( suc U. x e. A /\ y = suc U. x ) )
35 eleq1 
 |-  ( y = suc U. x -> ( y e. A <-> suc U. x e. A ) )
36 35 biimparc 
 |-  ( ( suc U. x e. A /\ y = suc U. x ) -> y e. A )
37 36 rexlimivw 
 |-  ( E. x e. B ( suc U. x e. A /\ y = suc U. x ) -> y e. A )
38 34 37 syl 
 |-  ( ( A. x e. B suc U. x e. A /\ E. x e. B y = suc U. x ) -> y e. A )
39 38 ex 
 |-  ( A. x e. B suc U. x e. A -> ( E. x e. B y = suc U. x -> y e. A ) )
40 33 39 syl 
 |-  ( ( Lim A /\ A. x e. B ( x C_ A /\ x ~< ( cf ` A ) ) ) -> ( E. x e. B y = suc U. x -> y e. A ) )
41 40 abssdv 
 |-  ( ( Lim A /\ A. x e. B ( x C_ A /\ x ~< ( cf ` A ) ) ) -> { y | E. x e. B y = suc U. x } C_ A )
42 vuniex 
 |-  U. x e. _V
43 42 sucex 
 |-  suc U. x e. _V
44 43 dfiun2 
 |-  U_ x e. B suc U. x = U. { y | E. x e. B y = suc U. x }
45 44 eqeq1i 
 |-  ( U_ x e. B suc U. x = A <-> U. { y | E. x e. B y = suc U. x } = A )
46 1 cfslb 
 |-  ( ( Lim A /\ { y | E. x e. B y = suc U. x } C_ A /\ U. { y | E. x e. B y = suc U. x } = A ) -> ( cf ` A ) ~<_ { y | E. x e. B y = suc U. x } )
47 46 3expia 
 |-  ( ( Lim A /\ { y | E. x e. B y = suc U. x } C_ A ) -> ( U. { y | E. x e. B y = suc U. x } = A -> ( cf ` A ) ~<_ { y | E. x e. B y = suc U. x } ) )
48 45 47 biimtrid 
 |-  ( ( Lim A /\ { y | E. x e. B y = suc U. x } C_ A ) -> ( U_ x e. B suc U. x = A -> ( cf ` A ) ~<_ { y | E. x e. B y = suc U. x } ) )
49 41 48 syldan 
 |-  ( ( Lim A /\ A. x e. B ( x C_ A /\ x ~< ( cf ` A ) ) ) -> ( U_ x e. B suc U. x = A -> ( cf ` A ) ~<_ { y | E. x e. B y = suc U. x } ) )
50 eqid 
 |-  ( x e. B |-> suc U. x ) = ( x e. B |-> suc U. x )
51 50 rnmpt 
 |-  ran ( x e. B |-> suc U. x ) = { y | E. x e. B y = suc U. x }
52 43 50 fnmpti 
 |-  ( x e. B |-> suc U. x ) Fn B
53 dffn4 
 |-  ( ( x e. B |-> suc U. x ) Fn B <-> ( x e. B |-> suc U. x ) : B -onto-> ran ( x e. B |-> suc U. x ) )
54 52 53 mpbi 
 |-  ( x e. B |-> suc U. x ) : B -onto-> ran ( x e. B |-> suc U. x )
55 relsdom 
 |-  Rel ~<
56 55 brrelex1i 
 |-  ( B ~< ( cf ` A ) -> B e. _V )
57 breq1 
 |-  ( y = B -> ( y ~< ( cf ` A ) <-> B ~< ( cf ` A ) ) )
58 foeq2 
 |-  ( y = B -> ( ( x e. B |-> suc U. x ) : y -onto-> ran ( x e. B |-> suc U. x ) <-> ( x e. B |-> suc U. x ) : B -onto-> ran ( x e. B |-> suc U. x ) ) )
59 breq2 
 |-  ( y = B -> ( ran ( x e. B |-> suc U. x ) ~<_ y <-> ran ( x e. B |-> suc U. x ) ~<_ B ) )
60 58 59 imbi12d 
 |-  ( y = B -> ( ( ( x e. B |-> suc U. x ) : y -onto-> ran ( x e. B |-> suc U. x ) -> ran ( x e. B |-> suc U. x ) ~<_ y ) <-> ( ( x e. B |-> suc U. x ) : B -onto-> ran ( x e. B |-> suc U. x ) -> ran ( x e. B |-> suc U. x ) ~<_ B ) ) )
61 57 60 imbi12d 
 |-  ( y = B -> ( ( y ~< ( cf ` A ) -> ( ( x e. B |-> suc U. x ) : y -onto-> ran ( x e. B |-> suc U. x ) -> ran ( x e. B |-> suc U. x ) ~<_ y ) ) <-> ( B ~< ( cf ` A ) -> ( ( x e. B |-> suc U. x ) : B -onto-> ran ( x e. B |-> suc U. x ) -> ran ( x e. B |-> suc U. x ) ~<_ B ) ) ) )
62 cfon 
 |-  ( cf ` A ) e. On
63 sdomdom 
 |-  ( y ~< ( cf ` A ) -> y ~<_ ( cf ` A ) )
64 ondomen 
 |-  ( ( ( cf ` A ) e. On /\ y ~<_ ( cf ` A ) ) -> y e. dom card )
65 62 63 64 sylancr 
 |-  ( y ~< ( cf ` A ) -> y e. dom card )
66 fodomnum 
 |-  ( y e. dom card -> ( ( x e. B |-> suc U. x ) : y -onto-> ran ( x e. B |-> suc U. x ) -> ran ( x e. B |-> suc U. x ) ~<_ y ) )
67 65 66 syl 
 |-  ( y ~< ( cf ` A ) -> ( ( x e. B |-> suc U. x ) : y -onto-> ran ( x e. B |-> suc U. x ) -> ran ( x e. B |-> suc U. x ) ~<_ y ) )
68 61 67 vtoclg 
 |-  ( B e. _V -> ( B ~< ( cf ` A ) -> ( ( x e. B |-> suc U. x ) : B -onto-> ran ( x e. B |-> suc U. x ) -> ran ( x e. B |-> suc U. x ) ~<_ B ) ) )
69 56 68 mpcom 
 |-  ( B ~< ( cf ` A ) -> ( ( x e. B |-> suc U. x ) : B -onto-> ran ( x e. B |-> suc U. x ) -> ran ( x e. B |-> suc U. x ) ~<_ B ) )
70 54 69 mpi 
 |-  ( B ~< ( cf ` A ) -> ran ( x e. B |-> suc U. x ) ~<_ B )
71 51 70 eqbrtrrid 
 |-  ( B ~< ( cf ` A ) -> { y | E. x e. B y = suc U. x } ~<_ B )
72 domtr 
 |-  ( ( ( cf ` A ) ~<_ { y | E. x e. B y = suc U. x } /\ { y | E. x e. B y = suc U. x } ~<_ B ) -> ( cf ` A ) ~<_ B )
73 71 72 sylan2 
 |-  ( ( ( cf ` A ) ~<_ { y | E. x e. B y = suc U. x } /\ B ~< ( cf ` A ) ) -> ( cf ` A ) ~<_ B )
74 domnsym 
 |-  ( ( cf ` A ) ~<_ B -> -. B ~< ( cf ` A ) )
75 73 74 syl 
 |-  ( ( ( cf ` A ) ~<_ { y | E. x e. B y = suc U. x } /\ B ~< ( cf ` A ) ) -> -. B ~< ( cf ` A ) )
76 75 pm2.01da 
 |-  ( ( cf ` A ) ~<_ { y | E. x e. B y = suc U. x } -> -. B ~< ( cf ` A ) )
77 76 a1i 
 |-  ( ( Lim A /\ A. x e. B ( x C_ A /\ x ~< ( cf ` A ) ) ) -> ( ( cf ` A ) ~<_ { y | E. x e. B y = suc U. x } -> -. B ~< ( cf ` A ) ) )
78 29 49 77 3syld 
 |-  ( ( Lim A /\ A. x e. B ( x C_ A /\ x ~< ( cf ` A ) ) ) -> ( U. B = A -> -. B ~< ( cf ` A ) ) )
79 78 necon2ad 
 |-  ( ( Lim A /\ A. x e. B ( x C_ A /\ x ~< ( cf ` A ) ) ) -> ( B ~< ( cf ` A ) -> U. B =/= A ) )