![]() |
Metamath
Proof Explorer Theorem List (p. 93 of 431) | < 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: | ![]() (1-28105) |
![]() (28106-29630) |
![]() (29631-43082) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | ccda 9201 | Extend class definition to include cardinal number addition. |
class +𝑐 | ||
Definition | df-cda 9202* | Define cardinal number addition. Definition of cardinal sum in [Mendelson] p. 258. See cdaval 9204 for its value and a description. (Contributed by NM, 24-Sep-2004.) |
⊢ +𝑐 = (𝑥 ∈ V, 𝑦 ∈ V ↦ ((𝑥 × {∅}) ∪ (𝑦 × {1𝑜}))) | ||
Theorem | cdafn 9203 | Cardinal number addition is a function. (Contributed by Mario Carneiro, 28-Apr-2015.) |
⊢ +𝑐 Fn (V × V) | ||
Theorem | cdaval 9204 | Value of cardinal addition. Definition of cardinal sum in [Mendelson] p. 258. For cardinal arithmetic, we follow Mendelson. Rather than defining operations restricted to cardinal numbers, we use this disjoint union operation for addition, while Cartesian product and set exponentiation stand in for cardinal multiplication and exponentiation. Equinumerosity and dominance serve the roles of equality and ordering. If we wanted to, we could easily convert our theorems to actual cardinal number operations via carden 9585, carddom 9588, and cardsdom 9589. The advantage of Mendelson's approach is that we can directly use many equinumerosity theorems that we already have available. (Contributed by NM, 24-Sep-2004.) (Revised by Mario Carneiro, 15-Sep-2013.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 +𝑐 𝐵) = ((𝐴 × {∅}) ∪ (𝐵 × {1𝑜}))) | ||
Theorem | uncdadom 9205 | Cardinal addition dominates union. (Contributed by NM, 28-Sep-2004.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ≼ (𝐴 +𝑐 𝐵)) | ||
Theorem | cdaun 9206 | Cardinal addition is equinumerous to union for disjoint sets. (Contributed by NM, 5-Apr-2007.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐴 +𝑐 𝐵) ≈ (𝐴 ∪ 𝐵)) | ||
Theorem | cdaen 9207 | Cardinal addition of equinumerous sets. Exercise 4.56(b) of [Mendelson] p. 258. (Contributed by NM, 28-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷) → (𝐴 +𝑐 𝐶) ≈ (𝐵 +𝑐 𝐷)) | ||
Theorem | cdaenun 9208 | Cardinal addition is equinumerous to union for disjoint sets. (Contributed by Mario Carneiro, 29-Apr-2015.) |
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷 ∧ (𝐵 ∩ 𝐷) = ∅) → (𝐴 +𝑐 𝐶) ≈ (𝐵 ∪ 𝐷)) | ||
Theorem | cda1en 9209 | Cardinal addition with cardinal one (which is the same as ordinal one). Used in proof of Theorem 6J of [Enderton] p. 143. (Contributed by NM, 28-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ 𝐴) → (𝐴 +𝑐 1𝑜) ≈ suc 𝐴) | ||
Theorem | cda1dif 9210 | Adding and subtracting one gives back the original set. Similar to pncan 10499 for cardinalities. (Contributed by Mario Carneiro, 18-May-2015.) |
⊢ (𝐵 ∈ (𝐴 +𝑐 1𝑜) → ((𝐴 +𝑐 1𝑜) ∖ {𝐵}) ≈ 𝐴) | ||
Theorem | pm110.643 9211 | 1+1=2 for cardinal number addition, derived from pm54.43 9036 as promised. Theorem *110.643 of Principia Mathematica, vol. II, p. 86, which adds the remark, "The above proposition is occasionally useful." Whitehead and Russell define cardinal addition on collections of all sets equinumerous to 1 and 2 (which for us are proper classes unless we restrict them as in karden 8933), but after applying definitions, our theorem is equivalent. The comment for cdaval 9204 explains why we use ≈ instead of =. See pm110.643ALT 9212 for a shorter proof that doesn't use pm54.43 9036. (Contributed by NM, 5-Apr-2007.) (Proof modification is discouraged.) |
⊢ (1𝑜 +𝑐 1𝑜) ≈ 2𝑜 | ||
Theorem | pm110.643ALT 9212 | Alternate proof of pm110.643 9211. (Contributed by Mario Carneiro, 29-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (1𝑜 +𝑐 1𝑜) ≈ 2𝑜 | ||
Theorem | cda0en 9213 | Cardinal addition with cardinal zero (the empty set). Part (a1) of proof of Theorem 6J of [Enderton] p. 143. (Contributed by NM, 27-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 +𝑐 ∅) ≈ 𝐴) | ||
Theorem | xp2cda 9214 | Two times a cardinal number. Exercise 4.56(g) of [Mendelson] p. 258. (Contributed by NM, 27-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 × 2𝑜) = (𝐴 +𝑐 𝐴)) | ||
Theorem | cdacomen 9215 | Commutative law for cardinal addition. Exercise 4.56(c) of [Mendelson] p. 258. (Contributed by NM, 24-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ (𝐴 +𝑐 𝐵) ≈ (𝐵 +𝑐 𝐴) | ||
Theorem | cdaassen 9216 | Associative law for cardinal addition. Exercise 4.56(c) of [Mendelson] p. 258. (Contributed by NM, 26-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐴 +𝑐 𝐵) +𝑐 𝐶) ≈ (𝐴 +𝑐 (𝐵 +𝑐 𝐶))) | ||
Theorem | xpcdaen 9217 | Cardinal multiplication distributes over cardinal addition. Theorem 6I(3) of [Enderton] p. 142. (Contributed by NM, 26-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 × (𝐵 +𝑐 𝐶)) ≈ ((𝐴 × 𝐵) +𝑐 (𝐴 × 𝐶))) | ||
Theorem | mapcdaen 9218 | Sum of exponents law for cardinal arithmetic. Theorem 6I(4) of [Enderton] p. 142. (Contributed by NM, 27-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 ↑𝑚 (𝐵 +𝑐 𝐶)) ≈ ((𝐴 ↑𝑚 𝐵) × (𝐴 ↑𝑚 𝐶))) | ||
Theorem | pwcdaen 9219 | Sum of exponents law for cardinal arithmetic. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝒫 (𝐴 +𝑐 𝐵) ≈ (𝒫 𝐴 × 𝒫 𝐵)) | ||
Theorem | cdadom1 9220 | Ordering law for cardinal addition. Exercise 4.56(f) of [Mendelson] p. 258. (Contributed by NM, 28-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ (𝐴 ≼ 𝐵 → (𝐴 +𝑐 𝐶) ≼ (𝐵 +𝑐 𝐶)) | ||
Theorem | cdadom2 9221 | Ordering law for cardinal addition. Theorem 6L(a) of [Enderton] p. 149. (Contributed by NM, 28-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ (𝐴 ≼ 𝐵 → (𝐶 +𝑐 𝐴) ≼ (𝐶 +𝑐 𝐵)) | ||
Theorem | cdadom3 9222 | A set is dominated by its cardinal sum with another. (Contributed by NM, 28-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐴 ≼ (𝐴 +𝑐 𝐵)) | ||
Theorem | cdaxpdom 9223 | Cartesian product dominates disjoint union for sets with cardinality greater than 1. Similar to Proposition 10.36 of [TakeutiZaring] p. 93. (Contributed by Mario Carneiro, 18-May-2015.) |
⊢ ((1𝑜 ≺ 𝐴 ∧ 1𝑜 ≺ 𝐵) → (𝐴 +𝑐 𝐵) ≼ (𝐴 × 𝐵)) | ||
Theorem | cdafi 9224 | The cardinal sum of two finite sets is finite. (Contributed by NM, 22-Oct-2004.) |
⊢ ((𝐴 ≺ ω ∧ 𝐵 ≺ ω) → (𝐴 +𝑐 𝐵) ≺ ω) | ||
Theorem | cdainflem 9225 | Any partition of omega into two pieces (which may be disjoint) contains an infinite subset. (Contributed by Mario Carneiro, 11-Feb-2013.) |
⊢ ((𝐴 ∪ 𝐵) ≈ ω → (𝐴 ≈ ω ∨ 𝐵 ≈ ω)) | ||
Theorem | cdainf 9226 | 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 | infcda1 9227 | An infinite set is equinumerous to itself added with one. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ (ω ≼ 𝐴 → (𝐴 +𝑐 1𝑜) ≈ 𝐴) | ||
Theorem | pwcda1 9228 | The sum of a powerset with itself is equipotent to the successor powerset. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ (𝐴 ∈ 𝑉 → (𝒫 𝐴 +𝑐 𝒫 𝐴) ≈ 𝒫 (𝐴 +𝑐 1𝑜)) | ||
Theorem | pwcdaidm 9229 | If the natural numbers inject into 𝐴, then 𝒫 𝐴 is idempotent under cardinal sum. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ (ω ≼ 𝐴 → (𝒫 𝐴 +𝑐 𝒫 𝐴) ≈ 𝒫 𝐴) | ||
Theorem | cdalepw 9230 | 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 | onacda 9231 | The cardinal and ordinal sums are always equinumerous. (Contributed by Mario Carneiro, 6-Feb-2013.) (Revised by Mario Carneiro, 30-May-2015.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +𝑜 𝐵) ≈ (𝐴 +𝑐 𝐵)) | ||
Theorem | cardacda 9232 | 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‘𝐴) +𝑜 (card‘𝐵))) | ||
Theorem | cdanum 9233 | The cardinal sum of two numerable sets is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.) |
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → (𝐴 +𝑐 𝐵) ∈ dom card) | ||
Theorem | unnum 9234 | The union of two numerable sets is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.) |
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → (𝐴 ∪ 𝐵) ∈ dom card) | ||
Theorem | nnacda 9235 | 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‘(𝐴 +𝑐 𝐵)) = (𝐴 +𝑜 𝐵)) | ||
Theorem | ficardun 9236 | 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‘𝐴) +𝑜 (card‘𝐵))) | ||
Theorem | ficardun2 9237 | 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‘𝐴) +𝑜 (card‘𝐵))) | ||
Theorem | pwsdompw 9238* | Lemma for domtriom 9477. This is the equinumerosity version of the algebraic identity Σ𝑘 ∈ 𝑛(2↑𝑘) = (2↑𝑛) − 1. (Contributed by Mario Carneiro, 7-Feb-2013.) |
⊢ ((𝑛 ∈ ω ∧ ∀𝑘 ∈ suc 𝑛(𝐵‘𝑘) ≈ 𝒫 𝑘) → ∪ 𝑘 ∈ 𝑛 (𝐵‘𝑘) ≺ (𝐵‘𝑛)) | ||
Theorem | unctb 9239 | The union of two countable sets is countable. (Contributed by FL, 25-Aug-2006.) (Proof shortened by Mario Carneiro, 30-Apr-2015.) |
⊢ ((𝐴 ≼ ω ∧ 𝐵 ≼ ω) → (𝐴 ∪ 𝐵) ≼ ω) | ||
Theorem | infcdaabs 9240 | 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 9241 | 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 | infcda 9242 | 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 9243 | 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 9244 | 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 9245 | 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 9246 | 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 9247 | The union of two sets that are strictly dominated by the infinite set 𝑋 is also dominated by 𝑋. This version of infunsdom 9248 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 9248 | 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 9249 | 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 | pwcdadom 9250 | A property of dominance over a powerset, and a main lemma for gchac 9715. Similar to Lemma 2.3 of [KanamoriPincus] p. 420. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ (𝒫 (𝐴 +𝑐 𝐴) ≼ (𝐴 +𝑐 𝐵) → 𝒫 𝐴 ≼ 𝐵) | ||
Theorem | infpss 9251* | Every infinite set has an equinumerous proper subset, proved without AC or Infinity. Exercise 7 of [TakeutiZaring] p. 91. See also infpssALT 9347. (Contributed by NM, 23-Oct-2004.) (Revised by Mario Carneiro, 30-Apr-2015.) |
⊢ (ω ≼ 𝐴 → ∃𝑥(𝑥 ⊊ 𝐴 ∧ 𝑥 ≈ 𝐴)) | ||
Theorem | infmap2 9252* | An exponentiation law for infinite cardinals. Similar to Lemma 6.2 of [Jech] p. 43. Although this version of infmap 9610 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.) |
⊢ ((ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ∧ (𝐴 ↑𝑚 𝐵) ∈ dom card) → (𝐴 ↑𝑚 𝐵) ≈ {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐵)}) | ||
Theorem | ackbij2lem1 9253 | Lemma for ackbij2 9277. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
⊢ (𝐴 ∈ ω → 𝒫 𝐴 ⊆ (𝒫 ω ∩ Fin)) | ||
Theorem | ackbij1lem1 9254 | Lemma for ackbij2 9277. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
⊢ (¬ 𝐴 ∈ 𝐵 → (𝐵 ∩ suc 𝐴) = (𝐵 ∩ 𝐴)) | ||
Theorem | ackbij1lem2 9255 | Lemma for ackbij2 9277. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
⊢ (𝐴 ∈ 𝐵 → (𝐵 ∩ suc 𝐴) = ({𝐴} ∪ (𝐵 ∩ 𝐴))) | ||
Theorem | ackbij1lem3 9256 | Lemma for ackbij2 9277. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
⊢ (𝐴 ∈ ω → 𝐴 ∈ (𝒫 ω ∩ Fin)) | ||
Theorem | ackbij1lem4 9257 | Lemma for ackbij2 9277. (Contributed by Stefan O'Rear, 19-Nov-2014.) |
⊢ (𝐴 ∈ ω → {𝐴} ∈ (𝒫 ω ∩ Fin)) | ||
Theorem | ackbij1lem5 9258 | Lemma for ackbij2 9277. (Contributed by Stefan O'Rear, 19-Nov-2014.) |
⊢ (𝐴 ∈ ω → (card‘𝒫 suc 𝐴) = ((card‘𝒫 𝐴) +𝑜 (card‘𝒫 𝐴))) | ||
Theorem | ackbij1lem6 9259 | Lemma for ackbij2 9277. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → (𝐴 ∪ 𝐵) ∈ (𝒫 ω ∩ Fin)) | ||
Theorem | ackbij1lem7 9260* | Lemma for ackbij1 9272. (Contributed by Stefan O'Rear, 21-Nov-2014.) |
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) ⇒ ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → (𝐹‘𝐴) = (card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦))) | ||
Theorem | ackbij1lem8 9261* | Lemma for ackbij1 9272. (Contributed by Stefan O'Rear, 19-Nov-2014.) |
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) ⇒ ⊢ (𝐴 ∈ ω → (𝐹‘{𝐴}) = (card‘𝒫 𝐴)) | ||
Theorem | ackbij1lem9 9262* | Lemma for ackbij1 9272. (Contributed by Stefan O'Rear, 19-Nov-2014.) |
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) ⇒ ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐹‘(𝐴 ∪ 𝐵)) = ((𝐹‘𝐴) +𝑜 (𝐹‘𝐵))) | ||
Theorem | ackbij1lem10 9263* | Lemma for ackbij1 9272. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) ⇒ ⊢ 𝐹:(𝒫 ω ∩ Fin)⟶ω | ||
Theorem | ackbij1lem11 9264* | Lemma for ackbij1 9272. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) ⇒ ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ (𝒫 ω ∩ Fin)) | ||
Theorem | ackbij1lem12 9265* | Lemma for ackbij1 9272. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) ⇒ ⊢ ((𝐵 ∈ (𝒫 ω ∩ Fin) ∧ 𝐴 ⊆ 𝐵) → (𝐹‘𝐴) ⊆ (𝐹‘𝐵)) | ||
Theorem | ackbij1lem13 9266* | Lemma for ackbij1 9272. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) ⇒ ⊢ (𝐹‘∅) = ∅ | ||
Theorem | ackbij1lem14 9267* | Lemma for ackbij1 9272. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) ⇒ ⊢ (𝐴 ∈ ω → (𝐹‘{𝐴}) = suc (𝐹‘𝐴)) | ||
Theorem | ackbij1lem15 9268* | Lemma for ackbij1 9272. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) ⇒ ⊢ (((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝑐 ∈ ω ∧ 𝑐 ∈ 𝐴 ∧ ¬ 𝑐 ∈ 𝐵)) → ¬ (𝐹‘(𝐴 ∩ suc 𝑐)) = (𝐹‘(𝐵 ∩ suc 𝑐))) | ||
Theorem | ackbij1lem16 9269* | Lemma for ackbij1 9272. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) ⇒ ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘𝐴) = (𝐹‘𝐵) → 𝐴 = 𝐵)) | ||
Theorem | ackbij1lem17 9270* | Lemma for ackbij1 9272. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) ⇒ ⊢ 𝐹:(𝒫 ω ∩ Fin)–1-1→ω | ||
Theorem | ackbij1lem18 9271* | Lemma for ackbij1 9272. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) ⇒ ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → ∃𝑏 ∈ (𝒫 ω ∩ Fin)(𝐹‘𝑏) = suc (𝐹‘𝐴)) | ||
Theorem | ackbij1 9272* | 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 9273* | The Ackermann bijection, part 1b: the bijection from ackbij1 9272 restricts naturally to the powers of particular naturals. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) ⇒ ⊢ (𝐴 ∈ ω → (𝐹 “ 𝒫 𝐴) = (card‘𝒫 𝐴)) | ||
Theorem | ackbij2lem2 9274* | Lemma for ackbij2 9277. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) & ⊢ 𝐺 = (𝑥 ∈ V ↦ (𝑦 ∈ 𝒫 dom 𝑥 ↦ (𝐹‘(𝑥 “ 𝑦)))) ⇒ ⊢ (𝐴 ∈ ω → (rec(𝐺, ∅)‘𝐴):(𝑅1‘𝐴)–1-1-onto→(card‘(𝑅1‘𝐴))) | ||
Theorem | ackbij2lem3 9275* | Lemma for ackbij2 9277. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) & ⊢ 𝐺 = (𝑥 ∈ V ↦ (𝑦 ∈ 𝒫 dom 𝑥 ↦ (𝐹‘(𝑥 “ 𝑦)))) ⇒ ⊢ (𝐴 ∈ ω → (rec(𝐺, ∅)‘𝐴) ⊆ (rec(𝐺, ∅)‘suc 𝐴)) | ||
Theorem | ackbij2lem4 9276* | Lemma for ackbij2 9277. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) & ⊢ 𝐺 = (𝑥 ∈ V ↦ (𝑦 ∈ 𝒫 dom 𝑥 ↦ (𝐹‘(𝑥 “ 𝑦)))) ⇒ ⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐵 ⊆ 𝐴) → (rec(𝐺, ∅)‘𝐵) ⊆ (rec(𝐺, ∅)‘𝐴)) | ||
Theorem | ackbij2 9277* | 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 9278 | The set of hereditarily finite sets is countable. See ackbij2 9277 for an explicit bijection that works without Infinity. See also r1omALT 9810. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
⊢ (𝑅1‘ω) ≈ ω | ||
Theorem | fictb 9279 | 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 9280* | 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 9281* | 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 9282 | 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 9283* | An upper bound on cofinality. (Contributed by NM, 25-Apr-2004.) (Revised by Mario Carneiro, 15-Sep-2013.) |
⊢ (cf‘𝐴) ⊆ ∩ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ ∪ 𝑦))} | ||
Theorem | cflm 9284* | 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 9285 | Value of the cofinality function at 0. Exercise 2 of [TakeutiZaring] p. 102. (Contributed by NM, 16-Apr-2004.) |
⊢ (cf‘∅) = ∅ | ||
Theorem | cardcf 9286 | 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 9287 | 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 9288 | 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 9289 | 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 9290 | Only the ordinal zero has cofinality zero. (Contributed by NM, 24-Apr-2004.) (Revised by Mario Carneiro, 12-Feb-2013.) |
⊢ (𝐴 ∈ On → ((cf‘𝐴) = ∅ ↔ 𝐴 = ∅)) | ||
Theorem | cfsuc 9291 | 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 𝐴) = 1𝑜) | ||
Theorem | cff1 9292* | 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 9293* | If there is a cofinal map from 𝐵 to 𝐴, then 𝐵 is at least (cf‘𝐴). This theorem and cff1 9292 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 9294* | Another expression for the cofinality function. (Contributed by Mario Carneiro, 28-Feb-2013.) |
⊢ (𝐴 ∈ On → (cf‘𝐴) = ∩ 𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤} (card‘𝑥)) | ||
Theorem | coflim 9295* | A simpler expression for the cofinality predicate, at a limit ordinal. (Contributed by Mario Carneiro, 28-Feb-2013.) |
⊢ ((Lim 𝐴 ∧ 𝐵 ⊆ 𝐴) → (∪ 𝐵 = 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦)) | ||
Theorem | cflim3 9296* | Another expression for the cofinality function. (Contributed by Mario Carneiro, 28-Feb-2013.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (Lim 𝐴 → (cf‘𝐴) = ∩ 𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} (card‘𝑥)) | ||
Theorem | cflim2 9297 | 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 9298 | 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 9299* | There is a cofinal subset of 𝐴 of cardinality (cf‘𝐴). (Contributed by Mario Carneiro, 24-Jun-2013.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (Lim 𝐴 → ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ (cf‘𝐴) ∧ ∪ 𝑥 = 𝐴)) | ||
Theorem | cfslb 9300 | Any cofinal subset of 𝐴 is at least as large as (cf‘𝐴). (Contributed by Mario Carneiro, 24-Jun-2013.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ((Lim 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ ∪ 𝐵 = 𝐴) → (cf‘𝐴) ≼ 𝐵) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |