P. 84 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 8301-8400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ressuppfi 8301	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.)
|- ( ph -> ( dom F \ B ) e. Fin )   &    |- ( ph -> F e. W )   &    |- ( ph -> G = ( F |` B ) )   &    |- ( ph -> ( G supp Z ) e. Fin )   &    |- ( ph -> Z e. V )   =>    |- ( ph -> ( F supp Z ) e. Fin )
Theorem	resfsupp 8302	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.)
|- ( ph -> ( dom F \ B ) e. Fin )   &    |- ( ph -> F e. W )   &    |- ( ph -> Fun F )   &    |- ( ph -> G = ( F |` B ) )   &    |- ( ph -> G finSupp Z )   &    |- ( ph -> Z e. V )   =>    |- ( ph -> F finSupp Z )
Theorem	resfifsupp 8303	The restriction of a function to a finite set is finitely supported. (Contributed by AV, 12-Dec-2019.)
|- ( ph -> Fun F )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> Z e. V )   =>    |- ( ph -> ( F |` X ) finSupp Z )
Theorem	frnfsuppbi 8304	Two ways of saying that a function with known codomain is finitely supported. (Contributed by AV, 8-Jul-2019.)
|- ( ( I e. V /\ Z e. W ) -> ( F : I --> S -> ( F finSupp Z <-> ( `' F " ( S \ { Z } ) ) e. Fin ) ) )
Theorem	fsuppmptif 8305*	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.)
|- ( ph -> F : A --> B )   &    |- ( ph -> A e. V )   &    |- ( ph -> Z e. W )   &    |- ( ph -> F finSupp Z )   =>    |- ( ph -> ( k e. A |-> if ( k e. D , ( F ` k ) , Z ) ) finSupp Z )
Theorem	fsuppcolem 8306	Lemma for fsuppco 8307. Formula building theorem for finite supports: rearranging the index set. (Contributed by Stefan O'Rear, 21-Mar-2015.)
|- ( ph -> ( `' F " ( _V \ { Z } ) ) e. Fin )   &    |- ( ph -> G : X -1-1-> Y )   =>    |- ( ph -> ( `' ( F o. G ) " ( _V \ { Z } ) ) e. Fin )
Theorem	fsuppco 8307	The composition of a 1-1 function with a finitely supported function is finitely supported. (Contributed by AV, 28-May-2019.)
|- ( ph -> F finSupp Z )   &    |- ( ph -> G : X -1-1-> Y )   &    |- ( ph -> Z e. W )   &    |- ( ph -> F e. V )   =>    |- ( ph -> ( F o. G ) finSupp Z )
Theorem	fsuppco2 8308	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 8309 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.)
|- ( ph -> Z e. W )   &    |- ( ph -> F : A --> B )   &    |- ( ph -> G : B --> B )   &    |- ( ph -> A e. U )   &    |- ( ph -> B e. V )   &    |- ( ph -> F finSupp Z )   &    |- ( ph -> ( G ` Z ) = Z )   =>    |- ( ph -> ( G o. F ) finSupp Z )
Theorem	fsuppcor 8309	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.)
|- ( ph -> .0. e. W )   &    |- ( ph -> Z e. B )   &    |- ( ph -> F : A --> C )   &    |- ( ph -> G : B --> D )   &    |- ( ph -> C C_ B )   &    |- ( ph -> A e. U )   &    |- ( ph -> B e. V )   &    |- ( ph -> F finSupp Z )   &    |- ( ph -> ( G ` Z ) = .0. )   =>    |- ( ph -> ( G o. F ) finSupp .0. )
Theorem	mapfienlem1 8310*	Lemma 1 for mapfien 8313. (Contributed by AV, 3-Jul-2019.)
|- S = { x e. ( B ^m A ) | x finSupp Z }   &    |- T = { x e. ( D ^m C ) | x finSupp W }   &    |- W = ( G ` Z )   &    |- ( ph -> F : C -1-1-onto-> A )   &    |- ( ph -> G : B -1-1-onto-> D )   &    |- ( ph -> A e. _V )   &    |- ( ph -> B e. _V )   &    |- ( ph -> C e. _V )   &    |- ( ph -> D e. _V )   &    |- ( ph -> Z e. B )   =>    |- ( ( ph /\ f e. S ) -> ( G o. ( f o. F ) ) finSupp W )
Theorem	mapfienlem2 8311*	Lemma 2 for mapfien 8313. (Contributed by AV, 3-Jul-2019.)
|- S = { x e. ( B ^m A ) | x finSupp Z }   &    |- T = { x e. ( D ^m C ) | x finSupp W }   &    |- W = ( G ` Z )   &    |- ( ph -> F : C -1-1-onto-> A )   &    |- ( ph -> G : B -1-1-onto-> D )   &    |- ( ph -> A e. _V )   &    |- ( ph -> B e. _V )   &    |- ( ph -> C e. _V )   &    |- ( ph -> D e. _V )   &    |- ( ph -> Z e. B )   =>    |- ( ( ph /\ g e. T ) -> ( ( `' G o. g ) o. `' F ) finSupp Z )
Theorem	mapfienlem3 8312*	Lemma 3 for mapfien 8313. (Contributed by AV, 3-Jul-2019.)
|- S = { x e. ( B ^m A ) | x finSupp Z }   &    |- T = { x e. ( D ^m C ) | x finSupp W }   &    |- W = ( G ` Z )   &    |- ( ph -> F : C -1-1-onto-> A )   &    |- ( ph -> G : B -1-1-onto-> D )   &    |- ( ph -> A e. _V )   &    |- ( ph -> B e. _V )   &    |- ( ph -> C e. _V )   &    |- ( ph -> D e. _V )   &    |- ( ph -> Z e. B )   =>    |- ( ( ph /\ g e. T ) -> ( ( `' G o. g ) o. `' F ) e. S )
Theorem	mapfien 8313*	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.)
|- S = { x e. ( B ^m A ) | x finSupp Z }   &    |- T = { x e. ( D ^m C ) | x finSupp W }   &    |- W = ( G ` Z )   &    |- ( ph -> F : C -1-1-onto-> A )   &    |- ( ph -> G : B -1-1-onto-> D )   &    |- ( ph -> A e. _V )   &    |- ( ph -> B e. _V )   &    |- ( ph -> C e. _V )   &    |- ( ph -> D e. _V )   &    |- ( ph -> Z e. B )   =>    |- ( ph -> ( f e. S |-> ( G o. ( f o. F ) ) ) : S -1-1-onto-> T )
Theorem	mapfien2 8314*	Equinumerousity relation for sets of finitely supported functions. (Contributed by Stefan O'Rear, 9-Jul-2015.) (Revised by AV, 7-Jul-2019.)
|- S = { x e. ( B ^m A ) | x finSupp .0. }   &    |- T = { x e. ( D ^m C ) | x finSupp W }   &    |- ( ph -> A ~~ C )   &    |- ( ph -> B ~~ D )   &    |- ( ph -> .0. e. B )   &    |- ( ph -> W e. D )   =>    |- ( ph -> S ~~ T )
Theorem	sniffsupp 8315*	A function mapping all but one arguments to zero is finitely supported. (Contributed by AV, 8-Jul-2019.)
|- ( ph -> I e. V )   &    |- ( ph -> .0. e. W )   &    |- F = ( x e. I |-> if ( x = X , A , .0. ) )   =>    |- ( ph -> F finSupp .0. )
2.4.29  Finite intersections
Syntax	cfi 8316	Extend class notation with the function whose value is the class of all the finite intersections of the elements of a given set.
class fi
Definition	df-fi 8317*	Function whose value is the class of all the finite intersections of the elements of x. (Contributed by FL, 27-Apr-2008.)
|- fi = ( x e. _V |-> { z | E. y e. ( ~P x i^i Fin ) z = |^| y } )
Theorem	fival 8318*	The set of all the finite intersections of the elements of A. (Contributed by FL, 27-Apr-2008.) (Revised by Mario Carneiro, 24-Nov-2013.)
|- ( A e. V -> ( fi ` A ) = { y | E. x e. ( ~P A i^i Fin ) y = |^| x } )
Theorem	elfi 8319*	Specific properties of an element of ( fi ` B ). (Contributed by FL, 27-Apr-2008.) (Revised by Mario Carneiro, 24-Nov-2013.)
|- ( ( A e. V /\ B e. W ) -> ( A e. ( fi ` B ) <-> E. x e. ( ~P B i^i Fin ) A = |^| x ) )
Theorem	elfi2 8320*	The empty intersection need not be considered in the set of finite intersections. (Contributed by Mario Carneiro, 21-Mar-2015.)
|- ( B e. V -> ( A e. ( fi ` B ) <-> E. x e. ( ( ~P B i^i Fin ) \ { (/) } ) A = |^| x ) )
Theorem	elfir 8321	Sufficient condition for an element of ( fi ` B ). (Contributed by Mario Carneiro, 24-Nov-2013.)
|- ( ( B e. V /\ ( A C_ B /\ A =/= (/) /\ A e. Fin ) ) -> |^| A e. ( fi ` B ) )
Theorem	intrnfi 8322	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.)
|- ( ( B e. V /\ ( F : A --> B /\ A =/= (/) /\ A e. Fin ) ) -> |^| ran F e. ( fi ` B ) )
Theorem	iinfi 8323*	An indexed intersection of elements of C is an element of the finite intersections of C. (Contributed by Mario Carneiro, 30-Aug-2015.)
|- ( ( C e. V /\ ( A. x e. A B e. C /\ A =/= (/) /\ A e. Fin ) ) -> |^|_ x e. A B e. ( fi ` C ) )
Theorem	inelfi 8324	The intersection of two sets is a finite intersection. (Contributed by Thierry Arnoux, 6-Jan-2017.)
|- ( ( X e. V /\ A e. X /\ B e. X ) -> ( A i^i B ) e. ( fi ` X ) )
Theorem	ssfii 8325	Any element of a set A is the intersection of a finite subset of A. (Contributed by FL, 27-Apr-2008.) (Proof shortened by Mario Carneiro, 21-Mar-2015.)
|- ( A e. V -> A C_ ( fi ` A ) )
Theorem	fi0 8326	The set of finite intersections of the empty set. (Contributed by Mario Carneiro, 30-Aug-2015.)
|- ( fi ` (/) ) = (/)
Theorem	fieq0 8327	If A is not empty, the class of all the finite intersections of A is not empty either. (Contributed by FL, 27-Apr-2008.) (Revised by Mario Carneiro, 24-Nov-2013.)
|- ( A e. V -> ( A = (/) <-> ( fi ` A ) = (/) ) )
Theorem	fiin 8328	The elements of ( fi ` C ) are closed under finite intersection. (Contributed by Mario Carneiro, 24-Nov-2013.)
|- ( ( A e. ( fi ` C ) /\ B e. ( fi ` C ) ) -> ( A i^i B ) e. ( fi ` C ) )
Theorem	dffi2 8329*	The set of finite intersections is the smallest set that contains A and is closed under pairwise intersection. (Contributed by Mario Carneiro, 24-Nov-2013.)
|- ( A e. V -> ( fi ` A ) = |^| { z | ( A C_ z /\ A. x e. z A. y e. z ( x i^i y ) e. z ) } )
Theorem	fiss 8330	Subset relationship for function fi. (Contributed by Jeff Hankins, 7-Oct-2009.) (Revised by Mario Carneiro, 24-Nov-2013.)
|- ( ( B e. V /\ A C_ B ) -> ( fi ` A ) C_ ( fi ` B ) )
Theorem	inficl 8331*	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.)
|- ( A e. V -> ( A. x e. A A. y e. A ( x i^i y ) e. A <-> ( fi ` A ) = A ) )
Theorem	fipwuni 8332	The set of finite intersections of a set is contained in the powerset of the union of the elements of A. (Contributed by Mario Carneiro, 24-Nov-2013.) (Proof shortened by Mario Carneiro, 21-Mar-2015.)
|- ( fi ` A ) C_ ~P U. A
Theorem	fisn 8333	A singleton is closed under finite intersections. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- ( fi ` { A } ) = { A }
Theorem	fiuni 8334	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.)
|- ( A e. V -> U. A = U. ( fi ` A ) )
Theorem	fipwss 8335	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.)
|- ( A C_ ~P X -> ( fi ` A ) C_ ~P X )
Theorem	elfiun 8336*	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.)
|- ( ( B e. D /\ C e. K ) -> ( A e. ( fi ` ( B u. C ) ) <-> ( A e. ( fi ` B ) \/ A e. ( fi ` C ) \/ E. x e. ( fi ` B ) E. y e. ( fi ` C ) A = ( x i^i y ) ) ) )
Theorem	dffi3 8337*	The set of finite intersections can be "constructed" inductively by iterating binary intersection om-many times. (Contributed by Mario Carneiro, 21-Mar-2015.)
|- R = ( u e. _V |-> ran ( y e. u , z e. u |-> ( y i^i z ) ) )   =>    |- ( A e. V -> ( fi ` A ) = U. ( rec ( R , A ) " om ) )
Theorem	fifo 8338*	Describe a surjection from nonempty finite sets to finite intersections. (Contributed by Mario Carneiro, 18-May-2015.)
|- F = ( y e. ( ( ~P A i^i Fin ) \ { (/) } ) |-> |^| y )   =>    |- ( A e. V -> F : ( ( ~P A i^i Fin ) \ { (/) } ) -onto-> ( fi ` A ) )
2.4.30  Hall's marriage theorem
Theorem	marypha1lem 8339*	Core induction for Philip Hall's marriage theorem. (Contributed by Stefan O'Rear, 19-Feb-2015.)
|- ( A e. Fin -> ( b e. Fin -> A. c e. ~P ( A X. b ) ( A. d e. ~P A d ~<_ ( c " d ) -> E. e e. ~P c e : A -1-1-> _V ) ) )
Theorem	marypha1 8340*	(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.)
|- ( ph -> A e. Fin )   &    |- ( ph -> B e. Fin )   &    |- ( ph -> C C_ ( A X. B ) )   &    |- ( ( ph /\ d C_ A ) -> d ~<_ ( C " d ) )   =>    |- ( ph -> E. f e. ~P C f : A -1-1-> B )
Theorem	marypha2lem1 8341*	Lemma for marypha2 8345. Properties of the used relation. (Contributed by Stefan O'Rear, 20-Feb-2015.)
|- T = U_ x e. A ( { x } X. ( F ` x ) )   =>    |- T C_ ( A X. U. ran F )
Theorem	marypha2lem2 8342*	Lemma for marypha2 8345. Properties of the used relation. (Contributed by Stefan O'Rear, 20-Feb-2015.)
|- T = U_ x e. A ( { x } X. ( F ` x ) )   =>    |- T = { <. x , y >. | ( x e. A /\ y e. ( F ` x ) ) }
Theorem	marypha2lem3 8343*	Lemma for marypha2 8345. Properties of the used relation. (Contributed by Stefan O'Rear, 20-Feb-2015.)
|- T = U_ x e. A ( { x } X. ( F ` x ) )   =>    |- ( ( F Fn A /\ G Fn A ) -> ( G C_ T <-> A. x e. A ( G ` x ) e. ( F ` x ) ) )
Theorem	marypha2lem4 8344*	Lemma for marypha2 8345. Properties of the used relation. (Contributed by Stefan O'Rear, 20-Feb-2015.)
|- T = U_ x e. A ( { x } X. ( F ` x ) )   =>    |- ( ( F Fn A /\ X C_ A ) -> ( T " X ) = U. ( F " X ) )
Theorem	marypha2 8345*	Version of marypha1 8340 using a functional family of sets instead of a relation. (Contributed by Stefan O'Rear, 20-Feb-2015.)
|- ( ph -> A e. Fin )   &    |- ( ph -> F : A --> Fin )   &    |- ( ( ph /\ d C_ A ) -> d ~<_ U. ( F " d ) )   =>    |- ( ph -> E. g ( g : A -1-1-> _V /\ A. x e. A ( g ` x ) e. ( F ` x ) ) )
2.4.31  Supremum and infimum
Syntax	csup 8346	Extend class notation to include supremum of class A. Here R is ordinarily a relation that strictly orders class B. For example, R could be 'less than' and B could be the set of real numbers.
class sup ( A , B , R )
Syntax	cinf 8347	Extend class notation to include infimum of class A. Here R is ordinarily a relation that strictly orders class B. For example, R could be 'less than' and B could be the set of real numbers.
class inf ( A , B , R )
Definition	df-sup 8348*	Define the supremum of class A. It is meaningful when R is a relation that strictly orders B and when the supremum exists. For example, R could be 'less than', B could be the set of real numbers, and A 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 13977. See dfsup2 8350 for alternate definition not requiring dummy variables. (Contributed by NM, 22-May-1999.)
|- sup ( A , B , R ) = U. { x e. B | ( A. y e. A -. x R y /\ A. y e. B ( y R x -> E. z e. A y R z ) ) }
Definition	df-inf 8349	Define the infimum of class A. It is meaningful when R is a relation that strictly orders B and when the infimum exists. For example, R could be 'less than', B could be the set of real numbers, and A 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 ( A , B , R ) = sup ( A , B , `' R )
Theorem	dfsup2 8350	Quantifier free definition of supremum. (Contributed by Scott Fenton, 19-Feb-2013.)
|- sup ( B , A , R ) = U. ( A \ ( ( `' R " B ) u. ( R " ( A \ ( `' R " B ) ) ) ) )
Theorem	supeq1 8351	Equality theorem for supremum. (Contributed by NM, 22-May-1999.)
|- ( B = C -> sup ( B , A , R ) = sup ( C , A , R ) )
Theorem	supeq1d 8352	Equality deduction for supremum. (Contributed by Paul Chapman, 22-Jun-2011.)
|- ( ph -> B = C )   =>    |- ( ph -> sup ( B , A , R ) = sup ( C , A , R ) )
Theorem	supeq1i 8353	Equality inference for supremum. (Contributed by Paul Chapman, 22-Jun-2011.)
|- B = C   =>    |- sup ( B , A , R ) = sup ( C , A , R )
Theorem	supeq2 8354	Equality theorem for supremum. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( B = C -> sup ( A , B , R ) = sup ( A , C , R ) )
Theorem	supeq3 8355	Equality theorem for supremum. (Contributed by Scott Fenton, 13-Jun-2018.)
|- ( R = S -> sup ( A , B , R ) = sup ( A , B , S ) )
Theorem	supeq123d 8356	Equality deduction for supremum. (Contributed by Stefan O'Rear, 20-Jan-2015.)
|- ( ph -> A = D )   &    |- ( ph -> B = E )   &    |- ( ph -> C = F )   =>    |- ( ph -> sup ( A , B , C ) = sup ( D , E , F ) )
Theorem	nfsup 8357	Hypothesis builder for supremum. (Contributed by Mario Carneiro, 20-Mar-2014.)
|- F/_ x A   &    |- F/_ x B   &    |- F/_ x R   =>    |- F/_ x sup ( A , B , R )
Theorem	supmo 8358*	Any class B has at most one supremum in A (where R is interpreted as 'less than'). (Contributed by NM, 5-May-1999.) (Revised by Mario Carneiro, 24-Dec-2016.)
|- ( ph -> R Or A )   =>    |- ( ph -> E* x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) )
Theorem	supexd 8359	A supremum is a set. (Contributed by NM, 22-May-1999.) (Revised by Mario Carneiro, 24-Dec-2016.)
|- ( ph -> R Or A )   =>    |- ( ph -> sup ( B , A , R ) e. _V )
Theorem	supeu 8360*	A supremum is unique. Similar to Theorem I.26 of [Apostol] p. 24 (but for suprema in general). (Contributed by NM, 12-Oct-2004.)
|- ( ph -> R Or A )   &    |- ( ph -> E. x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) )   =>    |- ( ph -> E! x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) )
Theorem	supval2 8361*	Alternate expression for the supremum. (Contributed by Mario Carneiro, 24-Dec-2016.) (Revised by Thierry Arnoux, 24-Sep-2017.)
|- ( ph -> R Or A )   =>    |- ( ph -> sup ( B , A , R ) = ( iota_ x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) ) )
Theorem	eqsup 8362*	Sufficient condition for an element to be equal to the supremum. (Contributed by Mario Carneiro, 21-Apr-2015.)
|- ( ph -> R Or A )   =>    |- ( ph -> ( ( C e. A /\ A. y e. B -. C R y /\ A. y e. A ( y R C -> E. z e. B y R z ) ) -> sup ( B , A , R ) = C ) )
Theorem	eqsupd 8363*	Sufficient condition for an element to be equal to the supremum. (Contributed by Mario Carneiro, 21-Apr-2015.)
|- ( ph -> R Or A )   &    |- ( ph -> C e. A )   &    |- ( ( ph /\ y e. B ) -> -. C R y )   &    |- ( ( ph /\ ( y e. A /\ y R C ) ) -> E. z e. B y R z )   =>    |- ( ph -> sup ( B , A , R ) = C )
Theorem	supcl 8364*	A supremum belongs to its base class (closure law). See also supub 8365 and suplub 8366. (Contributed by NM, 12-Oct-2004.)
|- ( ph -> R Or A )   &    |- ( ph -> E. x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) )   =>    |- ( ph -> sup ( B , A , R ) e. A )
Theorem	supub 8365*	A supremum is an upper bound. See also supcl 8364 and suplub 8366. This proof demonstrates how to expand an iota-based definition (df-iota 5851) using riotacl2 6624. (Contributed by NM, 12-Oct-2004.) (Proof shortened by Mario Carneiro, 24-Dec-2016.)
|- ( ph -> R Or A )   &    |- ( ph -> E. x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) )   =>    |- ( ph -> ( C e. B -> -. sup ( B , A , R ) R C ) )
Theorem	suplub 8366*	A supremum is the least upper bound. See also supcl 8364 and supub 8365. (Contributed by NM, 13-Oct-2004.) (Revised by Mario Carneiro, 24-Dec-2016.)
|- ( ph -> R Or A )   &    |- ( ph -> E. x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) )   =>    |- ( ph -> ( ( C e. A /\ C R sup ( B , A , R ) ) -> E. z e. B C R z ) )
Theorem	suplub2 8367*	Bidirectional form of suplub 8366. (Contributed by Mario Carneiro, 6-Sep-2014.)
|- ( ph -> R Or A )   &    |- ( ph -> E. x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) )   &    |- ( ph -> B C_ A )   =>    |- ( ( ph /\ C e. A ) -> ( C R sup ( B , A , R ) <-> E. z e. B C R z ) )
Theorem	supnub 8368*	An upper bound is not less than the supremum. (Contributed by NM, 13-Oct-2004.)
|- ( ph -> R Or A )   &    |- ( ph -> E. x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) )   =>    |- ( ph -> ( ( C e. A /\ A. z e. B -. C R z ) -> -. C R sup ( B , A , R ) ) )
Theorem	supex 8369	A supremum is a set. (Contributed by NM, 22-May-1999.)
|- R Or A   =>    |- sup ( B , A , R ) e. _V
Theorem	sup00 8370	The supremum under an empty base set is always the empty set. (Contributed by AV, 4-Sep-2020.)
|- sup ( B , (/) , R ) = (/)
Theorem	sup0riota 8371*	The supremum of an empty set is the smallest element of the base set. (Contributed by AV, 4-Sep-2020.)
|- ( R Or A -> sup ( (/) , A , R ) = ( iota_ x e. A A. y e. A -. y R x ) )
Theorem	sup0 8372*	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.)
|- ( ( R Or A /\ ( X e. A /\ A. y e. A -. y R X ) /\ E! x e. A A. y e. A -. y R x ) -> sup ( (/) , A , R ) = X )
Theorem	supmax 8373*	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.)
|- ( ph -> R Or A )   &    |- ( ph -> C e. A )   &    |- ( ph -> C e. B )   &    |- ( ( ph /\ y e. B ) -> -. C R y )   =>    |- ( ph -> sup ( B , A , R ) = C )
Theorem	fisup2g 8374*	A finite set satisfies the conditions to have a supremum. (Contributed by Mario Carneiro, 28-Apr-2015.)
|- ( ( R Or A /\ ( B e. Fin /\ B =/= (/) /\ B C_ A ) ) -> E. x e. B ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) )
Theorem	fisupcl 8375	A nonempty finite set contains its supremum. (Contributed by Jeff Madsen, 9-May-2011.)
|- ( ( R Or A /\ ( B e. Fin /\ B =/= (/) /\ B C_ A ) ) -> sup ( B , A , R ) e. B )
Theorem	supgtoreq 8376	The supremum of a finite set is greater than or equal to all the elements of the set. (Contributed by AV, 1-Oct-2019.)
|- ( ph -> R Or A )   &    |- ( ph -> B C_ A )   &    |- ( ph -> B e. Fin )   &    |- ( ph -> C e. B )   &    |- ( ph -> S = sup ( B , A , R ) )   =>    |- ( ph -> ( C R S \/ C = S ) )
Theorem	suppr 8377	The supremum of a pair. (Contributed by NM, 17-Jun-2007.) (Proof shortened by Mario Carneiro, 24-Dec-2016.)
|- ( ( R Or A /\ B e. A /\ C e. A ) -> sup ( { B , C } , A , R ) = if ( C R B , B , C ) )
Theorem	supsn 8378	The supremum of a singleton. (Contributed by NM, 2-Oct-2007.)
|- ( ( R Or A /\ B e. A ) -> sup ( { B } , A , R ) = B )
Theorem	supisolem 8379*	Lemma for supiso 8381. (Contributed by Mario Carneiro, 24-Dec-2016.)
|- ( ph -> F Isom R , S ( A , B ) )   &    |- ( ph -> C C_ A )   =>    |- ( ( ph /\ D e. A ) -> ( ( A. y e. C -. D R y /\ A. y e. A ( y R D -> E. z e. C y R z ) ) <-> ( A. w e. ( F " C ) -. ( F ` D ) S w /\ A. w e. B ( w S ( F ` D ) -> E. v e. ( F " C ) w S v ) ) ) )
Theorem	supisoex 8380*	Lemma for supiso 8381. (Contributed by Mario Carneiro, 24-Dec-2016.)
|- ( ph -> F Isom R , S ( A , B ) )   &    |- ( ph -> C C_ A )   &    |- ( ph -> E. x e. A ( A. y e. C -. x R y /\ A. y e. A ( y R x -> E. z e. C y R z ) ) )   =>    |- ( ph -> E. u e. B ( A. w e. ( F " C ) -. u S w /\ A. w e. B ( w S u -> E. v e. ( F " C ) w S v ) ) )
Theorem	supiso 8381*	Image of a supremum under an isomorphism. (Contributed by Mario Carneiro, 24-Dec-2016.)
|- ( ph -> F Isom R , S ( A , B ) )   &    |- ( ph -> C C_ A )   &    |- ( ph -> E. x e. A ( A. y e. C -. x R y /\ A. y e. A ( y R x -> E. z e. C y R z ) ) )   &    |- ( ph -> R Or A )   =>    |- ( ph -> sup ( ( F " C ) , B , S ) = ( F ` sup ( C , A , R ) ) )
Theorem	infeq1 8382	Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.)
|- ( B = C -> inf ( B , A , R ) = inf ( C , A , R ) )
Theorem	infeq1d 8383	Equality deduction for infimum. (Contributed by AV, 2-Sep-2020.)
|- ( ph -> B = C )   =>    |- ( ph -> inf ( B , A , R ) = inf ( C , A , R ) )
Theorem	infeq1i 8384	Equality inference for infimum. (Contributed by AV, 2-Sep-2020.)
|- B = C   =>    |- inf ( B , A , R ) = inf ( C , A , R )
Theorem	infeq2 8385	Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.)
|- ( B = C -> inf ( A , B , R ) = inf ( A , C , R ) )
Theorem	infeq3 8386	Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.)
|- ( R = S -> inf ( A , B , R ) = inf ( A , B , S ) )
Theorem	infeq123d 8387	Equality deduction for infimum. (Contributed by AV, 2-Sep-2020.)
|- ( ph -> A = D )   &    |- ( ph -> B = E )   &    |- ( ph -> C = F )   =>    |- ( ph -> inf ( A , B , C ) = inf ( D , E , F ) )
Theorem	nfinf 8388	Hypothesis builder for infimum. (Contributed by AV, 2-Sep-2020.)
|- F/_ x A   &    |- F/_ x B   &    |- F/_ x R   =>    |- F/_ xinf ( A , B , R )
Theorem	infexd 8389	An infimum is a set. (Contributed by AV, 2-Sep-2020.)
|- ( ph -> R Or A )   =>    |- ( ph -> inf ( B , A , R ) e. _V )
Theorem	eqinf 8390*	Sufficient condition for an element to be equal to the infimum. (Contributed by AV, 2-Sep-2020.)
|- ( ph -> R Or A )   =>    |- ( ph -> ( ( C e. A /\ A. y e. B -. y R C /\ A. y e. A ( C R y -> E. z e. B z R y ) ) -> inf ( B , A , R ) = C ) )
Theorem	eqinfd 8391*	Sufficient condition for an element to be equal to the infimum. (Contributed by AV, 3-Sep-2020.)
|- ( ph -> R Or A )   &    |- ( ph -> C e. A )   &    |- ( ( ph /\ y e. B ) -> -. y R C )   &    |- ( ( ph /\ ( y e. A /\ C R y ) ) -> E. z e. B z R y )   =>    |- ( ph -> inf ( B , A , R ) = C )
Theorem	infval 8392*	Alternate expression for the infimum. (Contributed by AV, 2-Sep-2020.)
|- ( ph -> R Or A )   =>    |- ( ph -> inf ( B , A , R ) = ( iota_ x e. A ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) ) )
Theorem	infcllem 8393*	Lemma for infcl 8394, inflb 8395, infglb 8396, etc. (Contributed by AV, 3-Sep-2020.)
|- ( ph -> R Or A )   &    |- ( ph -> E. x e. A ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) )   =>    |- ( ph -> E. x e. A ( A. y e. B -. x `' R y /\ A. y e. A ( y `' R x -> E. z e. B y `' R z ) ) )
Theorem	infcl 8394*	An infimum belongs to its base class (closure law). See also inflb 8395 and infglb 8396. (Contributed by AV, 3-Sep-2020.)
|- ( ph -> R Or A )   &    |- ( ph -> E. x e. A ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) )   =>    |- ( ph -> inf ( B , A , R ) e. A )
Theorem	inflb 8395*	An infimum is a lower bound. See also infcl 8394 and infglb 8396. (Contributed by AV, 3-Sep-2020.)
|- ( ph -> R Or A )   &    |- ( ph -> E. x e. A ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) )   =>    |- ( ph -> ( C e. B -> -. C Rinf ( B , A , R ) ) )
Theorem	infglb 8396*	An infimum is the greatest lower bound. See also infcl 8394 and inflb 8395. (Contributed by AV, 3-Sep-2020.)
|- ( ph -> R Or A )   &    |- ( ph -> E. x e. A ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) )   =>    |- ( ph -> ( ( C e. A /\ inf ( B , A , R ) R C ) -> E. z e. B z R C ) )
Theorem	infglbb 8397*	Bidirectional form of infglb 8396. (Contributed by AV, 3-Sep-2020.)
|- ( ph -> R Or A )   &    |- ( ph -> E. x e. A ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) )   &    |- ( ph -> B C_ A )   =>    |- ( ( ph /\ C e. A ) -> (inf ( B , A , R ) R C <-> E. z e. B z R C ) )
Theorem	infnlb 8398*	A lower bound is not greater than the infimum. (Contributed by AV, 3-Sep-2020.)
|- ( ph -> R Or A )   &    |- ( ph -> E. x e. A ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) )   =>    |- ( ph -> ( ( C e. A /\ A. z e. B -. z R C ) -> -. inf ( B , A , R ) R C ) )
Theorem	infex 8399	An infimum is a set. (Contributed by AV, 3-Sep-2020.)
|- R Or A   =>    |- inf ( B , A , R ) e. _V
Theorem	infmin 8400*	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.)
|- ( ph -> R Or A )   &    |- ( ph -> C e. A )   &    |- ( ph -> C e. B )   &    |- ( ( ph /\ y e. B ) -> -. y R C )   =>    |- ( ph -> inf ( B , A , R ) = C )