|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 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 8748) 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 8876 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 8796||. 2 FinIII|
|2||1||fin23lem40 8781||1 FinII FinIII|
|Colors of variables: wff setvar class|
|Syntax hints: wi 4 wcel 1868 FinIIcfin2 8709 FinIIIcfin3 8711|
|This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1665 ax-4 1678 ax-5 1748 ax-6 1794 ax-7 1839 ax-8 1870 ax-9 1872 ax-10 1887 ax-11 1892 ax-12 1905 ax-13 2053 ax-ext 2400 ax-rep 4533 ax-sep 4543 ax-nul 4551 ax-pow 4598 ax-pr 4656 ax-un 6593|
|This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-tru 1440 df-ex 1660 df-nf 1664 df-sb 1787 df-eu 2269 df-mo 2270 df-clab 2408 df-cleq 2414 df-clel 2417 df-nfc 2572 df-ne 2620 df-ral 2780 df-rex 2781 df-reu 2782 df-rmo 2783 df-rab 2784 df-v 3083 df-sbc 3300 df-csb 3396 df-dif 3439 df-un 3441 df-in 3443 df-ss 3450 df-pss 3452 df-nul 3762 df-if 3910 df-pw 3981 df-sn 3997 df-pr 3999 df-tp 4001 df-op 4003 df-uni 4217 df-int 4253 df-iun 4298 df-br 4421 df-opab 4480 df-mpt 4481 df-tr 4516 df-eprel 4760 df-id 4764 df-po 4770 df-so 4771 df-fr 4808 df-se 4809 df-we 4810 df-xp 4855 df-rel 4856 df-cnv 4857 df-co 4858 df-dm 4859 df-rn 4860 df-res 4861 df-ima 4862 df-pred 5395 df-ord 5441 df-on 5442 df-lim 5443 df-suc 5444 df-iota 5561 df-fun 5599 df-fn 5600 df-f 5601 df-f1 5602 df-fo 5603 df-f1o 5604 df-fv 5605 df-isom 5606 df-riota 6263 df-ov 6304 df-oprab 6305 df-mpt2 6306 df-rpss 6581 df-om 6703 df-1st 6803 df-2nd 6804 df-wrecs 7032 df-recs 7094 df-rdg 7132 df-seqom 7169 df-1o 7186 df-oadd 7190 df-er 7367 df-map 7478 df-en 7574 df-dom 7575 df-sdom 7576 df-fin 7577 df-wdom 8076 df-card 8374 df-fin2 8716 df-fin4 8717 df-fin3 8718|
|This theorem is referenced by: fin1a2s 8844 finngch 9080 fin2so 31843|
|Copyright terms: Public domain||W3C validator|