P. 92 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 9101-9200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	f1opwfi 9101*	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 9102*	A finite subset of a union is covered by finitely many elements. (Contributed by Stefan O'Rear, 2-Apr-2015.)
⊢ ((𝐴 ⊆ ∪ 𝐵 ∧ 𝐴 ∈ Fin) → ∃𝑐 ∈ (𝒫 𝐵 ∩ Fin)𝐴 ⊆ ∪ 𝑐)
Theorem	fipreima 9103*	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 9104*	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 23194 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 9105*	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 35888. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑀 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) → ∃𝑐 ∈ Fin (𝑐 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑))
2.4.31  Finitely supported functions
Syntax	cfsupp 9106	Extend class definition to include the predicate to be a finitely supported function.
class finSupp
Definition	df-fsupp 9107*	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 9108	The property of a function to be finitely supported is a relation. (Contributed by AV, 7-Jun-2019.)
⊢ Rel finSupp
Theorem	relprcnfsupp 9109	A proper class is never finitely supported. (Contributed by AV, 7-Jun-2019.)
⊢ (¬ 𝐴 ∈ V → ¬ 𝐴 finSupp 𝑍)
Theorem	isfsupp 9110	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 9111	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 9112	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 9113	A finitely supported function is a function with a finite support. (Contributed by AV, 6-Jun-2019.)
⊢ (𝜑 → 𝐹 finSupp 𝑍)    ⇒   ⊢ (𝜑 → (𝐹 supp 𝑍) ∈ Fin)
Theorem	fisuppfi 9114	A function on a finite set is finitely supported. (Contributed by Mario Carneiro, 20-Jun-2015.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    ⇒   ⊢ (𝜑 → (◡𝐹 “ 𝐶) ∈ Fin)
Theorem	fdmfisuppfi 9115	The support of a function with a finite domain is always finite. (Contributed by AV, 27-Apr-2019.)
⊢ (𝜑 → 𝐹:𝐷⟶𝑅)    &   ⊢ (𝜑 → 𝐷 ∈ Fin)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐹 supp 𝑍) ∈ Fin)
Theorem	fdmfifsupp 9116	A function with a finite domain is always finitely supported. (Contributed by AV, 25-May-2019.)
⊢ (𝜑 → 𝐹:𝐷⟶𝑅)    &   ⊢ (𝜑 → 𝐷 ∈ Fin)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐹 finSupp 𝑍)
Theorem	fsuppmptdm 9117*	A mapping with a finite domain is finitely supported. (Contributed by AV, 7-Jun-2019.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑌)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑊)    ⇒   ⊢ (𝜑 → 𝐹 finSupp 𝑍)
Theorem	fndmfisuppfi 9118	The support of a function with a finite domain is always finite. (Contributed by AV, 25-May-2019.)
⊢ (𝜑 → 𝐹 Fn 𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ Fin)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐹 supp 𝑍) ∈ Fin)
Theorem	fndmfifsupp 9119	A function with a finite domain is always finitely supported. (Contributed by AV, 25-May-2019.)
⊢ (𝜑 → 𝐹 Fn 𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ Fin)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐹 finSupp 𝑍)
Theorem	suppeqfsuppbi 9120	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 9121	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 9122	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 9123	The cartesian product of two finitely supported functions is finite. (Contributed by AV, 17-Jul-2019.)
⊢ ((𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍) → ((𝐹 supp 𝑍) × (𝐺 supp 𝑍)) ∈ Fin)
Theorem	fczfsuppd 9124	A constant function with value zero is finitely supported. (Contributed by AV, 30-Jun-2019.)
⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐵 × {𝑍}) finSupp 𝑍)
Theorem	fsuppun 9125	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 9126	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 9127	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 9128	The empty set is a finitely supported function. (Contributed by AV, 19-Jul-2019.)
⊢ (𝑍 ∈ 𝑉 → ∅ finSupp 𝑍)
Theorem	snopfsupp 9129	A singleton containing an ordered pair is a finitely supported function. (Contributed by AV, 19-Jul-2019.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → {⟨𝑋, 𝑌⟩} finSupp 𝑍)
Theorem	funsnfsupp 9130	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 9131	The restriction of a finitely supported function is finitely supported. (Contributed by AV, 14-Jul-2019.)
⊢ (𝜑 → 𝐹 finSupp 𝑍)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐹 ↾ 𝑋) finSupp 𝑍)
Theorem	ressuppfi 9132	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 9133	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 9134	The restriction of a function to a finite set is finitely supported. (Contributed by AV, 12-Dec-2019.)
⊢ (𝜑 → Fun 𝐹)    &   ⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐹 ↾ 𝑋) finSupp 𝑍)
Theorem	frnfsuppbi 9135	Two ways of saying that a function with known codomain is finitely supported. (Contributed by AV, 8-Jul-2019.)
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝐹:𝐼⟶𝑆 → (𝐹 finSupp 𝑍 ↔ (◡𝐹 “ (𝑆 ∖ {𝑍})) ∈ Fin)))
Theorem	fsuppmptif 9136*	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 9137*	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 9138	Lemma for fsuppco 9139. 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 9139	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 9140	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 9141 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 9141	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 9142*	Lemma 1 for mapfien 9145. (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 9143*	Lemma 2 for mapfien 9145. (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 9144*	Lemma 3 for mapfien 9145. (Contributed by AV, 3-Jul-2019.) (Revised by AV, 28-Jul-2024.)
⊢ 𝑆 = {𝑥 ∈ (𝐵 ↑m 𝐴) ∣ 𝑥 finSupp 𝑍}    &   ⊢ 𝑇 = {𝑥 ∈ (𝐷 ↑m 𝐶) ∣ 𝑥 finSupp 𝑊}    &   ⊢ 𝑊 = (𝐺‘𝑍)    &   ⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴)    &   ⊢ (𝜑 → 𝐺:𝐵–1-1-onto→𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑇) → ((◡𝐺 ∘ 𝑔) ∘ ◡𝐹) ∈ 𝑆)
Theorem	mapfien 9145*	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 9146*	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.32  Finite intersections
Syntax	cfi 9147	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 9148*	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 9151). (Contributed by FL, 27-Apr-2008.)
⊢ fi = (𝑥 ∈ V ↦ {𝑧 ∣ ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑧 = ∩ 𝑦})
Theorem	fival 9149*	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 9150*	Specific properties of an element of (fi‘𝐵). (Contributed by FL, 27-Apr-2008.) (Revised by Mario Carneiro, 24-Nov-2013.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∈ (fi‘𝐵) ↔ ∃𝑥 ∈ (𝒫 𝐵 ∩ Fin)𝐴 = ∩ 𝑥))
Theorem	elfi2 9151*	The empty intersection need not be considered in the set of finite intersections. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (fi‘𝐵) ↔ ∃𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})𝐴 = ∩ 𝑥))
Theorem	elfir 9152	Sufficient condition for an element of (fi‘𝐵). (Contributed by Mario Carneiro, 24-Nov-2013.)
⊢ ((𝐵 ∈ 𝑉 ∧ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin)) → ∩ 𝐴 ∈ (fi‘𝐵))
Theorem	intrnfi 9153	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 9154*	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 9155	The intersection of two sets is a finite intersection. (Contributed by Thierry Arnoux, 6-Jan-2017.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 ∩ 𝐵) ∈ (fi‘𝑋))
Theorem	ssfii 9156	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 9157	The set of finite intersections of the empty set. (Contributed by Mario Carneiro, 30-Aug-2015.)
⊢ (fi‘∅) = ∅
Theorem	fieq0 9158	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 9159	The elements of (fi‘𝐶) are closed under finite intersection. (Contributed by Mario Carneiro, 24-Nov-2013.)
⊢ ((𝐴 ∈ (fi‘𝐶) ∧ 𝐵 ∈ (fi‘𝐶)) → (𝐴 ∩ 𝐵) ∈ (fi‘𝐶))
Theorem	dffi2 9160*	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 9161	Subset relationship for function fi. (Contributed by Jeff Hankins, 7-Oct-2009.) (Revised by Mario Carneiro, 24-Nov-2013.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵) → (fi‘𝐴) ⊆ (fi‘𝐵))
Theorem	inficl 9162*	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 9163	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‘𝐴) ⊆ 𝒫 ∪ 𝐴
Theorem	fisn 9164	A singleton is closed under finite intersections. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ (fi‘{𝐴}) = {𝐴}
Theorem	fiuni 9165	The union of the finite intersections of a set is simply the union of the set itself. (Contributed by Jeff Hankins, 5-Sep-2009.) (Revised by Mario Carneiro, 24-Nov-2013.)
⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 = ∪ (fi‘𝐴))
Theorem	fipwss 9166	If a set is a family of subsets of some base set, then so is its finite intersection. (Contributed by Stefan O'Rear, 2-Aug-2015.)
⊢ (𝐴 ⊆ 𝒫 𝑋 → (fi‘𝐴) ⊆ 𝒫 𝑋)
Theorem	elfiun 9167*	A finite intersection of elements taken from a union of collections. (Contributed by Jeff Hankins, 15-Nov-2009.) (Proof shortened by Mario Carneiro, 26-Nov-2013.)
⊢ ((𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐾) → (𝐴 ∈ (fi‘(𝐵 ∪ 𝐶)) ↔ (𝐴 ∈ (fi‘𝐵) ∨ 𝐴 ∈ (fi‘𝐶) ∨ ∃𝑥 ∈ (fi‘𝐵)∃𝑦 ∈ (fi‘𝐶)𝐴 = (𝑥 ∩ 𝑦))))
Theorem	dffi3 9168*	The set of finite intersections can be "constructed" inductively by iterating binary intersection ω-many times. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ 𝑅 = (𝑢 ∈ V ↦ ran (𝑦 ∈ 𝑢, 𝑧 ∈ 𝑢 ↦ (𝑦 ∩ 𝑧)))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (fi‘𝐴) = ∪ (rec(𝑅, 𝐴) “ ω))
Theorem	fifo 9169*	Describe a surjection from nonempty finite sets to finite intersections. (Contributed by Mario Carneiro, 18-May-2015.)
⊢ 𝐹 = (𝑦 ∈ ((𝒫 𝐴 ∩ Fin) ∖ {∅}) ↦ ∩ 𝑦)    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝐹:((𝒫 𝐴 ∩ Fin) ∖ {∅})–onto→(fi‘𝐴))
2.4.33  Hall's marriage theorem
Theorem	marypha1lem 9170*	Core induction for Philip Hall's marriage theorem. (Contributed by Stefan O'Rear, 19-Feb-2015.)
⊢ (𝐴 ∈ Fin → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝐴 × 𝑏)(∀𝑑 ∈ 𝒫 𝐴𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝐴–1-1→V)))
Theorem	marypha1 9171*	(Philip) Hall's marriage theorem, sufficiency: a finite relation contains an injection if there is no subset of its domain which would be forced to violate the pigeonhole principle. (Contributed by Stefan O'Rear, 20-Feb-2015.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝐶 ⊆ (𝐴 × 𝐵))    &   ⊢ ((𝜑 ∧ 𝑑 ⊆ 𝐴) → 𝑑 ≼ (𝐶 “ 𝑑))    ⇒   ⊢ (𝜑 → ∃𝑓 ∈ 𝒫 𝐶𝑓:𝐴–1-1→𝐵)
Theorem	marypha2lem1 9172*	Lemma for marypha2 9176. Properties of the used relation. (Contributed by Stefan O'Rear, 20-Feb-2015.)
⊢ 𝑇 = ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥))    ⇒   ⊢ 𝑇 ⊆ (𝐴 × ∪ ran 𝐹)
Theorem	marypha2lem2 9173*	Lemma for marypha2 9176. Properties of the used relation. (Contributed by Stefan O'Rear, 20-Feb-2015.)
⊢ 𝑇 = ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥))    ⇒   ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))}
Theorem	marypha2lem3 9174*	Lemma for marypha2 9176. Properties of the used relation. (Contributed by Stefan O'Rear, 20-Feb-2015.)
⊢ 𝑇 = ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥))    ⇒   ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐺 ⊆ 𝑇 ↔ ∀𝑥 ∈ 𝐴 (𝐺‘𝑥) ∈ (𝐹‘𝑥)))
Theorem	marypha2lem4 9175*	Lemma for marypha2 9176. Properties of the used relation. (Contributed by Stefan O'Rear, 20-Feb-2015.)
⊢ 𝑇 = ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥))    ⇒   ⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ⊆ 𝐴) → (𝑇 “ 𝑋) = ∪ (𝐹 “ 𝑋))
Theorem	marypha2 9176*	Version of marypha1 9171 using a functional family of sets instead of a relation. (Contributed by Stefan O'Rear, 20-Feb-2015.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐹:𝐴⟶Fin)    &   ⊢ ((𝜑 ∧ 𝑑 ⊆ 𝐴) → 𝑑 ≼ ∪ (𝐹 “ 𝑑))    ⇒   ⊢ (𝜑 → ∃𝑔(𝑔:𝐴–1-1→V ∧ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝐹‘𝑥)))
2.4.34  Supremum and infimum
Syntax	csup 9177	Extend class notation to include supremum of class 𝐴. Here 𝑅 is ordinarily a relation that strictly orders class 𝐵. For example, 𝑅 could be 'less than' and 𝐵 could be the set of real numbers.
class sup(𝐴, 𝐵, 𝑅)
Syntax	cinf 9178	Extend class notation to include infimum of class 𝐴. Here 𝑅 is ordinarily a relation that strictly orders class 𝐵. For example, 𝑅 could be 'less than' and 𝐵 could be the set of real numbers.
class inf(𝐴, 𝐵, 𝑅)
Definition	df-sup 9179*	Define the supremum of class 𝐴. It is meaningful when 𝑅 is a relation that strictly orders 𝐵 and when the supremum exists. For example, 𝑅 could be 'less than', 𝐵 could be the set of real numbers, and 𝐴 could be the set of all positive reals whose square is less than 2; in this case the supremum is defined as the square root of 2 per sqrtval 14946. See dfsup2 9181 for alternate definition not requiring dummy variables. (Contributed by NM, 22-May-1999.)
⊢ sup(𝐴, 𝐵, 𝑅) = ∪ {𝑥 ∈ 𝐵 ∣ (∀𝑦 ∈ 𝐴 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐵 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦𝑅𝑧))}
Definition	df-inf 9180	Define the infimum of class 𝐴. It is meaningful when 𝑅 is a relation that strictly orders 𝐵 and when the infimum exists. For example, 𝑅 could be 'less than', 𝐵 could be the set of real numbers, and 𝐴 could be the set of all positive reals; in this case the infimum is 0. The infimum is defined as the supremum using the converse ordering relation. In the given example, 0 is the supremum of all reals (greatest real number) for which all positive reals are greater. (Contributed by AV, 2-Sep-2020.)
⊢ inf(𝐴, 𝐵, 𝑅) = sup(𝐴, 𝐵, ◡𝑅)
Theorem	dfsup2 9181	Quantifier-free definition of supremum. (Contributed by Scott Fenton, 19-Feb-2013.)
⊢ sup(𝐵, 𝐴, 𝑅) = ∪ (𝐴 ∖ ((◡𝑅 “ 𝐵) ∪ (𝑅 “ (𝐴 ∖ (◡𝑅 “ 𝐵)))))
Theorem	supeq1 9182	Equality theorem for supremum. (Contributed by NM, 22-May-1999.)
⊢ (𝐵 = 𝐶 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅))
Theorem	supeq1d 9183	Equality deduction for supremum. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅))
Theorem	supeq1i 9184	Equality inference for supremum. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ 𝐵 = 𝐶    ⇒   ⊢ sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅)
Theorem	supeq2 9185	Equality theorem for supremum. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝐵 = 𝐶 → sup(𝐴, 𝐵, 𝑅) = sup(𝐴, 𝐶, 𝑅))
Theorem	supeq3 9186	Equality theorem for supremum. (Contributed by Scott Fenton, 13-Jun-2018.)
⊢ (𝑅 = 𝑆 → sup(𝐴, 𝐵, 𝑅) = sup(𝐴, 𝐵, 𝑆))
Theorem	supeq123d 9187	Equality deduction for supremum. (Contributed by Stefan O'Rear, 20-Jan-2015.)
⊢ (𝜑 → 𝐴 = 𝐷)    &   ⊢ (𝜑 → 𝐵 = 𝐸)    &   ⊢ (𝜑 → 𝐶 = 𝐹)    ⇒   ⊢ (𝜑 → sup(𝐴, 𝐵, 𝐶) = sup(𝐷, 𝐸, 𝐹))
Theorem	nfsup 9188	Hypothesis builder for supremum. (Contributed by Mario Carneiro, 20-Mar-2014.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑥𝑅    ⇒   ⊢ Ⅎ𝑥sup(𝐴, 𝐵, 𝑅)
Theorem	supmo 9189*	Any class 𝐵 has at most one supremum in 𝐴 (where 𝑅 is interpreted as 'less than'). (Contributed by NM, 5-May-1999.) (Revised by Mario Carneiro, 24-Dec-2016.)
⊢ (𝜑 → 𝑅 Or 𝐴)    ⇒   ⊢ (𝜑 → ∃*𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)))
Theorem	supexd 9190	A supremum is a set. (Contributed by NM, 22-May-1999.) (Revised by Mario Carneiro, 24-Dec-2016.)
⊢ (𝜑 → 𝑅 Or 𝐴)    ⇒   ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) ∈ V)
Theorem	supeu 9191*	A supremum is unique. Similar to Theorem I.26 of [Apostol] p. 24 (but for suprema in general). (Contributed by NM, 12-Oct-2004.)
⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)))    ⇒   ⊢ (𝜑 → ∃!𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)))
Theorem	supval2 9192*	Alternate expression for the supremum. (Contributed by Mario Carneiro, 24-Dec-2016.) (Revised by Thierry Arnoux, 24-Sep-2017.)
⊢ (𝜑 → 𝑅 Or 𝐴)    ⇒   ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) = (℩𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))))
Theorem	eqsup 9193*	Sufficient condition for an element to be equal to the supremum. (Contributed by Mario Carneiro, 21-Apr-2015.)
⊢ (𝜑 → 𝑅 Or 𝐴)    ⇒   ⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝐶𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝐶 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)) → sup(𝐵, 𝐴, 𝑅) = 𝐶))
Theorem	eqsupd 9194*	Sufficient condition for an element to be equal to the supremum. (Contributed by Mario Carneiro, 21-Apr-2015.)
⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ¬ 𝐶𝑅𝑦)    &   ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝐶)) → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)    ⇒   ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) = 𝐶)
Theorem	supcl 9195*	A supremum belongs to its base class (closure law). See also supub 9196 and suplub 9197. (Contributed by NM, 12-Oct-2004.)
⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)))    ⇒   ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) ∈ 𝐴)
Theorem	supub 9196*	A supremum is an upper bound. See also supcl 9195 and suplub 9197. This proof demonstrates how to expand an iota-based definition (df-iota 6390) using riotacl2 7245. (Contributed by NM, 12-Oct-2004.) (Proof shortened by Mario Carneiro, 24-Dec-2016.)
⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)))    ⇒   ⊢ (𝜑 → (𝐶 ∈ 𝐵 → ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝐶))
Theorem	suplub 9197*	A supremum is the least upper bound. See also supcl 9195 and supub 9196. (Contributed by NM, 13-Oct-2004.) (Revised by Mario Carneiro, 24-Dec-2016.)
⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)))    ⇒   ⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ 𝐶𝑅sup(𝐵, 𝐴, 𝑅)) → ∃𝑧 ∈ 𝐵 𝐶𝑅𝑧))
Theorem	suplub2 9198*	Bidirectional form of suplub 9197. (Contributed by Mario Carneiro, 6-Sep-2014.)
⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)))    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    ⇒   ⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → (𝐶𝑅sup(𝐵, 𝐴, 𝑅) ↔ ∃𝑧 ∈ 𝐵 𝐶𝑅𝑧))
Theorem	supnub 9199*	An upper bound is not less than the supremum. (Contributed by NM, 13-Oct-2004.)
⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)))    ⇒   ⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ ∀𝑧 ∈ 𝐵 ¬ 𝐶𝑅𝑧) → ¬ 𝐶𝑅sup(𝐵, 𝐴, 𝑅)))
Theorem	supex 9200	A supremum is a set. (Contributed by NM, 22-May-1999.)
⊢ 𝑅 Or 𝐴    ⇒   ⊢ sup(𝐵, 𝐴, 𝑅) ∈ V