P. 102 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 10101-10200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dfacacn 10101	A choice equivalent: every set has choice sets of every length. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ (CHOICE ↔ ∀𝑥AC 𝑥 = V)
Theorem	dfac13 10102	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 10103*	Lemma for dfac12 10109. (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 10104*	Lemma for dfac12 10109. (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 10105*	Lemma for dfac12 10109. (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 10106	The axiom of choice holds iff every ordinal has a well-orderable powerset. This version of dfac12 10109 does not assume the Axiom of Regularity. (Contributed by Mario Carneiro, 29-May-2015.)
⊢ (∀𝑥 ∈ On 𝒫 𝑥 ∈ dom card ↔ ∪ (𝑅1 “ On) ⊆ dom card)
Theorem	dfac12k 10107*	Equivalence of dfac12 10109 and dfac12a 10108, without using Regularity. (Contributed by Mario Carneiro, 21-May-2015.)
⊢ (∀𝑥 ∈ On 𝒫 𝑥 ∈ dom card ↔ ∀𝑦 ∈ On 𝒫 (ℵ‘𝑦) ∈ dom card)
Theorem	dfac12a 10108	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 10109	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 10110*	Lemma for 5-quantifier AC of Kurt Maes, Th. 4, 1 => 2. (Contributed by NM, 5-Apr-2004.)
⊢ (∀𝑥((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑) → ∃𝑦∀𝑧 ∈ 𝑥 𝜓) → ∀𝑥(∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑 → ∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → 𝜓)))
Theorem	kmlem2 10111*	Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. (Contributed by NM, 25-Mar-2004.)
⊢ (∃𝑦∀𝑧 ∈ 𝑥 (𝜑 → ∃!𝑤 𝑤 ∈ (𝑧 ∩ 𝑦)) ↔ ∃𝑦(¬ 𝑦 ∈ 𝑥 ∧ ∀𝑧 ∈ 𝑥 (𝜑 → ∃!𝑤 𝑤 ∈ (𝑧 ∩ 𝑦))))
Theorem	kmlem3 10112*	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 10113*	Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. (Contributed by NM, 26-Mar-2004.)
⊢ ((𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤) → ((𝑧 ∖ ∪ (𝑥 ∖ {𝑧})) ∩ 𝑤) = ∅)
Theorem	kmlem5 10114*	Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. (Contributed by NM, 25-Mar-2004.)
⊢ ((𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤) → ((𝑧 ∖ ∪ (𝑥 ∖ {𝑧})) ∩ (𝑤 ∖ ∪ (𝑥 ∖ {𝑤}))) = ∅)
Theorem	kmlem6 10115*	Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 4 => 1. (Contributed by NM, 26-Mar-2004.)
⊢ ((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝜑 → 𝐴 = ∅)) → ∀𝑧 ∈ 𝑥 ∃𝑣 ∈ 𝑧 ∀𝑤 ∈ 𝑥 (𝜑 → ¬ 𝑣 ∈ 𝐴))
Theorem	kmlem7 10116*	Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 4 => 1. (Contributed by NM, 26-Mar-2004.)
⊢ ((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ¬ ∃𝑧 ∈ 𝑥 ∀𝑣 ∈ 𝑧 ∃𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 ∧ 𝑣 ∈ (𝑧 ∩ 𝑤)))
Theorem	kmlem8 10117*	Lemma for 5-quantifier AC of Kurt Maes, Th. 4 1 <=> 4. (Contributed by NM, 4-Apr-2004.)
⊢ ((¬ ∃𝑧 ∈ 𝑢 ∀𝑤 ∈ 𝑧 𝜓 → ∃𝑦∀𝑧 ∈ 𝑢 (𝑧 ≠ ∅ → ∃!𝑤 𝑤 ∈ (𝑧 ∩ 𝑦))) ↔ (∃𝑧 ∈ 𝑢 ∀𝑤 ∈ 𝑧 𝜓 ∨ ∃𝑦(¬ 𝑦 ∈ 𝑢 ∧ ∀𝑧 ∈ 𝑢 ∃!𝑤 𝑤 ∈ (𝑧 ∩ 𝑦))))
Theorem	kmlem9 10118*	Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. (Contributed by NM, 25-Mar-2004.)
⊢ 𝐴 = {𝑢 ∣ ∃𝑡 ∈ 𝑥 𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))}    ⇒   ⊢ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)
Theorem	kmlem10 10119*	Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. (Contributed by NM, 25-Mar-2004.)
⊢ 𝐴 = {𝑢 ∣ ∃𝑡 ∈ 𝑥 𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))}    ⇒   ⊢ (∀ℎ(∀𝑧 ∈ ℎ ∀𝑤 ∈ ℎ (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅) → ∃𝑦∀𝑧 ∈ ℎ 𝜑) → ∃𝑦∀𝑧 ∈ 𝐴 𝜑)
Theorem	kmlem11 10120*	Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. (Contributed by NM, 26-Mar-2004.)
⊢ 𝐴 = {𝑢 ∣ ∃𝑡 ∈ 𝑥 𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))}    ⇒   ⊢ (𝑧 ∈ 𝑥 → (𝑧 ∩ ∪ 𝐴) = (𝑧 ∖ ∪ (𝑥 ∖ {𝑧})))
Theorem	kmlem12 10121*	Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. (Contributed by NM, 27-Mar-2004.)
⊢ 𝐴 = {𝑢 ∣ ∃𝑡 ∈ 𝑥 𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))}    ⇒   ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ∖ ∪ (𝑥 ∖ {𝑧})) ≠ ∅ → (∀𝑧 ∈ 𝐴 (𝑧 ≠ ∅ → ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)) → ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ∃!𝑣 𝑣 ∈ (𝑧 ∩ (𝑦 ∩ ∪ 𝐴)))))
Theorem	kmlem13 10122*	Lemma for 5-quantifier AC of Kurt Maes, Th. 4 1 <=> 4. (Contributed by NM, 5-Apr-2004.)
⊢ 𝐴 = {𝑢 ∣ ∃𝑡 ∈ 𝑥 𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))}    ⇒   ⊢ (∀𝑥((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ∃𝑦∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)) ↔ ∀𝑥(¬ ∃𝑧 ∈ 𝑥 ∀𝑣 ∈ 𝑧 ∃𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 ∧ 𝑣 ∈ (𝑧 ∩ 𝑤)) → ∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦))))
Theorem	kmlem14 10123*	Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 5 <=> 4. (Contributed by NM, 4-Apr-2004.)
⊢ (𝜑 ↔ (𝑧 ∈ 𝑦 → ((𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣) ∧ 𝑧 ∈ 𝑣)))    &   ⊢ (𝜓 ↔ (𝑧 ∈ 𝑥 → ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣))))    &   ⊢ (𝜒 ↔ ∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦))    ⇒   ⊢ (∃𝑧 ∈ 𝑥 ∀𝑣 ∈ 𝑧 ∃𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 ∧ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ ∃𝑦∀𝑧∃𝑣∀𝑢(𝑦 ∈ 𝑥 ∧ 𝜑))
Theorem	kmlem15 10124*	Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 5 <=> 4. (Contributed by NM, 4-Apr-2004.)
⊢ (𝜑 ↔ (𝑧 ∈ 𝑦 → ((𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣) ∧ 𝑧 ∈ 𝑣)))    &   ⊢ (𝜓 ↔ (𝑧 ∈ 𝑥 → ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣))))    &   ⊢ (𝜒 ↔ ∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦))    ⇒   ⊢ ((¬ 𝑦 ∈ 𝑥 ∧ 𝜒) ↔ ∀𝑧∃𝑣∀𝑢(¬ 𝑦 ∈ 𝑥 ∧ 𝜓))
Theorem	kmlem16 10125*	Lemma for 5-quantifier AC of Kurt Maes, Th. 4 5 <=> 4. (Contributed by NM, 4-Apr-2004.)
⊢ (𝜑 ↔ (𝑧 ∈ 𝑦 → ((𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣) ∧ 𝑧 ∈ 𝑣)))    &   ⊢ (𝜓 ↔ (𝑧 ∈ 𝑥 → ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣))))    &   ⊢ (𝜒 ↔ ∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦))    ⇒   ⊢ ((∃𝑧 ∈ 𝑥 ∀𝑣 ∈ 𝑧 ∃𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 ∧ 𝑣 ∈ (𝑧 ∩ 𝑤)) ∨ ∃𝑦(¬ 𝑦 ∈ 𝑥 ∧ 𝜒)) ↔ ∃𝑦∀𝑧∃𝑣∀𝑢((𝑦 ∈ 𝑥 ∧ 𝜑) ∨ (¬ 𝑦 ∈ 𝑥 ∧ 𝜓)))
Theorem	dfackm 10126*	Equivalence of the Axiom of Choice and Maes' AC ackm 10424. The proof consists of lemmas kmlem1 10110 through kmlem16 10125 and this final theorem. AC is not used for the proof. Note: bypassing the first step (i.e., replacing dfac5 10088 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 ↔ ∀𝑥∃𝑦∀𝑧∃𝑣∀𝑢((𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → ((𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣) ∧ 𝑧 ∈ 𝑣))) ∨ (¬ 𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑥 → ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣))))))
2.6.13  Cardinal number arithmetic For cardinal arithmetic, we follow [Mendelson] p. 258. Rather than defining operations restricted to cardinal numbers, we use disjoint union df-dju 9860 (⊔) for cardinal addition, Cartesian product df-xp 5646 (×) for cardinal multiplication, and set exponentiation df-map 8803 (↑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 10510, carddom 10513, and cardsdom 10514. The advantage of Mendelson's approach is that we can directly use many equinumerosity theorems that we already have available.
Theorem	undjudom 10127	Cardinal addition dominates union. (Contributed by NM, 28-Sep-2004.) (Revised by Jim Kingdon, 15-Aug-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ≼ (𝐴 ⊔ 𝐵))
Theorem	endjudisj 10128	Equinumerosity of a disjoint union and a union of two disjoint sets. (Contributed by NM, 5-Apr-2007.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐴 ⊔ 𝐵) ≈ (𝐴 ∪ 𝐵))
Theorem	djuen 10129	Disjoint unions of equinumerous sets are equinumerous. (Contributed by NM, 28-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷) → (𝐴 ⊔ 𝐶) ≈ (𝐵 ⊔ 𝐷))
Theorem	djuenun 10130	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 10131	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 10132	Adding and subtracting one gives back the original cardinality. Similar to pncan 11433 for cardinalities. (Contributed by Mario Carneiro, 18-May-2015.) (Revised by Jim Kingdon, 20-Aug-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (𝐴 ⊔ 1o)) → ((𝐴 ⊔ 1o) ∖ {𝐵}) ≈ 𝐴)
Theorem	dju1p1e2 10133	1+1=2 for cardinal number addition, derived from pm54.43 9960 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 9854), 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 10134 for a shorter proof that doesn't use pm54.43 9960. (Contributed by NM, 5-Apr-2007.) (Proof modification is discouraged.)
⊢ (1o ⊔ 1o) ≈ 2o
Theorem	dju1p1e2ALT 10134	Alternate proof of dju1p1e2 10133. (Contributed by Mario Carneiro, 29-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (1o ⊔ 1o) ≈ 2o
Theorem	dju0en 10135	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 10136	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 10137	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 10138	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 10139	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 10140	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 10141	Sum of exponents law for cardinal arithmetic. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝒫 (𝐴 ⊔ 𝐵) ≈ (𝒫 𝐴 × 𝒫 𝐵))
Theorem	djudom1 10142	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 10143	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 10144	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 10145	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 10146	The disjoint union of two finite sets is finite. (Contributed by NM, 22-Oct-2004.)
⊢ ((𝐴 ≺ ω ∧ 𝐵 ≺ ω) → (𝐴 ⊔ 𝐵) ≺ ω)
Theorem	cdainflem 10147	Any partition of omega into two pieces (which may be disjoint) contains an infinite subset. (Contributed by Mario Carneiro, 11-Feb-2013.)
⊢ ((𝐴 ∪ 𝐵) ≈ ω → (𝐴 ≈ ω ∨ 𝐵 ≈ ω))
Theorem	djuinf 10148	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 10149	An infinite set is equinumerous to itself added with one. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ (ω ≼ 𝐴 → (𝐴 ⊔ 1o) ≈ 𝐴)
Theorem	pwdju1 10150	The sum of a powerset with itself is equipotent to the successor powerset. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ (𝐴 ∈ 𝑉 → (𝒫 𝐴 ⊔ 𝒫 𝐴) ≈ 𝒫 (𝐴 ⊔ 1o))
Theorem	pwdjuidm 10151	If the natural numbers inject into 𝐴, then 𝒫 𝐴 is idempotent under cardinal sum. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ (ω ≼ 𝐴 → (𝒫 𝐴 ⊔ 𝒫 𝐴) ≈ 𝒫 𝐴)
Theorem	djulepw 10152	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 10153	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 10154	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 10155	The disjoint union of two numerable sets is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.)
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → (𝐴 ⊔ 𝐵) ∈ dom card)
Theorem	unnum 10156	The union of two numerable sets is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.)
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → (𝐴 ∪ 𝐵) ∈ dom card)
Theorem	nnadju 10157	The cardinal and ordinal sums of finite ordinals are equal. For a shorter proof using ax-rep 5236, see nnadjuALT 10158. (Contributed by Paul Chapman, 11-Apr-2009.) (Revised by Mario Carneiro, 6-Feb-2013.) Avoid ax-rep 5236. (Revised by BTernaryTau, 2-Jul-2024.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (card‘(𝐴 ⊔ 𝐵)) = (𝐴 +o 𝐵))
Theorem	nnadjuALT 10158	Shorter proof of nnadju 10157 using ax-rep 5236. (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 10159	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 10160	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 5236. (Revised by BTernaryTau, 3-Jul-2024.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ (𝐴 ∩ 𝐵) = ∅) → (card‘(𝐴 ∪ 𝐵)) = ((card‘𝐴) +o (card‘𝐵)))
Theorem	ficardun2 10161	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 5236. (Revised by BTernaryTau, 3-Jul-2024.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (card‘(𝐴 ∪ 𝐵)) ⊆ ((card‘𝐴) +o (card‘𝐵)))
Theorem	pwsdompw 10162*	Lemma for domtriom 10402. This is the equinumerosity version of the algebraic identity Σ𝑘 ∈ 𝑛(2↑𝑘) = (2↑𝑛) − 1. (Contributed by Mario Carneiro, 7-Feb-2013.)
⊢ ((𝑛 ∈ ω ∧ ∀𝑘 ∈ suc 𝑛(𝐵‘𝑘) ≈ 𝒫 𝑘) → ∪ 𝑘 ∈ 𝑛 (𝐵‘𝑘) ≺ (𝐵‘𝑛))
Theorem	unctb 10163	The union of two countable sets is countable. (Contributed by FL, 25-Aug-2006.) (Proof shortened by Mario Carneiro, 30-Apr-2015.)
⊢ ((𝐴 ≼ ω ∧ 𝐵 ≼ ω) → (𝐴 ∪ 𝐵) ≼ ω)
Theorem	infdjuabs 10164	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 10165	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 10166	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 10167	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 10168	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 10169	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 10170	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 10171	The union of two sets that are strictly dominated by the infinite set 𝑋 is also dominated by 𝑋. This version of infunsdom 10172 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 10172	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 10173	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 10174	A property of dominance over a powerset, and a main lemma for gchac 10640. Similar to Lemma 2.3 of [KanamoriPincus] p. 420. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ (𝒫 (𝐴 ⊔ 𝐴) ≼ (𝐴 ⊔ 𝐵) → 𝒫 𝐴 ≼ 𝐵)
Theorem	infpss 10175*	Every infinite set has an equinumerous proper subset, proved without AC or Infinity. Exercise 7 of [TakeutiZaring] p. 91. See also infpssALT 10272. (Contributed by NM, 23-Oct-2004.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ (ω ≼ 𝐴 → ∃𝑥(𝑥 ⊊ 𝐴 ∧ 𝑥 ≈ 𝐴))
Theorem	infmap2 10176*	An exponentiation law for infinite cardinals. Similar to Lemma 6.2 of [Jech] p. 43. Although this version of infmap 10535 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 𝐵) ≈ {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐵)})
2.6.14  The Ackermann bijection
Theorem	ackbij2lem1 10177	Lemma for ackbij2 10201. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ (𝐴 ∈ ω → 𝒫 𝐴 ⊆ (𝒫 ω ∩ Fin))
Theorem	ackbij1lem1 10178	Lemma for ackbij2 10201. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ (¬ 𝐴 ∈ 𝐵 → (𝐵 ∩ suc 𝐴) = (𝐵 ∩ 𝐴))
Theorem	ackbij1lem2 10179	Lemma for ackbij2 10201. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ (𝐴 ∈ 𝐵 → (𝐵 ∩ suc 𝐴) = ({𝐴} ∪ (𝐵 ∩ 𝐴)))
Theorem	ackbij1lem3 10180	Lemma for ackbij2 10201. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ (𝐴 ∈ ω → 𝐴 ∈ (𝒫 ω ∩ Fin))
Theorem	ackbij1lem4 10181	Lemma for ackbij2 10201. (Contributed by Stefan O'Rear, 19-Nov-2014.)
⊢ (𝐴 ∈ ω → {𝐴} ∈ (𝒫 ω ∩ Fin))
Theorem	ackbij1lem5 10182	Lemma for ackbij2 10201. (Contributed by Stefan O'Rear, 19-Nov-2014.) (Proof shortened by AV, 18-Jul-2022.)
⊢ (𝐴 ∈ ω → (card‘𝒫 suc 𝐴) = ((card‘𝒫 𝐴) +o (card‘𝒫 𝐴)))
Theorem	ackbij1lem6 10183	Lemma for ackbij2 10201. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → (𝐴 ∪ 𝐵) ∈ (𝒫 ω ∩ Fin))
Theorem	ackbij1lem7 10184*	Lemma for ackbij1 10196. (Contributed by Stefan O'Rear, 21-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → (𝐹‘𝐴) = (card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)))
Theorem	ackbij1lem8 10185*	Lemma for ackbij1 10196. (Contributed by Stefan O'Rear, 19-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ (𝐴 ∈ ω → (𝐹‘{𝐴}) = (card‘𝒫 𝐴))
Theorem	ackbij1lem9 10186*	Lemma for ackbij1 10196. (Contributed by Stefan O'Rear, 19-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐹‘(𝐴 ∪ 𝐵)) = ((𝐹‘𝐴) +o (𝐹‘𝐵)))
Theorem	ackbij1lem10 10187*	Lemma for ackbij1 10196. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ 𝐹:(𝒫 ω ∩ Fin)⟶ω
Theorem	ackbij1lem11 10188*	Lemma for ackbij1 10196. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ (𝒫 ω ∩ Fin))
Theorem	ackbij1lem12 10189*	Lemma for ackbij1 10196. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ ((𝐵 ∈ (𝒫 ω ∩ Fin) ∧ 𝐴 ⊆ 𝐵) → (𝐹‘𝐴) ⊆ (𝐹‘𝐵))
Theorem	ackbij1lem13 10190*	Lemma for ackbij1 10196. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ (𝐹‘∅) = ∅
Theorem	ackbij1lem14 10191*	Lemma for ackbij1 10196. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ (𝐴 ∈ ω → (𝐹‘{𝐴}) = suc (𝐹‘𝐴))
Theorem	ackbij1lem15 10192*	Lemma for ackbij1 10196. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ (((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝑐 ∈ ω ∧ 𝑐 ∈ 𝐴 ∧ ¬ 𝑐 ∈ 𝐵)) → ¬ (𝐹‘(𝐴 ∩ suc 𝑐)) = (𝐹‘(𝐵 ∩ suc 𝑐)))
Theorem	ackbij1lem16 10193*	Lemma for ackbij1 10196. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘𝐴) = (𝐹‘𝐵) → 𝐴 = 𝐵))
Theorem	ackbij1lem17 10194*	Lemma for ackbij1 10196. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ 𝐹:(𝒫 ω ∩ Fin)–1-1→ω
Theorem	ackbij1lem18 10195*	Lemma for ackbij1 10196. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → ∃𝑏 ∈ (𝒫 ω ∩ Fin)(𝐹‘𝑏) = suc (𝐹‘𝐴))
Theorem	ackbij1 10196*	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 10197*	The Ackermann bijection, part 1b: the bijection from ackbij1 10196 restricts naturally to the powers of particular naturals. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ (𝐴 ∈ ω → (𝐹 “ 𝒫 𝐴) = (card‘𝒫 𝐴))
Theorem	ackbij2lem2 10198*	Lemma for ackbij2 10201. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    &   ⊢ 𝐺 = (𝑥 ∈ V ↦ (𝑦 ∈ 𝒫 dom 𝑥 ↦ (𝐹‘(𝑥 “ 𝑦))))    ⇒   ⊢ (𝐴 ∈ ω → (rec(𝐺, ∅)‘𝐴):(𝑅1‘𝐴)–1-1-onto→(card‘(𝑅1‘𝐴)))
Theorem	ackbij2lem3 10199*	Lemma for ackbij2 10201. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    &   ⊢ 𝐺 = (𝑥 ∈ V ↦ (𝑦 ∈ 𝒫 dom 𝑥 ↦ (𝐹‘(𝑥 “ 𝑦))))    ⇒   ⊢ (𝐴 ∈ ω → (rec(𝐺, ∅)‘𝐴) ⊆ (rec(𝐺, ∅)‘suc 𝐴))
Theorem	ackbij2lem4 10200*	Lemma for ackbij2 10201. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    &   ⊢ 𝐺 = (𝑥 ∈ V ↦ (𝑦 ∈ 𝒫 dom 𝑥 ↦ (𝐹‘(𝑥 “ 𝑦))))    ⇒   ⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐵 ⊆ 𝐴) → (rec(𝐺, ∅)‘𝐵) ⊆ (rec(𝐺, ∅)‘𝐴))