|Metamath Proof Explorer||
|Mirrors > Home > MPE Home > Th. List > fin23||Structured version Visualization 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 nonempty 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 8766) this sequence contains its intersection, call it ; since by induction every subset in the sequence is nonempty, the intersection must be nonempty.
Suppose that an element of has nonempty intersection with . Thus, said element has a nonempty 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 nonempty set .
The preceding 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 8894 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 8814||. 2 FinIII|
|2||1||fin23lem40 8799||1 FinII FinIII|
|Colors of variables: wff setvar class|
|Syntax hints: wi 4 wcel 1904 FinIIcfin2 8727 FinIIIcfin3 8729|
|This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-rep 4508 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602|
|This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-int 4227 df-iun 4271 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-se 4799 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-isom 5598 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-rpss 6590 df-om 6712 df-1st 6812 df-2nd 6813 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-seqom 7183 df-1o 7200 df-oadd 7204 df-er 7381 df-map 7492 df-en 7588 df-dom 7589 df-sdom 7590 df-fin 7591 df-wdom 8092 df-card 8391 df-fin2 8734 df-fin4 8735 df-fin3 8736|
|This theorem is referenced by: fin1a2s 8862 finngch 9098 fin2so 31996|
|Copyright terms: Public domain||W3C validator|