Metamath Proof Explorer

Theorem carden

Description: Two sets are equinumerous iff their cardinal numbers are equal. This important theorem expresses the essential concept behind "cardinality" or "size". This theorem appears as Proposition 10.10 of TakeutiZaring p. 85, Theorem 7P of Enderton p. 197, and Theorem 9 of Suppes p. 242 (among others). The Axiom of Choice is required for its proof. Related theorems are hasheni and the finite-set-only hashen .

This theorem is also known as Hume's Principle. Gottlob Frege's two-volumeGrundgesetze der Arithmetik used his Basic Law V to prove this theorem. Unfortunately Basic Law V caused Frege's system to be inconsistent because it was subject to Russell's paradox (see ru ). Later scholars have found that Frege primarily used Basic Law V to Hume's Principle. If Basic Law V is replaced by Hume's Principle in Frege's system, much of Frege's work is restored.Grundgesetze der Arithmetik, once Basic Law V is replaced, proves "Frege's theorem" (the Peano axioms of arithmetic can be derived in second-order logic from Hume's principle). See https://plato.stanford.edu/entries/frege-theorem . We take a different approach, using first-order logic and ZFC, to prove the Peano axioms of arithmetic.

The theory of cardinality can also be developed without AC by introducing "card" as a primitive notion and stating this theorem as an axiom, as is done with the axiom for cardinal numbers in Suppes p. 111. Finally, if we allow the Axiom of Regularity, we can avoid AC by defining the cardinal number of a set as the set of all sets equinumerous to it and having the least possible rank (see karden ). (Contributed by NM, 22-Oct-2003)

Ref Expression
Assertion carden ⊢ A ∈ C ∧ B ∈ D → card ⁡ A = card ⁡ B ↔ A ≈ B

Proof

Step Hyp Ref Expression
1 numth3 ⊢ A ∈ C → A ∈ dom ⁡ card
2 1 ad2antrr ⊢ A ∈ C ∧ B ∈ D ∧ card ⁡ A = card ⁡ B → A ∈ dom ⁡ card
3 cardid2 ⊢ A ∈ dom ⁡ card → card ⁡ A ≈ A
4 ensym ⊢ card ⁡ A ≈ A → A ≈ card ⁡ A
5 2 3 4 3syl ⊢ A ∈ C ∧ B ∈ D ∧ card ⁡ A = card ⁡ B → A ≈ card ⁡ A
6 simpr ⊢ A ∈ C ∧ B ∈ D ∧ card ⁡ A = card ⁡ B → card ⁡ A = card ⁡ B
7 numth3 ⊢ B ∈ D → B ∈ dom ⁡ card
8 7 ad2antlr ⊢ A ∈ C ∧ B ∈ D ∧ card ⁡ A = card ⁡ B → B ∈ dom ⁡ card
9 8 cardidd ⊢ A ∈ C ∧ B ∈ D ∧ card ⁡ A = card ⁡ B → card ⁡ B ≈ B
10 6 9 eqbrtrd ⊢ A ∈ C ∧ B ∈ D ∧ card ⁡ A = card ⁡ B → card ⁡ A ≈ B
11 entr ⊢ A ≈ card ⁡ A ∧ card ⁡ A ≈ B → A ≈ B
12 5 10 11 syl2anc ⊢ A ∈ C ∧ B ∈ D ∧ card ⁡ A = card ⁡ B → A ≈ B
13 12 ex ⊢ A ∈ C ∧ B ∈ D → card ⁡ A = card ⁡ B → A ≈ B
14 carden2b ⊢ A ≈ B → card ⁡ A = card ⁡ B
15 13 14 impbid1 ⊢ A ∈ C ∧ B ∈ D → card ⁡ A = card ⁡ B ↔ A ≈ B