P. 86 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 8501-8600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nnunifi 8501	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 8502*	Lemma for unbnn 8506. 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 8503*	Lemma for unbnn 8506. The value of the function 𝐹 belongs to the unbounded set of natural numbers 𝐴. (Contributed by NM, 3-Dec-2003.)
⊢ 𝐹 = (rec((𝑥 ∈ V ↦ ∩ (𝐴 ∖ suc 𝑥)), ∩ 𝐴) ↾ ω)    ⇒   ⊢ ((𝐴 ⊆ ω ∧ ∀𝑤 ∈ ω ∃𝑣 ∈ 𝐴 𝑤 ∈ 𝑣) → (𝑧 ∈ ω → (𝐹‘𝑧) ∈ 𝐴))
Theorem	unblem3 8504*	Lemma for unbnn 8506. 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 8505*	Lemma for unbnn 8506. 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 8506*	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 8855 for a stronger version without the first assumption. (Contributed by NM, 3-Dec-2003.)
⊢ ((ω ∈ V ∧ 𝐴 ⊆ ω ∧ ∀𝑥 ∈ ω ∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦) → 𝐴 ≈ ω)
Theorem	unbnn2 8507*	Version of unbnn 8506 that does not require a strict upper bound. (Contributed by NM, 24-Apr-2004.)
⊢ ((ω ∈ V ∧ 𝐴 ⊆ ω ∧ ∀𝑥 ∈ ω ∃𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦) → 𝐴 ≈ ω)
Theorem	isfinite2 8508	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 8509	Omega strictly dominates a natural number. Example 3 of [Enderton] p. 146. In order to avoid the Axiom of infinity, we include it as a hypothesis. (Contributed by NM, 15-Jun-1998.)
⊢ ((ω ∈ V ∧ 𝐴 ∈ ω) → 𝐴 ≺ ω)
Theorem	isfiniteg 8510	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 8511	An infinite set strictly dominates a natural number. (Contributed by NM, 22-Nov-2004.) (Revised by Mario Carneiro, 27-Apr-2015.)
⊢ ((ω ≼ 𝐴 ∧ 𝐵 ∈ ω) → 𝐵 ≺ 𝐴)
Theorem	infn0 8512	An infinite set is not empty. (Contributed by NM, 23-Oct-2004.)
⊢ (ω ≼ 𝐴 → 𝐴 ≠ ∅)
Theorem	fin2inf 8513	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 8514*	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 8515*	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 8516	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	unfi 8517	The union of two finite sets is finite. Part of Corollary 6K of [Enderton] p. 144. (Contributed by NM, 16-Nov-2002.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ∪ 𝐵) ∈ Fin)
Theorem	unfir 8518	If a union is finite, the operands are finite. Converse of unfi 8517. (Contributed by FL, 3-Aug-2009.)
⊢ ((𝐴 ∪ 𝐵) ∈ Fin → (𝐴 ∈ Fin ∧ 𝐵 ∈ Fin))
Theorem	unfi2 8519	The union of two finite sets is finite. Part of Corollary 6K of [Enderton] p. 144. This version of unfi 8517 is useful only if we assume the Axiom of Infinity (see comments in fin2inf 8513). (Contributed by NM, 22-Oct-2004.) (Revised by Mario Carneiro, 27-Apr-2015.)
⊢ ((𝐴 ≺ ω ∧ 𝐵 ≺ ω) → (𝐴 ∪ 𝐵) ≺ ω)
Theorem	difinf 8520	An infinite set 𝐴 minus a finite set is infinite. (Contributed by FL, 3-Aug-2009.)
⊢ ((¬ 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ¬ (𝐴 ∖ 𝐵) ∈ Fin)
Theorem	xpfi 8521	The Cartesian product of two finite sets is finite. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Mar-2015.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 × 𝐵) ∈ Fin)
Theorem	3xpfi 8522	The Cartesian product of three finite sets is a finite set. (Contributed by Alexander van der Vekens, 11-Mar-2018.)
⊢ (𝑉 ∈ Fin → ((𝑉 × 𝑉) × 𝑉) ∈ Fin)
Theorem	domunfican 8523	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 8524*	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 8525	An unordered pair is finite. (Contributed by NM, 22-Aug-2008.)
⊢ {𝐴, 𝐵} ∈ Fin
Theorem	tpfi 8526	An unordered triple is finite. (Contributed by Mario Carneiro, 28-Sep-2013.)
⊢ {𝐴, 𝐵, 𝐶} ∈ Fin
Theorem	fiint 8527*	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.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴 ↔ ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → ∩ 𝑥 ∈ 𝐴))
Theorem	fnfi 8528	A version of fnex 6755 for finite sets that does not require Replacement. (Contributed by Mario Carneiro, 16-Nov-2014.) (Revised by Mario Carneiro, 24-Jun-2015.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ Fin) → 𝐹 ∈ Fin)
Theorem	fodomfi 8529	An onto function implies dominance of domain over range, for finite sets. Unlike fodom 9681 for arbitrary sets, this theorem does not require the Axiom of Choice for its proof. (Contributed by NM, 23-Mar-2006.) (Proof shortened by Mario Carneiro, 16-Nov-2014.)
⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) → 𝐵 ≼ 𝐴)
Theorem	fodomfib 8530*	Equivalence of an onto mapping and dominance for a nonempty finite set. Unlike fodomb 9685 for arbitrary sets, this theorem does not require the Axiom of Choice for its proof. (Contributed by NM, 23-Mar-2006.)
⊢ (𝐴 ∈ Fin → ((𝐴 ≠ ∅ ∧ ∃𝑓 𝑓:𝐴–onto→𝐵) ↔ (∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴)))
Theorem	fofinf1o 8531	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 8532	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 8533	Any finite set dominates its domain. (Contributed by Mario Carneiro, 22-Sep-2013.) (Revised by Mario Carneiro, 16-Nov-2014.)
⊢ (𝐹 ∈ Fin → dom 𝐹 ≼ 𝐹)
Theorem	dmfi 8534	The domain of a finite set is finite. (Contributed by Mario Carneiro, 24-Sep-2013.)
⊢ (𝐴 ∈ Fin → dom 𝐴 ∈ Fin)
Theorem	fundmfibi 8535	A function is finite if and only if its domain is finite. (Contributed by AV, 10-Jan-2020.)
⊢ (Fun 𝐹 → (𝐹 ∈ Fin ↔ dom 𝐹 ∈ Fin))
Theorem	resfnfinfin 8536	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 8537	A restricted identity function is finite iff the restricting class is finite. (Contributed by AV, 10-Jan-2020.)
⊢ (( I ↾ 𝐴) ∈ Fin ↔ 𝐴 ∈ Fin)
Theorem	cnvfi 8538	If a set is finite, its converse is as well. (Contributed by Mario Carneiro, 28-Dec-2014.)
⊢ (𝐴 ∈ Fin → ◡𝐴 ∈ Fin)
Theorem	rnfi 8539	The range of a finite set is finite. (Contributed by Mario Carneiro, 28-Dec-2014.)
⊢ (𝐴 ∈ Fin → ran 𝐴 ∈ Fin)
Theorem	f1dmvrnfibi 8540	A one-to-one function whose domain is a set is finite if and only if its range is finite. See also f1vrnfibi 8541. (Contributed by AV, 10-Jan-2020.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴–1-1→𝐵) → (𝐹 ∈ Fin ↔ ran 𝐹 ∈ Fin))
Theorem	f1vrnfibi 8541	A one-to-one function which is a set is finite if and only if its range is finite. See also f1dmvrnfibi 8540. (Contributed by AV, 10-Jan-2020.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴–1-1→𝐵) → (𝐹 ∈ Fin ↔ ran 𝐹 ∈ Fin))
Theorem	fofi 8542	If a function has a finite domain, its range is finite. Theorem 37 of [Suppes] p. 104. (Contributed by NM, 25-Mar-2007.)
⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) → 𝐵 ∈ Fin)
Theorem	f1fi 8543	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	iunfi 8544*	The finite union of finite sets is finite. Exercise 13 of [Enderton] p. 144. This is the indexed union version of unifi 8545. 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 8545	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 8546*	The finite union of finite sets is finite. Exercise 13 of [Enderton] p. 144. This version of unifi 8545 is useful only if we assume the Axiom of Infinity (see comments in fin2inf 8513). (Contributed by NM, 11-Mar-2006.)
⊢ ((𝐴 ≺ ω ∧ ∀𝑥 ∈ 𝐴 𝑥 ≺ ω) → ∪ 𝐴 ≺ ω)
Theorem	infssuni 8547*	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 8548	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	imafi 8549	Images of finite sets are finite. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ ((Fun 𝐹 ∧ 𝑋 ∈ Fin) → (𝐹 “ 𝑋) ∈ Fin)
Theorem	pwfilem 8550*	Lemma for pwfi 8551. (Contributed by NM, 26-Mar-2007.)
⊢ 𝐹 = (𝑐 ∈ 𝒫 𝑏 ↦ (𝑐 ∪ {𝑥}))    ⇒   ⊢ (𝒫 𝑏 ∈ Fin → 𝒫 (𝑏 ∪ {𝑥}) ∈ Fin)
Theorem	pwfi 8551	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.)
⊢ (𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Fin)
Theorem	mapfi 8552	Set exponentiation of finite sets is finite. (Contributed by Jeff Madsen, 19-Jun-2011.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ↑𝑚 𝐵) ∈ Fin)
Theorem	ixpfi 8553*	A Cartesian product of finitely many finite sets is finite. (Contributed by Jeff Madsen, 19-Jun-2011.)
⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ Fin) → X𝑥 ∈ 𝐴 𝐵 ∈ Fin)
Theorem	ixpfi2 8554*	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 8555*	A finite mapping set is finite. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ (𝐴 ∈ Fin → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ Fin)
Theorem	abrexfi 8556*	An image set from a finite set is finite. (Contributed by Mario Carneiro, 13-Feb-2014.)
⊢ (𝐴 ∈ Fin → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ Fin)
Theorem	cnvimamptfin 8557*	A preimage of a mapping with a finite domain under any class is finite. In contrast to fisuppfi 8573, the range of the mapping needs not to be known. (Contributed by AV, 21-Dec-2018.)
⊢ (𝜑 → 𝑁 ∈ Fin)    ⇒   ⊢ (𝜑 → (◡(𝑝 ∈ 𝑁 ↦ 𝑋) “ 𝑌) ∈ Fin)
Theorem	elfpw 8558	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 8559	A set is the union of its finite subsets. (Contributed by Stefan O'Rear, 2-Apr-2015.)
⊢ ∪ (𝒫 𝐴 ∩ Fin) = 𝐴
Theorem	f1opwfi 8560*	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 8561*	A finite subset of a union is covered by finitely many elements. (Contributed by Stefan O'Rear, 2-Apr-2015.)
⊢ ((𝐴 ⊆ ∪ 𝐵 ∧ 𝐴 ∈ Fin) → ∃𝑐 ∈ (𝒫 𝐵 ∩ Fin)𝐴 ⊆ ∪ 𝑐)
Theorem	fipreima 8562*	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 8563*	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 22268 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 8564*	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 34163. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑀 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) → ∃𝑐 ∈ Fin (𝑐 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑))
2.4.28  Finitely supported functions
Syntax	cfsupp 8565	Extend class definition to include the predicate to be a finitely supported function.
class finSupp
Definition	df-fsupp 8566*	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 8567	The property of a function to be finitely supported is a relation. (Contributed by AV, 7-Jun-2019.)
⊢ Rel finSupp
Theorem	relprcnfsupp 8568	A proper class is never finitely supported. (Contributed by AV, 7-Jun-2019.)
⊢ (¬ 𝐴 ∈ V → ¬ 𝐴 finSupp 𝑍)
Theorem	isfsupp 8569	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	funisfsupp 8570	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 8571	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 8572	A finitely supported function is a function with a finite support. (Contributed by AV, 6-Jun-2019.)
⊢ (𝜑 → 𝐹 finSupp 𝑍)    ⇒   ⊢ (𝜑 → (𝐹 supp 𝑍) ∈ Fin)
Theorem	fisuppfi 8573	A function on a finite set is finitely supported. (Contributed by Mario Carneiro, 20-Jun-2015.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    ⇒   ⊢ (𝜑 → (◡𝐹 “ 𝐶) ∈ Fin)
Theorem	fdmfisuppfi 8574	The support of a function with a finite domain is always finite. (Contributed by AV, 27-Apr-2019.)
⊢ (𝜑 → 𝐹:𝐷⟶𝑅)    &   ⊢ (𝜑 → 𝐷 ∈ Fin)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐹 supp 𝑍) ∈ Fin)
Theorem	fdmfifsupp 8575	A function with a finite domain is always finitely supported. (Contributed by AV, 25-May-2019.)
⊢ (𝜑 → 𝐹:𝐷⟶𝑅)    &   ⊢ (𝜑 → 𝐷 ∈ Fin)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐹 finSupp 𝑍)
Theorem	fsuppmptdm 8576*	A mapping with a finite domain is finitely supported. (Contributed by AV, 7-Jun-2019.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑌)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑊)    ⇒   ⊢ (𝜑 → 𝐹 finSupp 𝑍)
Theorem	fndmfisuppfi 8577	The support of a function with a finite domain is always finite. (Contributed by AV, 25-May-2019.)
⊢ (𝜑 → 𝐹 Fn 𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ Fin)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐹 supp 𝑍) ∈ Fin)
Theorem	fndmfifsupp 8578	A function with a finite domain is always finitely supported. (Contributed by AV, 25-May-2019.)
⊢ (𝜑 → 𝐹 Fn 𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ Fin)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐹 finSupp 𝑍)
Theorem	suppeqfsuppbi 8579	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 8580	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 8581	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	fsuppxpfi 8582	The cartesian product of two finitely supported functions is finite. (Contributed by AV, 17-Jul-2019.)
⊢ ((𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍) → ((𝐹 supp 𝑍) × (𝐺 supp 𝑍)) ∈ Fin)
Theorem	fczfsuppd 8583	A constant function with value zero is finitely supported. (Contributed by AV, 30-Jun-2019.)
⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐵 × {𝑍}) finSupp 𝑍)
Theorem	fsuppun 8584	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 8585	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 8586	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 8587	The empty set is a finitely supported function. (Contributed by AV, 19-Jul-2019.)
⊢ (𝑍 ∈ 𝑉 → ∅ finSupp 𝑍)
Theorem	snopfsupp 8588	A singleton containing an ordered pair is a finitely supported function. (Contributed by AV, 19-Jul-2019.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → {⟨𝑋, 𝑌⟩} finSupp 𝑍)
Theorem	funsnfsupp 8589	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 8590	The restriction of a finitely supported function is finitely supported. (Contributed by AV, 14-Jul-2019.)
⊢ (𝜑 → 𝐹 finSupp 𝑍)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐹 ↾ 𝑋) finSupp 𝑍)
Theorem	ressuppfi 8591	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 8592	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 8593	The restriction of a function to a finite set is finitely supported. (Contributed by AV, 12-Dec-2019.)
⊢ (𝜑 → Fun 𝐹)    &   ⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐹 ↾ 𝑋) finSupp 𝑍)
Theorem	frnfsuppbi 8594	Two ways of saying that a function with known codomain is finitely supported. (Contributed by AV, 8-Jul-2019.)
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝐹:𝐼⟶𝑆 → (𝐹 finSupp 𝑍 ↔ (◡𝐹 “ (𝑆 ∖ {𝑍})) ∈ Fin)))
Theorem	fsuppmptif 8595*	A function mapping an argument to either a value of a finitely supported function or zero is finitely supported. (Contributed by AV, 6-Jun-2019.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐹 finSupp 𝑍)    ⇒   ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 𝑍)) finSupp 𝑍)
Theorem	fsuppcolem 8596	Lemma for fsuppco 8597. Formula building theorem for finite supports: rearranging the index set. (Contributed by Stefan O'Rear, 21-Mar-2015.)
⊢ (𝜑 → (◡𝐹 “ (V ∖ {𝑍})) ∈ Fin)    &   ⊢ (𝜑 → 𝐺:𝑋–1-1→𝑌)    ⇒   ⊢ (𝜑 → (◡(𝐹 ∘ 𝐺) “ (V ∖ {𝑍})) ∈ Fin)
Theorem	fsuppco 8597	The composition of a 1-1 function with a finitely supported function is finitely supported. (Contributed by AV, 28-May-2019.)
⊢ (𝜑 → 𝐹 finSupp 𝑍)    &   ⊢ (𝜑 → 𝐺:𝑋–1-1→𝑌)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐹 ∘ 𝐺) finSupp 𝑍)
Theorem	fsuppco2 8598	The composition of a function which maps the zero to zero with a finitely supported function is finitely supported. This is not only a special case of fsuppcor 8599 because it does not require that the "zero" is an element of the range of the finitely supported function. (Contributed by AV, 6-Jun-2019.)
⊢ (𝜑 → 𝑍 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐺:𝐵⟶𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 finSupp 𝑍)    &   ⊢ (𝜑 → (𝐺‘𝑍) = 𝑍)    ⇒   ⊢ (𝜑 → (𝐺 ∘ 𝐹) finSupp 𝑍)
Theorem	fsuppcor 8599	The composition of a function which maps the zero of the range of a finitely supported function to the zero of its range with this finitely supported function is finitely supported. (Contributed by AV, 6-Jun-2019.)
⊢ (𝜑 → 0 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐶)    &   ⊢ (𝜑 → 𝐺:𝐵⟶𝐷)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 finSupp 𝑍)    &   ⊢ (𝜑 → (𝐺‘𝑍) = 0 )    ⇒   ⊢ (𝜑 → (𝐺 ∘ 𝐹) finSupp 0 )
Theorem	mapfienlem1 8600*	Lemma 1 for mapfien 8603. (Contributed by AV, 3-Jul-2019.)
⊢ 𝑆 = {𝑥 ∈ (𝐵 ↑𝑚 𝐴) ∣ 𝑥 finSupp 𝑍}    &   ⊢ 𝑇 = {𝑥 ∈ (𝐷 ↑𝑚 𝐶) ∣ 𝑥 finSupp 𝑊}    &   ⊢ 𝑊 = (𝐺‘𝑍)    &   ⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴)    &   ⊢ (𝜑 → 𝐺:𝐵–1-1-onto→𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ V)    &   ⊢ (𝜑 → 𝐵 ∈ V)    &   ⊢ (𝜑 → 𝐶 ∈ V)    &   ⊢ (𝜑 → 𝐷 ∈ V)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑆) → (𝐺 ∘ (𝑓 ∘ 𝐹)) finSupp 𝑊)