|Metamath Proof Explorer||
|Mirrors > Home > MPE Home > Th. List > fin23||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 8145) 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 8273 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 8193||. 2 FinIII|
|2||1||fin23lem40 8178||1 FinII FinIII|
|Colors of variables: wff set class|
|Syntax hints: wi 4 wcel 1721 FinIIcfin2 8106 FinIIIcfin3 8108|
|This theorem is referenced by: fin1a2s 8241 finngch 8477|
|This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2382 ax-rep 4275 ax-sep 4285 ax-nul 4293 ax-pow 4332 ax-pr 4358 ax-un 4655|
|This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2256 df-mo 2257 df-clab 2388 df-cleq 2394 df-clel 2397 df-nfc 2526 df-ne 2566 df-ral 2668 df-rex 2669 df-reu 2670 df-rmo 2671 df-rab 2672 df-v 2915 df-sbc 3119 df-csb 3209 df-dif 3280 df-un 3282 df-in 3284 df-ss 3291 df-pss 3293 df-nul 3586 df-if 3697 df-pw 3758 df-sn 3777 df-pr 3778 df-tp 3779 df-op 3780 df-uni 3972 df-int 4007 df-iun 4051 df-br 4168 df-opab 4222 df-mpt 4223 df-tr 4258 df-eprel 4449 df-id 4453 df-po 4458 df-so 4459 df-fr 4496 df-se 4497 df-we 4498 df-ord 4539 df-on 4540 df-lim 4541 df-suc 4542 df-om 4800 df-xp 4838 df-rel 4839 df-cnv 4840 df-co 4841 df-dm 4842 df-rn 4843 df-res 4844 df-ima 4845 df-iota 5372 df-fun 5410 df-fn 5411 df-f 5412 df-f1 5413 df-fo 5414 df-f1o 5415 df-fv 5416 df-isom 5417 df-ov 6037 df-oprab 6038 df-mpt2 6039 df-1st 6302 df-2nd 6303 df-rpss 6472 df-riota 6499 df-recs 6583 df-rdg 6618 df-seqom 6655 df-1o 6674 df-oadd 6678 df-er 6855 df-map 6970 df-en 7060 df-dom 7061 df-sdom 7062 df-fin 7063 df-wdom 7474 df-card 7773 df-fin2 8113 df-fin4 8114 df-fin3 8115|
|Copyright terms: Public domain||W3C validator|