HomeTheorem List (p. 101 of 470)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 101 of 470) | < 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-29568) |
Hilbert Space Explorer
(29569-31091) |
Users' Mathboxes
(31092-46925) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | dfac10b 10001 | Axiom of Choice equivalent: every set is equinumerous to an ordinal (quantifier-free short cryptic version alluded to in df-ac 9978). (Contributed by Stefan O'Rear, 17-Jan-2015.) |
| ⊢ (CHOICE ↔ ( ≈ “ On) = V) | ||
| Theorem | acacni 10002 | A choice equivalent: every set has choice sets of every length. (Contributed by Mario Carneiro, 31-Aug-2015.) |
| ⊢ ((CHOICE ∧ 𝐴 ∈ 𝑉) → AC 𝐴 = V) | ||
| Theorem | dfacacn 10003 | A choice equivalent: every set has choice sets of every length. (Contributed by Mario Carneiro, 31-Aug-2015.) |
| ⊢ (CHOICE ↔ ∀𝑥AC 𝑥 = V) | ||
| Theorem | dfac13 10004 | The axiom of choice holds iff every set has choice sequences as long as itself. (Contributed by Mario Carneiro, 3-Sep-2015.) |
| ⊢ (CHOICE ↔ ∀𝑥 𝑥 ∈ AC 𝑥) | ||
| Theorem | dfac12lem1 10005* | Lemma for dfac12 10011. (Contributed by Mario Carneiro, 29-May-2015.) |
| ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐹:𝒫 (har‘(𝑅1‘𝐴))–1-1→On) & ⊢ 𝐺 = recs((𝑥 ∈ V ↦ (𝑦 ∈ (𝑅1‘dom 𝑥) ↦ if(dom 𝑥 = ∪ dom 𝑥, ((suc ∪ ran ∪ ran 𝑥 ·o (rank‘𝑦)) +o ((𝑥‘suc (rank‘𝑦))‘𝑦)), (𝐹‘((◡OrdIso( E , ran (𝑥‘∪ dom 𝑥)) ∘ (𝑥‘∪ dom 𝑥)) “ 𝑦)))))) & ⊢ (𝜑 → 𝐶 ∈ On) & ⊢ 𝐻 = (◡OrdIso( E , ran (𝐺‘∪ 𝐶)) ∘ (𝐺‘∪ 𝐶)) ⇒ ⊢ (𝜑 → (𝐺‘𝐶) = (𝑦 ∈ (𝑅1‘𝐶) ↦ if(𝐶 = ∪ 𝐶, ((suc ∪ ran ∪ (𝐺 “ 𝐶) ·o (rank‘𝑦)) +o ((𝐺‘suc (rank‘𝑦))‘𝑦)), (𝐹‘(𝐻 “ 𝑦))))) | ||
| Theorem | dfac12lem2 10006* | Lemma for dfac12 10011. (Contributed by Mario Carneiro, 29-May-2015.) |
| ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐹:𝒫 (har‘(𝑅1‘𝐴))–1-1→On) & ⊢ 𝐺 = recs((𝑥 ∈ V ↦ (𝑦 ∈ (𝑅1‘dom 𝑥) ↦ if(dom 𝑥 = ∪ dom 𝑥, ((suc ∪ ran ∪ ran 𝑥 ·o (rank‘𝑦)) +o ((𝑥‘suc (rank‘𝑦))‘𝑦)), (𝐹‘((◡OrdIso( E , ran (𝑥‘∪ dom 𝑥)) ∘ (𝑥‘∪ dom 𝑥)) “ 𝑦)))))) & ⊢ (𝜑 → 𝐶 ∈ On) & ⊢ 𝐻 = (◡OrdIso( E , ran (𝐺‘∪ 𝐶)) ∘ (𝐺‘∪ 𝐶)) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) & ⊢ (𝜑 → ∀𝑧 ∈ 𝐶 (𝐺‘𝑧):(𝑅1‘𝑧)–1-1→On) ⇒ ⊢ (𝜑 → (𝐺‘𝐶):(𝑅1‘𝐶)–1-1→On) | ||
| Theorem | dfac12lem3 10007* | Lemma for dfac12 10011. (Contributed by Mario Carneiro, 29-May-2015.) |
| ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐹:𝒫 (har‘(𝑅1‘𝐴))–1-1→On) & ⊢ 𝐺 = recs((𝑥 ∈ V ↦ (𝑦 ∈ (𝑅1‘dom 𝑥) ↦ if(dom 𝑥 = ∪ dom 𝑥, ((suc ∪ ran ∪ ran 𝑥 ·o (rank‘𝑦)) +o ((𝑥‘suc (rank‘𝑦))‘𝑦)), (𝐹‘((◡OrdIso( E , ran (𝑥‘∪ dom 𝑥)) ∘ (𝑥‘∪ dom 𝑥)) “ 𝑦)))))) ⇒ ⊢ (𝜑 → (𝑅1‘𝐴) ∈ dom card) | ||
| Theorem | dfac12r 10008 | The axiom of choice holds iff every ordinal has a well-orderable powerset. This version of dfac12 10011 does not assume the Axiom of Regularity. (Contributed by Mario Carneiro, 29-May-2015.) |
| ⊢ (∀𝑥 ∈ On 𝒫 𝑥 ∈ dom card ↔ ∪ (𝑅1 “ On) ⊆ dom card) | ||
| Theorem | dfac12k 10009* | Equivalence of dfac12 10011 and dfac12a 10010, without using Regularity. (Contributed by Mario Carneiro, 21-May-2015.) |
| ⊢ (∀𝑥 ∈ On 𝒫 𝑥 ∈ dom card ↔ ∀𝑦 ∈ On 𝒫 (ℵ‘𝑦) ∈ dom card) | ||
| Theorem | dfac12a 10010 | The axiom of choice holds iff every ordinal has a well-orderable powerset. (Contributed by Mario Carneiro, 29-May-2015.) |
| ⊢ (CHOICE ↔ ∀𝑥 ∈ On 𝒫 𝑥 ∈ dom card) | ||
| Theorem | dfac12 10011 | The axiom of choice holds iff every aleph has a well-orderable powerset. (Contributed by Mario Carneiro, 21-May-2015.) |
| ⊢ (CHOICE ↔ ∀𝑥 ∈ On 𝒫 (ℵ‘𝑥) ∈ dom card) | ||
| Theorem | kmlem1 10012* | Lemma for 5-quantifier AC of Kurt Maes, Th. 4, 1 => 2. (Contributed by NM, 5-Apr-2004.) |
| ⊢ (∀𝑥((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑) → ∃𝑦∀𝑧 ∈ 𝑥 𝜓) → ∀𝑥(∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑 → ∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → 𝜓))) | ||
| Theorem | kmlem2 10013* | Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. (Contributed by NM, 25-Mar-2004.) |
| ⊢ (∃𝑦∀𝑧 ∈ 𝑥 (𝜑 → ∃!𝑤 𝑤 ∈ (𝑧 ∩ 𝑦)) ↔ ∃𝑦(¬ 𝑦 ∈ 𝑥 ∧ ∀𝑧 ∈ 𝑥 (𝜑 → ∃!𝑤 𝑤 ∈ (𝑧 ∩ 𝑦)))) | ||
| Theorem | kmlem3 10014* | Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. The right-hand side is part of the hypothesis of 4. (Contributed by NM, 25-Mar-2004.) |
| ⊢ ((𝑧 ∖ ∪ (𝑥 ∖ {𝑧})) ≠ ∅ ↔ ∃𝑣 ∈ 𝑧 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤))) | ||
| Theorem | kmlem4 10015* | Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. (Contributed by NM, 26-Mar-2004.) |
| ⊢ ((𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤) → ((𝑧 ∖ ∪ (𝑥 ∖ {𝑧})) ∩ 𝑤) = ∅) | ||
| Theorem | kmlem5 10016* | Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. (Contributed by NM, 25-Mar-2004.) |
| ⊢ ((𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤) → ((𝑧 ∖ ∪ (𝑥 ∖ {𝑧})) ∩ (𝑤 ∖ ∪ (𝑥 ∖ {𝑤}))) = ∅) | ||
| Theorem | kmlem6 10017* | Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 4 => 1. (Contributed by NM, 26-Mar-2004.) |
| ⊢ ((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝜑 → 𝐴 = ∅)) → ∀𝑧 ∈ 𝑥 ∃𝑣 ∈ 𝑧 ∀𝑤 ∈ 𝑥 (𝜑 → ¬ 𝑣 ∈ 𝐴)) | ||
| Theorem | kmlem7 10018* | Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 4 => 1. (Contributed by NM, 26-Mar-2004.) |
| ⊢ ((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ¬ ∃𝑧 ∈ 𝑥 ∀𝑣 ∈ 𝑧 ∃𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 ∧ 𝑣 ∈ (𝑧 ∩ 𝑤))) | ||
| Theorem | kmlem8 10019* | Lemma for 5-quantifier AC of Kurt Maes, Th. 4 1 <=> 4. (Contributed by NM, 4-Apr-2004.) |
| ⊢ ((¬ ∃𝑧 ∈ 𝑢 ∀𝑤 ∈ 𝑧 𝜓 → ∃𝑦∀𝑧 ∈ 𝑢 (𝑧 ≠ ∅ → ∃!𝑤 𝑤 ∈ (𝑧 ∩ 𝑦))) ↔ (∃𝑧 ∈ 𝑢 ∀𝑤 ∈ 𝑧 𝜓 ∨ ∃𝑦(¬ 𝑦 ∈ 𝑢 ∧ ∀𝑧 ∈ 𝑢 ∃!𝑤 𝑤 ∈ (𝑧 ∩ 𝑦)))) | ||
| Theorem | kmlem9 10020* | Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. (Contributed by NM, 25-Mar-2004.) |
| ⊢ 𝐴 = {𝑢 ∣ ∃𝑡 ∈ 𝑥 𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))} ⇒ ⊢ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅) | ||
| Theorem | kmlem10 10021* | Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. (Contributed by NM, 25-Mar-2004.) |
| ⊢ 𝐴 = {𝑢 ∣ ∃𝑡 ∈ 𝑥 𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))} ⇒ ⊢ (∀ℎ(∀𝑧 ∈ ℎ ∀𝑤 ∈ ℎ (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅) → ∃𝑦∀𝑧 ∈ ℎ 𝜑) → ∃𝑦∀𝑧 ∈ 𝐴 𝜑) | ||
| Theorem | kmlem11 10022* | Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. (Contributed by NM, 26-Mar-2004.) |
| ⊢ 𝐴 = {𝑢 ∣ ∃𝑡 ∈ 𝑥 𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))} ⇒ ⊢ (𝑧 ∈ 𝑥 → (𝑧 ∩ ∪ 𝐴) = (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) | ||
| Theorem | kmlem12 10023* | Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. (Contributed by NM, 27-Mar-2004.) |
| ⊢ 𝐴 = {𝑢 ∣ ∃𝑡 ∈ 𝑥 𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))} ⇒ ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ∖ ∪ (𝑥 ∖ {𝑧})) ≠ ∅ → (∀𝑧 ∈ 𝐴 (𝑧 ≠ ∅ → ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)) → ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ∃!𝑣 𝑣 ∈ (𝑧 ∩ (𝑦 ∩ ∪ 𝐴))))) | ||
| Theorem | kmlem13 10024* | Lemma for 5-quantifier AC of Kurt Maes, Th. 4 1 <=> 4. (Contributed by NM, 5-Apr-2004.) |
| ⊢ 𝐴 = {𝑢 ∣ ∃𝑡 ∈ 𝑥 𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))} ⇒ ⊢ (∀𝑥((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ∃𝑦∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)) ↔ ∀𝑥(¬ ∃𝑧 ∈ 𝑥 ∀𝑣 ∈ 𝑧 ∃𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 ∧ 𝑣 ∈ (𝑧 ∩ 𝑤)) → ∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)))) | ||
| Theorem | kmlem14 10025* | Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 5 <=> 4. (Contributed by NM, 4-Apr-2004.) |
| ⊢ (𝜑 ↔ (𝑧 ∈ 𝑦 → ((𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣) ∧ 𝑧 ∈ 𝑣))) & ⊢ (𝜓 ↔ (𝑧 ∈ 𝑥 → ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣)))) & ⊢ (𝜒 ↔ ∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)) ⇒ ⊢ (∃𝑧 ∈ 𝑥 ∀𝑣 ∈ 𝑧 ∃𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 ∧ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ ∃𝑦∀𝑧∃𝑣∀𝑢(𝑦 ∈ 𝑥 ∧ 𝜑)) | ||
| Theorem | kmlem15 10026* | Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 5 <=> 4. (Contributed by NM, 4-Apr-2004.) |
| ⊢ (𝜑 ↔ (𝑧 ∈ 𝑦 → ((𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣) ∧ 𝑧 ∈ 𝑣))) & ⊢ (𝜓 ↔ (𝑧 ∈ 𝑥 → ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣)))) & ⊢ (𝜒 ↔ ∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)) ⇒ ⊢ ((¬ 𝑦 ∈ 𝑥 ∧ 𝜒) ↔ ∀𝑧∃𝑣∀𝑢(¬ 𝑦 ∈ 𝑥 ∧ 𝜓)) | ||
| Theorem | kmlem16 10027* | Lemma for 5-quantifier AC of Kurt Maes, Th. 4 5 <=> 4. (Contributed by NM, 4-Apr-2004.) |
| ⊢ (𝜑 ↔ (𝑧 ∈ 𝑦 → ((𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣) ∧ 𝑧 ∈ 𝑣))) & ⊢ (𝜓 ↔ (𝑧 ∈ 𝑥 → ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣)))) & ⊢ (𝜒 ↔ ∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)) ⇒ ⊢ ((∃𝑧 ∈ 𝑥 ∀𝑣 ∈ 𝑧 ∃𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 ∧ 𝑣 ∈ (𝑧 ∩ 𝑤)) ∨ ∃𝑦(¬ 𝑦 ∈ 𝑥 ∧ 𝜒)) ↔ ∃𝑦∀𝑧∃𝑣∀𝑢((𝑦 ∈ 𝑥 ∧ 𝜑) ∨ (¬ 𝑦 ∈ 𝑥 ∧ 𝜓))) | ||
| Theorem | dfackm 10028* | Equivalence of the Axiom of Choice and Maes' AC ackm 10327. The proof consists of lemmas kmlem1 10012 through kmlem16 10027 and this final theorem. AC is not used for the proof. Note: bypassing the first step (i.e., replacing dfac5 9990 with biid 261) establishes the AC equivalence shown by Maes' writeup. The left-hand-side AC shown here was chosen because it is shorter to display. (Contributed by NM, 13-Apr-2004.) (Revised by Mario Carneiro, 17-May-2015.) |
| ⊢ (CHOICE ↔ ∀𝑥∃𝑦∀𝑧∃𝑣∀𝑢((𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → ((𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣) ∧ 𝑧 ∈ 𝑣))) ∨ (¬ 𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑥 → ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣)))))) | ||
For cardinal arithmetic, we follow [Mendelson] p. 258. Rather than defining operations restricted to cardinal numbers, we use disjoint union df-dju 9763 (⊔) for cardinal addition, Cartesian product df-xp 5631 (×) for cardinal multiplication, and set exponentiation df-map 8693 (↑m) for cardinal 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 10413, carddom 10416, and cardsdom 10417. The advantage of Mendelson's approach is that we can directly use many equinumerosity theorems that we already have available. | ||
| Theorem | undjudom 10029 | Cardinal addition dominates union. (Contributed by NM, 28-Sep-2004.) (Revised by Jim Kingdon, 15-Aug-2023.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ≼ (𝐴 ⊔ 𝐵)) | ||
| Theorem | endjudisj 10030 | Equinumerosity of a disjoint union and a union of two disjoint sets. (Contributed by NM, 5-Apr-2007.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐴 ⊔ 𝐵) ≈ (𝐴 ∪ 𝐵)) | ||
| Theorem | djuen 10031 | Disjoint unions of equinumerous sets are equinumerous. (Contributed by NM, 28-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
| ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷) → (𝐴 ⊔ 𝐶) ≈ (𝐵 ⊔ 𝐷)) | ||
| Theorem | djuenun 10032 | Disjoint union is equinumerous to union for disjoint sets. (Contributed by Mario Carneiro, 29-Apr-2015.) (Revised by Jim Kingdon, 19-Aug-2023.) |
| ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷 ∧ (𝐵 ∩ 𝐷) = ∅) → (𝐴 ⊔ 𝐶) ≈ (𝐵 ∪ 𝐷)) | ||
| Theorem | dju1en 10033 | 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.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ 𝐴) → (𝐴 ⊔ 1o) ≈ suc 𝐴) | ||
| Theorem | dju1dif 10034 | Adding and subtracting one gives back the original cardinality. Similar to pncan 11333 for cardinalities. (Contributed by Mario Carneiro, 18-May-2015.) (Revised by Jim Kingdon, 20-Aug-2023.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (𝐴 ⊔ 1o)) → ((𝐴 ⊔ 1o) ∖ {𝐵}) ≈ 𝐴) | ||
| Theorem | dju1p1e2 10035 | 1+1=2 for cardinal number addition, derived from pm54.43 9863 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 9757), but after applying definitions, our theorem is equivalent. Because we use a disjoint union for cardinal addition (as explained in the comment at the top of this section), we use ≈ instead of =. See dju1p1e2ALT 10036 for a shorter proof that doesn't use pm54.43 9863. (Contributed by NM, 5-Apr-2007.) (Proof modification is discouraged.) |
| ⊢ (1o ⊔ 1o) ≈ 2o | ||
| Theorem | dju1p1e2ALT 10036 | Alternate proof of dju1p1e2 10035. (Contributed by Mario Carneiro, 29-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (1o ⊔ 1o) ≈ 2o | ||
| Theorem | dju0en 10037 | 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 | xp2dju 10038 | 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.) |
| ⊢ (2o × 𝐴) = (𝐴 ⊔ 𝐴) | ||
| Theorem | djucomen 10039 | 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 | djuassen 10040 | 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 | xpdjuen 10041 | 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 | mapdjuen 10042 | 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.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 ↑m (𝐵 ⊔ 𝐶)) ≈ ((𝐴 ↑m 𝐵) × (𝐴 ↑m 𝐶))) | ||
| Theorem | pwdjuen 10043 | Sum of exponents law for cardinal arithmetic. (Contributed by Mario Carneiro, 15-May-2015.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝒫 (𝐴 ⊔ 𝐵) ≈ (𝒫 𝐴 × 𝒫 𝐵)) | ||
| Theorem | djudom1 10044 | 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.) (Revised by Jim Kingdon, 1-Sep-2023.) |
| ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐶 ∈ 𝑉) → (𝐴 ⊔ 𝐶) ≼ (𝐵 ⊔ 𝐶)) | ||
| Theorem | djudom2 10045 | 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 | djudoml 10046 | A set is dominated by its disjoint union with another. (Contributed by NM, 28-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐴 ≼ (𝐴 ⊔ 𝐵)) | ||
| Theorem | djuxpdom 10047 | 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.) |
| ⊢ ((1o ≺ 𝐴 ∧ 1o ≺ 𝐵) → (𝐴 ⊔ 𝐵) ≼ (𝐴 × 𝐵)) | ||
| Theorem | djufi 10048 | The disjoint union of two finite sets is finite. (Contributed by NM, 22-Oct-2004.) |
| ⊢ ((𝐴 ≺ ω ∧ 𝐵 ≺ ω) → (𝐴 ⊔ 𝐵) ≺ ω) | ||
| Theorem | cdainflem 10049 | Any partition of omega into two pieces (which may be disjoint) contains an infinite subset. (Contributed by Mario Carneiro, 11-Feb-2013.) |
| ⊢ ((𝐴 ∪ 𝐵) ≈ ω → (𝐴 ≈ ω ∨ 𝐵 ≈ ω)) | ||
| Theorem | djuinf 10050 | 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 10051 | An infinite set is equinumerous to itself added with one. (Contributed by Mario Carneiro, 15-May-2015.) |
| ⊢ (ω ≼ 𝐴 → (𝐴 ⊔ 1o) ≈ 𝐴) | ||
| Theorem | pwdju1 10052 | The sum of a powerset with itself is equipotent to the successor powerset. (Contributed by Mario Carneiro, 15-May-2015.) |
| ⊢ (𝐴 ∈ 𝑉 → (𝒫 𝐴 ⊔ 𝒫 𝐴) ≈ 𝒫 (𝐴 ⊔ 1o)) | ||
| Theorem | pwdjuidm 10053 | If the natural numbers inject into 𝐴, then 𝒫 𝐴 is idempotent under cardinal sum. (Contributed by Mario Carneiro, 15-May-2015.) |
| ⊢ (ω ≼ 𝐴 → (𝒫 𝐴 ⊔ 𝒫 𝐴) ≈ 𝒫 𝐴) | ||
| Theorem | djulepw 10054 | 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 10055 | 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 10056 | 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 10057 | The disjoint union of two numerable sets is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.) |
| ⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → (𝐴 ⊔ 𝐵) ∈ dom card) | ||
| Theorem | unnum 10058 | The union of two numerable sets is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.) |
| ⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → (𝐴 ∪ 𝐵) ∈ dom card) | ||
| Theorem | nnadju 10059 | The cardinal and ordinal sums of finite ordinals are equal. For a shorter proof using ax-rep 5234, see nnadjuALT 10060. (Contributed by Paul Chapman, 11-Apr-2009.) (Revised by Mario Carneiro, 6-Feb-2013.) Avoid ax-rep 5234. (Revised by BTernaryTau, 2-Jul-2024.) |
| ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (card‘(𝐴 ⊔ 𝐵)) = (𝐴 +o 𝐵)) | ||
| Theorem | nnadjuALT 10060 | Shorter proof of nnadju 10059 using ax-rep 5234. (Contributed by Paul Chapman, 11-Apr-2009.) (Revised by Mario Carneiro, 6-Feb-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (card‘(𝐴 ⊔ 𝐵)) = (𝐴 +o 𝐵)) | ||
| Theorem | ficardadju 10061 | The disjoint union of finite sets is equinumerous to the ordinal sum of the cardinalities of those sets. (Contributed by BTernaryTau, 3-Jul-2024.) |
| ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ⊔ 𝐵) ≈ ((card‘𝐴) +o (card‘𝐵))) | ||
| Theorem | ficardun 10062 | 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.) Avoid ax-rep 5234. (Revised by BTernaryTau, 3-Jul-2024.) |
| ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ (𝐴 ∩ 𝐵) = ∅) → (card‘(𝐴 ∪ 𝐵)) = ((card‘𝐴) +o (card‘𝐵))) | ||
| Theorem | ficardunOLD 10063 | Obsolete version of ficardun 10062 as of 3-Jul-2024. (Contributed by Paul Chapman, 5-Jun-2009.) (Proof shortened by Mario Carneiro, 28-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ (𝐴 ∩ 𝐵) = ∅) → (card‘(𝐴 ∪ 𝐵)) = ((card‘𝐴) +o (card‘𝐵))) | ||
| Theorem | ficardun2 10064 | The cardinality of the union of finite sets is at most the ordinal sum of their cardinalities. (Contributed by Mario Carneiro, 5-Feb-2013.) Avoid ax-rep 5234. (Revised by BTernaryTau, 3-Jul-2024.) |
| ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (card‘(𝐴 ∪ 𝐵)) ⊆ ((card‘𝐴) +o (card‘𝐵))) | ||
| Theorem | ficardun2OLD 10065 | Obsolete version of ficardun2 10064 as of 3-Jul-2024. (Contributed by Mario Carneiro, 5-Feb-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (card‘(𝐴 ∪ 𝐵)) ⊆ ((card‘𝐴) +o (card‘𝐵))) | ||
| Theorem | pwsdompw 10066* | Lemma for domtriom 10305. This is the equinumerosity version of the algebraic identity Σ𝑘 ∈ 𝑛(2↑𝑘) = (2↑𝑛) − 1. (Contributed by Mario Carneiro, 7-Feb-2013.) |
| ⊢ ((𝑛 ∈ ω ∧ ∀𝑘 ∈ suc 𝑛(𝐵‘𝑘) ≈ 𝒫 𝑘) → ∪ 𝑘 ∈ 𝑛 (𝐵‘𝑘) ≺ (𝐵‘𝑛)) | ||
| Theorem | unctb 10067 | The union of two countable sets is countable. (Contributed by FL, 25-Aug-2006.) (Proof shortened by Mario Carneiro, 30-Apr-2015.) |
| ⊢ ((𝐴 ≼ ω ∧ 𝐵 ≼ ω) → (𝐴 ∪ 𝐵) ≼ ω) | ||
| Theorem | infdjuabs 10068 | 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 10069 | 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 10070 | 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 10071 | 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 10072 | 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 10073 | 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 10074 | 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 10075 | The union of two sets that are strictly dominated by the infinite set 𝑋 is also dominated by 𝑋. This version of infunsdom 10076 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 10076 | 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 10077 | 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 10078 | A property of dominance over a powerset, and a main lemma for gchac 10543. Similar to Lemma 2.3 of [KanamoriPincus] p. 420. (Contributed by Mario Carneiro, 15-May-2015.) |
| ⊢ (𝒫 (𝐴 ⊔ 𝐴) ≼ (𝐴 ⊔ 𝐵) → 𝒫 𝐴 ≼ 𝐵) | ||
| Theorem | infpss 10079* | Every infinite set has an equinumerous proper subset, proved without AC or Infinity. Exercise 7 of [TakeutiZaring] p. 91. See also infpssALT 10175. (Contributed by NM, 23-Oct-2004.) (Revised by Mario Carneiro, 30-Apr-2015.) |
| ⊢ (ω ≼ 𝐴 → ∃𝑥(𝑥 ⊊ 𝐴 ∧ 𝑥 ≈ 𝐴)) | ||
| Theorem | infmap2 10080* | An exponentiation law for infinite cardinals. Similar to Lemma 6.2 of [Jech] p. 43. Although this version of infmap 10438 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 10081 | Lemma for ackbij2 10105. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
| ⊢ (𝐴 ∈ ω → 𝒫 𝐴 ⊆ (𝒫 ω ∩ Fin)) | ||
| Theorem | ackbij1lem1 10082 | Lemma for ackbij2 10105. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
| ⊢ (¬ 𝐴 ∈ 𝐵 → (𝐵 ∩ suc 𝐴) = (𝐵 ∩ 𝐴)) | ||
| Theorem | ackbij1lem2 10083 | Lemma for ackbij2 10105. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
| ⊢ (𝐴 ∈ 𝐵 → (𝐵 ∩ suc 𝐴) = ({𝐴} ∪ (𝐵 ∩ 𝐴))) | ||
| Theorem | ackbij1lem3 10084 | Lemma for ackbij2 10105. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
| ⊢ (𝐴 ∈ ω → 𝐴 ∈ (𝒫 ω ∩ Fin)) | ||
| Theorem | ackbij1lem4 10085 | Lemma for ackbij2 10105. (Contributed by Stefan O'Rear, 19-Nov-2014.) |
| ⊢ (𝐴 ∈ ω → {𝐴} ∈ (𝒫 ω ∩ Fin)) | ||
| Theorem | ackbij1lem5 10086 | Lemma for ackbij2 10105. (Contributed by Stefan O'Rear, 19-Nov-2014.) (Proof shortened by AV, 18-Jul-2022.) |
| ⊢ (𝐴 ∈ ω → (card‘𝒫 suc 𝐴) = ((card‘𝒫 𝐴) +o (card‘𝒫 𝐴))) | ||
| Theorem | ackbij1lem6 10087 | Lemma for ackbij2 10105. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
| ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → (𝐴 ∪ 𝐵) ∈ (𝒫 ω ∩ Fin)) | ||
| Theorem | ackbij1lem7 10088* | Lemma for ackbij1 10100. (Contributed by Stefan O'Rear, 21-Nov-2014.) |
| ⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) ⇒ ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → (𝐹‘𝐴) = (card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦))) | ||
| Theorem | ackbij1lem8 10089* | Lemma for ackbij1 10100. (Contributed by Stefan O'Rear, 19-Nov-2014.) |
| ⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) ⇒ ⊢ (𝐴 ∈ ω → (𝐹‘{𝐴}) = (card‘𝒫 𝐴)) | ||
| Theorem | ackbij1lem9 10090* | Lemma for ackbij1 10100. (Contributed by Stefan O'Rear, 19-Nov-2014.) |
| ⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) ⇒ ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐹‘(𝐴 ∪ 𝐵)) = ((𝐹‘𝐴) +o (𝐹‘𝐵))) | ||
| Theorem | ackbij1lem10 10091* | Lemma for ackbij1 10100. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
| ⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) ⇒ ⊢ 𝐹:(𝒫 ω ∩ Fin)⟶ω | ||
| Theorem | ackbij1lem11 10092* | Lemma for ackbij1 10100. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
| ⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) ⇒ ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ (𝒫 ω ∩ Fin)) | ||
| Theorem | ackbij1lem12 10093* | Lemma for ackbij1 10100. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
| ⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) ⇒ ⊢ ((𝐵 ∈ (𝒫 ω ∩ Fin) ∧ 𝐴 ⊆ 𝐵) → (𝐹‘𝐴) ⊆ (𝐹‘𝐵)) | ||
| Theorem | ackbij1lem13 10094* | Lemma for ackbij1 10100. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
| ⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) ⇒ ⊢ (𝐹‘∅) = ∅ | ||
| Theorem | ackbij1lem14 10095* | Lemma for ackbij1 10100. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
| ⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) ⇒ ⊢ (𝐴 ∈ ω → (𝐹‘{𝐴}) = suc (𝐹‘𝐴)) | ||
| Theorem | ackbij1lem15 10096* | Lemma for ackbij1 10100. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
| ⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) ⇒ ⊢ (((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝑐 ∈ ω ∧ 𝑐 ∈ 𝐴 ∧ ¬ 𝑐 ∈ 𝐵)) → ¬ (𝐹‘(𝐴 ∩ suc 𝑐)) = (𝐹‘(𝐵 ∩ suc 𝑐))) | ||
| Theorem | ackbij1lem16 10097* | Lemma for ackbij1 10100. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
| ⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) ⇒ ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘𝐴) = (𝐹‘𝐵) → 𝐴 = 𝐵)) | ||
| Theorem | ackbij1lem17 10098* | Lemma for ackbij1 10100. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
| ⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) ⇒ ⊢ 𝐹:(𝒫 ω ∩ Fin)–1-1→ω | ||
| Theorem | ackbij1lem18 10099* | Lemma for ackbij1 10100. (Contributed by Stefan O'Rear, 18-Nov-2014.) |
| ⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦))) ⇒ ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → ∃𝑏 ∈ (𝒫 ω ∩ Fin)(𝐹‘𝑏) = suc (𝐹‘𝐴)) | ||
| Theorem | ackbij1 10100* | 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→ω | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |