Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  cfslb2n Structured version   Unicode version

Theorem cfslb2n 8705
 Description: Any small collection of small subsets of cannot have union , where "small" means smaller than the cofinality. This is a stronger version of cfslb 8703. This is a common application of cofinality: under AC, is regular, so it is not a countable union of countable sets. (Contributed by Mario Carneiro, 24-Jun-2013.)
Hypothesis
Ref Expression
cfslb.1
Assertion
Ref Expression
cfslb2n
Distinct variable groups:   ,   ,

Proof of Theorem cfslb2n
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 limord 5501 . . . . . . . . . 10
2 ordsson 6630 . . . . . . . . . 10
3 sstr 3472 . . . . . . . . . . 11
43expcom 436 . . . . . . . . . 10
51, 2, 43syl 18 . . . . . . . . 9
6 onsucuni 6669 . . . . . . . . 9
75, 6syl6 34 . . . . . . . 8
87adantrd 469 . . . . . . 7
98ralimdv 2832 . . . . . 6
10 uniiun 4352 . . . . . . 7
11 ss2iun 4315 . . . . . . 7
1210, 11syl5eqss 3508 . . . . . 6
139, 12syl6 34 . . . . 5
1413imp 430 . . . 4
15 cfslb.1 . . . . . . . . . 10
1615cfslbn 8704 . . . . . . . . 9
17163expib 1208 . . . . . . . 8
18 ordsucss 6659 . . . . . . . 8
191, 17, 18sylsyld 58 . . . . . . 7
2019ralimdv 2832 . . . . . 6
21 iunss 4340 . . . . . 6
2220, 21syl6ibr 230 . . . . 5
2322imp 430 . . . 4
24 sseq1 3485 . . . . . 6
25 eqss 3479 . . . . . . 7
2625simplbi2com 631 . . . . . 6
2724, 26syl6bi 231 . . . . 5
2827com3l 84 . . . 4
2914, 23, 28sylc 62 . . 3
30 limsuc 6690 . . . . . . . . 9
3117, 30sylibd 217 . . . . . . . 8
3231ralimdv 2832 . . . . . . 7
3332imp 430 . . . . . 6
34 r19.29 2960 . . . . . . . 8
35 eleq1 2495 . . . . . . . . . 10
3635biimparc 489 . . . . . . . . 9
3736rexlimivw 2911 . . . . . . . 8
3834, 37syl 17 . . . . . . 7
3938ex 435 . . . . . 6
4033, 39syl 17 . . . . 5
4140abssdv 3535 . . . 4
42 vex 3083 . . . . . . . . 9
4342uniex 6601 . . . . . . . 8
4443sucex 6652 . . . . . . 7
4544dfiun2 4333 . . . . . 6
4645eqeq1i 2429 . . . . 5
4715cfslb 8703 . . . . . 6
48473expia 1207 . . . . 5
4946, 48syl5bi 220 . . . 4
5041, 49syldan 472 . . 3
51 eqid 2422 . . . . . . . . 9
5251rnmpt 5099 . . . . . . . 8
5344, 51fnmpti 5724 . . . . . . . . . 10
54 dffn4 5816 . . . . . . . . . 10
5553, 54mpbi 211 . . . . . . . . 9
56 relsdom 7587 . . . . . . . . . . 11
5756brrelexi 4894 . . . . . . . . . 10
58 breq1 4426 . . . . . . . . . . . 12
59 foeq2 5807 . . . . . . . . . . . . 13
60 breq2 4427 . . . . . . . . . . . . 13
6159, 60imbi12d 321 . . . . . . . . . . . 12
6258, 61imbi12d 321 . . . . . . . . . . 11
63 cfon 8692 . . . . . . . . . . . . 13
64 sdomdom 7607 . . . . . . . . . . . . 13
65 ondomen 8475 . . . . . . . . . . . . 13
6663, 64, 65sylancr 667 . . . . . . . . . . . 12
67 fodomnum 8495 . . . . . . . . . . . 12
6866, 67syl 17 . . . . . . . . . . 11
6962, 68vtoclg 3139 . . . . . . . . . 10
7057, 69mpcom 37 . . . . . . . . 9
7155, 70mpi 20 . . . . . . . 8
7252, 71syl5eqbrr 4458 . . . . . . 7
73 domtr 7632 . . . . . . 7
7472, 73sylan2 476 . . . . . 6
75 domnsym 7707 . . . . . 6
7674, 75syl 17 . . . . 5
7776pm2.01da 443 . . . 4
7877a1i 11 . . 3
7929, 50, 783syld 57 . 2