|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 7944) 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 8072 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 7992||. 2 FinIII|
|2||1||fin23lem40 7977||1 FinII FinIII|
|Colors of variables: wff set class|
|Syntax hints: wi 4 wcel 1684 FinIIcfin2 7905 FinIIIcfin3 7907|
|This theorem is referenced by: fin1a2s 8040 finngch 8277|
|This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1533 ax-5 1544 ax-17 1603 ax-9 1635 ax-8 1643 ax-13 1686 ax-14 1688 ax-6 1703 ax-7 1708 ax-11 1715 ax-12 1866 ax-ext 2264 ax-rep 4131 ax-sep 4141 ax-nul 4149 ax-pow 4188 ax-pr 4214 ax-un 4512|
|This theorem depends on definitions: df-bi 177 df-or 359 df-an 360 df-3or 935 df-3an 936 df-tru 1310 df-ex 1529 df-nf 1532 df-sb 1630 df-eu 2147 df-mo 2148 df-clab 2270 df-cleq 2276 df-clel 2279 df-nfc 2408 df-ne 2448 df-ral 2548 df-rex 2549 df-reu 2550 df-rmo 2551 df-rab 2552 df-v 2790 df-sbc 2992 df-csb 3082 df-dif 3155 df-un 3157 df-in 3159 df-ss 3166 df-pss 3168 df-nul 3456 df-if 3566 df-pw 3627 df-sn 3646 df-pr 3647 df-tp 3648 df-op 3649 df-uni 3828 df-int 3863 df-iun 3907 df-br 4024 df-opab 4078 df-mpt 4079 df-tr 4114 df-eprel 4305 df-id 4309 df-po 4314 df-so 4315 df-fr 4352 df-se 4353 df-we 4354 df-ord 4395 df-on 4396 df-lim 4397 df-suc 4398 df-om 4657 df-xp 4695 df-rel 4696 df-cnv 4697 df-co 4698 df-dm 4699 df-rn 4700 df-res 4701 df-ima 4702 df-iota 5219 df-fun 5257 df-fn 5258 df-f 5259 df-f1 5260 df-fo 5261 df-f1o 5262 df-fv 5263 df-isom 5264 df-ov 5861 df-oprab 5862 df-mpt2 5863 df-1st 6122 df-2nd 6123 df-rpss 6277 df-riota 6304 df-recs 6388 df-rdg 6423 df-seqom 6460 df-1o 6479 df-oadd 6483 df-er 6660 df-map 6774 df-en 6864 df-dom 6865 df-sdom 6866 df-fin 6867 df-wdom 7273 df-card 7572 df-fin2 7912 df-fin4 7913 df-fin3 7914|
|Copyright terms: Public domain||W3C validator|