P. 95 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 9401-9500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mapfienlem1 9401*	Lemma 1 for mapfien 9404. (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 9402*	Lemma 2 for mapfien 9404. (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 9403*	Lemma 3 for mapfien 9404. (Contributed by AV, 3-Jul-2019.) (Revised by AV, 28-Jul-2024.)
⊢ 𝑆 = {𝑥 ∈ (𝐵 ↑m 𝐴) ∣ 𝑥 finSupp 𝑍}    &   ⊢ 𝑇 = {𝑥 ∈ (𝐷 ↑m 𝐶) ∣ 𝑥 finSupp 𝑊}    &   ⊢ 𝑊 = (𝐺‘𝑍)    &   ⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴)    &   ⊢ (𝜑 → 𝐺:𝐵–1-1-onto→𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑇) → ((◡𝐺 ∘ 𝑔) ∘ ◡𝐹) ∈ 𝑆)
Theorem	mapfien 9404*	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 9405*	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 9406	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 9407*	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 9410). (Contributed by FL, 27-Apr-2008.)
⊢ fi = (𝑥 ∈ V ↦ {𝑧 ∣ ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑧 = ∩ 𝑦})
Theorem	fival 9408*	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 9409*	Specific properties of an element of (fi‘𝐵). (Contributed by FL, 27-Apr-2008.) (Revised by Mario Carneiro, 24-Nov-2013.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∈ (fi‘𝐵) ↔ ∃𝑥 ∈ (𝒫 𝐵 ∩ Fin)𝐴 = ∩ 𝑥))
Theorem	elfi2 9410*	The empty intersection need not be considered in the set of finite intersections. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (fi‘𝐵) ↔ ∃𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})𝐴 = ∩ 𝑥))
Theorem	elfir 9411	Sufficient condition for an element of (fi‘𝐵). (Contributed by Mario Carneiro, 24-Nov-2013.)
⊢ ((𝐵 ∈ 𝑉 ∧ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin)) → ∩ 𝐴 ∈ (fi‘𝐵))
Theorem	intrnfi 9412	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 9413*	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 9414	The intersection of two sets is a finite intersection. (Contributed by Thierry Arnoux, 6-Jan-2017.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 ∩ 𝐵) ∈ (fi‘𝑋))
Theorem	ssfii 9415	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 9416	The set of finite intersections of the empty set. (Contributed by Mario Carneiro, 30-Aug-2015.)
⊢ (fi‘∅) = ∅
Theorem	fieq0 9417	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 9418	The elements of (fi‘𝐶) are closed under finite intersection. (Contributed by Mario Carneiro, 24-Nov-2013.)
⊢ ((𝐴 ∈ (fi‘𝐶) ∧ 𝐵 ∈ (fi‘𝐶)) → (𝐴 ∩ 𝐵) ∈ (fi‘𝐶))
Theorem	dffi2 9419*	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 9420	Subset relationship for function fi. (Contributed by Jeff Hankins, 7-Oct-2009.) (Revised by Mario Carneiro, 24-Nov-2013.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵) → (fi‘𝐴) ⊆ (fi‘𝐵))
Theorem	inficl 9421*	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 9422	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 9423	A singleton is closed under finite intersections. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ (fi‘{𝐴}) = {𝐴}
Theorem	fiuni 9424	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 9425	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 9426*	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 9427*	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 9428*	Describe a surjection from nonempty finite sets to finite intersections. (Contributed by Mario Carneiro, 18-May-2015.)
⊢ 𝐹 = (𝑦 ∈ ((𝒫 𝐴 ∩ Fin) ∖ {∅}) ↦ ∩ 𝑦)    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝐹:((𝒫 𝐴 ∩ Fin) ∖ {∅})–onto→(fi‘𝐴))
2.4.37  Hall's marriage theorem
Theorem	marypha1lem 9429*	Core induction for Philip Hall's marriage theorem. (Contributed by Stefan O'Rear, 19-Feb-2015.)
⊢ (𝐴 ∈ Fin → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝐴 × 𝑏)(∀𝑑 ∈ 𝒫 𝐴𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝐴–1-1→V)))
Theorem	marypha1 9430*	(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 9431*	Lemma for marypha2 9435. Properties of the used relation. (Contributed by Stefan O'Rear, 20-Feb-2015.)
⊢ 𝑇 = ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥))    ⇒   ⊢ 𝑇 ⊆ (𝐴 × ∪ ran 𝐹)
Theorem	marypha2lem2 9432*	Lemma for marypha2 9435. Properties of the used relation. (Contributed by Stefan O'Rear, 20-Feb-2015.)
⊢ 𝑇 = ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥))    ⇒   ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))}
Theorem	marypha2lem3 9433*	Lemma for marypha2 9435. Properties of the used relation. (Contributed by Stefan O'Rear, 20-Feb-2015.)
⊢ 𝑇 = ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥))    ⇒   ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐺 ⊆ 𝑇 ↔ ∀𝑥 ∈ 𝐴 (𝐺‘𝑥) ∈ (𝐹‘𝑥)))
Theorem	marypha2lem4 9434*	Lemma for marypha2 9435. Properties of the used relation. (Contributed by Stefan O'Rear, 20-Feb-2015.)
⊢ 𝑇 = ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥))    ⇒   ⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ⊆ 𝐴) → (𝑇 “ 𝑋) = ∪ (𝐹 “ 𝑋))
Theorem	marypha2 9435*	Version of marypha1 9430 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.38  Supremum and infimum
Syntax	csup 9436	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 9437	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 9438*	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 15410. See dfsup2 9440 for alternate definition not requiring dummy variables. (Contributed by NM, 22-May-1999.)
⊢ sup(𝐴, 𝐵, 𝑅) = ∪ {𝑥 ∈ 𝐵 ∣ (∀𝑦 ∈ 𝐴 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐵 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦𝑅𝑧))}
Definition	df-inf 9439	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 9440	Quantifier-free definition of supremum. (Contributed by Scott Fenton, 19-Feb-2013.)
⊢ sup(𝐵, 𝐴, 𝑅) = ∪ (𝐴 ∖ ((◡𝑅 “ 𝐵) ∪ (𝑅 “ (𝐴 ∖ (◡𝑅 “ 𝐵)))))
Theorem	supeq1 9441	Equality theorem for supremum. (Contributed by NM, 22-May-1999.)
⊢ (𝐵 = 𝐶 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅))
Theorem	supeq1d 9442	Equality deduction for supremum. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅))
Theorem	supeq1i 9443	Equality inference for supremum. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ 𝐵 = 𝐶    ⇒   ⊢ sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅)
Theorem	supeq2 9444	Equality theorem for supremum. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝐵 = 𝐶 → sup(𝐴, 𝐵, 𝑅) = sup(𝐴, 𝐶, 𝑅))
Theorem	supeq3 9445	Equality theorem for supremum. (Contributed by Scott Fenton, 13-Jun-2018.)
⊢ (𝑅 = 𝑆 → sup(𝐴, 𝐵, 𝑅) = sup(𝐴, 𝐵, 𝑆))
Theorem	supeq123d 9446	Equality deduction for supremum. (Contributed by Stefan O'Rear, 20-Jan-2015.)
⊢ (𝜑 → 𝐴 = 𝐷)    &   ⊢ (𝜑 → 𝐵 = 𝐸)    &   ⊢ (𝜑 → 𝐶 = 𝐹)    ⇒   ⊢ (𝜑 → sup(𝐴, 𝐵, 𝐶) = sup(𝐷, 𝐸, 𝐹))
Theorem	nfsup 9447	Hypothesis builder for supremum. (Contributed by Mario Carneiro, 20-Mar-2014.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑥𝑅    ⇒   ⊢ Ⅎ𝑥sup(𝐴, 𝐵, 𝑅)
Theorem	supmo 9448*	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 9449	A supremum is a set. (Contributed by NM, 22-May-1999.) (Revised by Mario Carneiro, 24-Dec-2016.)
⊢ (𝜑 → 𝑅 Or 𝐴)    ⇒   ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) ∈ V)
Theorem	supeu 9450*	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 9451*	Alternate expression for the supremum. (Contributed by Mario Carneiro, 24-Dec-2016.) (Revised by Thierry Arnoux, 24-Sep-2017.)
⊢ (𝜑 → 𝑅 Or 𝐴)    ⇒   ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) = (℩𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))))
Theorem	eqsup 9452*	Sufficient condition for an element to be equal to the supremum. (Contributed by Mario Carneiro, 21-Apr-2015.)
⊢ (𝜑 → 𝑅 Or 𝐴)    ⇒   ⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝐶𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝐶 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)) → sup(𝐵, 𝐴, 𝑅) = 𝐶))
Theorem	eqsupd 9453*	Sufficient condition for an element to be equal to the supremum. (Contributed by Mario Carneiro, 21-Apr-2015.)
⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ¬ 𝐶𝑅𝑦)    &   ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝐶)) → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)    ⇒   ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) = 𝐶)
Theorem	supcl 9454*	A supremum belongs to its base class (closure law). See also supub 9455 and suplub 9456. (Contributed by NM, 12-Oct-2004.)
⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)))    ⇒   ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) ∈ 𝐴)
Theorem	supub 9455*	A supremum is an upper bound. See also supcl 9454 and suplub 9456. This proof demonstrates how to expand an iota-based definition (df-iota 6494) using riotacl2 7394. (Contributed by NM, 12-Oct-2004.) (Proof shortened by Mario Carneiro, 24-Dec-2016.)
⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)))    ⇒   ⊢ (𝜑 → (𝐶 ∈ 𝐵 → ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝐶))
Theorem	suplub 9456*	A supremum is the least upper bound. See also supcl 9454 and supub 9455. (Contributed by NM, 13-Oct-2004.) (Revised by Mario Carneiro, 24-Dec-2016.)
⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)))    ⇒   ⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ 𝐶𝑅sup(𝐵, 𝐴, 𝑅)) → ∃𝑧 ∈ 𝐵 𝐶𝑅𝑧))
Theorem	suplub2 9457*	Bidirectional form of suplub 9456. (Contributed by Mario Carneiro, 6-Sep-2014.)
⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)))    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    ⇒   ⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → (𝐶𝑅sup(𝐵, 𝐴, 𝑅) ↔ ∃𝑧 ∈ 𝐵 𝐶𝑅𝑧))
Theorem	supnub 9458*	An upper bound is not less than the supremum. (Contributed by NM, 13-Oct-2004.)
⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)))    ⇒   ⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ ∀𝑧 ∈ 𝐵 ¬ 𝐶𝑅𝑧) → ¬ 𝐶𝑅sup(𝐵, 𝐴, 𝑅)))
Theorem	supssd 9459*	Inequality deduction for supremum of a subset. (Contributed by Thierry Arnoux, 21-Mar-2017.)
⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)))    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐶 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐶 𝑦𝑅𝑧)))    ⇒   ⊢ (𝜑 → ¬ sup(𝐶, 𝐴, 𝑅)𝑅sup(𝐵, 𝐴, 𝑅))
Theorem	supex 9460	A supremum is a set. (Contributed by NM, 22-May-1999.)
⊢ 𝑅 Or 𝐴    ⇒   ⊢ sup(𝐵, 𝐴, 𝑅) ∈ V
Theorem	sup00 9461	The supremum under an empty base set is always the empty set. (Contributed by AV, 4-Sep-2020.)
⊢ sup(𝐵, ∅, 𝑅) = ∅
Theorem	sup0riota 9462*	The supremum of an empty set is the smallest element of the base set. (Contributed by AV, 4-Sep-2020.)
⊢ (𝑅 Or 𝐴 → sup(∅, 𝐴, 𝑅) = (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑦𝑅𝑥))
Theorem	sup0 9463*	The supremum of an empty set under a base set which has a unique smallest element is the smallest element of the base set. (Contributed by AV, 4-Sep-2020.)
⊢ ((𝑅 Or 𝐴 ∧ (𝑋 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑦𝑅𝑋) ∧ ∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑦𝑅𝑥) → sup(∅, 𝐴, 𝑅) = 𝑋)
Theorem	supmax 9464*	The greatest element of a set is its supremum. Note that the converse is not true; the supremum might not be an element of the set considered. (Contributed by Jeff Hoffman, 17-Jun-2008.) (Proof shortened by OpenAI, 30-Mar-2020.)
⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ¬ 𝐶𝑅𝑦)    ⇒   ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) = 𝐶)
Theorem	fisup2g 9465*	A finite set satisfies the conditions to have a supremum. (Contributed by Mario Carneiro, 28-Apr-2015.)
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ Fin ∧ 𝐵 ≠ ∅ ∧ 𝐵 ⊆ 𝐴)) → ∃𝑥 ∈ 𝐵 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)))
Theorem	fisupcl 9466	A nonempty finite set contains its supremum. (Contributed by Jeff Madsen, 9-May-2011.)
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ Fin ∧ 𝐵 ≠ ∅ ∧ 𝐵 ⊆ 𝐴)) → sup(𝐵, 𝐴, 𝑅) ∈ 𝐵)
Theorem	supgtoreq 9467	The supremum of a finite set is greater than or equal to all the elements of the set. (Contributed by AV, 1-Oct-2019.)
⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑆 = sup(𝐵, 𝐴, 𝑅))    ⇒   ⊢ (𝜑 → (𝐶𝑅𝑆 ∨ 𝐶 = 𝑆))
Theorem	suppr 9468	The supremum of a pair. (Contributed by NM, 17-Jun-2007.) (Proof shortened by Mario Carneiro, 24-Dec-2016.)
⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → sup({𝐵, 𝐶}, 𝐴, 𝑅) = if(𝐶𝑅𝐵, 𝐵, 𝐶))
Theorem	supsn 9469	The supremum of a singleton. (Contributed by NM, 2-Oct-2007.)
⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴) → sup({𝐵}, 𝐴, 𝑅) = 𝐵)
Theorem	supisolem 9470*	Lemma for supiso 9472. (Contributed by Mario Carneiro, 24-Dec-2016.)
⊢ (𝜑 → 𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵))    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐴)    ⇒   ⊢ ((𝜑 ∧ 𝐷 ∈ 𝐴) → ((∀𝑦 ∈ 𝐶 ¬ 𝐷𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝐷 → ∃𝑧 ∈ 𝐶 𝑦𝑅𝑧)) ↔ (∀𝑤 ∈ (𝐹 “ 𝐶) ¬ (𝐹‘𝐷)𝑆𝑤 ∧ ∀𝑤 ∈ 𝐵 (𝑤𝑆(𝐹‘𝐷) → ∃𝑣 ∈ (𝐹 “ 𝐶)𝑤𝑆𝑣))))
Theorem	supisoex 9471*	Lemma for supiso 9472. (Contributed by Mario Carneiro, 24-Dec-2016.)
⊢ (𝜑 → 𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵))    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐶 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐶 𝑦𝑅𝑧)))    ⇒   ⊢ (𝜑 → ∃𝑢 ∈ 𝐵 (∀𝑤 ∈ (𝐹 “ 𝐶) ¬ 𝑢𝑆𝑤 ∧ ∀𝑤 ∈ 𝐵 (𝑤𝑆𝑢 → ∃𝑣 ∈ (𝐹 “ 𝐶)𝑤𝑆𝑣)))
Theorem	supiso 9472*	Image of a supremum under an isomorphism. (Contributed by Mario Carneiro, 24-Dec-2016.)
⊢ (𝜑 → 𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵))    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐶 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐶 𝑦𝑅𝑧)))    &   ⊢ (𝜑 → 𝑅 Or 𝐴)    ⇒   ⊢ (𝜑 → sup((𝐹 “ 𝐶), 𝐵, 𝑆) = (𝐹‘sup(𝐶, 𝐴, 𝑅)))
Theorem	infeq1 9473	Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.)
⊢ (𝐵 = 𝐶 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅))
Theorem	infeq1d 9474	Equality deduction for infimum. (Contributed by AV, 2-Sep-2020.)
⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅))
Theorem	infeq1i 9475	Equality inference for infimum. (Contributed by AV, 2-Sep-2020.)
⊢ 𝐵 = 𝐶    ⇒   ⊢ inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅)
Theorem	infeq2 9476	Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.)
⊢ (𝐵 = 𝐶 → inf(𝐴, 𝐵, 𝑅) = inf(𝐴, 𝐶, 𝑅))
Theorem	infeq3 9477	Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.)
⊢ (𝑅 = 𝑆 → inf(𝐴, 𝐵, 𝑅) = inf(𝐴, 𝐵, 𝑆))
Theorem	infeq123d 9478	Equality deduction for infimum. (Contributed by AV, 2-Sep-2020.)
⊢ (𝜑 → 𝐴 = 𝐷)    &   ⊢ (𝜑 → 𝐵 = 𝐸)    &   ⊢ (𝜑 → 𝐶 = 𝐹)    ⇒   ⊢ (𝜑 → inf(𝐴, 𝐵, 𝐶) = inf(𝐷, 𝐸, 𝐹))
Theorem	nfinf 9479	Hypothesis builder for infimum. (Contributed by AV, 2-Sep-2020.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑥𝑅    ⇒   ⊢ Ⅎ𝑥inf(𝐴, 𝐵, 𝑅)
Theorem	infexd 9480	An infimum is a set. (Contributed by AV, 2-Sep-2020.)
⊢ (𝜑 → 𝑅 Or 𝐴)    ⇒   ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) ∈ V)
Theorem	eqinf 9481*	Sufficient condition for an element to be equal to the infimum. (Contributed by AV, 2-Sep-2020.)
⊢ (𝜑 → 𝑅 Or 𝐴)    ⇒   ⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝐶 ∧ ∀𝑦 ∈ 𝐴 (𝐶𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)) → inf(𝐵, 𝐴, 𝑅) = 𝐶))
Theorem	eqinfd 9482*	Sufficient condition for an element to be equal to the infimum. (Contributed by AV, 3-Sep-2020.)
⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ¬ 𝑦𝑅𝐶)    &   ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝐶𝑅𝑦)) → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)    ⇒   ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) = 𝐶)
Theorem	infval 9483*	Alternate expression for the infimum. (Contributed by AV, 2-Sep-2020.)
⊢ (𝜑 → 𝑅 Or 𝐴)    ⇒   ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) = (℩𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))))
Theorem	infcllem 9484*	Lemma for infcl 9485, inflb 9486, infglb 9487, etc. (Contributed by AV, 3-Sep-2020.)
⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥◡𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦◡𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦◡𝑅𝑧)))
Theorem	infcl 9485*	An infimum belongs to its base class (closure law). See also inflb 9486 and infglb 9487. (Contributed by AV, 3-Sep-2020.)
⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)))    ⇒   ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) ∈ 𝐴)
Theorem	inflb 9486*	An infimum is a lower bound. See also infcl 9485 and infglb 9487. (Contributed by AV, 3-Sep-2020.)
⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)))    ⇒   ⊢ (𝜑 → (𝐶 ∈ 𝐵 → ¬ 𝐶𝑅inf(𝐵, 𝐴, 𝑅)))
Theorem	infglb 9487*	An infimum is the greatest lower bound. See also infcl 9485 and inflb 9486. (Contributed by AV, 3-Sep-2020.)
⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)))    ⇒   ⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ inf(𝐵, 𝐴, 𝑅)𝑅𝐶) → ∃𝑧 ∈ 𝐵 𝑧𝑅𝐶))
Theorem	infglbb 9488*	Bidirectional form of infglb 9487. (Contributed by AV, 3-Sep-2020.)
⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)))    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    ⇒   ⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → (inf(𝐵, 𝐴, 𝑅)𝑅𝐶 ↔ ∃𝑧 ∈ 𝐵 𝑧𝑅𝐶))
Theorem	infnlb 9489*	A lower bound is not greater than the infimum. (Contributed by AV, 3-Sep-2020.)
⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)))    ⇒   ⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ ∀𝑧 ∈ 𝐵 ¬ 𝑧𝑅𝐶) → ¬ inf(𝐵, 𝐴, 𝑅)𝑅𝐶))
Theorem	infssd 9490*	Inequality deduction for infimum of a subset. (Contributed by AV, 4-Oct-2020.)
⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐵)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐶 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐶 𝑧𝑅𝑦)))    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)))    ⇒   ⊢ (𝜑 → ¬ inf(𝐶, 𝐴, 𝑅)𝑅inf(𝐵, 𝐴, 𝑅))
Theorem	infex 9491	An infimum is a set. (Contributed by AV, 3-Sep-2020.)
⊢ 𝑅 Or 𝐴    ⇒   ⊢ inf(𝐵, 𝐴, 𝑅) ∈ V
Theorem	infmin 9492*	The smallest element of a set is its infimum. Note that the converse is not true; the infimum might not be an element of the set considered. (Contributed by AV, 3-Sep-2020.)
⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ¬ 𝑦𝑅𝐶)    ⇒   ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) = 𝐶)
Theorem	infmo 9493*	Any class 𝐵 has at most one infimum in 𝐴 (where 𝑅 is interpreted as 'less than'). (Contributed by AV, 6-Oct-2020.)
⊢ (𝜑 → 𝑅 Or 𝐴)    ⇒   ⊢ (𝜑 → ∃*𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)))
Theorem	infeu 9494*	An infimum is unique. (Contributed by AV, 6-Oct-2020.)
⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)))    ⇒   ⊢ (𝜑 → ∃!𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)))
Theorem	fimin2g 9495*	A finite set has a minimum under a total order. (Contributed by AV, 6-Oct-2020.)
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑦𝑅𝑥)
Theorem	fiming 9496*	A finite set has a minimum under a total order. (Contributed by AV, 6-Oct-2020.)
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → 𝑥𝑅𝑦))
Theorem	fiinfg 9497*	Lemma showing existence and closure of infimum of a finite set. (Contributed by AV, 6-Oct-2020.)
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐴 𝑧𝑅𝑦)))
Theorem	fiinf2g 9498*	A finite set satisfies the conditions to have an infimum. (Contributed by AV, 6-Oct-2020.)
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ Fin ∧ 𝐵 ≠ ∅ ∧ 𝐵 ⊆ 𝐴)) → ∃𝑥 ∈ 𝐵 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)))
Theorem	fiinfcl 9499	A nonempty finite set contains its infimum. (Contributed by AV, 3-Sep-2020.)
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ Fin ∧ 𝐵 ≠ ∅ ∧ 𝐵 ⊆ 𝐴)) → inf(𝐵, 𝐴, 𝑅) ∈ 𝐵)
Theorem	infltoreq 9500	The infimum of a finite set is less than or equal to all the elements of the set. (Contributed by AV, 4-Sep-2020.)
⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑆 = inf(𝐵, 𝐴, 𝑅))    ⇒   ⊢ (𝜑 → (𝑆𝑅𝐶 ∨ 𝐶 = 𝑆))