P. 94 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 9301-9400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fodomfir 9301*	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 9130). (Contributed by BTernaryTau, 23-Jun-2025.)
⊢ ((𝐴 ∈ Fin ∧ ∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → ∃𝑓 𝑓:𝐴–onto→𝐵)
Theorem	fodomfib 9302*	Equivalence of an onto mapping and dominance for a nonempty finite set. Unlike fodomb 10533 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 5334. (Revised by BTernaryTau, 23-Jun-2025.)
⊢ (𝐴 ∈ Fin → ((𝐴 ≠ ∅ ∧ ∃𝑓 𝑓:𝐴–onto→𝐵) ↔ (∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴)))
Theorem	fofinf1o 9303	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 9304	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 9305	Any finite set dominates its domain. (Contributed by Mario Carneiro, 22-Sep-2013.) (Revised by Mario Carneiro, 16-Nov-2014.)
⊢ (𝐹 ∈ Fin → dom 𝐹 ≼ 𝐹)
Theorem	dmfi 9306	The domain of a finite set is finite. (Contributed by Mario Carneiro, 24-Sep-2013.)
⊢ (𝐴 ∈ Fin → dom 𝐴 ∈ Fin)
Theorem	fundmfibi 9307	A function is finite if and only if its domain is finite. (Contributed by AV, 10-Jan-2020.)
⊢ (Fun 𝐹 → (𝐹 ∈ Fin ↔ dom 𝐹 ∈ Fin))
Theorem	resfnfinfin 9308	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 9309	A restricted identity function is finite iff the restricting class is finite. (Contributed by AV, 10-Jan-2020.)
⊢ (( I ↾ 𝐴) ∈ Fin ↔ 𝐴 ∈ Fin)
Theorem	cnvfiALT 9310	Shorter proof of cnvfi 9174 using ax-pow 5334. (Contributed by Mario Carneiro, 28-Dec-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ Fin → ◡𝐴 ∈ Fin)
Theorem	rnfi 9311	The range of a finite set is finite. (Contributed by Mario Carneiro, 28-Dec-2014.)
⊢ (𝐴 ∈ Fin → ran 𝐴 ∈ Fin)
Theorem	f1dmvrnfibi 9312	A one-to-one function whose domain is a set is finite if and only if its range is finite. See also f1vrnfibi 9313. (Contributed by AV, 10-Jan-2020.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴–1-1→𝐵) → (𝐹 ∈ Fin ↔ ran 𝐹 ∈ Fin))
Theorem	f1vrnfibi 9313	A one-to-one function which is a set is finite if and only if its range is finite. See also f1dmvrnfibi 9312. (Contributed by AV, 10-Jan-2020.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴–1-1→𝐵) → (𝐹 ∈ Fin ↔ ran 𝐹 ∈ Fin))
Theorem	iunfi 9314*	The finite union of finite sets is finite. Exercise 13 of [Enderton] p. 144. This is the indexed union version of unifi 9315. 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 9315	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 9316*	The finite union of finite sets is finite. Exercise 13 of [Enderton] p. 144. This version of unifi 9315 is useful only if we assume the Axiom of Infinity (see comments in fin2inf 9278). (Contributed by NM, 11-Mar-2006.)
⊢ ((𝐴 ≺ ω ∧ ∀𝑥 ∈ 𝐴 𝑥 ≺ ω) → ∪ 𝐴 ≺ ω)
Theorem	infssuni 9317*	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 9318	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 9319	Set exponentiation of finite sets is finite. (Contributed by Jeff Madsen, 19-Jun-2011.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ↑m 𝐵) ∈ Fin)
Theorem	ixpfi 9320*	A Cartesian product of finitely many finite sets is finite. (Contributed by Jeff Madsen, 19-Jun-2011.)
⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ Fin) → X𝑥 ∈ 𝐴 𝐵 ∈ Fin)
Theorem	ixpfi2 9321*	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 9322*	A finite mapping set is finite. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ (𝐴 ∈ Fin → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ Fin)
Theorem	abrexfi 9323*	An image set from a finite set is finite. (Contributed by Mario Carneiro, 13-Feb-2014.)
⊢ (𝐴 ∈ Fin → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ Fin)
Theorem	cnvimamptfin 9324*	A preimage of a mapping with a finite domain under any class is finite. In contrast to fisuppfi 9345, the range of the mapping needs not to be known. (Contributed by AV, 21-Dec-2018.)
⊢ (𝜑 → 𝑁 ∈ Fin)    ⇒   ⊢ (𝜑 → (◡(𝑝 ∈ 𝑁 ↦ 𝑋) “ 𝑌) ∈ Fin)
Theorem	elfpw 9325	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 9326	A set is the union of its finite subsets. (Contributed by Stefan O'Rear, 2-Apr-2015.)
⊢ ∪ (𝒫 𝐴 ∩ Fin) = 𝐴
Theorem	f1opwfi 9327*	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 9328*	A finite subset of a union is covered by finitely many elements. (Contributed by Stefan O'Rear, 2-Apr-2015.)
⊢ ((𝐴 ⊆ ∪ 𝐵 ∧ 𝐴 ∈ Fin) → ∃𝑐 ∈ (𝒫 𝐵 ∩ Fin)𝐴 ⊆ ∪ 𝑐)
Theorem	fipreima 9329*	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 9330*	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 24277 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 9331*	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 38492. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑀 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) → ∃𝑐 ∈ Fin (𝑐 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑))
Theorem	imafi2 9332	The image by a finite set is finite. See also imafi 9289. (Contributed by Thierry Arnoux, 25-Apr-2020.)
⊢ (𝐴 ∈ Fin → (𝐴 “ 𝐵) ∈ Fin)
Theorem	unifi3 9333	If a union is finite, then all its elements are finite. See unifi 9315. (Contributed by Thierry Arnoux, 27-Aug-2017.)
⊢ (∪ 𝐴 ∈ Fin → 𝐴 ⊆ Fin)
Theorem	tfsnfin2 9334	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 9335	Extend class definition to include the predicate to be a finitely supported function.
class finSupp
Definition	df-fsupp 9336*	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 9337	The property of a function to be finitely supported is a relation. (Contributed by AV, 7-Jun-2019.)
⊢ Rel finSupp
Theorem	relprcnfsupp 9338	A proper class is never finitely supported. (Contributed by AV, 7-Jun-2019.)
⊢ (¬ 𝐴 ∈ V → ¬ 𝐴 finSupp 𝑍)
Theorem	isfsupp 9339	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 9340	Deduction form of isfsupp 9339. (Contributed by SN, 29-Jul-2024.)
⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑊)    &   ⊢ (𝜑 → Fun 𝑅)    &   ⊢ (𝜑 → (𝑅 supp 𝑍) ∈ Fin)    ⇒   ⊢ (𝜑 → 𝑅 finSupp 𝑍)
Theorem	funisfsupp 9341	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 9342	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 9343	A finitely supported function is a function with a finite support. (Contributed by AV, 6-Jun-2019.)
⊢ (𝜑 → 𝐹 finSupp 𝑍)    ⇒   ⊢ (𝜑 → (𝐹 supp 𝑍) ∈ Fin)
Theorem	fsuppfund 9344	A finitely supported function is a function. (Contributed by SN, 8-Mar-2025.)
⊢ (𝜑 → 𝐹 finSupp 𝑍)    ⇒   ⊢ (𝜑 → Fun 𝐹)
Theorem	fisuppfi 9345	A function on a finite set is finitely supported. (Contributed by Mario Carneiro, 20-Jun-2015.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    ⇒   ⊢ (𝜑 → (◡𝐹 “ 𝐶) ∈ Fin)
Theorem	fidmfisupp 9346	A function with a finite domain is finitely supported. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ (𝜑 → 𝐹:𝐷⟶𝑅)    &   ⊢ (𝜑 → 𝐷 ∈ Fin)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐹 finSupp 𝑍)
Theorem	finnzfsuppd 9347*	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 9348	The support of a function with a finite domain is always finite. (Contributed by AV, 27-Apr-2019.)
⊢ (𝜑 → 𝐹:𝐷⟶𝑅)    &   ⊢ (𝜑 → 𝐷 ∈ Fin)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐹 supp 𝑍) ∈ Fin)
Theorem	fdmfifsupp 9349	A function with a finite domain is always finitely supported. (Contributed by AV, 25-May-2019.)
⊢ (𝜑 → 𝐹:𝐷⟶𝑅)    &   ⊢ (𝜑 → 𝐷 ∈ Fin)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐹 finSupp 𝑍)
Theorem	fsuppmptdm 9350*	A mapping with a finite domain is finitely supported. (Contributed by AV, 7-Jun-2019.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑌)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑊)    ⇒   ⊢ (𝜑 → 𝐹 finSupp 𝑍)
Theorem	fndmfisuppfi 9351	The support of a function with a finite domain is always finite. (Contributed by AV, 25-May-2019.)
⊢ (𝜑 → 𝐹 Fn 𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ Fin)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐹 supp 𝑍) ∈ Fin)
Theorem	fndmfifsupp 9352	A function with a finite domain is always finitely supported. (Contributed by AV, 25-May-2019.)
⊢ (𝜑 → 𝐹 Fn 𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ Fin)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐹 finSupp 𝑍)
Theorem	suppeqfsuppbi 9353	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 9354	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 9355	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 9356	If the support of a function is a subset of a finite support, it is finite. Deduction associated with fsuppsssupp 9355. (Contributed by SN, 6-Mar-2025.)
⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑊)    &   ⊢ (𝜑 → Fun 𝐺)    &   ⊢ (𝜑 → 𝐹 finSupp 𝑂)    &   ⊢ (𝜑 → (𝐺 supp 𝑍) ⊆ (𝐹 supp 𝑂))    ⇒   ⊢ (𝜑 → 𝐺 finSupp 𝑍)
Theorem	fsuppss 9357	A subset of a finitely supported function is a finitely supported function. (Contributed by SN, 8-Mar-2025.)
⊢ (𝜑 → 𝐹 ⊆ 𝐺)    &   ⊢ (𝜑 → 𝐺 finSupp 𝑍)    ⇒   ⊢ (𝜑 → 𝐹 finSupp 𝑍)
Theorem	fsuppssov1 9358*	Formula building theorem for finite support: operator with left annihilator. Finite support version of suppssov1 8199. (Contributed by SN, 26-Apr-2025.)
⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ 𝐴) finSupp 𝑌)    &   ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑅) → (𝑌𝑂𝑣) = 𝑍)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐵 ∈ 𝑅)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) finSupp 𝑍)
Theorem	fsuppxpfi 9359	The cartesian product of two finitely supported functions is finite. (Contributed by AV, 17-Jul-2019.)
⊢ ((𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍) → ((𝐹 supp 𝑍) × (𝐺 supp 𝑍)) ∈ Fin)
Theorem	fczfsuppd 9360	A constant function with value zero is finitely supported. (Contributed by AV, 30-Jun-2019.)
⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐵 × {𝑍}) finSupp 𝑍)
Theorem	fsuppun 9361	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 9362	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 9363	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 9364	The empty set is a finitely supported function. (Contributed by AV, 19-Jul-2019.)
⊢ (𝑍 ∈ 𝑉 → ∅ finSupp 𝑍)
Theorem	snopfsupp 9365	A singleton containing an ordered pair is a finitely supported function. (Contributed by AV, 19-Jul-2019.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → {⟨𝑋, 𝑌⟩} finSupp 𝑍)
Theorem	funsnfsupp 9366	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 9367	The restriction of a finitely supported function is finitely supported. (Contributed by AV, 14-Jul-2019.)
⊢ (𝜑 → 𝐹 finSupp 𝑍)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐹 ↾ 𝑋) finSupp 𝑍)
Theorem	fmptssfisupp 9368*	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 9369	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 9370	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 9371	The restriction of a function to a finite set is finitely supported. (Contributed by AV, 12-Dec-2019.)
⊢ (𝜑 → Fun 𝐹)    &   ⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐹 ↾ 𝑋) finSupp 𝑍)
Theorem	ffsuppbi 9372	Two ways of saying that a function with known codomain is finitely supported. (Contributed by AV, 8-Jul-2019.)
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝐹:𝐼⟶𝑆 → (𝐹 finSupp 𝑍 ↔ (◡𝐹 “ (𝑆 ∖ {𝑍})) ∈ Fin)))
Theorem	fsuppmptif 9373*	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	sniffsupp 9374*	A function mapping all but one arguments to zero is finitely supported. (Contributed by AV, 8-Jul-2019.)
⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 0 ∈ 𝑊)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑋, 𝐴, 0 ))    ⇒   ⊢ (𝜑 → 𝐹 finSupp 0 )
Theorem	fsuppcolem 9375	Lemma for fsuppco 9376. 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 9376	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 9377	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 9378 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 9378	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 9379*	Lemma 1 for mapfien 9382. (Contributed by AV, 3-Jul-2019.) (Revised by AV, 28-Jul-2024.)
⊢ 𝑆 = {𝑥 ∈ (𝐵 ↑m 𝐴) ∣ 𝑥 finSupp 𝑍}    &   ⊢ 𝑇 = {𝑥 ∈ (𝐷 ↑m 𝐶) ∣ 𝑥 finSupp 𝑊}    &   ⊢ 𝑊 = (𝐺‘𝑍)    &   ⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴)    &   ⊢ (𝜑 → 𝐺:𝐵–1-1-onto→𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑆) → (𝐺 ∘ (𝑓 ∘ 𝐹)) finSupp 𝑊)
Theorem	mapfienlem2 9380*	Lemma 2 for mapfien 9382. (Contributed by AV, 3-Jul-2019.) (Revised by AV, 28-Jul-2024.)
⊢ 𝑆 = {𝑥 ∈ (𝐵 ↑m 𝐴) ∣ 𝑥 finSupp 𝑍}    &   ⊢ 𝑇 = {𝑥 ∈ (𝐷 ↑m 𝐶) ∣ 𝑥 finSupp 𝑊}    &   ⊢ 𝑊 = (𝐺‘𝑍)    &   ⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴)    &   ⊢ (𝜑 → 𝐺:𝐵–1-1-onto→𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑇) → ((◡𝐺 ∘ 𝑔) ∘ ◡𝐹) finSupp 𝑍)
Theorem	mapfienlem3 9381*	Lemma 3 for mapfien 9382. (Contributed by AV, 3-Jul-2019.) (Revised by AV, 28-Jul-2024.)
⊢ 𝑆 = {𝑥 ∈ (𝐵 ↑m 𝐴) ∣ 𝑥 finSupp 𝑍}    &   ⊢ 𝑇 = {𝑥 ∈ (𝐷 ↑m 𝐶) ∣ 𝑥 finSupp 𝑊}    &   ⊢ 𝑊 = (𝐺‘𝑍)    &   ⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴)    &   ⊢ (𝜑 → 𝐺:𝐵–1-1-onto→𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑇) → ((◡𝐺 ∘ 𝑔) ∘ ◡𝐹) ∈ 𝑆)
Theorem	mapfien 9382*	A bijection of the base sets induces a bijection on the set of finitely supported functions. (Contributed by Mario Carneiro, 30-May-2015.) (Revised by AV, 3-Jul-2019.) (Revised by AV, 28-Jul-2024.)
⊢ 𝑆 = {𝑥 ∈ (𝐵 ↑m 𝐴) ∣ 𝑥 finSupp 𝑍}    &   ⊢ 𝑇 = {𝑥 ∈ (𝐷 ↑m 𝐶) ∣ 𝑥 finSupp 𝑊}    &   ⊢ 𝑊 = (𝐺‘𝑍)    &   ⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴)    &   ⊢ (𝜑 → 𝐺:𝐵–1-1-onto→𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑓 ∈ 𝑆 ↦ (𝐺 ∘ (𝑓 ∘ 𝐹))):𝑆–1-1-onto→𝑇)
Theorem	mapfien2 9383*	Equinumerousity relation for sets of finitely supported functions. (Contributed by Stefan O'Rear, 9-Jul-2015.) (Revised by AV, 7-Jul-2019.)
⊢ 𝑆 = {𝑥 ∈ (𝐵 ↑m 𝐴) ∣ 𝑥 finSupp 0 }    &   ⊢ 𝑇 = {𝑥 ∈ (𝐷 ↑m 𝐶) ∣ 𝑥 finSupp 𝑊}    &   ⊢ (𝜑 → 𝐴 ≈ 𝐶)    &   ⊢ (𝜑 → 𝐵 ≈ 𝐷)    &   ⊢ (𝜑 → 0 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐷)    ⇒   ⊢ (𝜑 → 𝑆 ≈ 𝑇)
2.4.36  Finite intersections
Syntax	cfi 9384	Extend class notation with the function whose value is the class of finite intersections of the elements of a given set.
class fi
Definition	df-fi 9385*	Function whose value is the class of finite intersections of the elements of the argument. Note that the empty intersection being the universal class, hence a proper class, it cannot be an element of that class. Therefore, the function value is the class of nonempty finite intersections of elements of the argument (see elfi2 9388). (Contributed by FL, 27-Apr-2008.)
⊢ fi = (𝑥 ∈ V ↦ {𝑧 ∣ ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑧 = ∩ 𝑦})
Theorem	fival 9386*	The set of all the finite intersections of the elements of 𝐴. (Contributed by FL, 27-Apr-2008.) (Revised by Mario Carneiro, 24-Nov-2013.)
⊢ (𝐴 ∈ 𝑉 → (fi‘𝐴) = {𝑦 ∣ ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ∩ 𝑥})
Theorem	elfi 9387*	Specific properties of an element of (fi‘𝐵). (Contributed by FL, 27-Apr-2008.) (Revised by Mario Carneiro, 24-Nov-2013.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∈ (fi‘𝐵) ↔ ∃𝑥 ∈ (𝒫 𝐵 ∩ Fin)𝐴 = ∩ 𝑥))
Theorem	elfi2 9388*	The empty intersection need not be considered in the set of finite intersections. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (fi‘𝐵) ↔ ∃𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})𝐴 = ∩ 𝑥))
Theorem	elfir 9389	Sufficient condition for an element of (fi‘𝐵). (Contributed by Mario Carneiro, 24-Nov-2013.)
⊢ ((𝐵 ∈ 𝑉 ∧ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin)) → ∩ 𝐴 ∈ (fi‘𝐵))
Theorem	intrnfi 9390	Sufficient condition for the intersection of the range of a function to be in the set of finite intersections. (Contributed by Mario Carneiro, 30-Aug-2015.)
⊢ ((𝐵 ∈ 𝑉 ∧ (𝐹:𝐴⟶𝐵 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin)) → ∩ ran 𝐹 ∈ (fi‘𝐵))
Theorem	iinfi 9391*	An indexed intersection of elements of 𝐶 is an element of the finite intersections of 𝐶. (Contributed by Mario Carneiro, 30-Aug-2015.)
⊢ ((𝐶 ∈ 𝑉 ∧ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin)) → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ (fi‘𝐶))
Theorem	inelfi 9392	The intersection of two sets is a finite intersection. (Contributed by Thierry Arnoux, 6-Jan-2017.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 ∩ 𝐵) ∈ (fi‘𝑋))
Theorem	ssfii 9393	Any element of a set 𝐴 is the intersection of a finite subset of 𝐴. (Contributed by FL, 27-Apr-2008.) (Proof shortened by Mario Carneiro, 21-Mar-2015.)
⊢ (𝐴 ∈ 𝑉 → 𝐴 ⊆ (fi‘𝐴))
Theorem	fi0 9394	The set of finite intersections of the empty set. (Contributed by Mario Carneiro, 30-Aug-2015.)
⊢ (fi‘∅) = ∅
Theorem	fieq0 9395	A set is empty iff the class of all the finite intersections of that set is empty. (Contributed by FL, 27-Apr-2008.) (Revised by Mario Carneiro, 24-Nov-2013.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 = ∅ ↔ (fi‘𝐴) = ∅))
Theorem	fiin 9396	The elements of (fi‘𝐶) are closed under finite intersection. (Contributed by Mario Carneiro, 24-Nov-2013.)
⊢ ((𝐴 ∈ (fi‘𝐶) ∧ 𝐵 ∈ (fi‘𝐶)) → (𝐴 ∩ 𝐵) ∈ (fi‘𝐶))
Theorem	dffi2 9397*	The set of finite intersections is the smallest set that contains 𝐴 and is closed under pairwise intersection. (Contributed by Mario Carneiro, 24-Nov-2013.)
⊢ (𝐴 ∈ 𝑉 → (fi‘𝐴) = ∩ {𝑧 ∣ (𝐴 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧)})
Theorem	fiss 9398	Subset relationship for function fi. (Contributed by Jeff Hankins, 7-Oct-2009.) (Revised by Mario Carneiro, 24-Nov-2013.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵) → (fi‘𝐴) ⊆ (fi‘𝐵))
Theorem	inficl 9399*	A set which is closed under pairwise intersection is closed under finite intersection. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 24-Nov-2013.)
⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴 ↔ (fi‘𝐴) = 𝐴))
Theorem	fipwuni 9400	The set of finite intersections of a set is contained in the powerset of the union of the elements of 𝐴. (Contributed by Mario Carneiro, 24-Nov-2013.) (Proof shortened by Mario Carneiro, 21-Mar-2015.)
⊢ (fi‘𝐴) ⊆ 𝒫 ∪ 𝐴