Subsets of finite sets are finite

Proof

1. 1
   Reduction to subsets of numerals. Let be a bijection ( , D034). The restriction is a function ; it is injective (its values are values of the injective ), and it is surjective onto the image . So (D033). If every subset of the natural is finite, then for some , and transitivity (L22 (iii)) gives : is finite. It remains to prove that subsets of naturals are finite.
2. 2
   Induction on (T05 on , Separation). Base: forces (D001, D002, Extensionality), and via the empty function, which is vacuously a bijection (D013, D016). So .
3. 3
   Step, easy case: let and . If , then , and the hypothesis makes finite directly.
4. 4
   Step, peeling case: if , let (D009, singleton by D003), so , and the hypothesis gives a bijection for some . Extend by one pair: , a set by pairing and union. Then is a function on : the new argument is not in , so single-valuedness survives (L01).
5. 5
   is a bijection : injective: is injective with values in , and the new value differs from every value of , since and (L05 (i)). Surjective onto : the values of cover , and covers the top (D006). So : finite. T05 closes , and with step 1 the lemma follows.

Used by