P. 103 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 10201-10300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	kmlem14 10201*	Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 5 <=> 4. (Contributed by NM, 4-Apr-2004.)
⊢ (𝜑 ↔ (𝑧 ∈ 𝑦 → ((𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣) ∧ 𝑧 ∈ 𝑣)))    &   ⊢ (𝜓 ↔ (𝑧 ∈ 𝑥 → ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣))))    &   ⊢ (𝜒 ↔ ∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦))    ⇒   ⊢ (∃𝑧 ∈ 𝑥 ∀𝑣 ∈ 𝑧 ∃𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 ∧ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ ∃𝑦∀𝑧∃𝑣∀𝑢(𝑦 ∈ 𝑥 ∧ 𝜑))
Theorem	kmlem15 10202*	Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 5 <=> 4. (Contributed by NM, 4-Apr-2004.)
⊢ (𝜑 ↔ (𝑧 ∈ 𝑦 → ((𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣) ∧ 𝑧 ∈ 𝑣)))    &   ⊢ (𝜓 ↔ (𝑧 ∈ 𝑥 → ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣))))    &   ⊢ (𝜒 ↔ ∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦))    ⇒   ⊢ ((¬ 𝑦 ∈ 𝑥 ∧ 𝜒) ↔ ∀𝑧∃𝑣∀𝑢(¬ 𝑦 ∈ 𝑥 ∧ 𝜓))
Theorem	kmlem16 10203*	Lemma for 5-quantifier AC of Kurt Maes, Th. 4 5 <=> 4. (Contributed by NM, 4-Apr-2004.)
⊢ (𝜑 ↔ (𝑧 ∈ 𝑦 → ((𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣) ∧ 𝑧 ∈ 𝑣)))    &   ⊢ (𝜓 ↔ (𝑧 ∈ 𝑥 → ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣))))    &   ⊢ (𝜒 ↔ ∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦))    ⇒   ⊢ ((∃𝑧 ∈ 𝑥 ∀𝑣 ∈ 𝑧 ∃𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 ∧ 𝑣 ∈ (𝑧 ∩ 𝑤)) ∨ ∃𝑦(¬ 𝑦 ∈ 𝑥 ∧ 𝜒)) ↔ ∃𝑦∀𝑧∃𝑣∀𝑢((𝑦 ∈ 𝑥 ∧ 𝜑) ∨ (¬ 𝑦 ∈ 𝑥 ∧ 𝜓)))
Theorem	dfackm 10204*	Equivalence of the Axiom of Choice and Maes' AC ackm 10502. The proof consists of lemmas kmlem1 10188 through kmlem16 10203 and this final theorem. AC is not used for the proof. Note: bypassing the first step (i.e., replacing dfac5 10166 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 9938 (⊔) for cardinal addition, Cartesian product df-xp 5694 (×) for cardinal multiplication, and set exponentiation df-map 8866 (↑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 10588, carddom 10591, and cardsdom 10592. The advantage of Mendelson's approach is that we can directly use many equinumerosity theorems that we already have available.
Theorem	undjudom 10205	Cardinal addition dominates union. (Contributed by NM, 28-Sep-2004.) (Revised by Jim Kingdon, 15-Aug-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ≼ (𝐴 ⊔ 𝐵))
Theorem	endjudisj 10206	Equinumerosity of a disjoint union and a union of two disjoint sets. (Contributed by NM, 5-Apr-2007.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐴 ⊔ 𝐵) ≈ (𝐴 ∪ 𝐵))
Theorem	djuen 10207	Disjoint unions of equinumerous sets are equinumerous. (Contributed by NM, 28-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷) → (𝐴 ⊔ 𝐶) ≈ (𝐵 ⊔ 𝐷))
Theorem	djuenun 10208	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 10209	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 10210	Adding and subtracting one gives back the original cardinality. Similar to pncan 11511 for cardinalities. (Contributed by Mario Carneiro, 18-May-2015.) (Revised by Jim Kingdon, 20-Aug-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (𝐴 ⊔ 1o)) → ((𝐴 ⊔ 1o) ∖ {𝐵}) ≈ 𝐴)
Theorem	dju1p1e2 10211	1+1=2 for cardinal number addition, derived from pm54.43 10038 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 9932), 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 10212 for a shorter proof that doesn't use pm54.43 10038. (Contributed by NM, 5-Apr-2007.) (Proof modification is discouraged.)
⊢ (1o ⊔ 1o) ≈ 2o
Theorem	dju1p1e2ALT 10212	Alternate proof of dju1p1e2 10211. (Contributed by Mario Carneiro, 29-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (1o ⊔ 1o) ≈ 2o
Theorem	dju0en 10213	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 10214	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 10215	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 10216	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 10217	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 10218	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 10219	Sum of exponents law for cardinal arithmetic. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝒫 (𝐴 ⊔ 𝐵) ≈ (𝒫 𝐴 × 𝒫 𝐵))
Theorem	djudom1 10220	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 10221	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 10222	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 10223	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 10224	The disjoint union of two finite sets is finite. (Contributed by NM, 22-Oct-2004.)
⊢ ((𝐴 ≺ ω ∧ 𝐵 ≺ ω) → (𝐴 ⊔ 𝐵) ≺ ω)
Theorem	cdainflem 10225	Any partition of omega into two pieces (which may be disjoint) contains an infinite subset. (Contributed by Mario Carneiro, 11-Feb-2013.)
⊢ ((𝐴 ∪ 𝐵) ≈ ω → (𝐴 ≈ ω ∨ 𝐵 ≈ ω))
Theorem	djuinf 10226	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 10227	An infinite set is equinumerous to itself added with one. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ (ω ≼ 𝐴 → (𝐴 ⊔ 1o) ≈ 𝐴)
Theorem	pwdju1 10228	The sum of a powerset with itself is equipotent to the successor powerset. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ (𝐴 ∈ 𝑉 → (𝒫 𝐴 ⊔ 𝒫 𝐴) ≈ 𝒫 (𝐴 ⊔ 1o))
Theorem	pwdjuidm 10229	If the natural numbers inject into 𝐴, then 𝒫 𝐴 is idempotent under cardinal sum. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ (ω ≼ 𝐴 → (𝒫 𝐴 ⊔ 𝒫 𝐴) ≈ 𝒫 𝐴)
Theorem	djulepw 10230	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 10231	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 10232	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 10233	The disjoint union of two numerable sets is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.)
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → (𝐴 ⊔ 𝐵) ∈ dom card)
Theorem	unnum 10234	The union of two numerable sets is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.)
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → (𝐴 ∪ 𝐵) ∈ dom card)
Theorem	nnadju 10235	The cardinal and ordinal sums of finite ordinals are equal. For a shorter proof using ax-rep 5284, see nnadjuALT 10236. (Contributed by Paul Chapman, 11-Apr-2009.) (Revised by Mario Carneiro, 6-Feb-2013.) Avoid ax-rep 5284. (Revised by BTernaryTau, 2-Jul-2024.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (card‘(𝐴 ⊔ 𝐵)) = (𝐴 +o 𝐵))
Theorem	nnadjuALT 10236	Shorter proof of nnadju 10235 using ax-rep 5284. (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 10237	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 10238	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 5284. (Revised by BTernaryTau, 3-Jul-2024.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ (𝐴 ∩ 𝐵) = ∅) → (card‘(𝐴 ∪ 𝐵)) = ((card‘𝐴) +o (card‘𝐵)))
Theorem	ficardun2 10239	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 5284. (Revised by BTernaryTau, 3-Jul-2024.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (card‘(𝐴 ∪ 𝐵)) ⊆ ((card‘𝐴) +o (card‘𝐵)))
Theorem	pwsdompw 10240*	Lemma for domtriom 10480. This is the equinumerosity version of the algebraic identity Σ𝑘 ∈ 𝑛(2↑𝑘) = (2↑𝑛) − 1. (Contributed by Mario Carneiro, 7-Feb-2013.)
⊢ ((𝑛 ∈ ω ∧ ∀𝑘 ∈ suc 𝑛(𝐵‘𝑘) ≈ 𝒫 𝑘) → ∪ 𝑘 ∈ 𝑛 (𝐵‘𝑘) ≺ (𝐵‘𝑛))
Theorem	unctb 10241	The union of two countable sets is countable. (Contributed by FL, 25-Aug-2006.) (Proof shortened by Mario Carneiro, 30-Apr-2015.)
⊢ ((𝐴 ≼ ω ∧ 𝐵 ≼ ω) → (𝐴 ∪ 𝐵) ≼ ω)
Theorem	infdjuabs 10242	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 10243	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 10244	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 10245	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 10246	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 10247	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 10248	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 10249	The union of two sets that are strictly dominated by the infinite set 𝑋 is also dominated by 𝑋. This version of infunsdom 10250 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 10250	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 10251	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 10252	A property of dominance over a powerset, and a main lemma for gchac 10718. Similar to Lemma 2.3 of [KanamoriPincus] p. 420. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ (𝒫 (𝐴 ⊔ 𝐴) ≼ (𝐴 ⊔ 𝐵) → 𝒫 𝐴 ≼ 𝐵)
Theorem	infpss 10253*	Every infinite set has an equinumerous proper subset, proved without AC or Infinity. Exercise 7 of [TakeutiZaring] p. 91. See also infpssALT 10350. (Contributed by NM, 23-Oct-2004.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ (ω ≼ 𝐴 → ∃𝑥(𝑥 ⊊ 𝐴 ∧ 𝑥 ≈ 𝐴))
Theorem	infmap2 10254*	An exponentiation law for infinite cardinals. Similar to Lemma 6.2 of [Jech] p. 43. Although this version of infmap 10613 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 10255	Lemma for ackbij2 10279. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ (𝐴 ∈ ω → 𝒫 𝐴 ⊆ (𝒫 ω ∩ Fin))
Theorem	ackbij1lem1 10256	Lemma for ackbij2 10279. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ (¬ 𝐴 ∈ 𝐵 → (𝐵 ∩ suc 𝐴) = (𝐵 ∩ 𝐴))
Theorem	ackbij1lem2 10257	Lemma for ackbij2 10279. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ (𝐴 ∈ 𝐵 → (𝐵 ∩ suc 𝐴) = ({𝐴} ∪ (𝐵 ∩ 𝐴)))
Theorem	ackbij1lem3 10258	Lemma for ackbij2 10279. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ (𝐴 ∈ ω → 𝐴 ∈ (𝒫 ω ∩ Fin))
Theorem	ackbij1lem4 10259	Lemma for ackbij2 10279. (Contributed by Stefan O'Rear, 19-Nov-2014.)
⊢ (𝐴 ∈ ω → {𝐴} ∈ (𝒫 ω ∩ Fin))
Theorem	ackbij1lem5 10260	Lemma for ackbij2 10279. (Contributed by Stefan O'Rear, 19-Nov-2014.) (Proof shortened by AV, 18-Jul-2022.)
⊢ (𝐴 ∈ ω → (card‘𝒫 suc 𝐴) = ((card‘𝒫 𝐴) +o (card‘𝒫 𝐴)))
Theorem	ackbij1lem6 10261	Lemma for ackbij2 10279. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → (𝐴 ∪ 𝐵) ∈ (𝒫 ω ∩ Fin))
Theorem	ackbij1lem7 10262*	Lemma for ackbij1 10274. (Contributed by Stefan O'Rear, 21-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → (𝐹‘𝐴) = (card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)))
Theorem	ackbij1lem8 10263*	Lemma for ackbij1 10274. (Contributed by Stefan O'Rear, 19-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ (𝐴 ∈ ω → (𝐹‘{𝐴}) = (card‘𝒫 𝐴))
Theorem	ackbij1lem9 10264*	Lemma for ackbij1 10274. (Contributed by Stefan O'Rear, 19-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐹‘(𝐴 ∪ 𝐵)) = ((𝐹‘𝐴) +o (𝐹‘𝐵)))
Theorem	ackbij1lem10 10265*	Lemma for ackbij1 10274. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ 𝐹:(𝒫 ω ∩ Fin)⟶ω
Theorem	ackbij1lem11 10266*	Lemma for ackbij1 10274. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ (𝒫 ω ∩ Fin))
Theorem	ackbij1lem12 10267*	Lemma for ackbij1 10274. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ ((𝐵 ∈ (𝒫 ω ∩ Fin) ∧ 𝐴 ⊆ 𝐵) → (𝐹‘𝐴) ⊆ (𝐹‘𝐵))
Theorem	ackbij1lem13 10268*	Lemma for ackbij1 10274. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ (𝐹‘∅) = ∅
Theorem	ackbij1lem14 10269*	Lemma for ackbij1 10274. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ (𝐴 ∈ ω → (𝐹‘{𝐴}) = suc (𝐹‘𝐴))
Theorem	ackbij1lem15 10270*	Lemma for ackbij1 10274. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ (((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝑐 ∈ ω ∧ 𝑐 ∈ 𝐴 ∧ ¬ 𝑐 ∈ 𝐵)) → ¬ (𝐹‘(𝐴 ∩ suc 𝑐)) = (𝐹‘(𝐵 ∩ suc 𝑐)))
Theorem	ackbij1lem16 10271*	Lemma for ackbij1 10274. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘𝐴) = (𝐹‘𝐵) → 𝐴 = 𝐵))
Theorem	ackbij1lem17 10272*	Lemma for ackbij1 10274. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ 𝐹:(𝒫 ω ∩ Fin)–1-1→ω
Theorem	ackbij1lem18 10273*	Lemma for ackbij1 10274. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → ∃𝑏 ∈ (𝒫 ω ∩ Fin)(𝐹‘𝑏) = suc (𝐹‘𝐴))
Theorem	ackbij1 10274*	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 10275*	The Ackermann bijection, part 1b: the bijection from ackbij1 10274 restricts naturally to the powers of particular naturals. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ (𝐴 ∈ ω → (𝐹 “ 𝒫 𝐴) = (card‘𝒫 𝐴))
Theorem	ackbij2lem2 10276*	Lemma for ackbij2 10279. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    &   ⊢ 𝐺 = (𝑥 ∈ V ↦ (𝑦 ∈ 𝒫 dom 𝑥 ↦ (𝐹‘(𝑥 “ 𝑦))))    ⇒   ⊢ (𝐴 ∈ ω → (rec(𝐺, ∅)‘𝐴):(𝑅1‘𝐴)–1-1-onto→(card‘(𝑅1‘𝐴)))
Theorem	ackbij2lem3 10277*	Lemma for ackbij2 10279. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    &   ⊢ 𝐺 = (𝑥 ∈ V ↦ (𝑦 ∈ 𝒫 dom 𝑥 ↦ (𝐹‘(𝑥 “ 𝑦))))    ⇒   ⊢ (𝐴 ∈ ω → (rec(𝐺, ∅)‘𝐴) ⊆ (rec(𝐺, ∅)‘suc 𝐴))
Theorem	ackbij2lem4 10278*	Lemma for ackbij2 10279. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    &   ⊢ 𝐺 = (𝑥 ∈ V ↦ (𝑦 ∈ 𝒫 dom 𝑥 ↦ (𝐹‘(𝑥 “ 𝑦))))    ⇒   ⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐵 ⊆ 𝐴) → (rec(𝐺, ∅)‘𝐵) ⊆ (rec(𝐺, ∅)‘𝐴))
Theorem	ackbij2 10279*	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 10280	The set of hereditarily finite sets is countable. See ackbij2 10279 for an explicit bijection that works without Infinity. See also r1omALT 10813. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ (𝑅1‘ω) ≈ ω
Theorem	fictb 10281	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‘𝐴) ≼ ω))
2.6.15  Cofinality (without Axiom of Choice)
Theorem	cflem 10282*	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.) Avoid ax-11 2154. (Revised by BTernaryTau, 25-Jul-2025.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)))
Theorem	cflemOLD 10283*	Obsolete version of cflem 10282 as of 25-Jul-2025. (Contributed by NM, 24-Apr-2004.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)))
Theorem	cfval 10284*	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 10285	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 10286*	An upper bound on cofinality. (Contributed by NM, 25-Apr-2004.) (Revised by Mario Carneiro, 15-Sep-2013.)
⊢ (cf‘𝐴) ⊆ ∩ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ ∪ 𝑦))}
Theorem	cflm 10287*	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 10288	Value of the cofinality function at 0. Exercise 2 of [TakeutiZaring] p. 102. (Contributed by NM, 16-Apr-2004.)
⊢ (cf‘∅) = ∅
Theorem	cardcf 10289	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 10290	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 10291	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 10292	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 10293	Only the ordinal zero has cofinality zero. (Contributed by NM, 24-Apr-2004.) (Revised by Mario Carneiro, 12-Feb-2013.)
⊢ (𝐴 ∈ On → ((cf‘𝐴) = ∅ ↔ 𝐴 = ∅))
Theorem	cfsuc 10294	Value of the cofinality function at a successor ordinal. Exercise 3 of [TakeutiZaring] p. 102. (Contributed by NM, 23-Apr-2004.) (Revised by Mario Carneiro, 12-Feb-2013.)
⊢ (𝐴 ∈ On → (cf‘suc 𝐴) = 1o)
Theorem	cff1 10295*	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 10296*	If there is a cofinal map from 𝐵 to 𝐴, then 𝐵 is at least (cf‘𝐴). This theorem and cff1 10295 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 10297*	Another expression for the cofinality function. (Contributed by Mario Carneiro, 28-Feb-2013.)
⊢ (𝐴 ∈ On → (cf‘𝐴) = ∩ 𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤} (card‘𝑥))
Theorem	coflim 10298*	A simpler expression for the cofinality predicate, at a limit ordinal. (Contributed by Mario Carneiro, 28-Feb-2013.)
⊢ ((Lim 𝐴 ∧ 𝐵 ⊆ 𝐴) → (∪ 𝐵 = 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦))
Theorem	cflim3 10299*	Another expression for the cofinality function. (Contributed by Mario Carneiro, 28-Feb-2013.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (Lim 𝐴 → (cf‘𝐴) = ∩ 𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} (card‘𝑥))
Theorem	cflim2 10300	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‘𝐴))