Home | Metamath
Proof Explorer Theorem List (p. 88 of 424) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | isinffi 8701* | An infinite set contains subsets equinumerous to every finite set. Extension of isinf 8058 from finite ordinals to all finite sets. (Contributed by Stefan O'Rear, 8-Oct-2014.) |
⊢ ((¬ 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ∃𝑓 𝑓:𝐵–1-1→𝐴) | ||
Theorem | fidomtri 8702 | Trichotomy of dominance without AC when one set is finite. (Contributed by Stefan O'Rear, 30-Oct-2014.) (Revised by Mario Carneiro, 27-Apr-2015.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) → (𝐴 ≼ 𝐵 ↔ ¬ 𝐵 ≺ 𝐴)) | ||
Theorem | fidomtri2 8703 | Trichotomy of dominance without AC when one set is finite. (Contributed by Stefan O'Rear, 30-Oct-2014.) (Revised by Mario Carneiro, 7-May-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin) → (𝐴 ≼ 𝐵 ↔ ¬ 𝐵 ≺ 𝐴)) | ||
Theorem | harsdom 8704 | The Hartogs number of a well-orderable set strictly dominates the set. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ (𝐴 ∈ dom card → 𝐴 ≺ (har‘𝐴)) | ||
Theorem | onsdom 8705* | Any well-orderable set is strictly dominated by an ordinal number. (Contributed by Jeff Hankins, 22-Oct-2009.) (Proof shortened by Mario Carneiro, 15-May-2015.) |
⊢ (𝐴 ∈ dom card → ∃𝑥 ∈ On 𝐴 ≺ 𝑥) | ||
Theorem | harval2 8706* | An alternate expression for the Hartogs number of a well-orderable set. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ (𝐴 ∈ dom card → (har‘𝐴) = ∩ {𝑥 ∈ On ∣ 𝐴 ≺ 𝑥}) | ||
Theorem | cardmin2 8707* | The smallest ordinal that strictly dominates a set is a cardinal, if it exists. (Contributed by Mario Carneiro, 2-Feb-2013.) |
⊢ (∃𝑥 ∈ On 𝐴 ≺ 𝑥 ↔ (card‘∩ {𝑥 ∈ On ∣ 𝐴 ≺ 𝑥}) = ∩ {𝑥 ∈ On ∣ 𝐴 ≺ 𝑥}) | ||
Theorem | pm54.43lem 8708* | In Theorem *54.43 of [WhiteheadRussell] p. 360, the number 1 is defined as the collection of all sets with cardinality 1 (i.e. all singletons; see card1 8677), so that their 𝐴 ∈ 1 means, in our notation, 𝐴 ∈ {𝑥 ∣ (card‘𝑥) = 1𝑜}. Here we show that this is equivalent to 𝐴 ≈ 1𝑜 so that we can use the latter more convenient notation in pm54.43 8709. (Contributed by NM, 4-Nov-2013.) |
⊢ (𝐴 ≈ 1𝑜 ↔ 𝐴 ∈ {𝑥 ∣ (card‘𝑥) = 1𝑜}) | ||
Theorem | pm54.43 8709 |
Theorem *54.43 of [WhiteheadRussell]
p. 360. "From this proposition it
will follow, when arithmetical addition has been defined, that
1+1=2."
See http://en.wikipedia.org/wiki/Principia_Mathematica#Quotations.
This theorem states that two sets of cardinality 1 are disjoint iff
their union has cardinality 2.
Whitehead and Russell define 1 as the collection of all sets with cardinality 1 (i.e. all singletons; see card1 8677), so that their 𝐴 ∈ 1 means, in our notation, 𝐴 ∈ {𝑥 ∣ (card‘𝑥) = 1𝑜} which is the same as 𝐴 ≈ 1𝑜 by pm54.43lem 8708. We do not have several of their earlier lemmas available (which would otherwise be unused by our different approach to arithmetic), so our proof is longer. (It is also longer because we must show every detail.) Theorem pm110.643 8882 shows the derivation of 1+1=2 for cardinal numbers from this theorem. (Contributed by NM, 4-Apr-2007.) |
⊢ ((𝐴 ≈ 1𝑜 ∧ 𝐵 ≈ 1𝑜) → ((𝐴 ∩ 𝐵) = ∅ ↔ (𝐴 ∪ 𝐵) ≈ 2𝑜)) | ||
Theorem | pr2nelem 8710 | Lemma for pr2ne 8711. (Contributed by FL, 17-Aug-2008.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵) → {𝐴, 𝐵} ≈ 2𝑜) | ||
Theorem | pr2ne 8711 | If an unordered pair has two elements they are different. (Contributed by FL, 14-Feb-2010.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ({𝐴, 𝐵} ≈ 2𝑜 ↔ 𝐴 ≠ 𝐵)) | ||
Theorem | prdom2 8712 | An unordered pair has at most two elements. (Contributed by FL, 22-Feb-2011.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → {𝐴, 𝐵} ≼ 2𝑜) | ||
Theorem | en2eqpr 8713 | Building a set with two elements. (Contributed by FL, 11-Aug-2008.) (Revised by Mario Carneiro, 10-Sep-2015.) |
⊢ ((𝐶 ≈ 2𝑜 ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → (𝐴 ≠ 𝐵 → 𝐶 = {𝐴, 𝐵})) | ||
Theorem | en2eleq 8714 | Express a set of pair cardinality as the unordered pair of a given element and the other element. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2𝑜) → 𝑃 = {𝑋, ∪ (𝑃 ∖ {𝑋})}) | ||
Theorem | en2other2 8715 | Taking the other element twice in a pair gets back to the original element. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2𝑜) → ∪ (𝑃 ∖ {∪ (𝑃 ∖ {𝑋})}) = 𝑋) | ||
Theorem | dif1card 8716 | The cardinality of a nonempty finite set is one greater than the cardinality of the set with one element removed. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 2-Feb-2013.) |
⊢ ((𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐴) → (card‘𝐴) = suc (card‘(𝐴 ∖ {𝑋}))) | ||
Theorem | leweon 8717* | Lexicographical order is a well-ordering of On × On. Proposition 7.56(1) of [TakeutiZaring] p. 54. Note that unlike r0weon 8718, this order is not set-like, as the preimage of 〈1𝑜, ∅〉 is the proper class ({∅} × On). (Contributed by Mario Carneiro, 9-Mar-2013.) |
⊢ 𝐿 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧ ((1st ‘𝑥) ∈ (1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd ‘𝑥) ∈ (2nd ‘𝑦))))} ⇒ ⊢ 𝐿 We (On × On) | ||
Theorem | r0weon 8718* | A set-like well-ordering of the class of ordinal pairs. Proposition 7.58(1) of [TakeutiZaring] p. 54. (Contributed by Mario Carneiro, 7-Mar-2013.) (Revised by Mario Carneiro, 26-Jun-2015.) |
⊢ 𝐿 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧ ((1st ‘𝑥) ∈ (1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd ‘𝑥) ∈ (2nd ‘𝑦))))} & ⊢ 𝑅 = {〈𝑧, 𝑤〉 ∣ ((𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On)) ∧ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∨ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∧ 𝑧𝐿𝑤)))} ⇒ ⊢ (𝑅 We (On × On) ∧ 𝑅 Se (On × On)) | ||
Theorem | infxpenlem 8719* | Lemma for infxpen 8720. (Contributed by Mario Carneiro, 9-Mar-2013.) (Revised by Mario Carneiro, 26-Jun-2015.) |
⊢ 𝐿 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧ ((1st ‘𝑥) ∈ (1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd ‘𝑥) ∈ (2nd ‘𝑦))))} & ⊢ 𝑅 = {〈𝑧, 𝑤〉 ∣ ((𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On)) ∧ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∨ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∧ 𝑧𝐿𝑤)))} & ⊢ 𝑄 = (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎))) & ⊢ (𝜑 ↔ ((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎))) & ⊢ 𝑀 = ((1st ‘𝑤) ∪ (2nd ‘𝑤)) & ⊢ 𝐽 = OrdIso(𝑄, (𝑎 × 𝑎)) ⇒ ⊢ ((𝐴 ∈ On ∧ ω ⊆ 𝐴) → (𝐴 × 𝐴) ≈ 𝐴) | ||
Theorem | infxpen 8720 | Every infinite ordinal is equinumerous to its Cartesian product. Proposition 10.39 of [TakeutiZaring] p. 94, whose proof we follow closely. The key idea is to show that the relation 𝑅 is a well-ordering of (On × On) with the additional property that 𝑅-initial segments of (𝑥 × 𝑥) (where 𝑥 is a limit ordinal) are of cardinality at most 𝑥. (Contributed by Mario Carneiro, 9-Mar-2013.) (Revised by Mario Carneiro, 26-Jun-2015.) |
⊢ ((𝐴 ∈ On ∧ ω ⊆ 𝐴) → (𝐴 × 𝐴) ≈ 𝐴) | ||
Theorem | xpomen 8721 | The Cartesian product of omega (the set of ordinal natural numbers) with itself is equinumerous to omega. Exercise 1 of [Enderton] p. 133. (Contributed by NM, 23-Jul-2004.) (Revised by Mario Carneiro, 9-Mar-2013.) |
⊢ (ω × ω) ≈ ω | ||
Theorem | xpct 8722 | The cartesian product of two countable sets is countable. (Contributed by Thierry Arnoux, 24-Sep-2017.) |
⊢ ((𝐴 ≼ ω ∧ 𝐵 ≼ ω) → (𝐴 × 𝐵) ≼ ω) | ||
Theorem | infxpidm2 8723 | The Cartesian product of an infinite set with itself is idempotent. This theorem provides the basis for infinite cardinal arithmetic. Proposition 10.40 of [TakeutiZaring] p. 95. See also infxpidm 9263. (Contributed by Mario Carneiro, 9-Mar-2013.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ ((𝐴 ∈ dom card ∧ ω ≼ 𝐴) → (𝐴 × 𝐴) ≈ 𝐴) | ||
Theorem | infxpenc 8724* | A canonical version of infxpen 8720, by a completely different approach (although it uses infxpen 8720 via xpomen 8721). Using Cantor's normal form, we can show that 𝐴 ↑𝑜 𝐵 respects equinumerosity (oef1o 8478), so that all the steps of (ω↑𝑊) · (ω↑𝑊) ≈ ω↑(2𝑊) ≈ (ω↑2)↑𝑊 ≈ ω↑𝑊 can be verified using bijections to do the ordinal commutations. (The assumption on 𝑁 can be satisfied using cnfcom3c 8486.) (Contributed by Mario Carneiro, 30-May-2015.) (Revised by AV, 7-Jul-2019.) |
⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → ω ⊆ 𝐴) & ⊢ (𝜑 → 𝑊 ∈ (On ∖ 1𝑜)) & ⊢ (𝜑 → 𝐹:(ω ↑𝑜 2𝑜)–1-1-onto→ω) & ⊢ (𝜑 → (𝐹‘∅) = ∅) & ⊢ (𝜑 → 𝑁:𝐴–1-1-onto→(ω ↑𝑜 𝑊)) & ⊢ 𝐾 = (𝑦 ∈ {𝑥 ∈ ((ω ↑𝑜 2𝑜) ↑𝑚 𝑊) ∣ 𝑥 finSupp ∅} ↦ (𝐹 ∘ (𝑦 ∘ ◡( I ↾ 𝑊)))) & ⊢ 𝐻 = (((ω CNF 𝑊) ∘ 𝐾) ∘ ◡((ω ↑𝑜 2𝑜) CNF 𝑊)) & ⊢ 𝐿 = (𝑦 ∈ {𝑥 ∈ (ω ↑𝑚 (𝑊 ·𝑜 2𝑜)) ∣ 𝑥 finSupp ∅} ↦ (( I ↾ ω) ∘ (𝑦 ∘ ◡(𝑌 ∘ ◡𝑋)))) & ⊢ 𝑋 = (𝑧 ∈ 2𝑜, 𝑤 ∈ 𝑊 ↦ ((𝑊 ·𝑜 𝑧) +𝑜 𝑤)) & ⊢ 𝑌 = (𝑧 ∈ 2𝑜, 𝑤 ∈ 𝑊 ↦ ((2𝑜 ·𝑜 𝑤) +𝑜 𝑧)) & ⊢ 𝐽 = (((ω CNF (2𝑜 ·𝑜 𝑊)) ∘ 𝐿) ∘ ◡(ω CNF (𝑊 ·𝑜 2𝑜))) & ⊢ 𝑍 = (𝑥 ∈ (ω ↑𝑜 𝑊), 𝑦 ∈ (ω ↑𝑜 𝑊) ↦ (((ω ↑𝑜 𝑊) ·𝑜 𝑥) +𝑜 𝑦)) & ⊢ 𝑇 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝑁‘𝑥), (𝑁‘𝑦)〉) & ⊢ 𝐺 = (◡𝑁 ∘ (((𝐻 ∘ 𝐽) ∘ 𝑍) ∘ 𝑇)) ⇒ ⊢ (𝜑 → 𝐺:(𝐴 × 𝐴)–1-1-onto→𝐴) | ||
Theorem | infxpenc2lem1 8725* | Lemma for infxpenc2 8728. (Contributed by Mario Carneiro, 30-May-2015.) |
⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → ∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1𝑜)(𝑛‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤))) & ⊢ 𝑊 = (◡(𝑥 ∈ (On ∖ 1𝑜) ↦ (ω ↑𝑜 𝑥))‘ran (𝑛‘𝑏)) ⇒ ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) → (𝑊 ∈ (On ∖ 1𝑜) ∧ (𝑛‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑊))) | ||
Theorem | infxpenc2lem2 8726* | Lemma for infxpenc2 8728. (Contributed by Mario Carneiro, 30-May-2015.) (Revised by AV, 7-Jul-2019.) |
⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → ∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1𝑜)(𝑛‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤))) & ⊢ 𝑊 = (◡(𝑥 ∈ (On ∖ 1𝑜) ↦ (ω ↑𝑜 𝑥))‘ran (𝑛‘𝑏)) & ⊢ (𝜑 → 𝐹:(ω ↑𝑜 2𝑜)–1-1-onto→ω) & ⊢ (𝜑 → (𝐹‘∅) = ∅) & ⊢ 𝐾 = (𝑦 ∈ {𝑥 ∈ ((ω ↑𝑜 2𝑜) ↑𝑚 𝑊) ∣ 𝑥 finSupp ∅} ↦ (𝐹 ∘ (𝑦 ∘ ◡( I ↾ 𝑊)))) & ⊢ 𝐻 = (((ω CNF 𝑊) ∘ 𝐾) ∘ ◡((ω ↑𝑜 2𝑜) CNF 𝑊)) & ⊢ 𝐿 = (𝑦 ∈ {𝑥 ∈ (ω ↑𝑚 (𝑊 ·𝑜 2𝑜)) ∣ 𝑥 finSupp ∅} ↦ (( I ↾ ω) ∘ (𝑦 ∘ ◡(𝑌 ∘ ◡𝑋)))) & ⊢ 𝑋 = (𝑧 ∈ 2𝑜, 𝑤 ∈ 𝑊 ↦ ((𝑊 ·𝑜 𝑧) +𝑜 𝑤)) & ⊢ 𝑌 = (𝑧 ∈ 2𝑜, 𝑤 ∈ 𝑊 ↦ ((2𝑜 ·𝑜 𝑤) +𝑜 𝑧)) & ⊢ 𝐽 = (((ω CNF (2𝑜 ·𝑜 𝑊)) ∘ 𝐿) ∘ ◡(ω CNF (𝑊 ·𝑜 2𝑜))) & ⊢ 𝑍 = (𝑥 ∈ (ω ↑𝑜 𝑊), 𝑦 ∈ (ω ↑𝑜 𝑊) ↦ (((ω ↑𝑜 𝑊) ·𝑜 𝑥) +𝑜 𝑦)) & ⊢ 𝑇 = (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ 〈((𝑛‘𝑏)‘𝑥), ((𝑛‘𝑏)‘𝑦)〉) & ⊢ 𝐺 = (◡(𝑛‘𝑏) ∘ (((𝐻 ∘ 𝐽) ∘ 𝑍) ∘ 𝑇)) ⇒ ⊢ (𝜑 → ∃𝑔∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → (𝑔‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) | ||
Theorem | infxpenc2lem3 8727* | Lemma for infxpenc2 8728. (Contributed by Mario Carneiro, 30-May-2015.) (Revised by AV, 7-Jul-2019.) |
⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → ∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1𝑜)(𝑛‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤))) & ⊢ 𝑊 = (◡(𝑥 ∈ (On ∖ 1𝑜) ↦ (ω ↑𝑜 𝑥))‘ran (𝑛‘𝑏)) & ⊢ (𝜑 → 𝐹:(ω ↑𝑜 2𝑜)–1-1-onto→ω) & ⊢ (𝜑 → (𝐹‘∅) = ∅) ⇒ ⊢ (𝜑 → ∃𝑔∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → (𝑔‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) | ||
Theorem | infxpenc2 8728* | Existence form of infxpenc 8724. A "uniform" or "canonical" version of infxpen 8720, asserting the existence of a single function 𝑔 that simultaneously demonstrates product idempotence of all ordinals below a given bound. (Contributed by Mario Carneiro, 30-May-2015.) |
⊢ (𝐴 ∈ On → ∃𝑔∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → (𝑔‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) | ||
Theorem | iunmapdisj 8729* | The union ∪ 𝑛 ∈ 𝐶(𝐴 ↑𝑚 𝑛) is a disjoint union. (Contributed by Mario Carneiro, 17-May-2015.) (Revised by NM, 16-Jun-2017.) |
⊢ ∃*𝑛 ∈ 𝐶 𝐵 ∈ (𝐴 ↑𝑚 𝑛) | ||
Theorem | fseqenlem1 8730* | Lemma for fseqen 8733. (Contributed by Mario Carneiro, 17-May-2015.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) & ⊢ (𝜑 → 𝐹:(𝐴 × 𝐴)–1-1-onto→𝐴) & ⊢ 𝐺 = seq𝜔((𝑛 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝐴 ↑𝑚 suc 𝑛) ↦ ((𝑓‘(𝑥 ↾ 𝑛))𝐹(𝑥‘𝑛)))), {〈∅, 𝐵〉}) ⇒ ⊢ ((𝜑 ∧ 𝐶 ∈ ω) → (𝐺‘𝐶):(𝐴 ↑𝑚 𝐶)–1-1→𝐴) | ||
Theorem | fseqenlem2 8731* | Lemma for fseqen 8733. (Contributed by Mario Carneiro, 17-May-2015.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) & ⊢ (𝜑 → 𝐹:(𝐴 × 𝐴)–1-1-onto→𝐴) & ⊢ 𝐺 = seq𝜔((𝑛 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝐴 ↑𝑚 suc 𝑛) ↦ ((𝑓‘(𝑥 ↾ 𝑛))𝐹(𝑥‘𝑛)))), {〈∅, 𝐵〉}) & ⊢ 𝐾 = (𝑦 ∈ ∪ 𝑘 ∈ ω (𝐴 ↑𝑚 𝑘) ↦ 〈dom 𝑦, ((𝐺‘dom 𝑦)‘𝑦)〉) ⇒ ⊢ (𝜑 → 𝐾:∪ 𝑘 ∈ ω (𝐴 ↑𝑚 𝑘)–1-1→(ω × 𝐴)) | ||
Theorem | fseqdom 8732* | One half of fseqen 8733. (Contributed by Mario Carneiro, 18-Nov-2014.) |
⊢ (𝐴 ∈ 𝑉 → (ω × 𝐴) ≼ ∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛)) | ||
Theorem | fseqen 8733* | A set that is equinumerous to its Cartesian product is equinumerous to the set of finite sequences on it. (This can be proven more easily using some choice but this proof avoids it.) (Contributed by Mario Carneiro, 18-Nov-2014.) |
⊢ (((𝐴 × 𝐴) ≈ 𝐴 ∧ 𝐴 ≠ ∅) → ∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛) ≈ (ω × 𝐴)) | ||
Theorem | infpwfidom 8734 | The collection of finite subsets of a set dominates the set. (We use the weaker sethood assumption (𝒫 𝐴 ∩ Fin) ∈ V because this theorem also implies that 𝐴 is a set if 𝒫 𝐴 ∩ Fin is.) (Contributed by Mario Carneiro, 17-May-2015.) |
⊢ ((𝒫 𝐴 ∩ Fin) ∈ V → 𝐴 ≼ (𝒫 𝐴 ∩ Fin)) | ||
Theorem | dfac8alem 8735* | Lemma for dfac8a 8736. If the power set of a set has a choice function, then the set is numerable. (Contributed by NM, 10-Feb-1997.) (Revised by Mario Carneiro, 5-Jan-2013.) |
⊢ 𝐹 = recs(𝐺) & ⊢ 𝐺 = (𝑓 ∈ V ↦ (𝑔‘(𝐴 ∖ ran 𝑓))) ⇒ ⊢ (𝐴 ∈ 𝐶 → (∃𝑔∀𝑦 ∈ 𝒫 𝐴(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) → 𝐴 ∈ dom card)) | ||
Theorem | dfac8a 8736* | Numeration theorem: every set with a choice function on its power set is numerable. With AC, this reduces to the statement that every set is numerable. Similar to Theorem 10.3 of [TakeutiZaring] p. 84. (Contributed by NM, 10-Feb-1997.) (Revised by Mario Carneiro, 5-Jan-2013.) |
⊢ (𝐴 ∈ 𝐵 → (∃ℎ∀𝑦 ∈ 𝒫 𝐴(𝑦 ≠ ∅ → (ℎ‘𝑦) ∈ 𝑦) → 𝐴 ∈ dom card)) | ||
Theorem | dfac8b 8737* | The well-ordering theorem: every numerable set is well-orderable. (Contributed by Mario Carneiro, 5-Jan-2013.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ (𝐴 ∈ dom card → ∃𝑥 𝑥 We 𝐴) | ||
Theorem | dfac8clem 8738* | Lemma for dfac8c 8739. (Contributed by Mario Carneiro, 10-Jan-2013.) |
⊢ 𝐹 = (𝑠 ∈ (𝐴 ∖ {∅}) ↦ (℩𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ¬ 𝑏𝑟𝑎)) ⇒ ⊢ (𝐴 ∈ 𝐵 → (∃𝑟 𝑟 We ∪ 𝐴 → ∃𝑓∀𝑧 ∈ 𝐴 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))) | ||
Theorem | dfac8c 8739* | If the union of a set is well-orderable, then the set has a choice function. (Contributed by Mario Carneiro, 5-Jan-2013.) |
⊢ (𝐴 ∈ 𝐵 → (∃𝑟 𝑟 We ∪ 𝐴 → ∃𝑓∀𝑧 ∈ 𝐴 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))) | ||
Theorem | ac10ct 8740* | A proof of the Well ordering theorem weth 9200, an Axiom of Choice equivalent, restricted to sets dominated by some ordinal (in particular finite sets and countable sets), proven in ZF without AC. (Contributed by Mario Carneiro, 5-Jan-2013.) |
⊢ (∃𝑦 ∈ On 𝐴 ≼ 𝑦 → ∃𝑥 𝑥 We 𝐴) | ||
Theorem | ween 8741* | A set is numerable iff it can be well-ordered. (Contributed by Mario Carneiro, 5-Jan-2013.) |
⊢ (𝐴 ∈ dom card ↔ ∃𝑟 𝑟 We 𝐴) | ||
Theorem | ac5num 8742* | A version of ac5b 9183 with the choice as a hypothesis. (Contributed by Mario Carneiro, 27-Aug-2015.) |
⊢ ((∪ 𝐴 ∈ dom card ∧ ¬ ∅ ∈ 𝐴) → ∃𝑓(𝑓:𝐴⟶∪ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝑥)) | ||
Theorem | ondomen 8743 | If a set is dominated by an ordinal, then it is numerable. (Contributed by Mario Carneiro, 5-Jan-2013.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ≼ 𝐴) → 𝐵 ∈ dom card) | ||
Theorem | numdom 8744 | A set dominated by a numerable set is numerable. (Contributed by Mario Carneiro, 28-Apr-2015.) |
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ≼ 𝐴) → 𝐵 ∈ dom card) | ||
Theorem | ssnum 8745 | A subset of a numerable set is numerable. (Contributed by Mario Carneiro, 28-Apr-2015.) |
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ dom card) | ||
Theorem | onssnum 8746 | All subsets of the ordinals are numerable. (Contributed by Mario Carneiro, 12-Feb-2013.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ On) → 𝐴 ∈ dom card) | ||
Theorem | indcardi 8747* | Indirect strong induction on the cardinality of a finite or numerable set. (Contributed by Stefan O'Rear, 24-Aug-2015.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑇 ∈ dom card) & ⊢ ((𝜑 ∧ 𝑅 ≼ 𝑇 ∧ ∀𝑦(𝑆 ≺ 𝑅 → 𝜒)) → 𝜓) & ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)) & ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃)) & ⊢ (𝑥 = 𝑦 → 𝑅 = 𝑆) & ⊢ (𝑥 = 𝐴 → 𝑅 = 𝑇) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | acnrcl 8748 | Reverse closure for the choice set predicate. (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ (𝑋 ∈ AC 𝐴 → 𝐴 ∈ V) | ||
Theorem | acneq 8749 | Equality theorem for the choice set function. (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ (𝐴 = 𝐶 → AC 𝐴 = AC 𝐶) | ||
Theorem | isacn 8750* | The property of being a choice set of length 𝐴. (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝑋 ∈ AC 𝐴 ↔ ∀𝑓 ∈ ((𝒫 𝑋 ∖ {∅}) ↑𝑚 𝐴)∃𝑔∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝑓‘𝑥))) | ||
Theorem | acni 8751* | The property of being a choice set of length 𝐴. (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ ((𝑋 ∈ AC 𝐴 ∧ 𝐹:𝐴⟶(𝒫 𝑋 ∖ {∅})) → ∃𝑔∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝐹‘𝑥)) | ||
Theorem | acni2 8752* | The property of being a choice set of length 𝐴. (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ ((𝑋 ∈ AC 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐵 ⊆ 𝑋 ∧ 𝐵 ≠ ∅)) → ∃𝑔(𝑔:𝐴⟶𝑋 ∧ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ 𝐵)) | ||
Theorem | acni3 8753* | The property of being a choice set of length 𝐴. (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ (𝑦 = (𝑔‘𝑥) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝑋 ∈ AC 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑋 𝜑) → ∃𝑔(𝑔:𝐴⟶𝑋 ∧ ∀𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | acnlem 8754* | Construct a mapping satisfying the consequent of isacn 8750. (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (𝑓‘𝑥)) → ∃𝑔∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝑓‘𝑥)) | ||
Theorem | numacn 8755 | A well-orderable set has choice sequences of every length. (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ (𝐴 ∈ 𝑉 → (𝑋 ∈ dom card → 𝑋 ∈ AC 𝐴)) | ||
Theorem | finacn 8756 | Every set has finite choice sequences. (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ (𝐴 ∈ Fin → AC 𝐴 = V) | ||
Theorem | acndom 8757 | A set with long choice sequences also has shorter choice sequences, where "shorter" here means the new index set is dominated by the old index set. (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ (𝐴 ≼ 𝐵 → (𝑋 ∈ AC 𝐵 → 𝑋 ∈ AC 𝐴)) | ||
Theorem | acnnum 8758 | A set 𝑋 which has choice sequences on it of length 𝒫 𝑋 is well-orderable (and hence has choice sequences of every length). (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ (𝑋 ∈ AC 𝒫 𝑋 ↔ 𝑋 ∈ dom card) | ||
Theorem | acnen 8759 | The class of choice sets of length 𝐴 is a cardinal invariant. (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ (𝐴 ≈ 𝐵 → AC 𝐴 = AC 𝐵) | ||
Theorem | acndom2 8760 | A set smaller than one with choice sequences of length 𝐴 also has choice sequences of length 𝐴. (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ (𝑋 ≼ 𝑌 → (𝑌 ∈ AC 𝐴 → 𝑋 ∈ AC 𝐴)) | ||
Theorem | acnen2 8761 | The class of sets with choice sequences of length 𝐴 is a cardinal invariant. (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ (𝑋 ≈ 𝑌 → (𝑋 ∈ AC 𝐴 ↔ 𝑌 ∈ AC 𝐴)) | ||
Theorem | fodomacn 8762 | A version of fodom 9227 that doesn't require the Axiom of Choice ax-ac 9164. If 𝐴 has choice sequences of length 𝐵, then any surjection from 𝐴 to 𝐵 can be inverted to an injection the other way. (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ (𝐴 ∈ AC 𝐵 → (𝐹:𝐴–onto→𝐵 → 𝐵 ≼ 𝐴)) | ||
Theorem | fodomnum 8763 | A version of fodom 9227 that doesn't require the Axiom of Choice ax-ac 9164. (Contributed by Mario Carneiro, 28-Feb-2013.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝐴 ∈ dom card → (𝐹:𝐴–onto→𝐵 → 𝐵 ≼ 𝐴)) | ||
Theorem | fonum 8764 | A surjection maps numerable sets to numerable sets. (Contributed by Mario Carneiro, 30-Apr-2015.) |
⊢ ((𝐴 ∈ dom card ∧ 𝐹:𝐴–onto→𝐵) → 𝐵 ∈ dom card) | ||
Theorem | numwdom 8765 | A surjection maps numerable sets to numerable sets. (Contributed by Mario Carneiro, 27-Aug-2015.) |
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ≼* 𝐴) → 𝐵 ∈ dom card) | ||
Theorem | fodomfi2 8766 | Onto functions define dominance when a finite number of choices need to be made. (Contributed by Stefan O'Rear, 28-Feb-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) → 𝐵 ≼ 𝐴) | ||
Theorem | wdomfil 8767 | Weak dominance agrees with normal for finite left sets. (Contributed by Stefan O'Rear, 28-Feb-2015.) (Revised by Mario Carneiro, 5-May-2015.) |
⊢ (𝑋 ∈ Fin → (𝑋 ≼* 𝑌 ↔ 𝑋 ≼ 𝑌)) | ||
Theorem | infpwfien 8768 | Any infinite well-orderable set is equinumerous to its set of finite subsets. (Contributed by Mario Carneiro, 18-May-2015.) |
⊢ ((𝐴 ∈ dom card ∧ ω ≼ 𝐴) → (𝒫 𝐴 ∩ Fin) ≈ 𝐴) | ||
Theorem | inffien 8769 | The set of finite intersections of an infinite well-orderable set is equinumerous to the set itself. (Contributed by Mario Carneiro, 18-May-2015.) |
⊢ ((𝐴 ∈ dom card ∧ ω ≼ 𝐴) → (fi‘𝐴) ≈ 𝐴) | ||
Theorem | wdomnumr 8770 | Weak dominance agrees with normal for numerable right sets. (Contributed by Stefan O'Rear, 28-Feb-2015.) (Revised by Mario Carneiro, 5-May-2015.) |
⊢ (𝐵 ∈ dom card → (𝐴 ≼* 𝐵 ↔ 𝐴 ≼ 𝐵)) | ||
Theorem | alephfnon 8771 | The aleph function is a function on the class of ordinal numbers. (Contributed by NM, 21-Oct-2003.) (Revised by Mario Carneiro, 13-Sep-2013.) |
⊢ ℵ Fn On | ||
Theorem | aleph0 8772 | The first infinite cardinal number, discovered by Georg Cantor in 1873, has the same size as the set of natural numbers ω (and under our particular definition is also equal to it). In the literature, the argument of the aleph function is often written as a subscript, and the first aleph is written ℵ_0. Exercise 3 of [TakeutiZaring] p. 91. Also Definition 12(i) of [Suppes] p. 228. From Moshé Machover, Set Theory, Logic, and Their Limitations, p. 95: "Aleph...the first letter in the Hebrew alphabet...is also the first letter of the Hebrew word...(einsoph, meaning infinity), which is a cabbalistic appellation of the deity. The notation is due to Cantor, who was deeply interested in mysticism." (Contributed by NM, 21-Oct-2003.) (Revised by Mario Carneiro, 13-Sep-2013.) |
⊢ (ℵ‘∅) = ω | ||
Theorem | alephlim 8773* | Value of the aleph function at a limit ordinal. Definition 12(iii) of [Suppes] p. 91. (Contributed by NM, 21-Oct-2003.) (Revised by Mario Carneiro, 13-Sep-2013.) |
⊢ ((𝐴 ∈ 𝑉 ∧ Lim 𝐴) → (ℵ‘𝐴) = ∪ 𝑥 ∈ 𝐴 (ℵ‘𝑥)) | ||
Theorem | alephsuc 8774 | Value of the aleph function at a successor ordinal. Definition 12(ii) of [Suppes] p. 91. Here we express the successor aleph in terms of the Hartogs function df-har 8346, which gives the smallest ordinal that strictly dominates its argument (or the supremum of all ordinals that are dominated by the argument). (Contributed by Mario Carneiro, 13-Sep-2013.) (Revised by Mario Carneiro, 15-May-2015.) |
⊢ (𝐴 ∈ On → (ℵ‘suc 𝐴) = (har‘(ℵ‘𝐴))) | ||
Theorem | alephon 8775 | An aleph is an ordinal number. (Contributed by NM, 10-Nov-2003.) (Revised by Mario Carneiro, 13-Sep-2013.) |
⊢ (ℵ‘𝐴) ∈ On | ||
Theorem | alephcard 8776 | Every aleph is a cardinal number. Theorem 65 of [Suppes] p. 229. (Contributed by NM, 25-Oct-2003.) (Revised by Mario Carneiro, 2-Feb-2013.) |
⊢ (card‘(ℵ‘𝐴)) = (ℵ‘𝐴) | ||
Theorem | alephnbtwn 8777 | No cardinal can be sandwiched between an aleph and its successor aleph. Theorem 67 of [Suppes] p. 229. (Contributed by NM, 10-Nov-2003.) (Revised by Mario Carneiro, 15-May-2015.) |
⊢ ((card‘𝐵) = 𝐵 → ¬ ((ℵ‘𝐴) ∈ 𝐵 ∧ 𝐵 ∈ (ℵ‘suc 𝐴))) | ||
Theorem | alephnbtwn2 8778 | No set has equinumerosity between an aleph and its successor aleph. (Contributed by NM, 3-Nov-2003.) (Revised by Mario Carneiro, 2-Feb-2013.) |
⊢ ¬ ((ℵ‘𝐴) ≺ 𝐵 ∧ 𝐵 ≺ (ℵ‘suc 𝐴)) | ||
Theorem | alephordilem1 8779 | Lemma for alephordi 8780. (Contributed by NM, 23-Oct-2009.) (Revised by Mario Carneiro, 15-May-2015.) |
⊢ (𝐴 ∈ On → (ℵ‘𝐴) ≺ (ℵ‘suc 𝐴)) | ||
Theorem | alephordi 8780 | Strict ordering property of the aleph function. (Contributed by Mario Carneiro, 2-Feb-2013.) |
⊢ (𝐵 ∈ On → (𝐴 ∈ 𝐵 → (ℵ‘𝐴) ≺ (ℵ‘𝐵))) | ||
Theorem | alephord 8781 | Ordering property of the aleph function. (Contributed by NM, 26-Oct-2003.) (Revised by Mario Carneiro, 9-Feb-2013.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∈ 𝐵 ↔ (ℵ‘𝐴) ≺ (ℵ‘𝐵))) | ||
Theorem | alephord2 8782 | Ordering property of the aleph function. Theorem 8A(a) of [Enderton] p. 213 and its converse. (Contributed by NM, 3-Nov-2003.) (Revised by Mario Carneiro, 9-Feb-2013.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∈ 𝐵 ↔ (ℵ‘𝐴) ∈ (ℵ‘𝐵))) | ||
Theorem | alephord2i 8783 | Ordering property of the aleph function. Theorem 66 of [Suppes] p. 229. (Contributed by NM, 25-Oct-2003.) |
⊢ (𝐵 ∈ On → (𝐴 ∈ 𝐵 → (ℵ‘𝐴) ∈ (ℵ‘𝐵))) | ||
Theorem | alephord3 8784 | Ordering property of the aleph function. (Contributed by NM, 11-Nov-2003.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 ↔ (ℵ‘𝐴) ⊆ (ℵ‘𝐵))) | ||
Theorem | alephsucdom 8785 | A set dominated by an aleph is strictly dominated by its successor aleph and vice-versa. (Contributed by NM, 3-Nov-2003.) (Revised by Mario Carneiro, 2-Feb-2013.) |
⊢ (𝐵 ∈ On → (𝐴 ≼ (ℵ‘𝐵) ↔ 𝐴 ≺ (ℵ‘suc 𝐵))) | ||
Theorem | alephsuc2 8786* | An alternate representation of a successor aleph. The aleph function is the function obtained from the hartogs 8332 function by transfinite recursion, starting from ω. Using this theorem we could define the aleph function with {𝑧 ∈ On ∣ 𝑧 ≼ 𝑥} in place of ∩ {𝑧 ∈ On ∣ 𝑥 ≺ 𝑧} in df-aleph 8649. (Contributed by NM, 3-Nov-2003.) (Revised by Mario Carneiro, 2-Feb-2013.) |
⊢ (𝐴 ∈ On → (ℵ‘suc 𝐴) = {𝑥 ∈ On ∣ 𝑥 ≼ (ℵ‘𝐴)}) | ||
Theorem | alephdom 8787 | Relationship between inclusion of ordinal numbers and dominance of infinite initial ordinals. (Contributed by Jeff Hankins, 23-Oct-2009.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 ↔ (ℵ‘𝐴) ≼ (ℵ‘𝐵))) | ||
Theorem | alephgeom 8788 | Every aleph is greater than or equal to the set of natural numbers. (Contributed by NM, 11-Nov-2003.) |
⊢ (𝐴 ∈ On ↔ ω ⊆ (ℵ‘𝐴)) | ||
Theorem | alephislim 8789 | Every aleph is a limit ordinal. (Contributed by NM, 11-Nov-2003.) |
⊢ (𝐴 ∈ On ↔ Lim (ℵ‘𝐴)) | ||
Theorem | aleph11 8790 | The aleph function is one-to-one. (Contributed by NM, 3-Aug-2004.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((ℵ‘𝐴) = (ℵ‘𝐵) ↔ 𝐴 = 𝐵)) | ||
Theorem | alephf1 8791 | The aleph function is a one-to-one mapping from the ordinals to the infinite cardinals. See also alephf1ALT 8809. (Contributed by Mario Carneiro, 2-Feb-2013.) |
⊢ ℵ:On–1-1→On | ||
Theorem | alephsdom 8792 | If an ordinal is smaller than an initial ordinal, it is strictly dominated by it. (Contributed by Jeff Hankins, 24-Oct-2009.) (Proof shortened by Mario Carneiro, 20-Sep-2014.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∈ (ℵ‘𝐵) ↔ 𝐴 ≺ (ℵ‘𝐵))) | ||
Theorem | alephdom2 8793 | A dominated initial ordinal is included. (Contributed by Jeff Hankins, 24-Oct-2009.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((ℵ‘𝐴) ⊆ 𝐵 ↔ (ℵ‘𝐴) ≼ 𝐵)) | ||
Theorem | alephle 8794 | The argument of the aleph function is less than or equal to its value. Exercise 2 of [TakeutiZaring] p. 91. (Later, in alephfp2 8815, we will that equality can sometimes hold.) (Contributed by NM, 9-Nov-2003.) (Proof shortened by Mario Carneiro, 22-Feb-2013.) |
⊢ (𝐴 ∈ On → 𝐴 ⊆ (ℵ‘𝐴)) | ||
Theorem | cardaleph 8795* | Given any transfinite cardinal number 𝐴, there is exactly one aleph that is equal to it. Here we compute that aleph explicitly. (Contributed by NM, 9-Nov-2003.) (Revised by Mario Carneiro, 2-Feb-2013.) |
⊢ ((ω ⊆ 𝐴 ∧ (card‘𝐴) = 𝐴) → 𝐴 = (ℵ‘∩ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)})) | ||
Theorem | cardalephex 8796* | Every transfinite cardinal is an aleph and vice-versa. Theorem 8A(b) of [Enderton] p. 213 and its converse. (Contributed by NM, 5-Nov-2003.) |
⊢ (ω ⊆ 𝐴 → ((card‘𝐴) = 𝐴 ↔ ∃𝑥 ∈ On 𝐴 = (ℵ‘𝑥))) | ||
Theorem | infenaleph 8797* | An infinite numerable set is equinumerous to an infinite initial ordinal. (Contributed by Jeff Hankins, 23-Oct-2009.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ ((𝐴 ∈ dom card ∧ ω ≼ 𝐴) → ∃𝑥 ∈ ran ℵ𝑥 ≈ 𝐴) | ||
Theorem | isinfcard 8798 | Two ways to express the property of being a transfinite cardinal. (Contributed by NM, 9-Nov-2003.) |
⊢ ((ω ⊆ 𝐴 ∧ (card‘𝐴) = 𝐴) ↔ 𝐴 ∈ ran ℵ) | ||
Theorem | iscard3 8799 | Two ways to express the property of being a cardinal number. (Contributed by NM, 9-Nov-2003.) |
⊢ ((card‘𝐴) = 𝐴 ↔ 𝐴 ∈ (ω ∪ ran ℵ)) | ||
Theorem | cardnum 8800 | Two ways to express the class of all cardinal numbers, which consists of the finite ordinals in ω plus the transfinite alephs. (Contributed by NM, 10-Sep-2004.) |
⊢ {𝑥 ∣ (card‘𝑥) = 𝑥} = (ω ∪ ran ℵ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |