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 syl6ibr
 |-  ( 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 syl6bi
 |-  ( 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 syl5bi
 |-  ( ( 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 ) )