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	infdif2 10201	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 10202	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 10203	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 10204	The union of two sets that are strictly dominated by the infinite set 𝑋 is also dominated by 𝑋. This version of infunsdom 10205 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 10205	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 10206	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 10207	A property of dominance over a powerset, and a main lemma for gchac 10672. Similar to Lemma 2.3 of [KanamoriPincus] p. 420. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ (𝒫 (𝐴 ⊔ 𝐴) ≼ (𝐴 ⊔ 𝐵) → 𝒫 𝐴 ≼ 𝐵)
Theorem	infpss 10208*	Every infinite set has an equinumerous proper subset, proved without AC or Infinity. Exercise 7 of [TakeutiZaring] p. 91. See also infpssALT 10304. (Contributed by NM, 23-Oct-2004.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ (ω ≼ 𝐴 → ∃𝑥(𝑥 ⊊ 𝐴 ∧ 𝑥 ≈ 𝐴))
Theorem	infmap2 10209*	An exponentiation law for infinite cardinals. Similar to Lemma 6.2 of [Jech] p. 43. Although this version of infmap 10567 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 10210	Lemma for ackbij2 10234. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ (𝐴 ∈ ω → 𝒫 𝐴 ⊆ (𝒫 ω ∩ Fin))
Theorem	ackbij1lem1 10211	Lemma for ackbij2 10234. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ (¬ 𝐴 ∈ 𝐵 → (𝐵 ∩ suc 𝐴) = (𝐵 ∩ 𝐴))
Theorem	ackbij1lem2 10212	Lemma for ackbij2 10234. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ (𝐴 ∈ 𝐵 → (𝐵 ∩ suc 𝐴) = ({𝐴} ∪ (𝐵 ∩ 𝐴)))
Theorem	ackbij1lem3 10213	Lemma for ackbij2 10234. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ (𝐴 ∈ ω → 𝐴 ∈ (𝒫 ω ∩ Fin))
Theorem	ackbij1lem4 10214	Lemma for ackbij2 10234. (Contributed by Stefan O'Rear, 19-Nov-2014.)
⊢ (𝐴 ∈ ω → {𝐴} ∈ (𝒫 ω ∩ Fin))
Theorem	ackbij1lem5 10215	Lemma for ackbij2 10234. (Contributed by Stefan O'Rear, 19-Nov-2014.) (Proof shortened by AV, 18-Jul-2022.)
⊢ (𝐴 ∈ ω → (card‘𝒫 suc 𝐴) = ((card‘𝒫 𝐴) +o (card‘𝒫 𝐴)))
Theorem	ackbij1lem6 10216	Lemma for ackbij2 10234. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → (𝐴 ∪ 𝐵) ∈ (𝒫 ω ∩ Fin))
Theorem	ackbij1lem7 10217*	Lemma for ackbij1 10229. (Contributed by Stefan O'Rear, 21-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → (𝐹‘𝐴) = (card‘∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝒫 𝑦)))
Theorem	ackbij1lem8 10218*	Lemma for ackbij1 10229. (Contributed by Stefan O'Rear, 19-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ (𝐴 ∈ ω → (𝐹‘{𝐴}) = (card‘𝒫 𝐴))
Theorem	ackbij1lem9 10219*	Lemma for ackbij1 10229. (Contributed by Stefan O'Rear, 19-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐹‘(𝐴 ∪ 𝐵)) = ((𝐹‘𝐴) +o (𝐹‘𝐵)))
Theorem	ackbij1lem10 10220*	Lemma for ackbij1 10229. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ 𝐹:(𝒫 ω ∩ Fin)⟶ω
Theorem	ackbij1lem11 10221*	Lemma for ackbij1 10229. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ (𝒫 ω ∩ Fin))
Theorem	ackbij1lem12 10222*	Lemma for ackbij1 10229. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ ((𝐵 ∈ (𝒫 ω ∩ Fin) ∧ 𝐴 ⊆ 𝐵) → (𝐹‘𝐴) ⊆ (𝐹‘𝐵))
Theorem	ackbij1lem13 10223*	Lemma for ackbij1 10229. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ (𝐹‘∅) = ∅
Theorem	ackbij1lem14 10224*	Lemma for ackbij1 10229. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ (𝐴 ∈ ω → (𝐹‘{𝐴}) = suc (𝐹‘𝐴))
Theorem	ackbij1lem15 10225*	Lemma for ackbij1 10229. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ (((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) ∧ (𝑐 ∈ ω ∧ 𝑐 ∈ 𝐴 ∧ ¬ 𝑐 ∈ 𝐵)) → ¬ (𝐹‘(𝐴 ∩ suc 𝑐)) = (𝐹‘(𝐵 ∩ suc 𝑐)))
Theorem	ackbij1lem16 10226*	Lemma for ackbij1 10229. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ ((𝐴 ∈ (𝒫 ω ∩ Fin) ∧ 𝐵 ∈ (𝒫 ω ∩ Fin)) → ((𝐹‘𝐴) = (𝐹‘𝐵) → 𝐴 = 𝐵))
Theorem	ackbij1lem17 10227*	Lemma for ackbij1 10229. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ 𝐹:(𝒫 ω ∩ Fin)–1-1→ω
Theorem	ackbij1lem18 10228*	Lemma for ackbij1 10229. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ (𝐴 ∈ (𝒫 ω ∩ Fin) → ∃𝑏 ∈ (𝒫 ω ∩ Fin)(𝐹‘𝑏) = suc (𝐹‘𝐴))
Theorem	ackbij1 10229*	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 10230*	The Ackermann bijection, part 1b: the bijection from ackbij1 10229 restricts naturally to the powers of particular naturals. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    ⇒   ⊢ (𝐴 ∈ ω → (𝐹 “ 𝒫 𝐴) = (card‘𝒫 𝐴))
Theorem	ackbij2lem2 10231*	Lemma for ackbij2 10234. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    &   ⊢ 𝐺 = (𝑥 ∈ V ↦ (𝑦 ∈ 𝒫 dom 𝑥 ↦ (𝐹‘(𝑥 “ 𝑦))))    ⇒   ⊢ (𝐴 ∈ ω → (rec(𝐺, ∅)‘𝐴):(𝑅1‘𝐴)–1-1-onto→(card‘(𝑅1‘𝐴)))
Theorem	ackbij2lem3 10232*	Lemma for ackbij2 10234. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    &   ⊢ 𝐺 = (𝑥 ∈ V ↦ (𝑦 ∈ 𝒫 dom 𝑥 ↦ (𝐹‘(𝑥 “ 𝑦))))    ⇒   ⊢ (𝐴 ∈ ω → (rec(𝐺, ∅)‘𝐴) ⊆ (rec(𝐺, ∅)‘suc 𝐴))
Theorem	ackbij2lem4 10233*	Lemma for ackbij2 10234. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝒫 ω ∩ Fin) ↦ (card‘∪ 𝑦 ∈ 𝑥 ({𝑦} × 𝒫 𝑦)))    &   ⊢ 𝐺 = (𝑥 ∈ V ↦ (𝑦 ∈ 𝒫 dom 𝑥 ↦ (𝐹‘(𝑥 “ 𝑦))))    ⇒   ⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐵 ⊆ 𝐴) → (rec(𝐺, ∅)‘𝐵) ⊆ (rec(𝐺, ∅)‘𝐴))
Theorem	ackbij2 10234*	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 10235	The set of hereditarily finite sets is countable. See ackbij2 10234 for an explicit bijection that works without Infinity. See also r1omALT 10767. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ (𝑅1‘ω) ≈ ω
Theorem	fictb 10236	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 10237*	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 10238*	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 10239	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 10240*	An upper bound on cofinality. (Contributed by NM, 25-Apr-2004.) (Revised by Mario Carneiro, 15-Sep-2013.)
⊢ (cf‘𝐴) ⊆ ∩ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ ∪ 𝑦))}
Theorem	cflm 10241*	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 10242	Value of the cofinality function at 0. Exercise 2 of [TakeutiZaring] p. 102. (Contributed by NM, 16-Apr-2004.)
⊢ (cf‘∅) = ∅
Theorem	cardcf 10243	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 10244	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 10245	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 10246	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 10247	Only the ordinal zero has cofinality zero. (Contributed by NM, 24-Apr-2004.) (Revised by Mario Carneiro, 12-Feb-2013.)
⊢ (𝐴 ∈ On → ((cf‘𝐴) = ∅ ↔ 𝐴 = ∅))
Theorem	cfsuc 10248	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 10249*	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 10250*	If there is a cofinal map from 𝐵 to 𝐴, then 𝐵 is at least (cf‘𝐴). This theorem and cff1 10249 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 10251*	Another expression for the cofinality function. (Contributed by Mario Carneiro, 28-Feb-2013.)
⊢ (𝐴 ∈ On → (cf‘𝐴) = ∩ 𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤} (card‘𝑥))
Theorem	coflim 10252*	A simpler expression for the cofinality predicate, at a limit ordinal. (Contributed by Mario Carneiro, 28-Feb-2013.)
⊢ ((Lim 𝐴 ∧ 𝐵 ⊆ 𝐴) → (∪ 𝐵 = 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦))
Theorem	cflim3 10253*	Another expression for the cofinality function. (Contributed by Mario Carneiro, 28-Feb-2013.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (Lim 𝐴 → (cf‘𝐴) = ∩ 𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} (card‘𝑥))
Theorem	cflim2 10254	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 10255	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 10256*	There is a cofinal subset of 𝐴 of cardinality (cf‘𝐴). (Contributed by Mario Carneiro, 24-Jun-2013.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (Lim 𝐴 → ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ (cf‘𝐴) ∧ ∪ 𝑥 = 𝐴))
Theorem	cfslb 10257	Any cofinal subset of 𝐴 is at least as large as (cf‘𝐴). (Contributed by Mario Carneiro, 24-Jun-2013.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ((Lim 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ ∪ 𝐵 = 𝐴) → (cf‘𝐴) ≼ 𝐵)
Theorem	cfslbn 10258	Any subset of 𝐴 smaller than its cofinality has union less than 𝐴. (This is the contrapositive to cfslb 10257.) (Contributed by Mario Carneiro, 24-Jun-2013.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ((Lim 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≺ (cf‘𝐴)) → ∪ 𝐵 ∈ 𝐴)
Theorem	cfslb2n 10259*	Any small collection of small subsets of 𝐴 cannot have union 𝐴, where "small" means smaller than the cofinality. This is a stronger version of cfslb 10257. This is a common application of cofinality: under AC, (ℵ‘1) is regular, so it is not a countable union of countable sets. (Contributed by Mario Carneiro, 24-Jun-2013.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ((Lim 𝐴 ∧ ∀𝑥 ∈ 𝐵 (𝑥 ⊆ 𝐴 ∧ 𝑥 ≺ (cf‘𝐴))) → (𝐵 ≺ (cf‘𝐴) → ∪ 𝐵 ≠ 𝐴))
Theorem	cofsmo 10260*	Any cofinal map implies the existence of a strictly monotone cofinal map with a domain no larger than the original. Proposition 11.7 of [TakeutiZaring] p. 101. (Contributed by Mario Carneiro, 20-Mar-2013.)
⊢ 𝐶 = {𝑦 ∈ 𝐵 ∣ ∀𝑤 ∈ 𝑦 (𝑓‘𝑤) ∈ (𝑓‘𝑦)}    &   ⊢ 𝐾 = ∩ {𝑥 ∈ 𝐵 ∣ 𝑧 ⊆ (𝑓‘𝑥)}    &   ⊢ 𝑂 = OrdIso( E , 𝐶)    ⇒   ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ On) → (∃𝑓(𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) → ∃𝑥 ∈ suc 𝐵∃𝑔(𝑔:𝑥⟶𝐴 ∧ Smo 𝑔 ∧ ∀𝑧 ∈ 𝐴 ∃𝑣 ∈ 𝑥 𝑧 ⊆ (𝑔‘𝑣))))
Theorem	cfsmolem 10261*	Lemma for cfsmo 10262. (Contributed by Mario Carneiro, 28-Feb-2013.)
⊢ 𝐹 = (𝑧 ∈ V ↦ ((𝑔‘dom 𝑧) ∪ ∪ 𝑡 ∈ dom 𝑧 suc (𝑧‘𝑡)))    &   ⊢ 𝐺 = (recs(𝐹) ↾ (cf‘𝐴))    ⇒   ⊢ (𝐴 ∈ On → ∃𝑓(𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓‘𝑤)))
Theorem	cfsmo 10262*	The map in cff1 10249 can be assumed to be a strictly monotone ordinal function without loss of generality. (Contributed by Mario Carneiro, 28-Feb-2013.)
⊢ (𝐴 ∈ On → ∃𝑓(𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓‘𝑤)))
Theorem	cfcoflem 10263*	Lemma for cfcof 10265, showing subset relation in one direction. (Contributed by Mario Carneiro, 9-Mar-2013.) (Revised by Mario Carneiro, 26-Dec-2014.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∃𝑓(𝑓:𝐵⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ (𝑓‘𝑦)) → (cf‘𝐴) ⊆ (cf‘𝐵)))
Theorem	coftr 10264*	If there is a cofinal map from 𝐵 to 𝐴 and another from 𝐶 to 𝐴, then there is also a cofinal map from 𝐶 to 𝐵. Proposition 11.9 of [TakeutiZaring] p. 102. A limited form of transitivity for the "cof" relation. This is really a lemma for cfcof 10265. (Contributed by Mario Carneiro, 16-Mar-2013.)
⊢ 𝐻 = (𝑡 ∈ 𝐶 ↦ ∩ {𝑛 ∈ 𝐵 ∣ (𝑔‘𝑡) ⊆ (𝑓‘𝑛)})    ⇒   ⊢ (∃𝑓(𝑓:𝐵⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ (𝑓‘𝑦)) → (∃𝑔(𝑔:𝐶⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐶 𝑧 ⊆ (𝑔‘𝑤)) → ∃ℎ(ℎ:𝐶⟶𝐵 ∧ ∀𝑠 ∈ 𝐵 ∃𝑤 ∈ 𝐶 𝑠 ⊆ (ℎ‘𝑤))))
Theorem	cfcof 10265*	If there is a cofinal map from 𝐴 to 𝐵, then they have the same cofinality. This was used as Definition 11.1 of [TakeutiZaring] p. 100, who defines an equivalence relation cof (𝐴, 𝐵) and defines our cf(𝐵) as the minimum 𝐵 such that cof (𝐴, 𝐵). (Contributed by Mario Carneiro, 20-Mar-2013.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∃𝑓(𝑓:𝐵⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) → (cf‘𝐴) = (cf‘𝐵)))
Theorem	cfidm 10266	The cofinality function is idempotent. (Contributed by Mario Carneiro, 7-Mar-2013.) (Revised by Mario Carneiro, 15-Sep-2013.)
⊢ (cf‘(cf‘𝐴)) = (cf‘𝐴)
Theorem	alephsing 10267	The cofinality of a limit aleph is the same as the cofinality of its argument, so if (ℵ‘𝐴) < 𝐴, then (ℵ‘𝐴) is singular. Conversely, if (ℵ‘𝐴) is regular (i.e. weakly inaccessible), then (ℵ‘𝐴) = 𝐴, so 𝐴 has to be rather large (see alephfp 10099). Proposition 11.13 of [TakeutiZaring] p. 103. (Contributed by Mario Carneiro, 9-Mar-2013.)
⊢ (Lim 𝐴 → (cf‘(ℵ‘𝐴)) = (cf‘𝐴))
2.6.16  Eight inequivalent definitions of finite set
Theorem	sornom 10268*	The range of a single-step monotone function from ω into a partially ordered set is a chain. (Contributed by Stefan O'Rear, 3-Nov-2014.)
⊢ ((𝐹 Fn ω ∧ ∀𝑎 ∈ ω ((𝐹‘𝑎)𝑅(𝐹‘suc 𝑎) ∨ (𝐹‘𝑎) = (𝐹‘suc 𝑎)) ∧ 𝑅 Po ran 𝐹) → 𝑅 Or ran 𝐹)
Syntax	cfin1a 10269	Extend class notation to include the class of Ia-finite sets.
class FinIa
Syntax	cfin2 10270	Extend class notation to include the class of II-finite sets.
class FinII
Syntax	cfin4 10271	Extend class notation to include the class of IV-finite sets.
class FinIV
Syntax	cfin3 10272	Extend class notation to include the class of III-finite sets.
class FinIII
Syntax	cfin5 10273	Extend class notation to include the class of V-finite sets.
class FinV
Syntax	cfin6 10274	Extend class notation to include the class of VI-finite sets.
class FinVI
Syntax	cfin7 10275	Extend class notation to include the class of VII-finite sets.
class FinVII
Definition	df-fin1a 10276*	A set is Ia-finite iff it is not the union of two I-infinite sets. Equivalent to definition Ia of [Levy58] p. 2. A I-infinite Ia-finite set is also known as an amorphous set. This is the second of Levy's eight definitions of finite set. Levy's I-finite is equivalent to our df-fin 8939 and not repeated here. These eight definitions are equivalent with Choice but strictly decreasing in strength in models where Choice fails; conversely, they provide a series of increasingly stronger notions of infiniteness. (Contributed by Stefan O'Rear, 12-Nov-2014.)
⊢ FinIa = {𝑥 ∣ ∀𝑦 ∈ 𝒫 𝑥(𝑦 ∈ Fin ∨ (𝑥 ∖ 𝑦) ∈ Fin)}
Definition	df-fin2 10277*	A set is II-finite (Tarski finite) iff every nonempty chain of subsets contains a maximum element. Definition II of [Levy58] p. 2. (Contributed by Stefan O'Rear, 12-Nov-2014.)
⊢ FinII = {𝑥 ∣ ∀𝑦 ∈ 𝒫 𝒫 𝑥((𝑦 ≠ ∅ ∧ [⊊] Or 𝑦) → ∪ 𝑦 ∈ 𝑦)}
Definition	df-fin4 10278*	A set is IV-finite (Dedekind finite) iff it has no equinumerous proper subset. Definition IV of [Levy58] p. 3. (Contributed by Stefan O'Rear, 12-Nov-2014.)
⊢ FinIV = {𝑥 ∣ ¬ ∃𝑦(𝑦 ⊊ 𝑥 ∧ 𝑦 ≈ 𝑥)}
Definition	df-fin3 10279	A set is III-finite (weakly Dedekind finite) iff its power set is Dedekind finite. Definition III of [Levy58] p. 2. (Contributed by Stefan O'Rear, 12-Nov-2014.)
⊢ FinIII = {𝑥 ∣ 𝒫 𝑥 ∈ FinIV}
Definition	df-fin5 10280	A set is V-finite iff it behaves finitely under ⊔. Definition V of [Levy58] p. 3. (Contributed by Stefan O'Rear, 12-Nov-2014.)
⊢ FinV = {𝑥 ∣ (𝑥 = ∅ ∨ 𝑥 ≺ (𝑥 ⊔ 𝑥))}
Definition	df-fin6 10281	A set is VI-finite iff it behaves finitely under ×. Definition VI of [Levy58] p. 4. (Contributed by Stefan O'Rear, 12-Nov-2014.)
⊢ FinVI = {𝑥 ∣ (𝑥 ≺ 2o ∨ 𝑥 ≺ (𝑥 × 𝑥))}
Definition	df-fin7 10282*	A set is VII-finite iff it cannot be infinitely well-ordered. Equivalent to definition VII of [Levy58] p. 4. (Contributed by Stefan O'Rear, 12-Nov-2014.)
⊢ FinVII = {𝑥 ∣ ¬ ∃𝑦 ∈ (On ∖ ω)𝑥 ≈ 𝑦}
Theorem	isfin1a 10283*	Definition of a Ia-finite set. (Contributed by Stefan O'Rear, 16-May-2015.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ FinIa ↔ ∀𝑦 ∈ 𝒫 𝐴(𝑦 ∈ Fin ∨ (𝐴 ∖ 𝑦) ∈ Fin)))
Theorem	fin1ai 10284	Property of a Ia-finite set. (Contributed by Stefan O'Rear, 16-May-2015.)
⊢ ((𝐴 ∈ FinIa ∧ 𝑋 ⊆ 𝐴) → (𝑋 ∈ Fin ∨ (𝐴 ∖ 𝑋) ∈ Fin))
Theorem	isfin2 10285*	Definition of a II-finite set. (Contributed by Stefan O'Rear, 16-May-2015.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ FinII ↔ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [⊊] Or 𝑦) → ∪ 𝑦 ∈ 𝑦)))
Theorem	fin2i 10286	Property of a II-finite set. (Contributed by Stefan O'Rear, 16-May-2015.)
⊢ (((𝐴 ∈ FinII ∧ 𝐵 ⊆ 𝒫 𝐴) ∧ (𝐵 ≠ ∅ ∧ [⊊] Or 𝐵)) → ∪ 𝐵 ∈ 𝐵)
Theorem	isfin3 10287	Definition of a III-finite set. (Contributed by Stefan O'Rear, 16-May-2015.)
⊢ (𝐴 ∈ FinIII ↔ 𝒫 𝐴 ∈ FinIV)
Theorem	isfin4 10288*	Definition of a IV-finite set. (Contributed by Stefan O'Rear, 16-May-2015.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ FinIV ↔ ¬ ∃𝑦(𝑦 ⊊ 𝐴 ∧ 𝑦 ≈ 𝐴)))
Theorem	fin4i 10289	Infer that a set is IV-infinite. (Contributed by Stefan O'Rear, 16-May-2015.)
⊢ ((𝑋 ⊊ 𝐴 ∧ 𝑋 ≈ 𝐴) → ¬ 𝐴 ∈ FinIV)
Theorem	isfin5 10290	Definition of a V-finite set. (Contributed by Stefan O'Rear, 16-May-2015.)
⊢ (𝐴 ∈ FinV ↔ (𝐴 = ∅ ∨ 𝐴 ≺ (𝐴 ⊔ 𝐴)))
Theorem	isfin6 10291	Definition of a VI-finite set. (Contributed by Stefan O'Rear, 16-May-2015.)
⊢ (𝐴 ∈ FinVI ↔ (𝐴 ≺ 2o ∨ 𝐴 ≺ (𝐴 × 𝐴)))
Theorem	isfin7 10292*	Definition of a VII-finite set. (Contributed by Stefan O'Rear, 16-May-2015.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ FinVII ↔ ¬ ∃𝑦 ∈ (On ∖ ω)𝐴 ≈ 𝑦))
Theorem	sdom2en01 10293	A set with less than two elements has 0 or 1. (Contributed by Stefan O'Rear, 30-Oct-2014.)
⊢ (𝐴 ≺ 2o ↔ (𝐴 = ∅ ∨ 𝐴 ≈ 1o))
Theorem	infpssrlem1 10294	Lemma for infpssr 10299. (Contributed by Stefan O'Rear, 30-Oct-2014.)
⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴 ∖ 𝐵))    &   ⊢ 𝐺 = (rec(◡𝐹, 𝐶) ↾ ω)    ⇒   ⊢ (𝜑 → (𝐺‘∅) = 𝐶)
Theorem	infpssrlem2 10295	Lemma for infpssr 10299. (Contributed by Stefan O'Rear, 30-Oct-2014.)
⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴 ∖ 𝐵))    &   ⊢ 𝐺 = (rec(◡𝐹, 𝐶) ↾ ω)    ⇒   ⊢ (𝑀 ∈ ω → (𝐺‘suc 𝑀) = (◡𝐹‘(𝐺‘𝑀)))
Theorem	infpssrlem3 10296	Lemma for infpssr 10299. (Contributed by Stefan O'Rear, 30-Oct-2014.)
⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴 ∖ 𝐵))    &   ⊢ 𝐺 = (rec(◡𝐹, 𝐶) ↾ ω)    ⇒   ⊢ (𝜑 → 𝐺:ω⟶𝐴)
Theorem	infpssrlem4 10297	Lemma for infpssr 10299. (Contributed by Stefan O'Rear, 30-Oct-2014.)
⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴 ∖ 𝐵))    &   ⊢ 𝐺 = (rec(◡𝐹, 𝐶) ↾ ω)    ⇒   ⊢ ((𝜑 ∧ 𝑀 ∈ ω ∧ 𝑁 ∈ 𝑀) → (𝐺‘𝑀) ≠ (𝐺‘𝑁))
Theorem	infpssrlem5 10298	Lemma for infpssr 10299. (Contributed by Stefan O'Rear, 30-Oct-2014.)
⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴 ∖ 𝐵))    &   ⊢ 𝐺 = (rec(◡𝐹, 𝐶) ↾ ω)    ⇒   ⊢ (𝜑 → (𝐴 ∈ 𝑉 → ω ≼ 𝐴))
Theorem	infpssr 10299	Dedekind infinity implies existence of a denumerable subset: take a single point witnessing the proper subset relation and iterate the embedding. (Contributed by Stefan O'Rear, 30-Oct-2014.) (Revised by Mario Carneiro, 16-May-2015.)
⊢ ((𝑋 ⊊ 𝐴 ∧ 𝑋 ≈ 𝐴) → ω ≼ 𝐴)
Theorem	fin4en1 10300	Dedekind finite is a cardinal property. (Contributed by Stefan O'Rear, 30-Oct-2014.) (Revised by Mario Carneiro, 16-May-2015.)
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ FinIV → 𝐵 ∈ FinIV))