Home | Metamath
Proof Explorer Theorem List (p. 97 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | djufi 9601 | The disjoint union of two finite sets is finite. (Contributed by NM, 22-Oct-2004.) |
⊢ ((𝐴 ≺ ω ∧ 𝐵 ≺ ω) → (𝐴 ⊔ 𝐵) ≺ ω) | ||
Theorem | cdainflem 9602 | Any partition of omega into two pieces (which may be disjoint) contains an infinite subset. (Contributed by Mario Carneiro, 11-Feb-2013.) |
⊢ ((𝐴 ∪ 𝐵) ≈ ω → (𝐴 ≈ ω ∨ 𝐵 ≈ ω)) | ||
Theorem | djuinf 9603 | A set is infinite iff the cardinal sum with itself is infinite. (Contributed by NM, 22-Oct-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ (ω ≼ 𝐴 ↔ ω ≼ (𝐴 ⊔ 𝐴)) | ||
Theorem | infdju1 9604 | An infinite set is equinumerous to itself added with one. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ (ω ≼ 𝐴 → (𝐴 ⊔ 1o) ≈ 𝐴) | ||
Theorem | pwdju1 9605 | The sum of a powerset with itself is equipotent to the successor powerset. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ (𝐴 ∈ 𝑉 → (𝒫 𝐴 ⊔ 𝒫 𝐴) ≈ 𝒫 (𝐴 ⊔ 1o)) | ||
Theorem | pwdjuidm 9606 | If the natural numbers inject into 𝐴, then 𝒫 𝐴 is idempotent under cardinal sum. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ (ω ≼ 𝐴 → (𝒫 𝐴 ⊔ 𝒫 𝐴) ≈ 𝒫 𝐴) | ||
Theorem | djulepw 9607 | If 𝐴 is idempotent under cardinal sum and 𝐵 is dominated by the power set of 𝐴, then so is the cardinal sum of 𝐴 and 𝐵. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ (((𝐴 ⊔ 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) → (𝐴 ⊔ 𝐵) ≼ 𝒫 𝐴) | ||
Theorem | onadju 9608 | The cardinal and ordinal sums are always equinumerous. (Contributed by Mario Carneiro, 6-Feb-2013.) (Revised by Jim Kingdon, 7-Sep-2023.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +o 𝐵) ≈ (𝐴 ⊔ 𝐵)) | ||
Theorem | cardadju 9609 | The cardinal sum is equinumerous to an ordinal sum of the cardinals. (Contributed by Mario Carneiro, 6-Feb-2013.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → (𝐴 ⊔ 𝐵) ≈ ((card‘𝐴) +o (card‘𝐵))) | ||
Theorem | djunum 9610 | The disjoint union of two numerable sets is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.) |
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → (𝐴 ⊔ 𝐵) ∈ dom card) | ||
Theorem | unnum 9611 | The union of two numerable sets is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.) |
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → (𝐴 ∪ 𝐵) ∈ dom card) | ||
Theorem | nnadju 9612 | The cardinal and ordinal sums of finite ordinals are equal. (Contributed by Paul Chapman, 11-Apr-2009.) (Revised by Mario Carneiro, 6-Feb-2013.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (card‘(𝐴 ⊔ 𝐵)) = (𝐴 +o 𝐵)) | ||
Theorem | ficardun 9613 | The cardinality of the union of disjoint, finite sets is the ordinal sum of their cardinalities. (Contributed by Paul Chapman, 5-Jun-2009.) (Proof shortened by Mario Carneiro, 28-Apr-2015.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ (𝐴 ∩ 𝐵) = ∅) → (card‘(𝐴 ∪ 𝐵)) = ((card‘𝐴) +o (card‘𝐵))) | ||
Theorem | ficardun2 9614 | The cardinality of the union of finite sets is at most the ordinal sum of their cardinalities. (Contributed by Mario Carneiro, 5-Feb-2013.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (card‘(𝐴 ∪ 𝐵)) ⊆ ((card‘𝐴) +o (card‘𝐵))) | ||
Theorem | pwsdompw 9615* | Lemma for domtriom 9854. This is the equinumerosity version of the algebraic identity Σ𝑘 ∈ 𝑛(2↑𝑘) = (2↑𝑛) − 1. (Contributed by Mario Carneiro, 7-Feb-2013.) |
⊢ ((𝑛 ∈ ω ∧ ∀𝑘 ∈ suc 𝑛(𝐵‘𝑘) ≈ 𝒫 𝑘) → ∪ 𝑘 ∈ 𝑛 (𝐵‘𝑘) ≺ (𝐵‘𝑛)) | ||
Theorem | unctb 9616 | The union of two countable sets is countable. (Contributed by FL, 25-Aug-2006.) (Proof shortened by Mario Carneiro, 30-Apr-2015.) |
⊢ ((𝐴 ≼ ω ∧ 𝐵 ≼ ω) → (𝐴 ∪ 𝐵) ≼ ω) | ||
Theorem | infdjuabs 9617 | Absorption law for addition to an infinite cardinal. (Contributed by NM, 30-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ ((𝐴 ∈ dom card ∧ ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴) → (𝐴 ⊔ 𝐵) ≈ 𝐴) | ||
Theorem | infunabs 9618 | An infinite set is equinumerous to its union with a smaller one. (Contributed by NM, 28-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ ((𝐴 ∈ dom card ∧ ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴) → (𝐴 ∪ 𝐵) ≈ 𝐴) | ||
Theorem | infdju 9619 | The sum of two cardinal numbers is their maximum, if one of them is infinite. Proposition 10.41 of [TakeutiZaring] p. 95. (Contributed by NM, 28-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ∧ ω ≼ 𝐴) → (𝐴 ⊔ 𝐵) ≈ (𝐴 ∪ 𝐵)) | ||
Theorem | infdif 9620 | The cardinality of an infinite set does not change after subtracting a strictly smaller one. Example in [Enderton] p. 164. (Contributed by NM, 22-Oct-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ ((𝐴 ∈ dom card ∧ ω ≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → (𝐴 ∖ 𝐵) ≈ 𝐴) | ||
Theorem | infdif2 9621 | Cardinality ordering for an infinite class difference. (Contributed by NM, 24-Mar-2007.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ∧ ω ≼ 𝐴) → ((𝐴 ∖ 𝐵) ≼ 𝐵 ↔ 𝐴 ≼ 𝐵)) | ||
Theorem | infxpdom 9622 | Dominance law for multiplication with an infinite cardinal. (Contributed by NM, 26-Mar-2006.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ ((𝐴 ∈ dom card ∧ ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴) → (𝐴 × 𝐵) ≼ 𝐴) | ||
Theorem | infxpabs 9623 | Absorption law for multiplication with an infinite cardinal. (Contributed by NM, 30-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ (((𝐴 ∈ dom card ∧ ω ≼ 𝐴) ∧ (𝐵 ≠ ∅ ∧ 𝐵 ≼ 𝐴)) → (𝐴 × 𝐵) ≈ 𝐴) | ||
Theorem | infunsdom1 9624 | The union of two sets that are strictly dominated by the infinite set 𝑋 is also dominated by 𝑋. This version of infunsdom 9625 assumes additionally that 𝐴 is the smaller of the two. (Contributed by Mario Carneiro, 14-Dec-2013.) (Revised by Mario Carneiro, 3-May-2015.) |
⊢ (((𝑋 ∈ dom card ∧ ω ≼ 𝑋) ∧ (𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝑋)) → (𝐴 ∪ 𝐵) ≺ 𝑋) | ||
Theorem | infunsdom 9625 | The union of two sets that are strictly dominated by the infinite set 𝑋 is also strictly dominated by 𝑋. (Contributed by Mario Carneiro, 3-May-2015.) |
⊢ (((𝑋 ∈ dom card ∧ ω ≼ 𝑋) ∧ (𝐴 ≺ 𝑋 ∧ 𝐵 ≺ 𝑋)) → (𝐴 ∪ 𝐵) ≺ 𝑋) | ||
Theorem | infxp 9626 | Absorption law for multiplication with an infinite cardinal. Equivalent to Proposition 10.41 of [TakeutiZaring] p. 95. (Contributed by NM, 28-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ (((𝐴 ∈ dom card ∧ ω ≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) → (𝐴 × 𝐵) ≈ (𝐴 ∪ 𝐵)) | ||
Theorem | pwdjudom 9627 | A property of dominance over a powerset, and a main lemma for gchac 10092. Similar to Lemma 2.3 of [KanamoriPincus] p. 420. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ (𝒫 (𝐴 ⊔ 𝐴) ≼ (𝐴 ⊔ 𝐵) → 𝒫 𝐴 ≼ 𝐵) | ||
Theorem | infpss 9628* | Every infinite set has an equinumerous proper subset, proved without AC or Infinity. Exercise 7 of [TakeutiZaring] p. 91. See also infpssALT 9724. (Contributed by NM, 23-Oct-2004.) (Revised by Mario Carneiro, 30-Apr-2015.) |
⊢ (ω ≼ 𝐴 → ∃𝑥(𝑥 ⊊ 𝐴 ∧ 𝑥 ≈ 𝐴)) | ||
Theorem | infmap2 9629* | An exponentiation law for infinite cardinals. Similar to Lemma 6.2 of [Jech] p. 43. Although this version of infmap 9987 avoids the axiom of choice, it requires the powerset of an infinite set to be well-orderable and so is usually not applicable. (Contributed by NM, 1-Oct-2004.) (Revised by Mario Carneiro, 30-Apr-2015.) |
⊢ ((ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ∧ (𝐴 ↑m 𝐵) ∈ dom card) → (𝐴 ↑m 𝐵) ≈ {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐵)}) | ||
Theorem | ackbij2lem1 9630 | Lemma for ackbij2 9654. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
⊢ (𝐴 ∈ ω → 𝒫 𝐴 ⊆ (𝒫 ω ∩ Fin)) | ||
Theorem | ackbij1lem1 9631 | Lemma for ackbij2 9654. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
⊢ (¬ 𝐴 ∈ 𝐵 → (𝐵 ∩ suc 𝐴) = (𝐵 ∩ 𝐴)) | ||
Theorem | ackbij1lem2 9632 | Lemma for ackbij2 9654. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
⊢ (𝐴 ∈ 𝐵 → (𝐵 ∩ suc 𝐴) = ({𝐴} ∪ (𝐵 ∩ 𝐴))) | ||
Theorem | ackbij1lem3 9633 | Lemma for ackbij2 9654. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
⊢ (𝐴 ∈ ω → 𝐴 ∈ (𝒫 ω ∩ Fin)) | ||
Theorem | ackbij1lem4 9634 | Lemma for ackbij2 9654. (Contributed by Stefan O'Rear, 19-Nov-2014.) |
⊢ (𝐴 ∈ ω → {𝐴} ∈ (𝒫 ω ∩ Fin)) | ||
Theorem | ackbij1lem5 9635 | Lemma for ackbij2 9654. (Contributed by Stefan O'Rear, 19-Nov-2014.) (Proof shortened by AV, 18-Jul-2022.) |
⊢ (𝐴 ∈ ω → (card‘𝒫 suc 𝐴) = ((card‘𝒫 𝐴) +o (card‘𝒫 𝐴))) | ||
Theorem | ackbij1lem6 9636 | Lemma for ackbij2 9654. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → (𝐴 ∪ 𝐵) ∈ (𝒫 ω ∩ Fin)) | ||
Theorem | ackbij1lem7 9637* | Lemma for ackbij1 9649. (Contributed by Stefan O'Rear, 21-Nov-2014.) |
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) ⇒ ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → (𝐹‘𝐴) = (card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦))) | ||
Theorem | ackbij1lem8 9638* | Lemma for ackbij1 9649. (Contributed by Stefan O'Rear, 19-Nov-2014.) |
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) ⇒ ⊢ (𝐴 ∈ ω → (𝐹‘{𝐴}) = (card‘𝒫 𝐴)) | ||
Theorem | ackbij1lem9 9639* | Lemma for ackbij1 9649. (Contributed by Stefan O'Rear, 19-Nov-2014.) |
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) ⇒ ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐹‘(𝐴 ∪ 𝐵)) = ((𝐹‘𝐴) +o (𝐹‘𝐵))) | ||
Theorem | ackbij1lem10 9640* | Lemma for ackbij1 9649. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) ⇒ ⊢ 𝐹:(𝒫 ω ∩ Fin)⟶ω | ||
Theorem | ackbij1lem11 9641* | Lemma for ackbij1 9649. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) ⇒ ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ (𝒫 ω ∩ Fin)) | ||
Theorem | ackbij1lem12 9642* | Lemma for ackbij1 9649. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) ⇒ ⊢ ((𝐵 ∈ (𝒫 ω ∩ Fin) ∧ 𝐴 ⊆ 𝐵) → (𝐹‘𝐴) ⊆ (𝐹‘𝐵)) | ||
Theorem | ackbij1lem13 9643* | Lemma for ackbij1 9649. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) ⇒ ⊢ (𝐹‘∅) = ∅ | ||
Theorem | ackbij1lem14 9644* | Lemma for ackbij1 9649. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) ⇒ ⊢ (𝐴 ∈ ω → (𝐹‘{𝐴}) = suc (𝐹‘𝐴)) | ||
Theorem | ackbij1lem15 9645* | Lemma for ackbij1 9649. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) ⇒ ⊢ (((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝑐 ∈ ω ∧ 𝑐 ∈ 𝐴 ∧ ¬ 𝑐 ∈ 𝐵)) → ¬ (𝐹‘(𝐴 ∩ suc 𝑐)) = (𝐹‘(𝐵 ∩ suc 𝑐))) | ||
Theorem | ackbij1lem16 9646* | Lemma for ackbij1 9649. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) ⇒ ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘𝐴) = (𝐹‘𝐵) → 𝐴 = 𝐵)) | ||
Theorem | ackbij1lem17 9647* | Lemma for ackbij1 9649. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) ⇒ ⊢ 𝐹:(𝒫 ω ∩ Fin)–1-1→ω | ||
Theorem | ackbij1lem18 9648* | Lemma for ackbij1 9649. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) ⇒ ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → ∃𝑏 ∈ (𝒫 ω ∩ Fin)(𝐹‘𝑏) = suc (𝐹‘𝐴)) | ||
Theorem | ackbij1 9649* | The Ackermann bijection, part 1: each natural number can be uniquely coded in binary as a finite set of natural numbers and conversely. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) ⇒ ⊢ 𝐹:(𝒫 ω ∩ Fin)–1-1-onto→ω | ||
Theorem | ackbij1b 9650* | The Ackermann bijection, part 1b: the bijection from ackbij1 9649 restricts naturally to the powers of particular naturals. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) ⇒ ⊢ (𝐴 ∈ ω → (𝐹 “ 𝒫 𝐴) = (card‘𝒫 𝐴)) | ||
Theorem | ackbij2lem2 9651* | Lemma for ackbij2 9654. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) & ⊢ 𝐺 = (𝑥 ∈ V ↦ (𝑦 ∈ 𝒫 dom 𝑥 ↦ (𝐹‘(𝑥 “ 𝑦)))) ⇒ ⊢ (𝐴 ∈ ω → (rec(𝐺, ∅)‘𝐴):(𝑅1‘𝐴)–1-1-onto→(card‘(𝑅1‘𝐴))) | ||
Theorem | ackbij2lem3 9652* | Lemma for ackbij2 9654. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) & ⊢ 𝐺 = (𝑥 ∈ V ↦ (𝑦 ∈ 𝒫 dom 𝑥 ↦ (𝐹‘(𝑥 “ 𝑦)))) ⇒ ⊢ (𝐴 ∈ ω → (rec(𝐺, ∅)‘𝐴) ⊆ (rec(𝐺, ∅)‘suc 𝐴)) | ||
Theorem | ackbij2lem4 9653* | Lemma for ackbij2 9654. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) & ⊢ 𝐺 = (𝑥 ∈ V ↦ (𝑦 ∈ 𝒫 dom 𝑥 ↦ (𝐹‘(𝑥 “ 𝑦)))) ⇒ ⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐵 ⊆ 𝐴) → (rec(𝐺, ∅)‘𝐵) ⊆ (rec(𝐺, ∅)‘𝐴)) | ||
Theorem | ackbij2 9654* | The Ackermann bijection, part 2: hereditarily finite sets can be represented by recursive binary notation. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) & ⊢ 𝐺 = (𝑥 ∈ V ↦ (𝑦 ∈ 𝒫 dom 𝑥 ↦ (𝐹‘(𝑥 “ 𝑦)))) & ⊢ 𝐻 = ∪ (rec(𝐺, ∅) “ ω) ⇒ ⊢ 𝐻:∪ (𝑅1 “ ω)–1-1-onto→ω | ||
Theorem | r1om 9655 | The set of hereditarily finite sets is countable. See ackbij2 9654 for an explicit bijection that works without Infinity. See also r1omALT 10187. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
⊢ (𝑅1‘ω) ≈ ω | ||
Theorem | fictb 9656 | A set is countable iff its collection of finite intersections is countable. (Contributed by Jeff Hankins, 24-Aug-2009.) (Proof shortened by Mario Carneiro, 17-May-2015.) |
⊢ (𝐴 ∈ 𝐵 → (𝐴 ≼ ω ↔ (fi‘𝐴) ≼ ω)) | ||
Theorem | cflem 9657* | A lemma used to simplify cofinality computations, showing the existence of the cardinal of an unbounded subset of a set 𝐴. (Contributed by NM, 24-Apr-2004.) |
⊢ (𝐴 ∈ 𝑉 → ∃𝑥∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))) | ||
Theorem | cfval 9658* | Value of the cofinality function. Definition B of Saharon Shelah, Cardinal Arithmetic (1994), p. xxx (Roman numeral 30). The cofinality of an ordinal number 𝐴 is the cardinality (size) of the smallest unbounded subset 𝑦 of the ordinal number. Unbounded means that for every member of 𝐴, there is a member of 𝑦 that is at least as large. Cofinality is a measure of how "reachable from below" an ordinal is. (Contributed by NM, 1-Apr-2004.) (Revised by Mario Carneiro, 15-Sep-2013.) |
⊢ (𝐴 ∈ On → (cf‘𝐴) = ∩ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))}) | ||
Theorem | cff 9659 | Cofinality is a function on the class of ordinal numbers to the class of cardinal numbers. (Contributed by Mario Carneiro, 15-Sep-2013.) |
⊢ cf:On⟶On | ||
Theorem | cfub 9660* | An upper bound on cofinality. (Contributed by NM, 25-Apr-2004.) (Revised by Mario Carneiro, 15-Sep-2013.) |
⊢ (cf‘𝐴) ⊆ ∩ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ ∪ 𝑦))} | ||
Theorem | cflm 9661* | Value of the cofinality function at a limit ordinal. Part of Definition of cofinality of [Enderton] p. 257. (Contributed by NM, 26-Apr-2004.) |
⊢ ((𝐴 ∈ 𝐵 ∧ Lim 𝐴) → (cf‘𝐴) = ∩ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))}) | ||
Theorem | cf0 9662 | Value of the cofinality function at 0. Exercise 2 of [TakeutiZaring] p. 102. (Contributed by NM, 16-Apr-2004.) |
⊢ (cf‘∅) = ∅ | ||
Theorem | cardcf 9663 | Cofinality is a cardinal number. Proposition 11.11 of [TakeutiZaring] p. 103. (Contributed by NM, 24-Apr-2004.) (Revised by Mario Carneiro, 15-Sep-2013.) |
⊢ (card‘(cf‘𝐴)) = (cf‘𝐴) | ||
Theorem | cflecard 9664 | Cofinality is bounded by the cardinality of its argument. (Contributed by NM, 24-Apr-2004.) (Revised by Mario Carneiro, 15-Sep-2013.) |
⊢ (cf‘𝐴) ⊆ (card‘𝐴) | ||
Theorem | cfle 9665 | Cofinality is bounded by its argument. Exercise 1 of [TakeutiZaring] p. 102. (Contributed by NM, 26-Apr-2004.) (Revised by Mario Carneiro, 15-Sep-2013.) |
⊢ (cf‘𝐴) ⊆ 𝐴 | ||
Theorem | cfon 9666 | The cofinality of any set is an ordinal (although it only makes sense when 𝐴 is an ordinal). (Contributed by Mario Carneiro, 9-Mar-2013.) |
⊢ (cf‘𝐴) ∈ On | ||
Theorem | cfeq0 9667 | Only the ordinal zero has cofinality zero. (Contributed by NM, 24-Apr-2004.) (Revised by Mario Carneiro, 12-Feb-2013.) |
⊢ (𝐴 ∈ On → ((cf‘𝐴) = ∅ ↔ 𝐴 = ∅)) | ||
Theorem | cfsuc 9668 | Value of the cofinality function at a successor ordinal. Exercise 3 of [TakeutiZaring] p. 102. (Contributed by NM, 23-Apr-2004.) (Revised by Mario Carneiro, 12-Feb-2013.) |
⊢ (𝐴 ∈ On → (cf‘suc 𝐴) = 1o) | ||
Theorem | cff1 9669* | There is always a map from (cf‘𝐴) to 𝐴 (this is a stronger condition than the definition, which only presupposes a map from some 𝑦 ≈ (cf‘𝐴). (Contributed by Mario Carneiro, 28-Feb-2013.) |
⊢ (𝐴 ∈ On → ∃𝑓(𝑓:(cf‘𝐴)–1-1→𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓‘𝑤))) | ||
Theorem | cfflb 9670* | If there is a cofinal map from 𝐵 to 𝐴, then 𝐵 is at least (cf‘𝐴). This theorem and cff1 9669 motivate the picture of (cf‘𝐴) as the greatest lower bound of the domain of cofinal maps into 𝐴. (Contributed by Mario Carneiro, 28-Feb-2013.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∃𝑓(𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) → (cf‘𝐴) ⊆ 𝐵)) | ||
Theorem | cfval2 9671* | Another expression for the cofinality function. (Contributed by Mario Carneiro, 28-Feb-2013.) |
⊢ (𝐴 ∈ On → (cf‘𝐴) = ∩ 𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤} (card‘𝑥)) | ||
Theorem | coflim 9672* | A simpler expression for the cofinality predicate, at a limit ordinal. (Contributed by Mario Carneiro, 28-Feb-2013.) |
⊢ ((Lim 𝐴 ∧ 𝐵 ⊆ 𝐴) → (∪ 𝐵 = 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦)) | ||
Theorem | cflim3 9673* | Another expression for the cofinality function. (Contributed by Mario Carneiro, 28-Feb-2013.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (Lim 𝐴 → (cf‘𝐴) = ∩ 𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} (card‘𝑥)) | ||
Theorem | cflim2 9674 | The cofinality function is a limit ordinal iff its argument is. (Contributed by Mario Carneiro, 28-Feb-2013.) (Revised by Mario Carneiro, 15-Sep-2013.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (Lim 𝐴 ↔ Lim (cf‘𝐴)) | ||
Theorem | cfom 9675 | Value of the cofinality function at omega (the set of natural numbers). Exercise 4 of [TakeutiZaring] p. 102. (Contributed by NM, 23-Apr-2004.) (Proof shortened by Mario Carneiro, 11-Jun-2015.) |
⊢ (cf‘ω) = ω | ||
Theorem | cfss 9676* | There is a cofinal subset of 𝐴 of cardinality (cf‘𝐴). (Contributed by Mario Carneiro, 24-Jun-2013.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (Lim 𝐴 → ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ (cf‘𝐴) ∧ ∪ 𝑥 = 𝐴)) | ||
Theorem | cfslb 9677 | Any cofinal subset of 𝐴 is at least as large as (cf‘𝐴). (Contributed by Mario Carneiro, 24-Jun-2013.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ((Lim 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ ∪ 𝐵 = 𝐴) → (cf‘𝐴) ≼ 𝐵) | ||
Theorem | cfslbn 9678 | Any subset of 𝐴 smaller than its cofinality has union less than 𝐴. (This is the contrapositive to cfslb 9677.) (Contributed by Mario Carneiro, 24-Jun-2013.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ((Lim 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≺ (cf‘𝐴)) → ∪ 𝐵 ∈ 𝐴) | ||
Theorem | cfslb2n 9679* | Any small collection of small subsets of 𝐴 cannot have union 𝐴, where "small" means smaller than the cofinality. This is a stronger version of cfslb 9677. This is a common application of cofinality: under AC, (ℵ‘1) is regular, so it is not a countable union of countable sets. (Contributed by Mario Carneiro, 24-Jun-2013.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ((Lim 𝐴 ∧ ∀𝑥 ∈ 𝐵 (𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ (cf‘𝐴))) → (𝐵 ≺ (cf‘𝐴) → ∪ 𝐵 ≠ 𝐴)) | ||
Theorem | cofsmo 9680* | Any cofinal map implies the existence of a strictly monotone cofinal map with a domain no larger than the original. Proposition 11.7 of [TakeutiZaring] p. 101. (Contributed by Mario Carneiro, 20-Mar-2013.) |
⊢ 𝐶 = {𝑦 ∈ 𝐵 ∣ ∀𝑤 ∈ 𝑦 (𝑓‘𝑤) ∈ (𝑓‘𝑦)} & ⊢ 𝐾 = ∩ {𝑥 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑥)} & ⊢ 𝑂 = OrdIso( E , 𝐶) ⇒ ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ On) → (∃𝑓(𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) → ∃𝑥 ∈ suc 𝐵∃𝑔(𝑔:𝑥⟶𝐴 ∧ Smo 𝑔 ∧ ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ 𝑥 𝑧 ⊆ (𝑔‘𝑣)))) | ||
Theorem | cfsmolem 9681* | Lemma for cfsmo 9682. (Contributed by Mario Carneiro, 28-Feb-2013.) |
⊢ 𝐹 = (𝑧 ∈ V ↦ ((𝑔‘dom 𝑧) ∪ ∪ 𝑡 ∈ dom 𝑧 suc (𝑧‘𝑡))) & ⊢ 𝐺 = (recs(𝐹) ↾ (cf‘𝐴)) ⇒ ⊢ (𝐴 ∈ On → ∃𝑓(𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓‘𝑤))) | ||
Theorem | cfsmo 9682* | The map in cff1 9669 can be assumed to be a strictly monotone ordinal function without loss of generality. (Contributed by Mario Carneiro, 28-Feb-2013.) |
⊢ (𝐴 ∈ On → ∃𝑓(𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓‘𝑤))) | ||
Theorem | cfcoflem 9683* | Lemma for cfcof 9685, showing subset relation in one direction. (Contributed by Mario Carneiro, 9-Mar-2013.) (Revised by Mario Carneiro, 26-Dec-2014.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∃𝑓(𝑓:𝐵⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ (𝑓‘𝑦)) → (cf‘𝐴) ⊆ (cf‘𝐵))) | ||
Theorem | coftr 9684* | If there is a cofinal map from 𝐵 to 𝐴 and another from 𝐶 to 𝐴, then there is also a cofinal map from 𝐶 to 𝐵. Proposition 11.9 of [TakeutiZaring] p. 102. A limited form of transitivity for the "cof" relation. This is really a lemma for cfcof 9685. (Contributed by Mario Carneiro, 16-Mar-2013.) |
⊢ 𝐻 = (𝑡 ∈ 𝐶 ↦ ∩ {𝑛 ∈ 𝐵 ∣ (𝑔‘𝑡) ⊆ (𝑓‘𝑛)}) ⇒ ⊢ (∃𝑓(𝑓:𝐵⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ (𝑓‘𝑦)) → (∃𝑔(𝑔:𝐶⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐶 𝑧 ⊆ (𝑔‘𝑤)) → ∃ℎ(ℎ:𝐶⟶𝐵 ∧ ∀𝑠 ∈ 𝐵 ∃𝑤 ∈ 𝐶 𝑠 ⊆ (ℎ‘𝑤)))) | ||
Theorem | cfcof 9685* | If there is a cofinal map from 𝐴 to 𝐵, then they have the same cofinality. This was used as Definition 11.1 of [TakeutiZaring] p. 100, who defines an equivalence relation cof (𝐴, 𝐵) and defines our cf(𝐵) as the minimum 𝐵 such that cof (𝐴, 𝐵). (Contributed by Mario Carneiro, 20-Mar-2013.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∃𝑓(𝑓:𝐵⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) → (cf‘𝐴) = (cf‘𝐵))) | ||
Theorem | cfidm 9686 | The cofinality function is idempotent. (Contributed by Mario Carneiro, 7-Mar-2013.) (Revised by Mario Carneiro, 15-Sep-2013.) |
⊢ (cf‘(cf‘𝐴)) = (cf‘𝐴) | ||
Theorem | alephsing 9687 | The cofinality of a limit aleph is the same as the cofinality of its argument, so if (ℵ‘𝐴) < 𝐴, then (ℵ‘𝐴) is singular. Conversely, if (ℵ‘𝐴) is regular (i.e. weakly inaccessible), then (ℵ‘𝐴) = 𝐴, so 𝐴 has to be rather large (see alephfp 9523). Proposition 11.13 of [TakeutiZaring] p. 103. (Contributed by Mario Carneiro, 9-Mar-2013.) |
⊢ (Lim 𝐴 → (cf‘(ℵ‘𝐴)) = (cf‘𝐴)) | ||
Theorem | sornom 9688* | The range of a single-step monotone function from ω into a partially ordered set is a chain. (Contributed by Stefan O'Rear, 3-Nov-2014.) |
⊢ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → 𝑅 Or ran 𝐹) | ||
Syntax | cfin1a 9689 | Extend class notation to include the class of Ia-finite sets. |
class FinIa | ||
Syntax | cfin2 9690 | Extend class notation to include the class of II-finite sets. |
class FinII | ||
Syntax | cfin4 9691 | Extend class notation to include the class of IV-finite sets. |
class FinIV | ||
Syntax | cfin3 9692 | Extend class notation to include the class of III-finite sets. |
class FinIII | ||
Syntax | cfin5 9693 | Extend class notation to include the class of V-finite sets. |
class FinV | ||
Syntax | cfin6 9694 | Extend class notation to include the class of VI-finite sets. |
class FinVI | ||
Syntax | cfin7 9695 | Extend class notation to include the class of VII-finite sets. |
class FinVII | ||
Definition | df-fin1a 9696* | A set is Ia-finite iff it is not the union of two I-infinite sets. Equivalent to definition Ia of [Levy58] p. 2. A I-infinite Ia-finite set is also known as an amorphous set. This is the second of Levy's eight definitions of finite set. Levy's I-finite is equivalent to our df-fin 8502 and not repeated here. These eight definitions are equivalent with Choice but strictly decreasing in strength in models where Choice fails; conversely, they provide a series of increasingly stronger notions of infiniteness. (Contributed by Stefan O'Rear, 12-Nov-2014.) |
⊢ FinIa = {𝑥 ∣ ∀𝑦 ∈ 𝒫 𝑥(𝑦 ∈ Fin ∨ (𝑥 ∖ 𝑦) ∈ Fin)} | ||
Definition | df-fin2 9697* | A set is II-finite (Tarski finite) iff every nonempty chain of subsets contains a maximum element. Definition II of [Levy58] p. 2. (Contributed by Stefan O'Rear, 12-Nov-2014.) |
⊢ FinII = {𝑥 ∣ ∀𝑦 ∈ 𝒫 𝒫 𝑥((𝑦 ≠ ∅ ∧ [⊊] Or 𝑦) → ∪ 𝑦 ∈ 𝑦)} | ||
Definition | df-fin4 9698* | A set is IV-finite (Dedekind finite) iff it has no equinumerous proper subset. Definition IV of [Levy58] p. 3. (Contributed by Stefan O'Rear, 12-Nov-2014.) |
⊢ FinIV = {𝑥 ∣ ¬ ∃𝑦(𝑦 ⊊ 𝑥 ∧ 𝑦 ≈ 𝑥)} | ||
Definition | df-fin3 9699 | A set is III-finite (weakly Dedekind finite) iff its power set is Dedekind finite. Definition III of [Levy58] p. 2. (Contributed by Stefan O'Rear, 12-Nov-2014.) |
⊢ FinIII = {𝑥 ∣ 𝒫 𝑥 ∈ FinIV} | ||
Definition | df-fin5 9700 | A set is V-finite iff it behaves finitely under ⊔. Definition V of [Levy58] p. 3. (Contributed by Stefan O'Rear, 12-Nov-2014.) |
⊢ FinV = {𝑥 ∣ (𝑥 = ∅ ∨ 𝑥 ≺ (𝑥 ⊔ 𝑥))} |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |