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
Theorem	ominf 9201	The set of natural numbers is infinite. Corollary 6D(b) of [Enderton] p. 136. (Contributed by NM, 2-Jun-1998.) Avoid ax-pow 5319. (Revised by BTernaryTau, 2-Jan-2025.)
⊢ ¬ ω ∈ Fin
Theorem	isinf 9202*	Any set that is not finite is literally infinite, in the sense that it contains subsets of arbitrarily large finite cardinality. (It cannot be proven that the set has countably infinite subsets unless AC is invoked.) The proof does not require the Axiom of Infinity. (Contributed by Mario Carneiro, 15-Jan-2013.) Avoid ax-pow 5319. (Revised by BTernaryTau, 2-Jan-2025.)
⊢ (¬ 𝐴 ∈ Fin → ∀𝑛 ∈ ω ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛))
Theorem	fineqvlem 9203	Lemma for fineqv 9204. (Contributed by Mario Carneiro, 20-Jan-2013.) (Proof shortened by Stefan O'Rear, 3-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → ω ≼ 𝒫 𝒫 𝐴)
Theorem	fineqv 9204	If the Axiom of Infinity is denied, then all sets are finite (which implies the Axiom of Choice). (Contributed by Mario Carneiro, 20-Jan-2013.) (Revised by Mario Carneiro, 3-Jan-2015.)
⊢ (¬ ω ∈ V ↔ Fin = V)
Theorem	xpfir 9205	The components of a nonempty finite Cartesian product are finite. (Contributed by Paul Chapman, 11-Apr-2009.) (Proof shortened by Mario Carneiro, 29-Apr-2015.)
⊢ (((𝐴 × 𝐵) ∈ Fin ∧ (𝐴 × 𝐵) ≠ ∅) → (𝐴 ∈ Fin ∧ 𝐵 ∈ Fin))
Theorem	ssfid 9206	A subset of a finite set is finite, deduction version of ssfi 9134. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → 𝐵 ∈ Fin)
Theorem	infi 9207	The intersection of two sets is finite if one of them is. (Contributed by Thierry Arnoux, 14-Feb-2017.)
⊢ (𝐴 ∈ Fin → (𝐴 ∩ 𝐵) ∈ Fin)
Theorem	rabfi 9208*	A restricted class built from a finite set is finite. (Contributed by Thierry Arnoux, 14-Feb-2017.)
⊢ (𝐴 ∈ Fin → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ Fin)
Theorem	finresfin 9209	The restriction of a finite set is finite. (Contributed by Alexander van der Vekens, 3-Jan-2018.)
⊢ (𝐸 ∈ Fin → (𝐸 ↾ 𝐵) ∈ Fin)
Theorem	f1finf1o 9210	Any injection from one finite set to another of equal size must be a bijection. (Contributed by Jeff Madsen, 5-Jun-2010.) (Revised by Mario Carneiro, 27-Feb-2014.) Avoid ax-pow 5319. (Revised by BTernaryTau, 4-Jan-2025.)
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → (𝐹:𝐴–1-1→𝐵 ↔ 𝐹:𝐴–1-1-onto→𝐵))
Theorem	nfielex 9211*	If a class is not finite, then it contains at least one element. (Contributed by Alexander van der Vekens, 12-Jan-2018.)
⊢ (¬ 𝐴 ∈ Fin → ∃𝑥 𝑥 ∈ 𝐴)
Theorem	en1eqsn 9212	A set with one element is a singleton. (Contributed by FL, 18-Aug-2008.) Avoid ax-pow 5319, ax-un 7712. (Revised by BTernaryTau, 4-Jan-2025.)
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ≈ 1o) → 𝐵 = {𝐴})
Theorem	en1eqsnbi 9213	A set containing an element has exactly one element iff it is a singleton. Formerly part of proof for rngen1zr 20813. (Contributed by FL, 13-Feb-2010.) (Revised by AV, 25-Jan-2020.)
⊢ (𝐴 ∈ 𝐵 → (𝐵 ≈ 1o ↔ 𝐵 = {𝐴}))
Theorem	dif1ennnALT 9214	Alternate proof of dif1ennn 9124 using ax-pow 5319. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Stefan O'Rear, 16-Aug-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴) → (𝐴 ∖ {𝑋}) ≈ 𝑀)
Theorem	enp1ilem 9215	Lemma for uses of enp1i 9216. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ 𝑇 = ({𝑥} ∪ 𝑆)    ⇒   ⊢ (𝑥 ∈ 𝐴 → ((𝐴 ∖ {𝑥}) = 𝑆 → 𝐴 = 𝑇))
Theorem	enp1i 9216*	Proof induction for en2 9217 and related theorems. (Contributed by Mario Carneiro, 5-Jan-2016.) Generalize to all ordinals and avoid ax-pow 5319, ax-un 7712. (Revised by BTernaryTau, 6-Jan-2025.)
⊢ Ord 𝑀    &   ⊢ 𝑁 = suc 𝑀    &   ⊢ ((𝐴 ∖ {𝑥}) ≈ 𝑀 → 𝜑)    &   ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))    ⇒   ⊢ (𝐴 ≈ 𝑁 → ∃𝑥𝜓)
Theorem	en2 9217*	A set equinumerous to ordinal 2 is an unordered pair. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ (𝐴 ≈ 2o → ∃𝑥∃𝑦 𝐴 = {𝑥, 𝑦})
Theorem	en3 9218*	A set equinumerous to ordinal 3 is a triple. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ (𝐴 ≈ 3o → ∃𝑥∃𝑦∃𝑧 𝐴 = {𝑥, 𝑦, 𝑧})
Theorem	en4 9219*	A set equinumerous to ordinal 4 is a quadruple. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ (𝐴 ≈ 4o → ∃𝑥∃𝑦∃𝑧∃𝑤 𝐴 = ({𝑥, 𝑦} ∪ {𝑧, 𝑤}))
Theorem	findcard3 9220*	Schema for strong induction on the cardinality of a finite set. The inductive hypothesis is that the result is true on any proper subset. The result is then proven to be true for all finite sets. (Contributed by Mario Carneiro, 13-Dec-2013.) Avoid ax-pow 5319. (Revised by BTernaryTau, 7-Jan-2025.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))    &   ⊢ (𝑦 ∈ Fin → (∀𝑥(𝑥 ⊊ 𝑦 → 𝜑) → 𝜒))    ⇒   ⊢ (𝐴 ∈ Fin → 𝜏)
Theorem	ac6sfi 9221*	A version of ac6s 10434 for finite sets. (Contributed by Jeff Hankins, 26-Jun-2009.) (Proof shortened by Mario Carneiro, 29-Jan-2014.)
⊢ (𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) → ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝜓))
Theorem	frfi 9222	A partial order is well-founded on a finite set. (Contributed by Jeff Madsen, 18-Jun-2010.) (Proof shortened by Mario Carneiro, 29-Jan-2014.)
⊢ ((𝑅 Po 𝐴 ∧ 𝐴 ∈ Fin) → 𝑅 Fr 𝐴)
Theorem	fimax2g 9223*	A finite set has a maximum under a total order. (Contributed by Jeff Madsen, 18-Jun-2010.) (Proof shortened by Mario Carneiro, 29-Jan-2014.)
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥𝑅𝑦)
Theorem	fimaxg 9224*	A finite set has a maximum under a total order. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 29-Jan-2014.)
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → 𝑦𝑅𝑥))
Theorem	fisupg 9225*	Lemma showing existence and closure of supremum of a finite set. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦𝑅𝑧)))
Theorem	wofi 9226	A total order on a finite set is a well-order. (Contributed by Jeff Madsen, 18-Jun-2010.) (Proof shortened by Mario Carneiro, 29-Jan-2014.)
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → 𝑅 We 𝐴)
Theorem	ordunifi 9227	The maximum of a finite collection of ordinals is in the set. (Contributed by Mario Carneiro, 28-May-2013.) (Revised by Mario Carneiro, 29-Jan-2014.)
⊢ ((𝐴 ⊆ On ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → ∪ 𝐴 ∈ 𝐴)
Theorem	nnunifi 9228	The union (supremum) of a finite set of finite ordinals is a finite ordinal. (Contributed by Stefan O'Rear, 5-Nov-2014.)
⊢ ((𝑆 ⊆ ω ∧ 𝑆 ∈ Fin) → ∪ 𝑆 ∈ ω)
Theorem	unblem1 9229*	Lemma for unbnn 9233. After removing the successor of an element from an unbounded set of natural numbers, the intersection of the result belongs to the original unbounded set. (Contributed by NM, 3-Dec-2003.)
⊢ (((𝐵 ⊆ ω ∧ ∀𝑥 ∈ ω ∃𝑦 ∈ 𝐵 𝑥 ∈ 𝑦) ∧ 𝐴 ∈ 𝐵) → ∩ (𝐵 ∖ suc 𝐴) ∈ 𝐵)
Theorem	unblem2 9230*	Lemma for unbnn 9233. The value of the function 𝐹 belongs to the unbounded set of natural numbers 𝐴. (Contributed by NM, 3-Dec-2003.)
⊢ 𝐹 = (rec((𝑥 ∈ V ↦ ∩ (𝐴 ∖ suc 𝑥)), ∩ 𝐴) ↾ ω)    ⇒   ⊢ ((𝐴 ⊆ ω ∧ ∀𝑤 ∈ ω ∃𝑣 ∈ 𝐴 𝑤 ∈ 𝑣) → (𝑧 ∈ ω → (𝐹‘𝑧) ∈ 𝐴))
Theorem	unblem3 9231*	Lemma for unbnn 9233. The value of the function 𝐹 is less than its value at a successor. (Contributed by NM, 3-Dec-2003.)
⊢ 𝐹 = (rec((𝑥 ∈ V ↦ ∩ (𝐴 ∖ suc 𝑥)), ∩ 𝐴) ↾ ω)    ⇒   ⊢ ((𝐴 ⊆ ω ∧ ∀𝑤 ∈ ω ∃𝑣 ∈ 𝐴 𝑤 ∈ 𝑣) → (𝑧 ∈ ω → (𝐹‘𝑧) ∈ (𝐹‘suc 𝑧)))
Theorem	unblem4 9232*	Lemma for unbnn 9233. The function 𝐹 maps the set of natural numbers one-to-one to the set of unbounded natural numbers 𝐴. (Contributed by NM, 3-Dec-2003.)
⊢ 𝐹 = (rec((𝑥 ∈ V ↦ ∩ (𝐴 ∖ suc 𝑥)), ∩ 𝐴) ↾ ω)    ⇒   ⊢ ((𝐴 ⊆ ω ∧ ∀𝑤 ∈ ω ∃𝑣 ∈ 𝐴 𝑤 ∈ 𝑣) → 𝐹:ω–1-1→𝐴)
Theorem	unbnn 9233*	Any unbounded subset of natural numbers is equinumerous to the set of all natural numbers. Part of the proof of Theorem 42 of [Suppes] p. 151. See unbnn3 9607 for a stronger version without the first assumption. (Contributed by NM, 3-Dec-2003.)
⊢ ((ω ∈ V ∧ 𝐴 ⊆ ω ∧ ∀𝑥 ∈ ω ∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦) → 𝐴 ≈ ω)
Theorem	unbnn2 9234*	Version of unbnn 9233 that does not require a strict upper bound. (Contributed by NM, 24-Apr-2004.)
⊢ ((ω ∈ V ∧ 𝐴 ⊆ ω ∧ ∀𝑥 ∈ ω ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦) → 𝐴 ≈ ω)
Theorem	isfinite2 9235	Any set strictly dominated by the class of natural numbers is finite. Sufficiency part of Theorem 42 of [Suppes] p. 151. This theorem does not require the Axiom of Infinity. (Contributed by NM, 24-Apr-2004.)
⊢ (𝐴 ≺ ω → 𝐴 ∈ Fin)
Theorem	nnsdomg 9236	Omega strictly dominates a natural number. Example 3 of [Enderton] p. 146. In order to avoid the Axiom of Infinity, we include it as part of the antecedent. See nnsdom 9602 for the version without this sethood requirement. (Contributed by NM, 15-Jun-1998.) Avoid ax-pow 5319. (Revised by BTernaryTau, 7-Jan-2025.)
⊢ ((ω ∈ V ∧ 𝐴 ∈ ω) → 𝐴 ≺ ω)
Theorem	isfiniteg 9237	A set is finite iff it is strictly dominated by the class of natural number. Theorem 42 of [Suppes] p. 151. In order to avoid the Axiom of infinity, we include it as a hypothesis. (Contributed by NM, 3-Nov-2002.) (Revised by Mario Carneiro, 27-Apr-2015.)
⊢ (ω ∈ V → (𝐴 ∈ Fin ↔ 𝐴 ≺ ω))
Theorem	infsdomnn 9238	An infinite set strictly dominates a natural number. (Contributed by NM, 22-Nov-2004.) (Revised by Mario Carneiro, 27-Apr-2015.) Avoid ax-pow 5319. (Revised by BTernaryTau, 7-Jan-2025.)
⊢ ((ω ≼ 𝐴 ∧ 𝐵 ∈ ω) → 𝐵 ≺ 𝐴)
Theorem	infn0 9239	An infinite set is not empty. For a shorter proof using ax-un 7712, see infn0ALT 9240. (Contributed by NM, 23-Oct-2004.) Avoid ax-un 7712. (Revised by BTernaryTau, 8-Jan-2025.)
⊢ (ω ≼ 𝐴 → 𝐴 ≠ ∅)
Theorem	infn0ALT 9240	Shorter proof of infn0 9239 using ax-un 7712. (Contributed by NM, 23-Oct-2004.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (ω ≼ 𝐴 → 𝐴 ≠ ∅)
Theorem	fin2inf 9241	This (useless) theorem, which was proved without the Axiom of Infinity, demonstrates an artifact of our definition of binary relation, which is meaningful only when its arguments exist. In particular, the antecedent cannot be satisfied unless ω exists. (Contributed by NM, 13-Nov-2003.)
⊢ (𝐴 ≺ ω → ω ∈ V)
Theorem	unfilem1 9242*	Lemma for proving that the union of two finite sets is finite. (Contributed by NM, 10-Nov-2002.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ 𝐴 ∈ ω    &   ⊢ 𝐵 ∈ ω    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐴 +o 𝑥))    ⇒   ⊢ ran 𝐹 = ((𝐴 +o 𝐵) ∖ 𝐴)
Theorem	unfilem2 9243*	Lemma for proving that the union of two finite sets is finite. (Contributed by NM, 10-Nov-2002.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ 𝐴 ∈ ω    &   ⊢ 𝐵 ∈ ω    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐴 +o 𝑥))    ⇒   ⊢ 𝐹:𝐵–1-1-onto→((𝐴 +o 𝐵) ∖ 𝐴)
Theorem	unfilem3 9244	Lemma for proving that the union of two finite sets is finite. (Contributed by NM, 16-Nov-2002.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → 𝐵 ≈ ((𝐴 +o 𝐵) ∖ 𝐴))
Theorem	unfir 9245	If a union is finite, the operands are finite. Converse of unfi 9132. (Contributed by FL, 3-Aug-2009.)
⊢ ((𝐴 ∪ 𝐵) ∈ Fin → (𝐴 ∈ Fin ∧ 𝐵 ∈ Fin))
Theorem	unfib 9246	A union is finite if and only if the operands are finite. (Contributed by AV, 10-May-2025.)
⊢ ((𝐴 ∪ 𝐵) ∈ Fin ↔ (𝐴 ∈ Fin ∧ 𝐵 ∈ Fin))
Theorem	unfi2 9247	The union of two finite sets is finite. Part of Corollary 6K of [Enderton] p. 144. This version of unfi 9132 is useful only if we assume the Axiom of Infinity (see comments in fin2inf 9241). (Contributed by NM, 22-Oct-2004.) (Revised by Mario Carneiro, 27-Apr-2015.)
⊢ ((𝐴 ≺ ω ∧ 𝐵 ≺ ω) → (𝐴 ∪ 𝐵) ≺ ω)
Theorem	difinf 9248	An infinite set 𝐴 minus a finite set is infinite. (Contributed by FL, 3-Aug-2009.)
⊢ ((¬ 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ¬ (𝐴 ∖ 𝐵) ∈ Fin)
Theorem	fodomfi 9249	An onto function implies dominance of domain over range, for finite sets. Unlike fodomg 10472 for arbitrary sets, this theorem does not require the Axiom of Replacement nor the Axiom of Power Sets nor the Axiom of Choice for its proof. (Contributed by NM, 23-Mar-2006.) (Proof shortened by Mario Carneiro, 16-Nov-2014.) Avoid ax-pow 5319. (Revised by BTernaryTau, 20-Jun-2025.)
⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) → 𝐵 ≼ 𝐴)
Theorem	fofi 9250	If an onto function has a finite domain, its codomain/range is finite. Theorem 37 of [Suppes] p. 104. (Contributed by NM, 25-Mar-2007.)
⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) → 𝐵 ∈ Fin)
Theorem	f1fi 9251	If a 1-to-1 function has a finite codomain its domain is finite. (Contributed by FL, 31-Jul-2009.) (Revised by Mario Carneiro, 24-Jun-2015.)
⊢ ((𝐵 ∈ Fin ∧ 𝐹:𝐴–1-1→𝐵) → 𝐴 ∈ Fin)
Theorem	imafi 9252	Images of finite sets are finite. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ ((Fun 𝐹 ∧ 𝑋 ∈ Fin) → (𝐹 “ 𝑋) ∈ Fin)
Theorem	imafiOLD 9253	Obsolete version of imafi 9252 as of 25-Jun-2025. (Contributed by Stefan O'Rear, 22-Feb-2015.) Avoid ax-pow 5319. (Revised by BTernaryTau, 7-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((Fun 𝐹 ∧ 𝑋 ∈ Fin) → (𝐹 “ 𝑋) ∈ Fin)
Theorem	pwfir 9254	If the power set of a set is finite, then the set itself is finite. (Contributed by BTernaryTau, 7-Sep-2024.)
⊢ (𝒫 𝐵 ∈ Fin → 𝐵 ∈ Fin)
Theorem	pwfilem 9255*	Lemma for pwfi 9256. (Contributed by NM, 26-Mar-2007.) Avoid ax-pow 5319. (Revised by BTernaryTau, 7-Sep-2024.)
⊢ 𝐹 = (𝑐 ∈ 𝒫 𝑏 ↦ (𝑐 ∪ {𝑥}))    ⇒   ⊢ (𝒫 𝑏 ∈ Fin → 𝒫 (𝑏 ∪ {𝑥}) ∈ Fin)
Theorem	pwfi 9256	The power set of a finite set is finite and vice-versa. Theorem 38 of [Suppes] p. 104 and its converse, Theorem 40 of [Suppes] p. 105. (Contributed by NM, 26-Mar-2007.) Avoid ax-pow 5319. (Revised by BTernaryTau, 7-Sep-2024.)
⊢ (𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Fin)
Theorem	xpfi 9257	The Cartesian product of two finite sets is finite. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Mar-2015.) Avoid ax-pow 5319. (Revised by BTernaryTau, 10-Jan-2025.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 × 𝐵) ∈ Fin)
Theorem	3xpfi 9258	The Cartesian product of three finite sets is a finite set. (Contributed by Alexander van der Vekens, 11-Mar-2018.)
⊢ (𝑉 ∈ Fin → ((𝑉 × 𝑉) × 𝑉) ∈ Fin)
Theorem	domunfican 9259	A finite set union cancellation law for dominance. (Contributed by Stefan O'Rear, 19-Feb-2015.) (Revised by Stefan O'Rear, 5-May-2015.)
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ≈ 𝐴) ∧ ((𝐴 ∩ 𝑋) = ∅ ∧ (𝐵 ∩ 𝑌) = ∅)) → ((𝐴 ∪ 𝑋) ≼ (𝐵 ∪ 𝑌) ↔ 𝑋 ≼ 𝑌))
Theorem	infcntss 9260*	Every infinite set has a denumerable subset. Similar to Exercise 8 of [TakeutiZaring] p. 91. (However, we need neither AC nor the Axiom of Infinity because of the way we express "infinite" in the antecedent.) (Contributed by NM, 23-Oct-2004.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (ω ≼ 𝐴 → ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ω))
Theorem	prfi 9261	An unordered pair is finite. For a shorter proof using ax-un 7712, see prfiALT 9262. (Contributed by NM, 22-Aug-2008.) Avoid ax-11 2190, ax-un 7712. (Revised by BTernaryTau, 13-Jan-2025.)
⊢ {𝐴, 𝐵} ∈ Fin
Theorem	prfiALT 9262	Shorter proof of prfi 9261 using ax-un 7712. (Contributed by NM, 22-Aug-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ {𝐴, 𝐵} ∈ Fin
Theorem	tpfi 9263	An unordered triple is finite. (Contributed by Mario Carneiro, 28-Sep-2013.)
⊢ {𝐴, 𝐵, 𝐶} ∈ Fin
Theorem	fiint 9264*	Equivalent ways of stating the finite intersection property. We show two ways of saying, "the intersection of elements in every finite nonempty subcollection of 𝐴 is in 𝐴". This theorem is applicable to a topology, which (among other axioms) is closed under finite intersections. Some texts use the left-hand version of this axiom and others the right-hand version, but as our proof here shows, their "intuitively obvious" equivalence can be non-trivial to establish formally. (Contributed by NM, 22-Sep-2002.) Use a separate setvar for the right-hand side and avoid ax-pow 5319. (Revised by BTernaryTau, 14-Jan-2025.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴 ↔ ∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ 𝑧 ∈ Fin) → ∩ 𝑧 ∈ 𝐴))
Theorem	fodomfir 9265*	There exists a mapping from a finite set onto any nonempty set that it dominates, proved without using the Axiom of Power Sets (unlike fodomr 9093). (Contributed by BTernaryTau, 23-Jun-2025.)
⊢ ((𝐴 ∈ Fin ∧ ∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → ∃𝑓 𝑓:𝐴–onto→𝐵)
Theorem	fodomfib 9266*	Equivalence of an onto mapping and dominance for a nonempty finite set. Unlike fodomb 10476 for arbitrary sets, this theorem does not require the Axiom of Replacement nor the Axiom of Power Sets nor the Axiom of Choice for its proof. (Contributed by NM, 23-Mar-2006.) Avoid ax-pow 5319. (Revised by BTernaryTau, 23-Jun-2025.)
⊢ (𝐴 ∈ Fin → ((𝐴 ≠ ∅ ∧ ∃𝑓 𝑓:𝐴–onto→𝐵) ↔ (∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴)))
Theorem	fodomfibOLD 9267*	Obsolete version of fodomfib 9266 as of 23-Jun-2025. (Contributed by NM, 23-Mar-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ Fin → ((𝐴 ≠ ∅ ∧ ∃𝑓 𝑓:𝐴–onto→𝐵) ↔ (∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴)))
Theorem	fofinf1o 9268	Any surjection from one finite set to another of equal size must be a bijection. (Contributed by Mario Carneiro, 19-Aug-2014.)
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → 𝐹:𝐴–1-1-onto→𝐵)
Theorem	rneqdmfinf1o 9269	Any function from a finite set onto the same set must be a bijection. (Contributed by AV, 5-Jul-2021.)
⊢ ((𝐴 ∈ Fin ∧ 𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐴) → 𝐹:𝐴–1-1-onto→𝐴)
Theorem	fidomdm 9270	Any finite set dominates its domain. (Contributed by Mario Carneiro, 22-Sep-2013.) (Revised by Mario Carneiro, 16-Nov-2014.)
⊢ (𝐹 ∈ Fin → dom 𝐹 ≼ 𝐹)
Theorem	dmfi 9271	The domain of a finite set is finite. (Contributed by Mario Carneiro, 24-Sep-2013.)
⊢ (𝐴 ∈ Fin → dom 𝐴 ∈ Fin)
Theorem	fundmfibi 9272	A function is finite if and only if its domain is finite. (Contributed by AV, 10-Jan-2020.)
⊢ (Fun 𝐹 → (𝐹 ∈ Fin ↔ dom 𝐹 ∈ Fin))
Theorem	resfnfinfin 9273	The restriction of a function to a finite set is finite. (Contributed by Alexander van der Vekens, 3-Feb-2018.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ Fin) → (𝐹 ↾ 𝐵) ∈ Fin)
Theorem	residfi 9274	A restricted identity function is finite iff the restricting class is finite. (Contributed by AV, 10-Jan-2020.)
⊢ (( I ↾ 𝐴) ∈ Fin ↔ 𝐴 ∈ Fin)
Theorem	cnvfiALT 9275	Shorter proof of cnvfi 9137 using ax-pow 5319. (Contributed by Mario Carneiro, 28-Dec-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ Fin → ◡𝐴 ∈ Fin)
Theorem	rnfi 9276	The range of a finite set is finite. (Contributed by Mario Carneiro, 28-Dec-2014.)
⊢ (𝐴 ∈ Fin → ran 𝐴 ∈ Fin)
Theorem	f1dmvrnfibi 9277	A one-to-one function whose domain is a set is finite if and only if its range is finite. See also f1vrnfibi 9278. (Contributed by AV, 10-Jan-2020.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴–1-1→𝐵) → (𝐹 ∈ Fin ↔ ran 𝐹 ∈ Fin))
Theorem	f1vrnfibi 9278	A one-to-one function which is a set is finite if and only if its range is finite. See also f1dmvrnfibi 9277. (Contributed by AV, 10-Jan-2020.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴–1-1→𝐵) → (𝐹 ∈ Fin ↔ ran 𝐹 ∈ Fin))
Theorem	iunfi 9279*	The finite union of finite sets is finite. Exercise 13 of [Enderton] p. 144. This is the indexed union version of unifi 9280. Note that 𝐵 depends on 𝑥, i.e. can be thought of as 𝐵(𝑥). (Contributed by NM, 23-Mar-2006.) (Proof shortened by Mario Carneiro, 31-Aug-2015.)
⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ Fin) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ Fin)
Theorem	unifi 9280	The finite union of finite sets is finite. Exercise 13 of [Enderton] p. 144. (Contributed by NM, 22-Aug-2008.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ∪ 𝐴 ∈ Fin)
Theorem	unifi2 9281*	The finite union of finite sets is finite. Exercise 13 of [Enderton] p. 144. This version of unifi 9280 is useful only if we assume the Axiom of Infinity (see comments in fin2inf 9241). (Contributed by NM, 11-Mar-2006.)
⊢ ((𝐴 ≺ ω ∧ ∀𝑥 ∈ 𝐴 𝑥 ≺ ω) → ∪ 𝐴 ≺ ω)
Theorem	infssuni 9282*	If an infinite set 𝐴 is included in the underlying set of a finite cover 𝐵, then there exists a set of the cover that contains an infinite number of element of 𝐴. (Contributed by FL, 2-Aug-2009.)
⊢ ((¬ 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ 𝐴 ⊆ ∪ 𝐵) → ∃𝑥 ∈ 𝐵 ¬ (𝐴 ∩ 𝑥) ∈ Fin)
Theorem	unirnffid 9283	The union of the range of a function from a finite set into the class of finite sets is finite. Deduction form. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐹:𝑇⟶Fin)    &   ⊢ (𝜑 → 𝑇 ∈ Fin)    ⇒   ⊢ (𝜑 → ∪ ran 𝐹 ∈ Fin)
Theorem	mapfi 9284	Set exponentiation of finite sets is finite. (Contributed by Jeff Madsen, 19-Jun-2011.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ↑m 𝐵) ∈ Fin)
Theorem	ixpfi 9285*	A Cartesian product of finitely many finite sets is finite. (Contributed by Jeff Madsen, 19-Jun-2011.)
⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ Fin) → X𝑥 ∈ 𝐴 𝐵 ∈ Fin)
Theorem	ixpfi2 9286*	A Cartesian product of finite sets such that all but finitely many are singletons is finite. (Note that 𝐵(𝑥) and 𝐷(𝑥) are both possibly dependent on 𝑥.) (Contributed by Mario Carneiro, 25-Jan-2015.)
⊢ (𝜑 → 𝐶 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ 𝐶)) → 𝐵 ⊆ {𝐷})    ⇒   ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 ∈ Fin)
Theorem	mptfi 9287*	A finite mapping set is finite. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ (𝐴 ∈ Fin → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ Fin)
Theorem	abrexfi 9288*	An image set from a finite set is finite. (Contributed by Mario Carneiro, 13-Feb-2014.)
⊢ (𝐴 ∈ Fin → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ Fin)
Theorem	cnvimamptfin 9289*	A preimage of a mapping with a finite domain under any class is finite. In contrast to fisuppfi 9310, the range of the mapping needs not to be known. (Contributed by AV, 21-Dec-2018.)
⊢ (𝜑 → 𝑁 ∈ Fin)    ⇒   ⊢ (𝜑 → (◡(𝑝 ∈ 𝑁 ↦ 𝑋) “ 𝑌) ∈ Fin)
Theorem	elfpw 9290	Membership in a class of finite subsets. (Contributed by Stefan O'Rear, 4-Apr-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
⊢ (𝐴 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ∈ Fin))
Theorem	unifpw 9291	A set is the union of its finite subsets. (Contributed by Stefan O'Rear, 2-Apr-2015.)
⊢ ∪ (𝒫 𝐴 ∩ Fin) = 𝐴
Theorem	f1opwfi 9292*	A one-to-one mapping induces a one-to-one mapping on finite subsets. (Contributed by Mario Carneiro, 25-Jan-2015.)
⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐹 “ 𝑏)):(𝒫 𝐴 ∩ Fin)–1-1-onto→(𝒫 𝐵 ∩ Fin))
Theorem	fissuni 9293*	A finite subset of a union is covered by finitely many elements. (Contributed by Stefan O'Rear, 2-Apr-2015.)
⊢ ((𝐴 ⊆ ∪ 𝐵 ∧ 𝐴 ∈ Fin) → ∃𝑐 ∈ (𝒫 𝐵 ∩ Fin)𝐴 ⊆ ∪ 𝑐)
Theorem	fipreima 9294*	Given a finite subset 𝐴 of the range of a function, there exists a finite subset of the domain whose image is 𝐴. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Stefan O'Rear, 22-Feb-2015.)
⊢ ((𝐹 Fn 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ∈ Fin) → ∃𝑐 ∈ (𝒫 𝐵 ∩ Fin)(𝐹 “ 𝑐) = 𝐴)
Theorem	finsschain 9295*	A finite subset of the union of a superset chain is a subset of some element of the chain. A useful preliminary result for alexsub 24092 and others. (Contributed by Jeff Hankins, 25-Jan-2010.) (Proof shortened by Mario Carneiro, 11-Feb-2015.) (Revised by Mario Carneiro, 18-May-2015.)
⊢ (((𝐴 ≠ ∅ ∧ [⊊] Or 𝐴) ∧ (𝐵 ∈ Fin ∧ 𝐵 ⊆ ∪ 𝐴)) → ∃𝑧 ∈ 𝐴 𝐵 ⊆ 𝑧)
Theorem	indexfi 9296*	If for every element of a finite indexing set 𝐴 there exists a corresponding element of another set 𝐵, then there exists a finite subset of 𝐵 consisting only of those elements which are indexed by 𝐴. Proven without the Axiom of Choice, unlike indexdom 38193. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑀 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) → ∃𝑐 ∈ Fin (𝑐 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑))
Theorem	imafi2 9297	The image by a finite set is finite. See also imafi 9252. (Contributed by Thierry Arnoux, 25-Apr-2020.)
⊢ (𝐴 ∈ Fin → (𝐴 “ 𝐵) ∈ Fin)
Theorem	unifi3 9298	If a union is finite, then all its elements are finite. See unifi 9280. (Contributed by Thierry Arnoux, 27-Aug-2017.)
⊢ (∪ 𝐴 ∈ Fin → 𝐴 ⊆ Fin)
Theorem	tfsnfin2 9299	A transfinite sequence is infinite iff its domain is greater than or equal to omega. Theorem 5 in Grzegorz Bancerek, "Epsilon Numbers and Cantor Normal Form", Formalized Mathematics, Vol. 17, No. 4, Pages 249–256, 2009. DOI: 10.2478/v10037-009-0032-8 (Contributed by RP, 1-Mar-2025.)
⊢ ((𝐴 Fn 𝐵 ∧ Ord 𝐵) → (¬ 𝐴 ∈ Fin ↔ ω ⊆ 𝐵))
2.4.35  Finitely supported functions
Syntax	cfsupp 9300	Extend class definition to include the predicate to be a finitely supported function.
class finSupp