|Metamath Proof Explorer||
|Mirrors > Home > MPE Home > Th. List > fin23||Structured version Unicode version|
|Description: Every II-finite set
(every chain of subsets has a maximal element) is
III-finite (has no denumerable collection of subsets). The proof here
is the only one I could find, from
p.94 (writeup by
Tarski, credited to Kuratowski). Translated into English and modern
notation, the proof proceeds as follows (variables renamed for
Suppose for a contradiction that is a set which is II-finite but not III-finite.
For any countable sequence of distinct subsets of , we can form a decreasing sequence of non-empty subsets by taking finite intersections of initial segments of while skipping over any element of which would cause the intersection to be empty.
By II-finiteness (as fin2i2 8198) this sequence contains its intersection, call it ; since by induction every subset in the sequence is non-empty, the intersection must be non-empty.
Suppose that an element of has non-empty intersection with . Thus, said element has a non-empty intersection with the corresponding element of , therefore it was used in the construction of and all further elements of are subsets of , thus contains the . That is, all elements of either contain or are disjoint from it.
Since there are only two cases, there must exist an infinite subset of which uniformly either contain or are disjoint from it. In the former case we can create an infinite set by subtracting from each element. In either case, call the result ; this is an infinite set of subsets of , each of which is disjoint from and contained in the union of ; the union of is strictly contained in the union of , because only the latter is a superset of the non-empty set .
The preceeding four steps may be iterated a countable number of times starting from the assumed denumerable set of subsets to produce a denumerable sequence of the sets from each stage. Great caution is required to avoid ax-dc 8326 here; in particular an effective version of the pigeonhole principle (for aleph-null pigeons and 2 holes) is required. Since a denumerable set of subsets is assumed to exist, we can conclude without the axiom.
This sequence is strictly decreasing, thus it has no minimum, contradicting the first assumption. (Contributed by Stefan O'Rear, 2-Nov-2014.) (Proof shortened by Mario Carneiro, 17-May-2015.)
|1||isf33lem 8246||. 2 FinIII|
|2||1||fin23lem40 8231||1 FinII FinIII|
|Colors of variables: wff set class|
|Syntax hints: wi 4 wcel 1725 FinIIcfin2 8159 FinIIIcfin3 8161|
|This theorem is referenced by: fin1a2s 8294 finngch 8530|
|This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1555 ax-5 1566 ax-17 1626 ax-9 1666 ax-8 1687 ax-13 1727 ax-14 1729 ax-6 1744 ax-7 1749 ax-11 1761 ax-12 1950 ax-ext 2417 ax-rep 4320 ax-sep 4330 ax-nul 4338 ax-pow 4377 ax-pr 4403 ax-un 4701|
|This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1328 df-ex 1551 df-nf 1554 df-sb 1659 df-eu 2285 df-mo 2286 df-clab 2423 df-cleq 2429 df-clel 2432 df-nfc 2561 df-ne 2601 df-ral 2710 df-rex 2711 df-reu 2712 df-rmo 2713 df-rab 2714 df-v 2958 df-sbc 3162 df-csb 3252 df-dif 3323 df-un 3325 df-in 3327 df-ss 3334 df-pss 3336 df-nul 3629 df-if 3740 df-pw 3801 df-sn 3820 df-pr 3821 df-tp 3822 df-op 3823 df-uni 4016 df-int 4051 df-iun 4095 df-br 4213 df-opab 4267 df-mpt 4268 df-tr 4303 df-eprel 4494 df-id 4498 df-po 4503 df-so 4504 df-fr 4541 df-se 4542 df-we 4543 df-ord 4584 df-on 4585 df-lim 4586 df-suc 4587 df-om 4846 df-xp 4884 df-rel 4885 df-cnv 4886 df-co 4887 df-dm 4888 df-rn 4889 df-res 4890 df-ima 4891 df-iota 5418 df-fun 5456 df-fn 5457 df-f 5458 df-f1 5459 df-fo 5460 df-f1o 5461 df-fv 5462 df-isom 5463 df-ov 6084 df-oprab 6085 df-mpt2 6086 df-1st 6349 df-2nd 6350 df-rpss 6522 df-riota 6549 df-recs 6633 df-rdg 6668 df-seqom 6705 df-1o 6724 df-oadd 6728 df-er 6905 df-map 7020 df-en 7110 df-dom 7111 df-sdom 7112 df-fin 7113 df-wdom 7527 df-card 7826 df-fin2 8166 df-fin4 8167 df-fin3 8168|
|Copyright terms: Public domain||W3C validator|