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	infsdomnn 9201	An infinite set strictly dominates a natural number. (Contributed by NM, 22-Nov-2004.) (Revised by Mario Carneiro, 27-Apr-2015.) Avoid ax-pow 5310. (Revised by BTernaryTau, 7-Jan-2025.)
⊢ ((ω ≼ 𝐴 ∧ 𝐵 ∈ ω) → 𝐵 ≺ 𝐴)
Theorem	infn0 9202	An infinite set is not empty. For a shorter proof using ax-un 7680, see infn0ALT 9203. (Contributed by NM, 23-Oct-2004.) Avoid ax-un 7680. (Revised by BTernaryTau, 8-Jan-2025.)
⊢ (ω ≼ 𝐴 → 𝐴 ≠ ∅)
Theorem	infn0ALT 9203	Shorter proof of infn0 9202 using ax-un 7680. (Contributed by NM, 23-Oct-2004.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (ω ≼ 𝐴 → 𝐴 ≠ ∅)
Theorem	fin2inf 9204	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 9205*	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 9206*	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 9207	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 9208	If a union is finite, the operands are finite. Converse of unfi 9095. (Contributed by FL, 3-Aug-2009.)
⊢ ((𝐴 ∪ 𝐵) ∈ Fin → (𝐴 ∈ Fin ∧ 𝐵 ∈ Fin))
Theorem	unfib 9209	A union is finite if and only if the operands are finite. (Contributed by AV, 10-May-2025.)
⊢ ((𝐴 ∪ 𝐵) ∈ Fin ↔ (𝐴 ∈ Fin ∧ 𝐵 ∈ Fin))
Theorem	unfi2 9210	The union of two finite sets is finite. Part of Corollary 6K of [Enderton] p. 144. This version of unfi 9095 is useful only if we assume the Axiom of Infinity (see comments in fin2inf 9204). (Contributed by NM, 22-Oct-2004.) (Revised by Mario Carneiro, 27-Apr-2015.)
⊢ ((𝐴 ≺ ω ∧ 𝐵 ≺ ω) → (𝐴 ∪ 𝐵) ≺ ω)
Theorem	difinf 9211	An infinite set 𝐴 minus a finite set is infinite. (Contributed by FL, 3-Aug-2009.)
⊢ ((¬ 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ¬ (𝐴 ∖ 𝐵) ∈ Fin)
Theorem	fodomfi 9212	An onto function implies dominance of domain over range, for finite sets. Unlike fodomg 10432 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 5310. (Revised by BTernaryTau, 20-Jun-2025.)
⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) → 𝐵 ≼ 𝐴)
Theorem	fofi 9213	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 9214	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 9215	Images of finite sets are finite. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ ((Fun 𝐹 ∧ 𝑋 ∈ Fin) → (𝐹 “ 𝑋) ∈ Fin)
Theorem	imafiOLD 9216	Obsolete version of imafi 9215 as of 25-Jun-2025. (Contributed by Stefan O'Rear, 22-Feb-2015.) Avoid ax-pow 5310. (Revised by BTernaryTau, 7-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((Fun 𝐹 ∧ 𝑋 ∈ Fin) → (𝐹 “ 𝑋) ∈ Fin)
Theorem	pwfir 9217	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 9218*	Lemma for pwfi 9219. (Contributed by NM, 26-Mar-2007.) Avoid ax-pow 5310. (Revised by BTernaryTau, 7-Sep-2024.)
⊢ 𝐹 = (𝑐 ∈ 𝒫 𝑏 ↦ (𝑐 ∪ {𝑥}))    ⇒   ⊢ (𝒫 𝑏 ∈ Fin → 𝒫 (𝑏 ∪ {𝑥}) ∈ Fin)
Theorem	pwfi 9219	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 5310. (Revised by BTernaryTau, 7-Sep-2024.)
⊢ (𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Fin)
Theorem	xpfi 9220	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 5310. (Revised by BTernaryTau, 10-Jan-2025.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 × 𝐵) ∈ Fin)
Theorem	3xpfi 9221	The Cartesian product of three finite sets is a finite set. (Contributed by Alexander van der Vekens, 11-Mar-2018.)
⊢ (𝑉 ∈ Fin → ((𝑉 × 𝑉) × 𝑉) ∈ Fin)
Theorem	domunfican 9222	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 9223*	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 9224	An unordered pair is finite. For a shorter proof using ax-un 7680, see prfiALT 9225. (Contributed by NM, 22-Aug-2008.) Avoid ax-11 2162, ax-un 7680. (Revised by BTernaryTau, 13-Jan-2025.)
⊢ {𝐴, 𝐵} ∈ Fin
Theorem	prfiALT 9225	Shorter proof of prfi 9224 using ax-un 7680. (Contributed by NM, 22-Aug-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ {𝐴, 𝐵} ∈ Fin
Theorem	tpfi 9226	An unordered triple is finite. (Contributed by Mario Carneiro, 28-Sep-2013.)
⊢ {𝐴, 𝐵, 𝐶} ∈ Fin
Theorem	fiint 9227*	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 5310. (Revised by BTernaryTau, 14-Jan-2025.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴 ↔ ∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ 𝑧 ∈ Fin) → ∩ 𝑧 ∈ 𝐴))
Theorem	fodomfir 9228*	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 9056). (Contributed by BTernaryTau, 23-Jun-2025.)
⊢ ((𝐴 ∈ Fin ∧ ∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → ∃𝑓 𝑓:𝐴–onto→𝐵)
Theorem	fodomfib 9229*	Equivalence of an onto mapping and dominance for a nonempty finite set. Unlike fodomb 10436 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 5310. (Revised by BTernaryTau, 23-Jun-2025.)
⊢ (𝐴 ∈ Fin → ((𝐴 ≠ ∅ ∧ ∃𝑓 𝑓:𝐴–onto→𝐵) ↔ (∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴)))
Theorem	fodomfiOLD 9230	Obsolete version of fodomfi 9212 as of 20-Jun-2025. (Contributed by NM, 23-Mar-2006.) (Proof shortened by Mario Carneiro, 16-Nov-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) → 𝐵 ≼ 𝐴)
Theorem	fodomfibOLD 9231*	Obsolete version of fodomfib 9229 as of 23-Jun-2025. (Contributed by NM, 23-Mar-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ Fin → ((𝐴 ≠ ∅ ∧ ∃𝑓 𝑓:𝐴–onto→𝐵) ↔ (∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴)))
Theorem	fofinf1o 9232	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 9233	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 9234	Any finite set dominates its domain. (Contributed by Mario Carneiro, 22-Sep-2013.) (Revised by Mario Carneiro, 16-Nov-2014.)
⊢ (𝐹 ∈ Fin → dom 𝐹 ≼ 𝐹)
Theorem	dmfi 9235	The domain of a finite set is finite. (Contributed by Mario Carneiro, 24-Sep-2013.)
⊢ (𝐴 ∈ Fin → dom 𝐴 ∈ Fin)
Theorem	fundmfibi 9236	A function is finite if and only if its domain is finite. (Contributed by AV, 10-Jan-2020.)
⊢ (Fun 𝐹 → (𝐹 ∈ Fin ↔ dom 𝐹 ∈ Fin))
Theorem	resfnfinfin 9237	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 9238	A restricted identity function is finite iff the restricting class is finite. (Contributed by AV, 10-Jan-2020.)
⊢ (( I ↾ 𝐴) ∈ Fin ↔ 𝐴 ∈ Fin)
Theorem	cnvfiALT 9239	Shorter proof of cnvfi 9100 using ax-pow 5310. (Contributed by Mario Carneiro, 28-Dec-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ Fin → ◡𝐴 ∈ Fin)
Theorem	rnfi 9240	The range of a finite set is finite. (Contributed by Mario Carneiro, 28-Dec-2014.)
⊢ (𝐴 ∈ Fin → ran 𝐴 ∈ Fin)
Theorem	f1dmvrnfibi 9241	A one-to-one function whose domain is a set is finite if and only if its range is finite. See also f1vrnfibi 9242. (Contributed by AV, 10-Jan-2020.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴–1-1→𝐵) → (𝐹 ∈ Fin ↔ ran 𝐹 ∈ Fin))
Theorem	f1vrnfibi 9242	A one-to-one function which is a set is finite if and only if its range is finite. See also f1dmvrnfibi 9241. (Contributed by AV, 10-Jan-2020.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴–1-1→𝐵) → (𝐹 ∈ Fin ↔ ran 𝐹 ∈ Fin))
Theorem	iunfi 9243*	The finite union of finite sets is finite. Exercise 13 of [Enderton] p. 144. This is the indexed union version of unifi 9244. 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 9244	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 9245*	The finite union of finite sets is finite. Exercise 13 of [Enderton] p. 144. This version of unifi 9244 is useful only if we assume the Axiom of Infinity (see comments in fin2inf 9204). (Contributed by NM, 11-Mar-2006.)
⊢ ((𝐴 ≺ ω ∧ ∀𝑥 ∈ 𝐴 𝑥 ≺ ω) → ∪ 𝐴 ≺ ω)
Theorem	infssuni 9246*	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 9247	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 9248	Set exponentiation of finite sets is finite. (Contributed by Jeff Madsen, 19-Jun-2011.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ↑m 𝐵) ∈ Fin)
Theorem	ixpfi 9249*	A Cartesian product of finitely many finite sets is finite. (Contributed by Jeff Madsen, 19-Jun-2011.)
⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ Fin) → X𝑥 ∈ 𝐴 𝐵 ∈ Fin)
Theorem	ixpfi2 9250*	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 9251*	A finite mapping set is finite. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ (𝐴 ∈ Fin → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ Fin)
Theorem	abrexfi 9252*	An image set from a finite set is finite. (Contributed by Mario Carneiro, 13-Feb-2014.)
⊢ (𝐴 ∈ Fin → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ Fin)
Theorem	cnvimamptfin 9253*	A preimage of a mapping with a finite domain under any class is finite. In contrast to fisuppfi 9274, the range of the mapping needs not to be known. (Contributed by AV, 21-Dec-2018.)
⊢ (𝜑 → 𝑁 ∈ Fin)    ⇒   ⊢ (𝜑 → (◡(𝑝 ∈ 𝑁 ↦ 𝑋) “ 𝑌) ∈ Fin)
Theorem	elfpw 9254	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 9255	A set is the union of its finite subsets. (Contributed by Stefan O'Rear, 2-Apr-2015.)
⊢ ∪ (𝒫 𝐴 ∩ Fin) = 𝐴
Theorem	f1opwfi 9256*	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 9257*	A finite subset of a union is covered by finitely many elements. (Contributed by Stefan O'Rear, 2-Apr-2015.)
⊢ ((𝐴 ⊆ ∪ 𝐵 ∧ 𝐴 ∈ Fin) → ∃𝑐 ∈ (𝒫 𝐵 ∩ Fin)𝐴 ⊆ ∪ 𝑐)
Theorem	fipreima 9258*	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 9259*	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 23989 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 9260*	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 37931. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑀 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) → ∃𝑐 ∈ Fin (𝑐 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑))
Theorem	imafi2 9261	The image by a finite set is finite. See also imafi 9215. (Contributed by Thierry Arnoux, 25-Apr-2020.)
⊢ (𝐴 ∈ Fin → (𝐴 “ 𝐵) ∈ Fin)
Theorem	unifi3 9262	If a union is finite, then all its elements are finite. See unifi 9244. (Contributed by Thierry Arnoux, 27-Aug-2017.)
⊢ (∪ 𝐴 ∈ Fin → 𝐴 ⊆ Fin)
Theorem	tfsnfin2 9263	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 9264	Extend class definition to include the predicate to be a finitely supported function.
class finSupp
Definition	df-fsupp 9265*	Define the property of a function to be finitely supported (in relation to a given zero). (Contributed by AV, 23-May-2019.)
⊢ finSupp = {⟨𝑟, 𝑧⟩ ∣ (Fun 𝑟 ∧ (𝑟 supp 𝑧) ∈ Fin)}
Theorem	relfsupp 9266	The property of a function to be finitely supported is a relation. (Contributed by AV, 7-Jun-2019.)
⊢ Rel finSupp
Theorem	relprcnfsupp 9267	A proper class is never finitely supported. (Contributed by AV, 7-Jun-2019.)
⊢ (¬ 𝐴 ∈ V → ¬ 𝐴 finSupp 𝑍)
Theorem	isfsupp 9268	The property of a class to be a finitely supported function (in relation to a given zero). (Contributed by AV, 23-May-2019.)
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑅 finSupp 𝑍 ↔ (Fun 𝑅 ∧ (𝑅 supp 𝑍) ∈ Fin)))
Theorem	isfsuppd 9269	Deduction form of isfsupp 9268. (Contributed by SN, 29-Jul-2024.)
⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑊)    &   ⊢ (𝜑 → Fun 𝑅)    &   ⊢ (𝜑 → (𝑅 supp 𝑍) ∈ Fin)    ⇒   ⊢ (𝜑 → 𝑅 finSupp 𝑍)
Theorem	funisfsupp 9270	The property of a function to be finitely supported (in relation to a given zero). (Contributed by AV, 23-May-2019.)
⊢ ((Fun 𝑅 ∧ 𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑅 finSupp 𝑍 ↔ (𝑅 supp 𝑍) ∈ Fin))
Theorem	fsuppimp 9271	Implications of a class being a finitely supported function (in relation to a given zero). (Contributed by AV, 26-May-2019.)
⊢ (𝑅 finSupp 𝑍 → (Fun 𝑅 ∧ (𝑅 supp 𝑍) ∈ Fin))
Theorem	fsuppimpd 9272	A finitely supported function is a function with a finite support. (Contributed by AV, 6-Jun-2019.)
⊢ (𝜑 → 𝐹 finSupp 𝑍)    ⇒   ⊢ (𝜑 → (𝐹 supp 𝑍) ∈ Fin)
Theorem	fsuppfund 9273	A finitely supported function is a function. (Contributed by SN, 8-Mar-2025.)
⊢ (𝜑 → 𝐹 finSupp 𝑍)    ⇒   ⊢ (𝜑 → Fun 𝐹)
Theorem	fisuppfi 9274	A function on a finite set is finitely supported. (Contributed by Mario Carneiro, 20-Jun-2015.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    ⇒   ⊢ (𝜑 → (◡𝐹 “ 𝐶) ∈ Fin)
Theorem	fidmfisupp 9275	A function with a finite domain is finitely supported. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ (𝜑 → 𝐹:𝐷⟶𝑅)    &   ⊢ (𝜑 → 𝐷 ∈ Fin)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐹 finSupp 𝑍)
Theorem	finnzfsuppd 9276*	If a function is zero outside of a finite set, it has finite support. (Contributed by Rohan Ridenour, 13-May-2024.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 Fn 𝐷)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑥 ∈ 𝐴 ∨ (𝐹‘𝑥) = 𝑍))    ⇒   ⊢ (𝜑 → 𝐹 finSupp 𝑍)
Theorem	fdmfisuppfi 9277	The support of a function with a finite domain is always finite. (Contributed by AV, 27-Apr-2019.)
⊢ (𝜑 → 𝐹:𝐷⟶𝑅)    &   ⊢ (𝜑 → 𝐷 ∈ Fin)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐹 supp 𝑍) ∈ Fin)
Theorem	fdmfifsupp 9278	A function with a finite domain is always finitely supported. (Contributed by AV, 25-May-2019.)
⊢ (𝜑 → 𝐹:𝐷⟶𝑅)    &   ⊢ (𝜑 → 𝐷 ∈ Fin)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐹 finSupp 𝑍)
Theorem	fsuppmptdm 9279*	A mapping with a finite domain is finitely supported. (Contributed by AV, 7-Jun-2019.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑌)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑊)    ⇒   ⊢ (𝜑 → 𝐹 finSupp 𝑍)
Theorem	fndmfisuppfi 9280	The support of a function with a finite domain is always finite. (Contributed by AV, 25-May-2019.)
⊢ (𝜑 → 𝐹 Fn 𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ Fin)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐹 supp 𝑍) ∈ Fin)
Theorem	fndmfifsupp 9281	A function with a finite domain is always finitely supported. (Contributed by AV, 25-May-2019.)
⊢ (𝜑 → 𝐹 Fn 𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ Fin)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐹 finSupp 𝑍)
Theorem	suppeqfsuppbi 9282	If two functions have the same support, one function is finitely supported iff the other one is finitely supported. (Contributed by AV, 30-Jun-2019.)
⊢ (((𝐹 ∈ 𝑈 ∧ Fun 𝐹) ∧ (𝐺 ∈ 𝑉 ∧ Fun 𝐺)) → ((𝐹 supp 𝑍) = (𝐺 supp 𝑍) → (𝐹 finSupp 𝑍 ↔ 𝐺 finSupp 𝑍)))
Theorem	suppssfifsupp 9283	If the support of a function is a subset of a finite set, the function is finitely supported. (Contributed by AV, 15-Jul-2019.)
⊢ (((𝐺 ∈ 𝑉 ∧ Fun 𝐺 ∧ 𝑍 ∈ 𝑊) ∧ (𝐹 ∈ Fin ∧ (𝐺 supp 𝑍) ⊆ 𝐹)) → 𝐺 finSupp 𝑍)
Theorem	fsuppsssupp 9284	If the support of a function is a subset of the support of a finitely supported function, the function is finitely supported. (Contributed by AV, 2-Jul-2019.) (Proof shortened by AV, 15-Jul-2019.)
⊢ (((𝐺 ∈ 𝑉 ∧ Fun 𝐺) ∧ (𝐹 finSupp 𝑍 ∧ (𝐺 supp 𝑍) ⊆ (𝐹 supp 𝑍))) → 𝐺 finSupp 𝑍)
Theorem	fsuppsssuppgd 9285	If the support of a function is a subset of a finite support, it is finite. Deduction associated with fsuppsssupp 9284. (Contributed by SN, 6-Mar-2025.)
⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑊)    &   ⊢ (𝜑 → Fun 𝐺)    &   ⊢ (𝜑 → 𝐹 finSupp 𝑂)    &   ⊢ (𝜑 → (𝐺 supp 𝑍) ⊆ (𝐹 supp 𝑂))    ⇒   ⊢ (𝜑 → 𝐺 finSupp 𝑍)
Theorem	fsuppss 9286	A subset of a finitely supported function is a finitely supported function. (Contributed by SN, 8-Mar-2025.)
⊢ (𝜑 → 𝐹 ⊆ 𝐺)    &   ⊢ (𝜑 → 𝐺 finSupp 𝑍)    ⇒   ⊢ (𝜑 → 𝐹 finSupp 𝑍)
Theorem	fsuppssov1 9287*	Formula building theorem for finite support: operator with left annihilator. Finite support version of suppssov1 8139. (Contributed by SN, 26-Apr-2025.)
⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ 𝐴) finSupp 𝑌)    &   ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑅) → (𝑌𝑂𝑣) = 𝑍)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐵 ∈ 𝑅)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) finSupp 𝑍)
Theorem	fsuppxpfi 9288	The cartesian product of two finitely supported functions is finite. (Contributed by AV, 17-Jul-2019.)
⊢ ((𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍) → ((𝐹 supp 𝑍) × (𝐺 supp 𝑍)) ∈ Fin)
Theorem	fczfsuppd 9289	A constant function with value zero is finitely supported. (Contributed by AV, 30-Jun-2019.)
⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐵 × {𝑍}) finSupp 𝑍)
Theorem	fsuppun 9290	The union of two finitely supported functions is finitely supported (but not necessarily a function!). (Contributed by AV, 3-Jun-2019.)
⊢ (𝜑 → 𝐹 finSupp 𝑍)    &   ⊢ (𝜑 → 𝐺 finSupp 𝑍)    ⇒   ⊢ (𝜑 → ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin)
Theorem	fsuppunfi 9291	The union of the support of two finitely supported functions is finite. (Contributed by AV, 1-Jul-2019.)
⊢ (𝜑 → 𝐹 finSupp 𝑍)    &   ⊢ (𝜑 → 𝐺 finSupp 𝑍)    ⇒   ⊢ (𝜑 → ((𝐹 supp 𝑍) ∪ (𝐺 supp 𝑍)) ∈ Fin)
Theorem	fsuppunbi 9292	If the union of two classes/functions is a function, this union is finitely supported iff the two functions are finitely supported. (Contributed by AV, 18-Jun-2019.)
⊢ (𝜑 → Fun (𝐹 ∪ 𝐺))    ⇒   ⊢ (𝜑 → ((𝐹 ∪ 𝐺) finSupp 𝑍 ↔ (𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍)))
Theorem	0fsupp 9293	The empty set is a finitely supported function. (Contributed by AV, 19-Jul-2019.)
⊢ (𝑍 ∈ 𝑉 → ∅ finSupp 𝑍)
Theorem	snopfsupp 9294	A singleton containing an ordered pair is a finitely supported function. (Contributed by AV, 19-Jul-2019.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → {⟨𝑋, 𝑌⟩} finSupp 𝑍)
Theorem	funsnfsupp 9295	Finite support for a function extended by a singleton. (Contributed by Stefan O'Rear, 27-Feb-2015.) (Revised by AV, 19-Jul-2019.)
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (Fun 𝐹 ∧ 𝑋 ∉ dom 𝐹)) → ((𝐹 ∪ {⟨𝑋, 𝑌⟩}) finSupp 𝑍 ↔ 𝐹 finSupp 𝑍))
Theorem	fsuppres 9296	The restriction of a finitely supported function is finitely supported. (Contributed by AV, 14-Jul-2019.)
⊢ (𝜑 → 𝐹 finSupp 𝑍)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐹 ↾ 𝑋) finSupp 𝑍)
Theorem	fmptssfisupp 9297*	The restriction of a mapping function has finite support if that function has finite support. (Contributed by Thierry Arnoux, 21-Jan-2024.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) finSupp 𝑍)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ 𝐵) finSupp 𝑍)
Theorem	ressuppfi 9298	If the support of the restriction of a function by a set which, subtracted from the domain of the function so that its difference is finite, the support of the function itself is finite. (Contributed by AV, 22-Apr-2019.)
⊢ (𝜑 → (dom 𝐹 ∖ 𝐵) ∈ Fin)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐺 = (𝐹 ↾ 𝐵))    &   ⊢ (𝜑 → (𝐺 supp 𝑍) ∈ Fin)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐹 supp 𝑍) ∈ Fin)
Theorem	resfsupp 9299	If the restriction of a function by a set which, subtracted from the domain of the function so that its difference is finitely supported, the function itself is finitely supported. (Contributed by AV, 27-May-2019.)
⊢ (𝜑 → (dom 𝐹 ∖ 𝐵) ∈ Fin)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑊)    &   ⊢ (𝜑 → Fun 𝐹)    &   ⊢ (𝜑 → 𝐺 = (𝐹 ↾ 𝐵))    &   ⊢ (𝜑 → 𝐺 finSupp 𝑍)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐹 finSupp 𝑍)
Theorem	resfifsupp 9300	The restriction of a function to a finite set is finitely supported. (Contributed by AV, 12-Dec-2019.)
⊢ (𝜑 → Fun 𝐹)    &   ⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐹 ↾ 𝑋) finSupp 𝑍)