|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 8499) 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 8627 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 8547||. 2 FinIII|
|2||1||fin23lem40 8532||1 FinII FinIII|
|Colors of variables: wff setvar class|
|Syntax hints: wi 4 wcel 1756 FinIIcfin2 8460 FinIIIcfin3 8462|
|This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2423 ax-rep 4415 ax-sep 4425 ax-nul 4433 ax-pow 4482 ax-pr 4543 ax-un 6384|
|This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2257 df-mo 2258 df-clab 2430 df-cleq 2436 df-clel 2439 df-nfc 2577 df-ne 2620 df-ral 2732 df-rex 2733 df-reu 2734 df-rmo 2735 df-rab 2736 df-v 2986 df-sbc 3199 df-csb 3301 df-dif 3343 df-un 3345 df-in 3347 df-ss 3354 df-pss 3356 df-nul 3650 df-if 3804 df-pw 3874 df-sn 3890 df-pr 3892 df-tp 3894 df-op 3896 df-uni 4104 df-int 4141 df-iun 4185 df-br 4305 df-opab 4363 df-mpt 4364 df-tr 4398 df-eprel 4644 df-id 4648 df-po 4653 df-so 4654 df-fr 4691 df-se 4692 df-we 4693 df-ord 4734 df-on 4735 df-lim 4736 df-suc 4737 df-xp 4858 df-rel 4859 df-cnv 4860 df-co 4861 df-dm 4862 df-rn 4863 df-res 4864 df-ima 4865 df-iota 5393 df-fun 5432 df-fn 5433 df-f 5434 df-f1 5435 df-fo 5436 df-f1o 5437 df-fv 5438 df-isom 5439 df-riota 6064 df-ov 6106 df-oprab 6107 df-mpt2 6108 df-rpss 6372 df-om 6489 df-1st 6589 df-2nd 6590 df-recs 6844 df-rdg 6878 df-seqom 6915 df-1o 6932 df-oadd 6936 df-er 7113 df-map 7228 df-en 7323 df-dom 7324 df-sdom 7325 df-fin 7326 df-wdom 7786 df-card 8121 df-fin2 8467 df-fin4 8468 df-fin3 8469|
|This theorem is referenced by: fin1a2s 8595 finngch 8834 fin2so 28428|
|Copyright terms: Public domain||W3C validator|