Skip to content
Axiomatic Wiki
Lemma·L34

A subset of the full size is everything

A subset of a finite set whose cardinality equals the whole set's must be the whole set.

If is finite, (D001), and (D035), then .
In words
Inside a finite set, a subset that has just as many elements as the whole set cannot be missing any of them, so it is the whole set.
Rests onF02F03F04F05F06F08F09F11F12F14A01A02A06A08
Never needed: F10 · F13 · A03 · A04 · A05 · A07 (computed from the citation graph, not asserted).

Proof

  1. 1
    Split into disjoint pieces (D009: each either lies in or not, excluded middle, and supplies the rest). Both pieces are finite: by hypothesis, and by L24.
  2. 2
    By L26, . Since and (D027), we get , and cancellation L10 gives .
  3. 3
    A set of cardinality is empty: a bijection (D002) can have no argument, since an argument would be sent to a member of . So .
  4. 4
    Then no satisfies (D009), i.e. ; with the hypothesis , Extensionality gives .
∎

Remarks

The finiteness is essential: the even naturals are a proper subset of yet equinumerous with it. The lemma is the counting fact behind prime-order groups being cyclic: a cyclic subgroup of full size must be the whole group.
Wikipedia ↗Finset.eq_of_subset_of_card_le ↗

Used by

T16
Propose an edit1 published revision