|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 7989) 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 8117 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 8037||. 2 FinIII|
|2||1||fin23lem40 8022||1 FinII FinIII|
|Colors of variables: wff set class|
|Syntax hints: wi 4 wcel 1701 FinIIcfin2 7950 FinIIIcfin3 7952|
|This theorem is referenced by: fin1a2s 8085 finngch 8322|
|This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1537 ax-5 1548 ax-17 1607 ax-9 1645 ax-8 1666 ax-13 1703 ax-14 1705 ax-6 1720 ax-7 1725 ax-11 1732 ax-12 1897 ax-ext 2297 ax-rep 4168 ax-sep 4178 ax-nul 4186 ax-pow 4225 ax-pr 4251 ax-un 4549|
|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 1533 df-nf 1536 df-sb 1640 df-eu 2180 df-mo 2181 df-clab 2303 df-cleq 2309 df-clel 2312 df-nfc 2441 df-ne 2481 df-ral 2582 df-rex 2583 df-reu 2584 df-rmo 2585 df-rab 2586 df-v 2824 df-sbc 3026 df-csb 3116 df-dif 3189 df-un 3191 df-in 3193 df-ss 3200 df-pss 3202 df-nul 3490 df-if 3600 df-pw 3661 df-sn 3680 df-pr 3681 df-tp 3682 df-op 3683 df-uni 3865 df-int 3900 df-iun 3944 df-br 4061 df-opab 4115 df-mpt 4116 df-tr 4151 df-eprel 4342 df-id 4346 df-po 4351 df-so 4352 df-fr 4389 df-se 4390 df-we 4391 df-ord 4432 df-on 4433 df-lim 4434 df-suc 4435 df-om 4694 df-xp 4732 df-rel 4733 df-cnv 4734 df-co 4735 df-dm 4736 df-rn 4737 df-res 4738 df-ima 4739 df-iota 5256 df-fun 5294 df-fn 5295 df-f 5296 df-f1 5297 df-fo 5298 df-f1o 5299 df-fv 5300 df-isom 5301 df-ov 5903 df-oprab 5904 df-mpt2 5905 df-1st 6164 df-2nd 6165 df-rpss 6319 df-riota 6346 df-recs 6430 df-rdg 6465 df-seqom 6502 df-1o 6521 df-oadd 6525 df-er 6702 df-map 6817 df-en 6907 df-dom 6908 df-sdom 6909 df-fin 6910 df-wdom 7318 df-card 7617 df-fin2 7957 df-fin4 7958 df-fin3 7959|
|Copyright terms: Public domain||W3C validator|