P. 99 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 9801-9900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	iunfictbso 9801	Countability of a countable union of finite sets with a strict (not globally well) order fulfilling the choice role. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ ((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪ 𝐴) → ∪ 𝐴 ≼ ω)
2.6.12  Axiom of Choice equivalents
Syntax	wac 9802	Wff for an abbreviation of the axiom of choice.
wff CHOICE
Definition	df-ac 9803*	The expression CHOICE will be used as a readable shorthand for any form of the axiom of choice; all concrete forms are long, cryptic, have dummy variables, or all three, making it useful to have a short name. Similar to the Axiom of Choice (first form) of [Enderton] p. 49. There is a slight problem with taking the exact form of ax-ac 10146 as our definition, because the equivalence to more standard forms (dfac2 9818) requires the Axiom of Regularity, which we often try to avoid. Thus, we take the first of the "textbook forms" as the definition and derive the form of ax-ac 10146 itself as dfac0 9820. (Contributed by Mario Carneiro, 22-Feb-2015.)
⊢ (CHOICE ↔ ∀𝑥∃𝑓(𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥))
Theorem	aceq1 9804*	Equivalence of two versions of the Axiom of Choice ax-ac 10146. The proof uses neither AC nor the Axiom of Regularity. The right-hand side expresses our AC with the fewest number of different variables. (Contributed by NM, 5-Apr-2004.)
⊢ (∃𝑦∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∃𝑦∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
Theorem	aceq0 9805*	Equivalence of two versions of the Axiom of Choice. The proof uses neither AC nor the Axiom of Regularity. The right-hand side is our original ax-ac 10146. (Contributed by NM, 5-Apr-2004.)
⊢ (∃𝑦∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∃𝑦∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑣∀𝑢(∃𝑡((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦)) ↔ 𝑢 = 𝑣)))
Theorem	aceq2 9806*	Equivalence of two versions of the Axiom of Choice. The proof uses neither AC nor the Axiom of Regularity. (Contributed by NM, 5-Apr-2004.)
⊢ (∃𝑦∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ 𝑦 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
Theorem	aceq3lem 9807*	Lemma for dfac3 9808. (Contributed by NM, 2-Apr-2004.) (Revised by Mario Carneiro, 26-Jun-2015.)
⊢ 𝐹 = (𝑤 ∈ dom 𝑦 ↦ (𝑓‘{𝑢 ∣ 𝑤𝑦𝑢}))    ⇒   ⊢ (∀𝑥∃𝑓∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧) → ∃𝑓(𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦))
Theorem	dfac3 9808*	Equivalence of two versions of the Axiom of Choice. The left-hand side is defined as the Axiom of Choice (first form) of [Enderton] p. 49. The right-hand side is the Axiom of Choice of [TakeutiZaring] p. 83. The proof does not depend on AC. (Contributed by NM, 24-Mar-2004.) (Revised by Stefan O'Rear, 22-Feb-2015.)
⊢ (CHOICE ↔ ∀𝑥∃𝑓∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))
Theorem	dfac4 9809*	Equivalence of two versions of the Axiom of Choice. The right-hand side is Axiom AC of [BellMachover] p. 488. The proof does not depend on AC. (Contributed by NM, 24-Mar-2004.) (Revised by Mario Carneiro, 26-Jun-2015.)
⊢ (CHOICE ↔ ∀𝑥∃𝑓(𝑓 Fn 𝑥 ∧ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)))
Theorem	dfac5lem1 9810*	Lemma for dfac5 9815. (Contributed by NM, 12-Apr-2004.)
⊢ (∃!𝑣 𝑣 ∈ (({𝑤} × 𝑤) ∩ 𝑦) ↔ ∃!𝑔(𝑔 ∈ 𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦))
Theorem	dfac5lem2 9811*	Lemma for dfac5 9815. (Contributed by NM, 12-Apr-2004.)
⊢ 𝐴 = {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))}    ⇒   ⊢ (⟨𝑤, 𝑔⟩ ∈ ∪ 𝐴 ↔ (𝑤 ∈ ℎ ∧ 𝑔 ∈ 𝑤))
Theorem	dfac5lem3 9812*	Lemma for dfac5 9815. (Contributed by NM, 12-Apr-2004.)
⊢ 𝐴 = {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))}    ⇒   ⊢ (({𝑤} × 𝑤) ∈ 𝐴 ↔ (𝑤 ≠ ∅ ∧ 𝑤 ∈ ℎ))
Theorem	dfac5lem4 9813*	Lemma for dfac5 9815. (Contributed by NM, 11-Apr-2004.)
⊢ 𝐴 = {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))}    &   ⊢ 𝐵 = (∪ 𝐴 ∩ 𝑦)    &   ⊢ (𝜑 ↔ ∀𝑥((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ∃𝑦∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)))    ⇒   ⊢ (𝜑 → ∃𝑦∀𝑧 ∈ 𝐴 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦))
Theorem	dfac5lem5 9814*	Lemma for dfac5 9815. (Contributed by NM, 12-Apr-2004.)
⊢ 𝐴 = {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))}    &   ⊢ 𝐵 = (∪ 𝐴 ∩ 𝑦)    &   ⊢ (𝜑 ↔ ∀𝑥((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ∃𝑦∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)))    ⇒   ⊢ (𝜑 → ∃𝑓∀𝑤 ∈ ℎ (𝑤 ≠ ∅ → (𝑓‘𝑤) ∈ 𝑤))
Theorem	dfac5 9815*	Equivalence of two versions of the Axiom of Choice. The right-hand side is Theorem 6M(4) of [Enderton] p. 151 and asserts that given a family of mutually disjoint nonempty sets, a set exists containing exactly one member from each set in the family. The proof does not depend on AC. (Contributed by NM, 11-Apr-2004.) (Revised by Mario Carneiro, 17-May-2015.)
⊢ (CHOICE ↔ ∀𝑥((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ∃𝑦∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)))
Theorem	dfac2a 9816*	Our Axiom of Choice (in the form of ac3 10149) implies the Axiom of Choice (first form) of [Enderton] p. 49. The proof uses neither AC nor the Axiom of Regularity. See dfac2b 9817 for the converse (which does use the Axiom of Regularity). (Contributed by NM, 5-Apr-2004.) (Revised by Mario Carneiro, 26-Jun-2015.)
⊢ (∀𝑥∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ 𝑦 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) → CHOICE)
Theorem	dfac2b 9817*	Axiom of Choice (first form) of [Enderton] p. 49 implies our Axiom of Choice (in the form of ac3 10149). The proof does not make use of AC. Note that the Axiom of Regularity is used by the proof. Specifically, elneq 9287 and preleq 9304 that are referenced in the proof each make use of Regularity for their derivations. (The reverse implication can be derived without using Regularity; see dfac2a 9816.) (Contributed by NM, 5-Apr-2004.) (Revised by Mario Carneiro, 26-Jun-2015.) (Revised by AV, 16-Jun-2022.)
⊢ (CHOICE → ∀𝑥∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ 𝑦 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
Theorem	dfac2 9818*	Axiom of Choice (first form) of [Enderton] p. 49 corresponds to our Axiom of Choice (in the form of ac3 10149). The proof does not make use of AC, but the Axiom of Regularity is used (by applying dfac2b 9817). (Contributed by NM, 5-Apr-2004.) (Revised by Mario Carneiro, 26-Jun-2015.) (Revised by AV, 16-Jun-2022.)
⊢ (CHOICE ↔ ∀𝑥∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ∃!𝑤 ∈ 𝑧 ∃𝑣 ∈ 𝑦 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)))
Theorem	dfac7 9819*	Equivalence of the Axiom of Choice (first form) of [Enderton] p. 49 and our Axiom of Choice (in the form of ac2 10148). The proof does not depend on AC but does depend on the Axiom of Regularity. (Contributed by Mario Carneiro, 17-May-2015.)
⊢ (CHOICE ↔ ∀𝑥∃𝑦∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢))
Theorem	dfac0 9820*	Equivalence of two versions of the Axiom of Choice. The proof uses the Axiom of Regularity. The right-hand side is our original ax-ac 10146. (Contributed by Mario Carneiro, 17-May-2015.)
⊢ (CHOICE ↔ ∀𝑥∃𝑦∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑣∀𝑢(∃𝑡((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦)) ↔ 𝑢 = 𝑣)))
Theorem	dfac1 9821*	Equivalence of two versions of the Axiom of Choice ax-ac 10146. The proof uses the Axiom of Regularity. The right-hand side expresses our AC with the fewest number of different variables. (Contributed by Mario Carneiro, 17-May-2015.)
⊢ (CHOICE ↔ ∀𝑥∃𝑦∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
Theorem	dfac8 9822*	A proof of the equivalency of the well-ordering theorem weth 10182 and the axiom of choice ac7 10160. (Contributed by Mario Carneiro, 5-Jan-2013.)
⊢ (CHOICE ↔ ∀𝑥∃𝑟 𝑟 We 𝑥)
Theorem	dfac9 9823*	Equivalence of the axiom of choice with a statement related to ac9 10170; definition AC3 of [Schechter] p. 139. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ (CHOICE ↔ ∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅))
Theorem	dfac10 9824	Axiom of Choice equivalent: the cardinality function measures every set. (Contributed by Mario Carneiro, 6-May-2015.)
⊢ (CHOICE ↔ dom card = V)
Theorem	dfac10c 9825*	Axiom of Choice equivalent: every set is equinumerous to an ordinal. (Contributed by Stefan O'Rear, 17-Jan-2015.)
⊢ (CHOICE ↔ ∀𝑥∃𝑦 ∈ On 𝑦 ≈ 𝑥)
Theorem	dfac10b 9826	Axiom of Choice equivalent: every set is equinumerous to an ordinal (quantifier-free short cryptic version alluded to in df-ac 9803). (Contributed by Stefan O'Rear, 17-Jan-2015.)
⊢ (CHOICE ↔ ( ≈ “ On) = V)
Theorem	acacni 9827	A choice equivalent: every set has choice sets of every length. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ ((CHOICE ∧ 𝐴 ∈ 𝑉) → AC 𝐴 = V)
Theorem	dfacacn 9828	A choice equivalent: every set has choice sets of every length. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ (CHOICE ↔ ∀𝑥AC 𝑥 = V)
Theorem	dfac13 9829	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 9830*	Lemma for dfac12 9836. (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 9831*	Lemma for dfac12 9836. (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 9832*	Lemma for dfac12 9836. (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 9833	The axiom of choice holds iff every ordinal has a well-orderable powerset. This version of dfac12 9836 does not assume the Axiom of Regularity. (Contributed by Mario Carneiro, 29-May-2015.)
⊢ (∀𝑥 ∈ On 𝒫 𝑥 ∈ dom card ↔ ∪ (𝑅1 “ On) ⊆ dom card)
Theorem	dfac12k 9834*	Equivalence of dfac12 9836 and dfac12a 9835, without using Regularity. (Contributed by Mario Carneiro, 21-May-2015.)
⊢ (∀𝑥 ∈ On 𝒫 𝑥 ∈ dom card ↔ ∀𝑦 ∈ On 𝒫 (ℵ‘𝑦) ∈ dom card)
Theorem	dfac12a 9835	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 9836	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 9837*	Lemma for 5-quantifier AC of Kurt Maes, Th. 4, 1 => 2. (Contributed by NM, 5-Apr-2004.)
⊢ (∀𝑥((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑) → ∃𝑦∀𝑧 ∈ 𝑥 𝜓) → ∀𝑥(∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 𝜑 → ∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → 𝜓)))
Theorem	kmlem2 9838*	Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. (Contributed by NM, 25-Mar-2004.)
⊢ (∃𝑦∀𝑧 ∈ 𝑥 (𝜑 → ∃!𝑤 𝑤 ∈ (𝑧 ∩ 𝑦)) ↔ ∃𝑦(¬ 𝑦 ∈ 𝑥 ∧ ∀𝑧 ∈ 𝑥 (𝜑 → ∃!𝑤 𝑤 ∈ (𝑧 ∩ 𝑦))))
Theorem	kmlem3 9839*	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 9840*	Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. (Contributed by NM, 26-Mar-2004.)
⊢ ((𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤) → ((𝑧 ∖ ∪ (𝑥 ∖ {𝑧})) ∩ 𝑤) = ∅)
Theorem	kmlem5 9841*	Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. (Contributed by NM, 25-Mar-2004.)
⊢ ((𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤) → ((𝑧 ∖ ∪ (𝑥 ∖ {𝑧})) ∩ (𝑤 ∖ ∪ (𝑥 ∖ {𝑤}))) = ∅)
Theorem	kmlem6 9842*	Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 4 => 1. (Contributed by NM, 26-Mar-2004.)
⊢ ((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝜑 → 𝐴 = ∅)) → ∀𝑧 ∈ 𝑥 ∃𝑣 ∈ 𝑧 ∀𝑤 ∈ 𝑥 (𝜑 → ¬ 𝑣 ∈ 𝐴))
Theorem	kmlem7 9843*	Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 4 => 1. (Contributed by NM, 26-Mar-2004.)
⊢ ((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ¬ ∃𝑧 ∈ 𝑥 ∀𝑣 ∈ 𝑧 ∃𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 ∧ 𝑣 ∈ (𝑧 ∩ 𝑤)))
Theorem	kmlem8 9844*	Lemma for 5-quantifier AC of Kurt Maes, Th. 4 1 <=> 4. (Contributed by NM, 4-Apr-2004.)
⊢ ((¬ ∃𝑧 ∈ 𝑢 ∀𝑤 ∈ 𝑧 𝜓 → ∃𝑦∀𝑧 ∈ 𝑢 (𝑧 ≠ ∅ → ∃!𝑤 𝑤 ∈ (𝑧 ∩ 𝑦))) ↔ (∃𝑧 ∈ 𝑢 ∀𝑤 ∈ 𝑧 𝜓 ∨ ∃𝑦(¬ 𝑦 ∈ 𝑢 ∧ ∀𝑧 ∈ 𝑢 ∃!𝑤 𝑤 ∈ (𝑧 ∩ 𝑦))))
Theorem	kmlem9 9845*	Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. (Contributed by NM, 25-Mar-2004.)
⊢ 𝐴 = {𝑢 ∣ ∃𝑡 ∈ 𝑥 𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))}    ⇒   ⊢ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)
Theorem	kmlem10 9846*	Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. (Contributed by NM, 25-Mar-2004.)
⊢ 𝐴 = {𝑢 ∣ ∃𝑡 ∈ 𝑥 𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))}    ⇒   ⊢ (∀ℎ(∀𝑧 ∈ ℎ ∀𝑤 ∈ ℎ (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅) → ∃𝑦∀𝑧 ∈ ℎ 𝜑) → ∃𝑦∀𝑧 ∈ 𝐴 𝜑)
Theorem	kmlem11 9847*	Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. (Contributed by NM, 26-Mar-2004.)
⊢ 𝐴 = {𝑢 ∣ ∃𝑡 ∈ 𝑥 𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))}    ⇒   ⊢ (𝑧 ∈ 𝑥 → (𝑧 ∩ ∪ 𝐴) = (𝑧 ∖ ∪ (𝑥 ∖ {𝑧})))
Theorem	kmlem12 9848*	Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. (Contributed by NM, 27-Mar-2004.)
⊢ 𝐴 = {𝑢 ∣ ∃𝑡 ∈ 𝑥 𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))}    ⇒   ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ∖ ∪ (𝑥 ∖ {𝑧})) ≠ ∅ → (∀𝑧 ∈ 𝐴 (𝑧 ≠ ∅ → ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)) → ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ∃!𝑣 𝑣 ∈ (𝑧 ∩ (𝑦 ∩ ∪ 𝐴)))))
Theorem	kmlem13 9849*	Lemma for 5-quantifier AC of Kurt Maes, Th. 4 1 <=> 4. (Contributed by NM, 5-Apr-2004.)
⊢ 𝐴 = {𝑢 ∣ ∃𝑡 ∈ 𝑥 𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))}    ⇒   ⊢ (∀𝑥((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ∃𝑦∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)) ↔ ∀𝑥(¬ ∃𝑧 ∈ 𝑥 ∀𝑣 ∈ 𝑧 ∃𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 ∧ 𝑣 ∈ (𝑧 ∩ 𝑤)) → ∃𝑦∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦))))
Theorem	kmlem14 9850*	Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 5 <=> 4. (Contributed by NM, 4-Apr-2004.)
⊢ (𝜑 ↔ (𝑧 ∈ 𝑦 → ((𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣) ∧ 𝑧 ∈ 𝑣)))    &   ⊢ (𝜓 ↔ (𝑧 ∈ 𝑥 → ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣))))    &   ⊢ (𝜒 ↔ ∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦))    ⇒   ⊢ (∃𝑧 ∈ 𝑥 ∀𝑣 ∈ 𝑧 ∃𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 ∧ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ ∃𝑦∀𝑧∃𝑣∀𝑢(𝑦 ∈ 𝑥 ∧ 𝜑))
Theorem	kmlem15 9851*	Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 5 <=> 4. (Contributed by NM, 4-Apr-2004.)
⊢ (𝜑 ↔ (𝑧 ∈ 𝑦 → ((𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣) ∧ 𝑧 ∈ 𝑣)))    &   ⊢ (𝜓 ↔ (𝑧 ∈ 𝑥 → ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣))))    &   ⊢ (𝜒 ↔ ∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦))    ⇒   ⊢ ((¬ 𝑦 ∈ 𝑥 ∧ 𝜒) ↔ ∀𝑧∃𝑣∀𝑢(¬ 𝑦 ∈ 𝑥 ∧ 𝜓))
Theorem	kmlem16 9852*	Lemma for 5-quantifier AC of Kurt Maes, Th. 4 5 <=> 4. (Contributed by NM, 4-Apr-2004.)
⊢ (𝜑 ↔ (𝑧 ∈ 𝑦 → ((𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣) ∧ 𝑧 ∈ 𝑣)))    &   ⊢ (𝜓 ↔ (𝑧 ∈ 𝑥 → ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣))))    &   ⊢ (𝜒 ↔ ∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦))    ⇒   ⊢ ((∃𝑧 ∈ 𝑥 ∀𝑣 ∈ 𝑧 ∃𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 ∧ 𝑣 ∈ (𝑧 ∩ 𝑤)) ∨ ∃𝑦(¬ 𝑦 ∈ 𝑥 ∧ 𝜒)) ↔ ∃𝑦∀𝑧∃𝑣∀𝑢((𝑦 ∈ 𝑥 ∧ 𝜑) ∨ (¬ 𝑦 ∈ 𝑥 ∧ 𝜓)))
Theorem	dfackm 9853*	Equivalence of the Axiom of Choice and Maes' AC ackm 10152. The proof consists of lemmas kmlem1 9837 through kmlem16 9852 and this final theorem. AC is not used for the proof. Note: bypassing the first step (i.e., replacing dfac5 9815 with biid 260) 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 9590 (⊔) for cardinal addition, Cartesian product df-xp 5586 (×) for cardinal multiplication, and set exponentiation df-map 8575 (↑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 10238, carddom 10241, and cardsdom 10242. The advantage of Mendelson's approach is that we can directly use many equinumerosity theorems that we already have available.
Theorem	undjudom 9854	Cardinal addition dominates union. (Contributed by NM, 28-Sep-2004.) (Revised by Jim Kingdon, 15-Aug-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ≼ (𝐴 ⊔ 𝐵))
Theorem	endjudisj 9855	Equinumerosity of a disjoint union and a union of two disjoint sets. (Contributed by NM, 5-Apr-2007.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐴 ⊔ 𝐵) ≈ (𝐴 ∪ 𝐵))
Theorem	djuen 9856	Disjoint unions of equinumerous sets are equinumerous. (Contributed by NM, 28-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷) → (𝐴 ⊔ 𝐶) ≈ (𝐵 ⊔ 𝐷))
Theorem	djuenun 9857	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 9858	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 9859	Adding and subtracting one gives back the original cardinality. Similar to pncan 11157 for cardinalities. (Contributed by Mario Carneiro, 18-May-2015.) (Revised by Jim Kingdon, 20-Aug-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (𝐴 ⊔ 1o)) → ((𝐴 ⊔ 1o) ∖ {𝐵}) ≈ 𝐴)
Theorem	dju1p1e2 9860	1+1=2 for cardinal number addition, derived from pm54.43 9690 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 9584), 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 9861 for a shorter proof that doesn't use pm54.43 9690. (Contributed by NM, 5-Apr-2007.) (Proof modification is discouraged.)
⊢ (1o ⊔ 1o) ≈ 2o
Theorem	dju1p1e2ALT 9861	Alternate proof of dju1p1e2 9860. (Contributed by Mario Carneiro, 29-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (1o ⊔ 1o) ≈ 2o
Theorem	dju0en 9862	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 9863	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 9864	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 9865	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 9866	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 9867	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 9868	Sum of exponents law for cardinal arithmetic. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝒫 (𝐴 ⊔ 𝐵) ≈ (𝒫 𝐴 × 𝒫 𝐵))
Theorem	djudom1 9869	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 9870	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 9871	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 9872	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 9873	The disjoint union of two finite sets is finite. (Contributed by NM, 22-Oct-2004.)
⊢ ((𝐴 ≺ ω ∧ 𝐵 ≺ ω) → (𝐴 ⊔ 𝐵) ≺ ω)
Theorem	cdainflem 9874	Any partition of omega into two pieces (which may be disjoint) contains an infinite subset. (Contributed by Mario Carneiro, 11-Feb-2013.)
⊢ ((𝐴 ∪ 𝐵) ≈ ω → (𝐴 ≈ ω ∨ 𝐵 ≈ ω))
Theorem	djuinf 9875	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 9876	An infinite set is equinumerous to itself added with one. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ (ω ≼ 𝐴 → (𝐴 ⊔ 1o) ≈ 𝐴)
Theorem	pwdju1 9877	The sum of a powerset with itself is equipotent to the successor powerset. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ (𝐴 ∈ 𝑉 → (𝒫 𝐴 ⊔ 𝒫 𝐴) ≈ 𝒫 (𝐴 ⊔ 1o))
Theorem	pwdjuidm 9878	If the natural numbers inject into 𝐴, then 𝒫 𝐴 is idempotent under cardinal sum. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ (ω ≼ 𝐴 → (𝒫 𝐴 ⊔ 𝒫 𝐴) ≈ 𝒫 𝐴)
Theorem	djulepw 9879	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 9880	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 9881	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 9882	The disjoint union of two numerable sets is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.)
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → (𝐴 ⊔ 𝐵) ∈ dom card)
Theorem	unnum 9883	The union of two numerable sets is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.)
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → (𝐴 ∪ 𝐵) ∈ dom card)
Theorem	nnadju 9884	The cardinal and ordinal sums of finite ordinals are equal. For a shorter proof using ax-rep 5205, see nnadjuALT 9885. (Contributed by Paul Chapman, 11-Apr-2009.) (Revised by Mario Carneiro, 6-Feb-2013.) Avoid ax-rep 5205. (Revised by BTernaryTau, 2-Jul-2024.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (card‘(𝐴 ⊔ 𝐵)) = (𝐴 +o 𝐵))
Theorem	nnadjuALT 9885	Shorter proof of nnadju 9884 using ax-rep 5205. (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 9886	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 9887	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 5205. (Revised by BTernaryTau, 3-Jul-2024.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ (𝐴 ∩ 𝐵) = ∅) → (card‘(𝐴 ∪ 𝐵)) = ((card‘𝐴) +o (card‘𝐵)))
Theorem	ficardunOLD 9888	Obsolete version of ficardun 9887 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 9889	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 5205. (Revised by BTernaryTau, 3-Jul-2024.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (card‘(𝐴 ∪ 𝐵)) ⊆ ((card‘𝐴) +o (card‘𝐵)))
Theorem	ficardun2OLD 9890	Obsolete version of ficardun2 9889 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 9891*	Lemma for domtriom 10130. This is the equinumerosity version of the algebraic identity Σ𝑘 ∈ 𝑛(2↑𝑘) = (2↑𝑛) − 1. (Contributed by Mario Carneiro, 7-Feb-2013.)
⊢ ((𝑛 ∈ ω ∧ ∀𝑘 ∈ suc 𝑛(𝐵‘𝑘) ≈ 𝒫 𝑘) → ∪ 𝑘 ∈ 𝑛 (𝐵‘𝑘) ≺ (𝐵‘𝑛))
Theorem	unctb 9892	The union of two countable sets is countable. (Contributed by FL, 25-Aug-2006.) (Proof shortened by Mario Carneiro, 30-Apr-2015.)
⊢ ((𝐴 ≼ ω ∧ 𝐵 ≼ ω) → (𝐴 ∪ 𝐵) ≼ ω)
Theorem	infdjuabs 9893	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 9894	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 9895	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 9896	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 9897	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 9898	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 9899	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 9900	The union of two sets that are strictly dominated by the infinite set 𝑋 is also dominated by 𝑋. This version of infunsdom 9901 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 ∧ ω ≼ 𝑋) ∧ (𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝑋)) → (𝐴 ∪ 𝐵) ≺ 𝑋)