P. 93 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 9201-9300   *Has distinct variable group(s)

Type	Label	Description
Statement
2.6.10  Cardinal number arithmetic
Syntax	ccda 9201	Extend class definition to include cardinal number addition.
class +𝑐
Definition	df-cda 9202*	Define cardinal number addition. Definition of cardinal sum in [Mendelson] p. 258. See cdaval 9204 for its value and a description. (Contributed by NM, 24-Sep-2004.)
⊢ +𝑐 = (𝑥 ∈ V, 𝑦 ∈ V ↦ ((𝑥 × {∅}) ∪ (𝑦 × {1𝑜})))
Theorem	cdafn 9203	Cardinal number addition is a function. (Contributed by Mario Carneiro, 28-Apr-2015.)
⊢ +𝑐 Fn (V × V)
Theorem	cdaval 9204	Value of cardinal addition. Definition of cardinal sum in [Mendelson] p. 258. For cardinal arithmetic, we follow Mendelson. Rather than defining operations restricted to cardinal numbers, we use this disjoint union operation for addition, while Cartesian product and set exponentiation stand in for cardinal multiplication and exponentiation. Equinumerosity and dominance serve the roles of equality and ordering. If we wanted to, we could easily convert our theorems to actual cardinal number operations via carden 9585, carddom 9588, and cardsdom 9589. The advantage of Mendelson's approach is that we can directly use many equinumerosity theorems that we already have available. (Contributed by NM, 24-Sep-2004.) (Revised by Mario Carneiro, 15-Sep-2013.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 +𝑐 𝐵) = ((𝐴 × {∅}) ∪ (𝐵 × {1𝑜})))
Theorem	uncdadom 9205	Cardinal addition dominates union. (Contributed by NM, 28-Sep-2004.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ≼ (𝐴 +𝑐 𝐵))
Theorem	cdaun 9206	Cardinal addition is equinumerous to union for disjoint sets. (Contributed by NM, 5-Apr-2007.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐴 +𝑐 𝐵) ≈ (𝐴 ∪ 𝐵))
Theorem	cdaen 9207	Cardinal addition of equinumerous sets. Exercise 4.56(b) of [Mendelson] p. 258. (Contributed by NM, 28-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷) → (𝐴 +𝑐 𝐶) ≈ (𝐵 +𝑐 𝐷))
Theorem	cdaenun 9208	Cardinal addition is equinumerous to union for disjoint sets. (Contributed by Mario Carneiro, 29-Apr-2015.)
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷 ∧ (𝐵 ∩ 𝐷) = ∅) → (𝐴 +𝑐 𝐶) ≈ (𝐵 ∪ 𝐷))
Theorem	cda1en 9209	Cardinal addition with cardinal one (which is the same as ordinal one). Used in proof of Theorem 6J of [Enderton] p. 143. (Contributed by NM, 28-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ 𝐴) → (𝐴 +𝑐 1𝑜) ≈ suc 𝐴)
Theorem	cda1dif 9210	Adding and subtracting one gives back the original set. Similar to pncan 10499 for cardinalities. (Contributed by Mario Carneiro, 18-May-2015.)
⊢ (𝐵 ∈ (𝐴 +𝑐 1𝑜) → ((𝐴 +𝑐 1𝑜) ∖ {𝐵}) ≈ 𝐴)
Theorem	pm110.643 9211	1+1=2 for cardinal number addition, derived from pm54.43 9036 as promised. Theorem *110.643 of Principia Mathematica, vol. II, p. 86, which adds the remark, "The above proposition is occasionally useful." Whitehead and Russell define cardinal addition on collections of all sets equinumerous to 1 and 2 (which for us are proper classes unless we restrict them as in karden 8933), but after applying definitions, our theorem is equivalent. The comment for cdaval 9204 explains why we use ≈ instead of =. See pm110.643ALT 9212 for a shorter proof that doesn't use pm54.43 9036. (Contributed by NM, 5-Apr-2007.) (Proof modification is discouraged.)
⊢ (1𝑜 +𝑐 1𝑜) ≈ 2𝑜
Theorem	pm110.643ALT 9212	Alternate proof of pm110.643 9211. (Contributed by Mario Carneiro, 29-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (1𝑜 +𝑐 1𝑜) ≈ 2𝑜
Theorem	cda0en 9213	Cardinal addition with cardinal zero (the empty set). Part (a1) of proof of Theorem 6J of [Enderton] p. 143. (Contributed by NM, 27-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 +𝑐 ∅) ≈ 𝐴)
Theorem	xp2cda 9214	Two times a cardinal number. Exercise 4.56(g) of [Mendelson] p. 258. (Contributed by NM, 27-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 × 2𝑜) = (𝐴 +𝑐 𝐴))
Theorem	cdacomen 9215	Commutative law for cardinal addition. Exercise 4.56(c) of [Mendelson] p. 258. (Contributed by NM, 24-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
⊢ (𝐴 +𝑐 𝐵) ≈ (𝐵 +𝑐 𝐴)
Theorem	cdaassen 9216	Associative law for cardinal addition. Exercise 4.56(c) of [Mendelson] p. 258. (Contributed by NM, 26-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐴 +𝑐 𝐵) +𝑐 𝐶) ≈ (𝐴 +𝑐 (𝐵 +𝑐 𝐶)))
Theorem	xpcdaen 9217	Cardinal multiplication distributes over cardinal addition. Theorem 6I(3) of [Enderton] p. 142. (Contributed by NM, 26-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 × (𝐵 +𝑐 𝐶)) ≈ ((𝐴 × 𝐵) +𝑐 (𝐴 × 𝐶)))
Theorem	mapcdaen 9218	Sum of exponents law for cardinal arithmetic. Theorem 6I(4) of [Enderton] p. 142. (Contributed by NM, 27-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 ↑𝑚 (𝐵 +𝑐 𝐶)) ≈ ((𝐴 ↑𝑚 𝐵) × (𝐴 ↑𝑚 𝐶)))
Theorem	pwcdaen 9219	Sum of exponents law for cardinal arithmetic. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝒫 (𝐴 +𝑐 𝐵) ≈ (𝒫 𝐴 × 𝒫 𝐵))
Theorem	cdadom1 9220	Ordering law for cardinal addition. Exercise 4.56(f) of [Mendelson] p. 258. (Contributed by NM, 28-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
⊢ (𝐴 ≼ 𝐵 → (𝐴 +𝑐 𝐶) ≼ (𝐵 +𝑐 𝐶))
Theorem	cdadom2 9221	Ordering law for cardinal addition. Theorem 6L(a) of [Enderton] p. 149. (Contributed by NM, 28-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
⊢ (𝐴 ≼ 𝐵 → (𝐶 +𝑐 𝐴) ≼ (𝐶 +𝑐 𝐵))
Theorem	cdadom3 9222	A set is dominated by its cardinal sum with another. (Contributed by NM, 28-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐴 ≼ (𝐴 +𝑐 𝐵))
Theorem	cdaxpdom 9223	Cartesian product dominates disjoint union for sets with cardinality greater than 1. Similar to Proposition 10.36 of [TakeutiZaring] p. 93. (Contributed by Mario Carneiro, 18-May-2015.)
⊢ ((1𝑜 ≺ 𝐴 ∧ 1𝑜 ≺ 𝐵) → (𝐴 +𝑐 𝐵) ≼ (𝐴 × 𝐵))
Theorem	cdafi 9224	The cardinal sum of two finite sets is finite. (Contributed by NM, 22-Oct-2004.)
⊢ ((𝐴 ≺ ω ∧ 𝐵 ≺ ω) → (𝐴 +𝑐 𝐵) ≺ ω)
Theorem	cdainflem 9225	Any partition of omega into two pieces (which may be disjoint) contains an infinite subset. (Contributed by Mario Carneiro, 11-Feb-2013.)
⊢ ((𝐴 ∪ 𝐵) ≈ ω → (𝐴 ≈ ω ∨ 𝐵 ≈ ω))
Theorem	cdainf 9226	A set is infinite iff the cardinal sum with itself is infinite. (Contributed by NM, 22-Oct-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
⊢ (ω ≼ 𝐴 ↔ ω ≼ (𝐴 +𝑐 𝐴))
Theorem	infcda1 9227	An infinite set is equinumerous to itself added with one. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ (ω ≼ 𝐴 → (𝐴 +𝑐 1𝑜) ≈ 𝐴)
Theorem	pwcda1 9228	The sum of a powerset with itself is equipotent to the successor powerset. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ (𝐴 ∈ 𝑉 → (𝒫 𝐴 +𝑐 𝒫 𝐴) ≈ 𝒫 (𝐴 +𝑐 1𝑜))
Theorem	pwcdaidm 9229	If the natural numbers inject into 𝐴, then 𝒫 𝐴 is idempotent under cardinal sum. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ (ω ≼ 𝐴 → (𝒫 𝐴 +𝑐 𝒫 𝐴) ≈ 𝒫 𝐴)
Theorem	cdalepw 9230	If 𝐴 is idempotent under cardinal sum and 𝐵 is dominated by the power set of 𝐴, then so is the cardinal sum of 𝐴 and 𝐵. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ (((𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) → (𝐴 +𝑐 𝐵) ≼ 𝒫 𝐴)
Theorem	onacda 9231	The cardinal and ordinal sums are always equinumerous. (Contributed by Mario Carneiro, 6-Feb-2013.) (Revised by Mario Carneiro, 30-May-2015.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +𝑜 𝐵) ≈ (𝐴 +𝑐 𝐵))
Theorem	cardacda 9232	The cardinal sum is equinumerous to an ordinal sum of the cardinals. (Contributed by Mario Carneiro, 6-Feb-2013.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → (𝐴 +𝑐 𝐵) ≈ ((card‘𝐴) +𝑜 (card‘𝐵)))
Theorem	cdanum 9233	The cardinal sum of two numerable sets is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.)
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → (𝐴 +𝑐 𝐵) ∈ dom card)
Theorem	unnum 9234	The union of two numerable sets is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.)
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → (𝐴 ∪ 𝐵) ∈ dom card)
Theorem	nnacda 9235	The cardinal and ordinal sums of finite ordinals are equal. (Contributed by Paul Chapman, 11-Apr-2009.) (Revised by Mario Carneiro, 6-Feb-2013.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (card‘(𝐴 +𝑐 𝐵)) = (𝐴 +𝑜 𝐵))
Theorem	ficardun 9236	The cardinality of the union of disjoint, finite sets is the ordinal sum of their cardinalities. (Contributed by Paul Chapman, 5-Jun-2009.) (Proof shortened by Mario Carneiro, 28-Apr-2015.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ (𝐴 ∩ 𝐵) = ∅) → (card‘(𝐴 ∪ 𝐵)) = ((card‘𝐴) +𝑜 (card‘𝐵)))
Theorem	ficardun2 9237	The cardinality of the union of finite sets is at most the ordinal sum of their cardinalities. (Contributed by Mario Carneiro, 5-Feb-2013.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (card‘(𝐴 ∪ 𝐵)) ⊆ ((card‘𝐴) +𝑜 (card‘𝐵)))
Theorem	pwsdompw 9238*	Lemma for domtriom 9477. This is the equinumerosity version of the algebraic identity Σ𝑘 ∈ 𝑛(2↑𝑘) = (2↑𝑛) − 1. (Contributed by Mario Carneiro, 7-Feb-2013.)
⊢ ((𝑛 ∈ ω ∧ ∀𝑘 ∈ suc 𝑛(𝐵‘𝑘) ≈ 𝒫 𝑘) → ∪ 𝑘 ∈ 𝑛 (𝐵‘𝑘) ≺ (𝐵‘𝑛))
Theorem	unctb 9239	The union of two countable sets is countable. (Contributed by FL, 25-Aug-2006.) (Proof shortened by Mario Carneiro, 30-Apr-2015.)
⊢ ((𝐴 ≼ ω ∧ 𝐵 ≼ ω) → (𝐴 ∪ 𝐵) ≼ ω)
Theorem	infcdaabs 9240	Absorption law for addition to an infinite cardinal. (Contributed by NM, 30-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
⊢ ((𝐴 ∈ dom card ∧ ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴) → (𝐴 +𝑐 𝐵) ≈ 𝐴)
Theorem	infunabs 9241	An infinite set is equinumerous to its union with a smaller one. (Contributed by NM, 28-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
⊢ ((𝐴 ∈ dom card ∧ ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴) → (𝐴 ∪ 𝐵) ≈ 𝐴)
Theorem	infcda 9242	The sum of two cardinal numbers is their maximum, if one of them is infinite. Proposition 10.41 of [TakeutiZaring] p. 95. (Contributed by NM, 28-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ∧ ω ≼ 𝐴) → (𝐴 +𝑐 𝐵) ≈ (𝐴 ∪ 𝐵))
Theorem	infdif 9243	The cardinality of an infinite set does not change after subtracting a strictly smaller one. Example in [Enderton] p. 164. (Contributed by NM, 22-Oct-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
⊢ ((𝐴 ∈ dom card ∧ ω ≼ 𝐴 ∧ 𝐵 ≺ 𝐴) → (𝐴 ∖ 𝐵) ≈ 𝐴)
Theorem	infdif2 9244	Cardinality ordering for an infinite class difference. (Contributed by NM, 24-Mar-2007.) (Revised by Mario Carneiro, 29-Apr-2015.)
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ∧ ω ≼ 𝐴) → ((𝐴 ∖ 𝐵) ≼ 𝐵 ↔ 𝐴 ≼ 𝐵))
Theorem	infxpdom 9245	Dominance law for multiplication with an infinite cardinal. (Contributed by NM, 26-Mar-2006.) (Revised by Mario Carneiro, 29-Apr-2015.)
⊢ ((𝐴 ∈ dom card ∧ ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴) → (𝐴 × 𝐵) ≼ 𝐴)
Theorem	infxpabs 9246	Absorption law for multiplication with an infinite cardinal. (Contributed by NM, 30-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
⊢ (((𝐴 ∈ dom card ∧ ω ≼ 𝐴) ∧ (𝐵 ≠ ∅ ∧ 𝐵 ≼ 𝐴)) → (𝐴 × 𝐵) ≈ 𝐴)
Theorem	infunsdom1 9247	The union of two sets that are strictly dominated by the infinite set 𝑋 is also dominated by 𝑋. This version of infunsdom 9248 assumes additionally that 𝐴 is the smaller of the two. (Contributed by Mario Carneiro, 14-Dec-2013.) (Revised by Mario Carneiro, 3-May-2015.)
⊢ (((𝑋 ∈ dom card ∧ ω ≼ 𝑋) ∧ (𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝑋)) → (𝐴 ∪ 𝐵) ≺ 𝑋)
Theorem	infunsdom 9248	The union of two sets that are strictly dominated by the infinite set 𝑋 is also strictly dominated by 𝑋. (Contributed by Mario Carneiro, 3-May-2015.)
⊢ (((𝑋 ∈ dom card ∧ ω ≼ 𝑋) ∧ (𝐴 ≺ 𝑋 ∧ 𝐵 ≺ 𝑋)) → (𝐴 ∪ 𝐵) ≺ 𝑋)
Theorem	infxp 9249	Absorption law for multiplication with an infinite cardinal. Equivalent to Proposition 10.41 of [TakeutiZaring] p. 95. (Contributed by NM, 28-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
⊢ (((𝐴 ∈ dom card ∧ ω ≼ 𝐴) ∧ (𝐵 ∈ dom card ∧ 𝐵 ≠ ∅)) → (𝐴 × 𝐵) ≈ (𝐴 ∪ 𝐵))
Theorem	pwcdadom 9250	A property of dominance over a powerset, and a main lemma for gchac 9715. Similar to Lemma 2.3 of [KanamoriPincus] p. 420. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ (𝒫 (𝐴 +𝑐 𝐴) ≼ (𝐴 +𝑐 𝐵) → 𝒫 𝐴 ≼ 𝐵)
Theorem	infpss 9251*	Every infinite set has an equinumerous proper subset, proved without AC or Infinity. Exercise 7 of [TakeutiZaring] p. 91. See also infpssALT 9347. (Contributed by NM, 23-Oct-2004.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ (ω ≼ 𝐴 → ∃𝑥(𝑥 ⊊ 𝐴 ∧ 𝑥 ≈ 𝐴))
Theorem	infmap2 9252*	An exponentiation law for infinite cardinals. Similar to Lemma 6.2 of [Jech] p. 43. Although this version of infmap 9610 avoids the axiom of choice, it requires the powerset of an infinite set to be well-orderable and so is usually not applicable. (Contributed by NM, 1-Oct-2004.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ ((ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ∧ (𝐴 ↑𝑚 𝐵) ∈ dom card) → (𝐴 ↑𝑚 𝐵) ≈ {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐵)})
2.6.11  The Ackermann bijection
Theorem	ackbij2lem1 9253	Lemma for ackbij2 9277. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ (𝐴 ∈ ω → 𝒫 𝐴 ⊆ (𝒫 ω ∩ Fin))
Theorem	ackbij1lem1 9254	Lemma for ackbij2 9277. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ (¬ 𝐴 ∈ 𝐵 → (𝐵 ∩ suc 𝐴) = (𝐵 ∩ 𝐴))
Theorem	ackbij1lem2 9255	Lemma for ackbij2 9277. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ (𝐴 ∈ 𝐵 → (𝐵 ∩ suc 𝐴) = ({𝐴} ∪ (𝐵 ∩ 𝐴)))
Theorem	ackbij1lem3 9256	Lemma for ackbij2 9277. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ (𝐴 ∈ ω → 𝐴 ∈ (𝒫 ω ∩ Fin))
Theorem	ackbij1lem4 9257	Lemma for ackbij2 9277. (Contributed by Stefan O'Rear, 19-Nov-2014.)
⊢ (𝐴 ∈ ω → {𝐴} ∈ (𝒫 ω ∩ Fin))
Theorem	ackbij1lem5 9258	Lemma for ackbij2 9277. (Contributed by Stefan O'Rear, 19-Nov-2014.)
⊢ (𝐴 ∈ ω → (card‘𝒫 suc 𝐴) = ((card‘𝒫 𝐴) +𝑜 (card‘𝒫 𝐴)))
Theorem	ackbij1lem6 9259	Lemma for ackbij2 9277. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → (𝐴 ∪ 𝐵) ∈ (𝒫 ω ∩ Fin))
Theorem	ackbij1lem7 9260*	Lemma for ackbij1 9272. (Contributed by Stefan O'Rear, 21-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → (𝐹‘𝐴) = (card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)))
Theorem	ackbij1lem8 9261*	Lemma for ackbij1 9272. (Contributed by Stefan O'Rear, 19-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ (𝐴 ∈ ω → (𝐹‘{𝐴}) = (card‘𝒫 𝐴))
Theorem	ackbij1lem9 9262*	Lemma for ackbij1 9272. (Contributed by Stefan O'Rear, 19-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐹‘(𝐴 ∪ 𝐵)) = ((𝐹‘𝐴) +𝑜 (𝐹‘𝐵)))
Theorem	ackbij1lem10 9263*	Lemma for ackbij1 9272. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ 𝐹:(𝒫 ω ∩ Fin)⟶ω
Theorem	ackbij1lem11 9264*	Lemma for ackbij1 9272. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ (𝒫 ω ∩ Fin))
Theorem	ackbij1lem12 9265*	Lemma for ackbij1 9272. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ ((𝐵 ∈ (𝒫 ω ∩ Fin) ∧ 𝐴 ⊆ 𝐵) → (𝐹‘𝐴) ⊆ (𝐹‘𝐵))
Theorem	ackbij1lem13 9266*	Lemma for ackbij1 9272. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ (𝐹‘∅) = ∅
Theorem	ackbij1lem14 9267*	Lemma for ackbij1 9272. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ (𝐴 ∈ ω → (𝐹‘{𝐴}) = suc (𝐹‘𝐴))
Theorem	ackbij1lem15 9268*	Lemma for ackbij1 9272. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ (((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝑐 ∈ ω ∧ 𝑐 ∈ 𝐴 ∧ ¬ 𝑐 ∈ 𝐵)) → ¬ (𝐹‘(𝐴 ∩ suc 𝑐)) = (𝐹‘(𝐵 ∩ suc 𝑐)))
Theorem	ackbij1lem16 9269*	Lemma for ackbij1 9272. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘𝐴) = (𝐹‘𝐵) → 𝐴 = 𝐵))
Theorem	ackbij1lem17 9270*	Lemma for ackbij1 9272. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ 𝐹:(𝒫 ω ∩ Fin)–1-1→ω
Theorem	ackbij1lem18 9271*	Lemma for ackbij1 9272. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → ∃𝑏 ∈ (𝒫 ω ∩ Fin)(𝐹‘𝑏) = suc (𝐹‘𝐴))
Theorem	ackbij1 9272*	The Ackermann bijection, part 1: each natural number can be uniquely coded in binary as a finite set of natural numbers and conversely. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ 𝐹:(𝒫 ω ∩ Fin)–1-1-onto→ω
Theorem	ackbij1b 9273*	The Ackermann bijection, part 1b: the bijection from ackbij1 9272 restricts naturally to the powers of particular naturals. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ (𝐴 ∈ ω → (𝐹 “ 𝒫 𝐴) = (card‘𝒫 𝐴))
Theorem	ackbij2lem2 9274*	Lemma for ackbij2 9277. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    &   ⊢ 𝐺 = (𝑥 ∈ V ↦ (𝑦 ∈ 𝒫 dom 𝑥 ↦ (𝐹‘(𝑥 “ 𝑦))))    ⇒   ⊢ (𝐴 ∈ ω → (rec(𝐺, ∅)‘𝐴):(𝑅1‘𝐴)–1-1-onto→(card‘(𝑅1‘𝐴)))
Theorem	ackbij2lem3 9275*	Lemma for ackbij2 9277. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    &   ⊢ 𝐺 = (𝑥 ∈ V ↦ (𝑦 ∈ 𝒫 dom 𝑥 ↦ (𝐹‘(𝑥 “ 𝑦))))    ⇒   ⊢ (𝐴 ∈ ω → (rec(𝐺, ∅)‘𝐴) ⊆ (rec(𝐺, ∅)‘suc 𝐴))
Theorem	ackbij2lem4 9276*	Lemma for ackbij2 9277. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    &   ⊢ 𝐺 = (𝑥 ∈ V ↦ (𝑦 ∈ 𝒫 dom 𝑥 ↦ (𝐹‘(𝑥 “ 𝑦))))    ⇒   ⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐵 ⊆ 𝐴) → (rec(𝐺, ∅)‘𝐵) ⊆ (rec(𝐺, ∅)‘𝐴))
Theorem	ackbij2 9277*	The Ackermann bijection, part 2: hereditarily finite sets can be represented by recursive binary notation. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    &   ⊢ 𝐺 = (𝑥 ∈ V ↦ (𝑦 ∈ 𝒫 dom 𝑥 ↦ (𝐹‘(𝑥 “ 𝑦))))    &   ⊢ 𝐻 = ∪ (rec(𝐺, ∅) “ ω)    ⇒   ⊢ 𝐻:∪ (𝑅1 “ ω)–1-1-onto→ω
Theorem	r1om 9278	The set of hereditarily finite sets is countable. See ackbij2 9277 for an explicit bijection that works without Infinity. See also r1omALT 9810. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ (𝑅1‘ω) ≈ ω
Theorem	fictb 9279	A set is countable iff its collection of finite intersections is countable. (Contributed by Jeff Hankins, 24-Aug-2009.) (Proof shortened by Mario Carneiro, 17-May-2015.)
⊢ (𝐴 ∈ 𝐵 → (𝐴 ≼ ω ↔ (fi‘𝐴) ≼ ω))
2.6.12  Cofinality (without Axiom of Choice)
Theorem	cflem 9280*	A lemma used to simplify cofinality computations, showing the existence of the cardinal of an unbounded subset of a set 𝐴. (Contributed by NM, 24-Apr-2004.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)))
Theorem	cfval 9281*	Value of the cofinality function. Definition B of Saharon Shelah, Cardinal Arithmetic (1994), p. xxx (Roman numeral 30). The cofinality of an ordinal number 𝐴 is the cardinality (size) of the smallest unbounded subset 𝑦 of the ordinal number. Unbounded means that for every member of 𝐴, there is a member of 𝑦 that is at least as large. Cofinality is a measure of how "reachable from below" an ordinal is. (Contributed by NM, 1-Apr-2004.) (Revised by Mario Carneiro, 15-Sep-2013.)
⊢ (𝐴 ∈ On → (cf‘𝐴) = ∩ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))})
Theorem	cff 9282	Cofinality is a function on the class of ordinal numbers to the class of cardinal numbers. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ cf:On⟶On
Theorem	cfub 9283*	An upper bound on cofinality. (Contributed by NM, 25-Apr-2004.) (Revised by Mario Carneiro, 15-Sep-2013.)
⊢ (cf‘𝐴) ⊆ ∩ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ ∪ 𝑦))}
Theorem	cflm 9284*	Value of the cofinality function at a limit ordinal. Part of Definition of cofinality of [Enderton] p. 257. (Contributed by NM, 26-Apr-2004.)
⊢ ((𝐴 ∈ 𝐵 ∧ Lim 𝐴) → (cf‘𝐴) = ∩ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))})
Theorem	cf0 9285	Value of the cofinality function at 0. Exercise 2 of [TakeutiZaring] p. 102. (Contributed by NM, 16-Apr-2004.)
⊢ (cf‘∅) = ∅
Theorem	cardcf 9286	Cofinality is a cardinal number. Proposition 11.11 of [TakeutiZaring] p. 103. (Contributed by NM, 24-Apr-2004.) (Revised by Mario Carneiro, 15-Sep-2013.)
⊢ (card‘(cf‘𝐴)) = (cf‘𝐴)
Theorem	cflecard 9287	Cofinality is bounded by the cardinality of its argument. (Contributed by NM, 24-Apr-2004.) (Revised by Mario Carneiro, 15-Sep-2013.)
⊢ (cf‘𝐴) ⊆ (card‘𝐴)
Theorem	cfle 9288	Cofinality is bounded by its argument. Exercise 1 of [TakeutiZaring] p. 102. (Contributed by NM, 26-Apr-2004.) (Revised by Mario Carneiro, 15-Sep-2013.)
⊢ (cf‘𝐴) ⊆ 𝐴
Theorem	cfon 9289	The cofinality of any set is an ordinal (although it only makes sense when 𝐴 is an ordinal). (Contributed by Mario Carneiro, 9-Mar-2013.)
⊢ (cf‘𝐴) ∈ On
Theorem	cfeq0 9290	Only the ordinal zero has cofinality zero. (Contributed by NM, 24-Apr-2004.) (Revised by Mario Carneiro, 12-Feb-2013.)
⊢ (𝐴 ∈ On → ((cf‘𝐴) = ∅ ↔ 𝐴 = ∅))
Theorem	cfsuc 9291	Value of the cofinality function at a successor ordinal. Exercise 3 of [TakeutiZaring] p. 102. (Contributed by NM, 23-Apr-2004.) (Revised by Mario Carneiro, 12-Feb-2013.)
⊢ (𝐴 ∈ On → (cf‘suc 𝐴) = 1𝑜)
Theorem	cff1 9292*	There is always a map from (cf‘𝐴) to 𝐴 (this is a stronger condition than the definition, which only presupposes a map from some 𝑦 ≈ (cf‘𝐴). (Contributed by Mario Carneiro, 28-Feb-2013.)
⊢ (𝐴 ∈ On → ∃𝑓(𝑓:(cf‘𝐴)–1-1→𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓‘𝑤)))
Theorem	cfflb 9293*	If there is a cofinal map from 𝐵 to 𝐴, then 𝐵 is at least (cf‘𝐴). This theorem and cff1 9292 motivate the picture of (cf‘𝐴) as the greatest lower bound of the domain of cofinal maps into 𝐴. (Contributed by Mario Carneiro, 28-Feb-2013.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∃𝑓(𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) → (cf‘𝐴) ⊆ 𝐵))
Theorem	cfval2 9294*	Another expression for the cofinality function. (Contributed by Mario Carneiro, 28-Feb-2013.)
⊢ (𝐴 ∈ On → (cf‘𝐴) = ∩ 𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤} (card‘𝑥))
Theorem	coflim 9295*	A simpler expression for the cofinality predicate, at a limit ordinal. (Contributed by Mario Carneiro, 28-Feb-2013.)
⊢ ((Lim 𝐴 ∧ 𝐵 ⊆ 𝐴) → (∪ 𝐵 = 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦))
Theorem	cflim3 9296*	Another expression for the cofinality function. (Contributed by Mario Carneiro, 28-Feb-2013.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (Lim 𝐴 → (cf‘𝐴) = ∩ 𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} (card‘𝑥))
Theorem	cflim2 9297	The cofinality function is a limit ordinal iff its argument is. (Contributed by Mario Carneiro, 28-Feb-2013.) (Revised by Mario Carneiro, 15-Sep-2013.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (Lim 𝐴 ↔ Lim (cf‘𝐴))
Theorem	cfom 9298	Value of the cofinality function at omega (the set of natural numbers). Exercise 4 of [TakeutiZaring] p. 102. (Contributed by NM, 23-Apr-2004.) (Proof shortened by Mario Carneiro, 11-Jun-2015.)
⊢ (cf‘ω) = ω
Theorem	cfss 9299*	There is a cofinal subset of 𝐴 of cardinality (cf‘𝐴). (Contributed by Mario Carneiro, 24-Jun-2013.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (Lim 𝐴 → ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ (cf‘𝐴) ∧ ∪ 𝑥 = 𝐴))
Theorem	cfslb 9300	Any cofinal subset of 𝐴 is at least as large as (cf‘𝐴). (Contributed by Mario Carneiro, 24-Jun-2013.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ((Lim 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ ∪ 𝐵 = 𝐴) → (cf‘𝐴) ≼ 𝐵)