P. 73 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 7201-7300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	infidc 7201*	The intersection of two sets is finite if one of them is and the other is decidable. (Contributed by Jim Kingdon, 24-May-2025.)
|- ( ( A e. Fin /\ A. x e. A DECID x e. B ) -> ( A i^i B ) e. Fin )
Theorem	snon0 7202	An ordinal which is a singleton is { (/) }. (Contributed by Jim Kingdon, 19-Oct-2021.)
|- ( ( A e. V /\ { A } e. On ) -> A = (/) )
Theorem	fnfi 7203	A version of fnex 5906 for finite sets. (Contributed by Mario Carneiro, 16-Nov-2014.) (Revised by Mario Carneiro, 24-Jun-2015.)
|- ( ( F Fn A /\ A e. Fin ) -> F e. Fin )
Theorem	fundmfi 7204	The domain of a finite function is finite. (Contributed by Jim Kingdon, 5-Feb-2022.)
|- ( ( A e. Fin /\ Fun A ) -> dom A e. Fin )
Theorem	fundmfibi 7205	A function is finite if and only if its domain is finite. (Contributed by AV, 10-Jan-2020.)
|- ( Fun F -> ( F e. Fin <-> dom F e. Fin ) )
Theorem	resfnfinfinss 7206	The restriction of a function to a finite subset of its domain is finite. (Contributed by Alexander van der Vekens, 3-Feb-2018.)
|- ( ( F Fn A /\ B e. Fin /\ B C_ A ) -> ( F |` B ) e. Fin )
Theorem	residfi 7207	A restricted identity function is finite iff the restricting class is finite. (Contributed by AV, 10-Jan-2020.)
|- ( ( _I |` A ) e. Fin <-> A e. Fin )
Theorem	relcnvfi 7208	If a relation is finite, its converse is as well. (Contributed by Jim Kingdon, 5-Feb-2022.)
|- ( ( Rel A /\ A e. Fin ) -> `' A e. Fin )
Theorem	funrnfi 7209	The range of a finite relation is finite if its converse is a function. (Contributed by Jim Kingdon, 5-Feb-2022.)
|- ( ( Rel A /\ Fun `' A /\ A e. Fin ) -> ran A e. Fin )
Theorem	f1ofi 7210	If a 1-1 and onto function has a finite domain, its range is finite. (Contributed by Jim Kingdon, 21-Feb-2022.)
|- ( ( A e. Fin /\ F : A -1-1-onto-> B ) -> B e. Fin )
Theorem	f1dmvrnfibi 7211	A one-to-one function whose domain is a set is finite if and only if its range is finite. See also f1vrnfibi 7212. (Contributed by AV, 10-Jan-2020.)
|- ( ( A e. V /\ F : A -1-1-> B ) -> ( F e. Fin <-> ran F e. Fin ) )
Theorem	f1vrnfibi 7212	A one-to-one function which is a set is finite if and only if its range is finite. See also f1dmvrnfibi 7211. (Contributed by AV, 10-Jan-2020.)
|- ( ( F e. V /\ F : A -1-1-> B ) -> ( F e. Fin <-> ran F e. Fin ) )
Theorem	iunfidisj 7213*	The finite union of disjoint finite sets is finite. Note that B depends on x, i.e. can be thought of as B ( x ). (Contributed by NM, 23-Mar-2006.) (Revised by Jim Kingdon, 7-Oct-2022.)
|- ( ( A e. Fin /\ A. x e. A B e. Fin /\ Disj x e. A B ) -> U_ x e. A B e. Fin )
Theorem	mapfi 7214	Set exponentiation of finite sets is finite. (Contributed by Jeff Madsen, 19-Jun-2011.)
|- ( ( A e. Fin /\ B e. Fin ) -> ( A ^m B ) e. Fin )
Theorem	elfpw 7215	Membership in a class of finite subsets. (Contributed by Stefan O'Rear, 4-Apr-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( A e. ( ~P B i^i Fin ) <-> ( A C_ B /\ A e. Fin ) )
Theorem	fissfi 7216*	A finite subset of a finite set is a decidable subset. (Contributed by Jim Kingdon, 18-May-2026.)
|- ( ( S C_ A /\ A e. Fin /\ S e. Fin ) -> A. x e. A DECID x e. S )
Theorem	f1finf1o 7217	Any injection from one finite set to another of equal size must be a bijection. (Contributed by Jeff Madsen, 5-Jun-2010.)
|- ( ( A ~~ B /\ B e. Fin ) -> ( F : A -1-1-> B <-> F : A -1-1-onto-> B ) )
Theorem	en1eqsn 7218	A set with one element is a singleton. (Contributed by FL, 18-Aug-2008.)
|- ( ( A e. B /\ B ~~ 1o ) -> B = { A } )
Theorem	en1eqsnbi 7219	A set containing an element has exactly one element iff it is a singleton. (Contributed by FL, 13-Feb-2010.) (Revised by AV, 25-Jan-2020.)
|- ( A e. B -> ( B ~~ 1o <-> B = { A } ) )
Theorem	snexxph 7220*	A case where the antecedent of snexg 4297 is not needed. The class { x | ph } is from dcextest 4703. (Contributed by Mario Carneiro and Jim Kingdon, 4-Jul-2022.)
|- { { x | ph } } e. _V
Theorem	preimaf1ofi 7221	The preimage of a finite set under a one-to-one, onto function is finite. (Contributed by Jim Kingdon, 24-Sep-2022.)
|- ( ph -> C C_ B )   &    |- ( ph -> F : A -1-1-onto-> B )   &    |- ( ph -> C e. Fin )   =>    |- ( ph -> ( `' F " C ) e. Fin )
Theorem	fidcenumlemim 7222*	Lemma for fidcenum 7226. Forward direction. (Contributed by Jim Kingdon, 19-Oct-2022.)
|- ( A e. Fin -> ( A. x e. A A. y e. A DECID x = y /\ E. n e. om E. f f : n -onto-> A ) )
Theorem	fidcenumlemrks 7223*	Lemma for fidcenum 7226. Induction step for fidcenumlemrk 7224. (Contributed by Jim Kingdon, 20-Oct-2022.)
|- ( ph -> A. x e. A A. y e. A DECID x = y )   &    |- ( ph -> F : N -onto-> A )   &    |- ( ph -> J e. om )   &    |- ( ph -> suc J C_ N )   &    |- ( ph -> ( X e. ( F " J ) \/ -. X e. ( F " J ) ) )   &    |- ( ph -> X e. A )   =>    |- ( ph -> ( X e. ( F " suc J ) \/ -. X e. ( F " suc J ) ) )
Theorem	fidcenumlemrk 7224*	Lemma for fidcenum 7226. (Contributed by Jim Kingdon, 20-Oct-2022.)
|- ( ph -> A. x e. A A. y e. A DECID x = y )   &    |- ( ph -> F : N -onto-> A )   &    |- ( ph -> K e. om )   &    |- ( ph -> K C_ N )   &    |- ( ph -> X e. A )   =>    |- ( ph -> ( X e. ( F " K ) \/ -. X e. ( F " K ) ) )
Theorem	fidcenumlemr 7225*	Lemma for fidcenum 7226. Reverse direction (put into deduction form). (Contributed by Jim Kingdon, 19-Oct-2022.)
|- ( ph -> A. x e. A A. y e. A DECID x = y )   &    |- ( ph -> F : N -onto-> A )   &    |- ( ph -> N e. om )   =>    |- ( ph -> A e. Fin )
Theorem	fidcenum 7226*	A set is finite if and only if it has decidable equality and is finitely enumerable. Proposition 8.1.11 of [AczelRathjen], p. 72. The definition of "finitely enumerable" as E. n e. om E. f f : n -onto-> A is Definition 8.1.4 of [AczelRathjen], p. 71. (Contributed by Jim Kingdon, 19-Oct-2022.)
|- ( A e. Fin <-> ( A. x e. A A. y e. A DECID x = y /\ E. n e. om E. f f : n -onto-> A ) )
2.6.33  Schroeder-Bernstein Theorem
Theorem	sbthlem1 7227*	Lemma for isbth 7237. (Contributed by NM, 22-Mar-1998.)
|- A e. _V   &    |- D = { x | ( x C_ A /\ ( g " ( B \ ( f " x ) ) ) C_ ( A \ x ) ) }   =>    |- U. D C_ ( A \ ( g " ( B \ ( f " U. D ) ) ) )
Theorem	sbthlem2 7228*	Lemma for isbth 7237. (Contributed by NM, 22-Mar-1998.)
|- A e. _V   &    |- D = { x | ( x C_ A /\ ( g " ( B \ ( f " x ) ) ) C_ ( A \ x ) ) }   =>    |- ( ran g C_ A -> ( A \ ( g " ( B \ ( f " U. D ) ) ) ) C_ U. D )
Theorem	sbthlemi3 7229*	Lemma for isbth 7237. (Contributed by NM, 22-Mar-1998.)
|- A e. _V   &    |- D = { x | ( x C_ A /\ ( g " ( B \ ( f " x ) ) ) C_ ( A \ x ) ) }   =>    |- ( (EXMID /\ ran g C_ A ) -> ( g " ( B \ ( f " U. D ) ) ) = ( A \ U. D ) )
Theorem	sbthlemi4 7230*	Lemma for isbth 7237. (Contributed by NM, 27-Mar-1998.)
|- A e. _V   &    |- D = { x | ( x C_ A /\ ( g " ( B \ ( f " x ) ) ) C_ ( A \ x ) ) }   =>    |- ( (EXMID /\ ( dom g = B /\ ran g C_ A ) /\ Fun `' g ) -> ( `' g " ( A \ U. D ) ) = ( B \ ( f " U. D ) ) )
Theorem	sbthlemi5 7231*	Lemma for isbth 7237. (Contributed by NM, 22-Mar-1998.)
|- A e. _V   &    |- D = { x | ( x C_ A /\ ( g " ( B \ ( f " x ) ) ) C_ ( A \ x ) ) }   &    |- H = ( ( f |` U. D ) u. ( `' g |` ( A \ U. D ) ) )   =>    |- ( (EXMID /\ ( dom f = A /\ ran g C_ A ) ) -> dom H = A )
Theorem	sbthlemi6 7232*	Lemma for isbth 7237. (Contributed by NM, 27-Mar-1998.)
|- A e. _V   &    |- D = { x | ( x C_ A /\ ( g " ( B \ ( f " x ) ) ) C_ ( A \ x ) ) }   &    |- H = ( ( f |` U. D ) u. ( `' g |` ( A \ U. D ) ) )   =>    |- ( ( (EXMID /\ ran f C_ B ) /\ ( ( dom g = B /\ ran g C_ A ) /\ Fun `' g ) ) -> ran H = B )
Theorem	sbthlem7 7233*	Lemma for isbth 7237. (Contributed by NM, 27-Mar-1998.)
|- A e. _V   &    |- D = { x | ( x C_ A /\ ( g " ( B \ ( f " x ) ) ) C_ ( A \ x ) ) }   &    |- H = ( ( f |` U. D ) u. ( `' g |` ( A \ U. D ) ) )   =>    |- ( ( Fun f /\ Fun `' g ) -> Fun H )
Theorem	sbthlemi8 7234*	Lemma for isbth 7237. (Contributed by NM, 27-Mar-1998.)
|- A e. _V   &    |- D = { x | ( x C_ A /\ ( g " ( B \ ( f " x ) ) ) C_ ( A \ x ) ) }   &    |- H = ( ( f |` U. D ) u. ( `' g |` ( A \ U. D ) ) )   =>    |- ( ( (EXMID /\ Fun `' f ) /\ ( ( ( Fun g /\ dom g = B ) /\ ran g C_ A ) /\ Fun `' g ) ) -> Fun `' H )
Theorem	sbthlemi9 7235*	Lemma for isbth 7237. (Contributed by NM, 28-Mar-1998.)
|- A e. _V   &    |- D = { x | ( x C_ A /\ ( g " ( B \ ( f " x ) ) ) C_ ( A \ x ) ) }   &    |- H = ( ( f |` U. D ) u. ( `' g |` ( A \ U. D ) ) )   =>    |- ( (EXMID /\ f : A -1-1-> B /\ g : B -1-1-> A ) -> H : A -1-1-onto-> B )
Theorem	sbthlemi10 7236*	Lemma for isbth 7237. (Contributed by NM, 28-Mar-1998.)
|- A e. _V   &    |- D = { x | ( x C_ A /\ ( g " ( B \ ( f " x ) ) ) C_ ( A \ x ) ) }   &    |- H = ( ( f |` U. D ) u. ( `' g |` ( A \ U. D ) ) )   &    |- B e. _V   =>    |- ( (EXMID /\ ( A ~<_ B /\ B ~<_ A ) ) -> A ~~ B )
Theorem	isbth 7237	Schroeder-Bernstein Theorem. Theorem 18 of [Suppes] p. 95. This theorem states that if set A is smaller (has lower cardinality) than B and vice-versa, then A and B are equinumerous (have the same cardinality). The interesting thing is that this can be proved without invoking the Axiom of Choice, as we do here, but the proof as you can see is quite difficult. (The theorem can be proved more easily if we allow AC.) The main proof consists of lemmas sbthlem1 7227 through sbthlemi10 7236; this final piece mainly changes bound variables to eliminate the hypotheses of sbthlemi10 7236. We follow closely the proof in Suppes, which you should consult to understand our proof at a higher level. Note that Suppes' proof, which is credited to J. M. Whitaker, does not require the Axiom of Infinity. The proof does require the law of the excluded middle which cannot be avoided as shown at exmidsbthr 16803. (Contributed by NM, 8-Jun-1998.)
|- ( (EXMID /\ ( A ~<_ B /\ B ~<_ A ) ) -> A ~~ B )
2.6.34  Finitely supported functions
Syntax	cfsupp 7238	Extend class definition to include the predicate to be a finitely supported function.
class finSupp
Definition	df-fsupp 7239*	Define the property of a function to be finitely supported (in relation to a given zero). (Contributed by AV, 23-May-2019.)
|- finSupp = { <. r , z >. | ( Fun r /\ ( r supp z ) e. Fin ) }
Theorem	relfsupp 7240	The property of a function to be finitely supported is a relation. (Contributed by AV, 7-Jun-2019.)
|- Rel finSupp
Theorem	relprcnfsupp 7241	A proper class is never finitely supported. (Contributed by AV, 7-Jun-2019.)
|- ( -. A e. _V -> -. A finSupp Z )
Theorem	isfsupp 7242	The property of a class to be a finitely supported function (in relation to a given zero). (Contributed by AV, 23-May-2019.)
|- ( ( R e. V /\ Z e. W ) -> ( R finSupp Z <-> ( Fun R /\ ( R supp Z ) e. Fin ) ) )
Theorem	isfsuppd 7243	Deduction form of isfsupp 7242. (Contributed by SN, 29-Jul-2024.)
|- ( ph -> R e. V )   &    |- ( ph -> Z e. W )   &    |- ( ph -> Fun R )   &    |- ( ph -> ( R supp Z ) e. Fin )   =>    |- ( ph -> R finSupp Z )
Theorem	funisfsupp 7244	The property of a function to be finitely supported (in relation to a given zero). (Contributed by AV, 23-May-2019.)
|- ( ( Fun R /\ R e. V /\ Z e. W ) -> ( R finSupp Z <-> ( R supp Z ) e. Fin ) )
Theorem	fsuppimp 7245	Implications of a class being a finitely supported function (in relation to a given zero). (Contributed by AV, 26-May-2019.)
|- ( R finSupp Z -> ( Fun R /\ ( R supp Z ) e. Fin ) )
Theorem	fsuppimpd 7246	A finitely supported function is a function with a finite support. (Contributed by AV, 6-Jun-2019.)
|- ( ph -> F finSupp Z )   =>    |- ( ph -> ( F supp Z ) e. Fin )
Theorem	fsuppfund 7247	A finitely supported function is a function. (Contributed by SN, 8-Mar-2025.)
|- ( ph -> F finSupp Z )   =>    |- ( ph -> Fun F )
Theorem	suppeqfsuppbi 7248	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.)
|- ( ( ( F e. U /\ Fun F ) /\ ( G e. V /\ Fun G ) ) -> ( ( F supp Z ) = ( G supp Z ) -> ( F finSupp Z <-> G finSupp Z ) ) )
Theorem	fsuppxpfi 7249	The cartesian product of two finitely supported functions is finite. (Contributed by AV, 17-Jul-2019.)
|- ( ( F finSupp Z /\ G finSupp Z ) -> ( ( F supp Z ) X. ( G supp Z ) ) e. Fin )
Theorem	fczfsuppd 7250	A constant function with value zero is finitely supported. (Contributed by AV, 30-Jun-2019.)
|- ( ph -> B e. V )   &    |- ( ph -> Z e. W )   =>    |- ( ph -> ( B X. { Z } ) finSupp Z )
Theorem	0fsupp 7251	The empty set is a finitely supported function. (Contributed by AV, 19-Jul-2019.)
|- ( Z e. V -> (/) finSupp Z )
Theorem	snopfsuppdc 7252	A singleton containing an ordered pair is a finitely supported function. (Contributed by AV, 19-Jul-2019.)
|- ( ph -> X e. V )   &    |- ( ph -> Y e. W )   &    |- ( ph -> Z e. U )   &    |- ( ph -> DECID Y = Z )   =>    |- ( ph -> { <. X , Y >. } finSupp Z )
Theorem	ffsuppbi 7253	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	fsuppcorn 7254	The composition of a 1-1 function with a finitely supported function is finitely supported. The purpose of the ( F supp Z ) C_ ran G condition is to ensure we don't subset the support of the function in such a way as to fun afoul of exmidssfi 7199. (Other alternative conditions might also be sufficient). (Contributed by AV, 28-May-2019.) (Revised by Jim Kingdon, 15-May-2026.)
|- ( ph -> F finSupp Z )   &    |- ( ph -> G : X -1-1-> Y )   &    |- ( ph -> Z e. W )   &    |- ( ph -> F e. V )   &    |- ( ph -> G e. U )   &    |- ( ph -> ( F supp Z ) C_ ran G )   =>    |- ( ph -> ( F o. G ) finSupp Z )
2.6.35  Finite intersections
Syntax	cfi 7255	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 7256*	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 7259). (Contributed by FL, 27-Apr-2008.)
|- fi = ( x e. _V |-> { z | E. y e. ( ~P x i^i Fin ) z = |^| y } )
Theorem	fival 7257*	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 7258*	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 7259*	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 7260	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	ssfii 7261	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 7262	The set of finite intersections of the empty set. (Contributed by Mario Carneiro, 30-Aug-2015.)
|- ( fi ` (/) ) = (/)
Theorem	fieq0 7263	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.)
|- ( A e. V -> ( A = (/) <-> ( fi ` A ) = (/) ) )
Theorem	fiss 7264	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	fiuni 7265	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	fipwssg 7266	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 e. V /\ A C_ ~P X ) -> ( fi ` A ) C_ ~P X )
Theorem	fifo 7267*	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 ) )
Theorem	dcfi 7268*	Decidability of a family of propositions indexed by a finite set. (Contributed by Jim Kingdon, 30-Sep-2024.)
|- ( ( A e. Fin /\ A. x e. A DECID ph ) -> DECID A. x e. A ph )
2.6.36  The sizes of sets
Theorem	2omap 7269*	Mapping between ( 2o ^m A ) and decidable subsets of A. (Contributed by Jim Kingdon, 12-Nov-2025.)
|- F = ( s e. ( 2o ^m A ) |-> { z e. A | ( s ` z ) = 1o } )   =>    |- ( A e. V -> F : ( 2o ^m A ) -1-1-onto-> { x e. ~P A | A. y e. A DECID y e. x } )
Theorem	2omapen 7270*	Equinumerosity of ( 2o ^m A ) and the set of decidable subsets of A. (Contributed by Jim Kingdon, 14-Nov-2025.)
|- ( A e. V -> ( 2o ^m A ) ~~ { x e. ~P A | A. y e. A DECID y e. x } )
Theorem	2omapfi 7271	The number of finite subsets of a finite set. For a similar theorem with set size expressed using ♯ (df-ihash 11139), see hashpwfi 11193. (Contributed by Jim Kingdon, 18-May-2026.)
|- ( A e. Fin -> ( 2o ^m A ) ~~ ( ~P A i^i Fin ) )
Theorem	fipwfi 7272	The set of finite subsets of a finite set is finite. (Contributed by Jim Kingdon, 19-May-2026.)
|- ( A e. Fin -> ( ~P A i^i Fin ) e. Fin )
2.6.37  Supremum and infimum
Syntax	csup 7273	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 7274	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 7275*	Define the supremum of class A. It is meaningful when R is a relation that strictly orders B and when the supremum exists. (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 7276	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	supeq1 7277	Equality theorem for supremum. (Contributed by NM, 22-May-1999.)
|- ( B = C -> sup ( B , A , R ) = sup ( C , A , R ) )
Theorem	supeq1d 7278	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 7279	Equality inference for supremum. (Contributed by Paul Chapman, 22-Jun-2011.)
|- B = C   =>    |- sup ( B , A , R ) = sup ( C , A , R )
Theorem	supeq2 7280	Equality theorem for supremum. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( B = C -> sup ( A , B , R ) = sup ( A , C , R ) )
Theorem	supeq3 7281	Equality theorem for supremum. (Contributed by Scott Fenton, 13-Jun-2018.)
|- ( R = S -> sup ( A , B , R ) = sup ( A , B , S ) )
Theorem	supeq123d 7282	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 7283	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	supmoti 7284*	Any class B has at most one supremum in A (where R is interpreted as 'less than'). The hypothesis is satisfied by real numbers (see lttri3 8353) or other orders which correspond to tight apartnesses. (Contributed by Jim Kingdon, 23-Nov-2021.)
|- ( ( ph /\ ( u e. A /\ v e. A ) ) -> ( u = v <-> ( -. u R v /\ -. v R u ) ) )   =>    |- ( 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	supeuti 7285*	A supremum is unique. Similar to Theorem I.26 of [Apostol] p. 24 (but for suprema in general). (Contributed by Jim Kingdon, 23-Nov-2021.)
|- ( ( ph /\ ( u e. A /\ v e. A ) ) -> ( u = v <-> ( -. u R v /\ -. v R u ) ) )   &    |- ( 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	supval2ti 7286*	Alternate expression for the supremum. (Contributed by Jim Kingdon, 23-Nov-2021.)
|- ( ( ph /\ ( u e. A /\ v e. A ) ) -> ( u = v <-> ( -. u R v /\ -. v R u ) ) )   &    |- ( 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 ) = ( 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	eqsupti 7287*	Sufficient condition for an element to be equal to the supremum. (Contributed by Jim Kingdon, 23-Nov-2021.)
|- ( ( ph /\ ( u e. A /\ v e. A ) ) -> ( u = v <-> ( -. u R v /\ -. v R u ) ) )   =>    |- ( 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	eqsuptid 7288*	Sufficient condition for an element to be equal to the supremum. (Contributed by Jim Kingdon, 24-Nov-2021.)
|- ( ( ph /\ ( u e. A /\ v e. A ) ) -> ( u = v <-> ( -. u R v /\ -. v R u ) ) )   &    |- ( 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	supclti 7289*	A supremum belongs to its base class (closure law). See also supubti 7290 and suplubti 7291. (Contributed by Jim Kingdon, 24-Nov-2021.)
|- ( ( ph /\ ( u e. A /\ v e. A ) ) -> ( u = v <-> ( -. u R v /\ -. v R u ) ) )   &    |- ( 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	supubti 7290*	A supremum is an upper bound. See also supclti 7289 and suplubti 7291. This proof demonstrates how to expand an iota-based definition (df-iota 5312) using riotacl2 6018. (Contributed by Jim Kingdon, 24-Nov-2021.)
|- ( ( ph /\ ( u e. A /\ v e. A ) ) -> ( u = v <-> ( -. u R v /\ -. v R u ) ) )   &    |- ( 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	suplubti 7291*	A supremum is the least upper bound. See also supclti 7289 and supubti 7290. (Contributed by Jim Kingdon, 24-Nov-2021.)
|- ( ( ph /\ ( u e. A /\ v e. A ) ) -> ( u = v <-> ( -. u R v /\ -. v R u ) ) )   &    |- ( 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	suplub2ti 7292*	Bidirectional form of suplubti 7291. (Contributed by Jim Kingdon, 17-Jan-2022.)
|- ( ( ph /\ ( u e. A /\ v e. A ) ) -> ( u = v <-> ( -. u R v /\ -. v R u ) ) )   &    |- ( 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 -> R Or A )   &    |- ( ph -> B C_ A )   =>    |- ( ( ph /\ C e. A ) -> ( C R sup ( B , A , R ) <-> E. z e. B C R z ) )
Theorem	supelti 7293*	Supremum membership in a set. (Contributed by Jim Kingdon, 16-Jan-2022.)
|- ( ( ph /\ ( u e. A /\ v e. A ) ) -> ( u = v <-> ( -. u R v /\ -. v R u ) ) )   &    |- ( ph -> E. x e. C ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) )   &    |- ( ph -> C C_ A )   =>    |- ( ph -> sup ( B , A , R ) e. C )
Theorem	sup00 7294	The supremum under an empty base set is always the empty set. (Contributed by AV, 4-Sep-2020.)
|- sup ( B , (/) , R ) = (/)
Theorem	supmaxti 7295*	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 Jim Kingdon, 24-Nov-2021.)
|- ( ( ph /\ ( u e. A /\ v e. A ) ) -> ( u = v <-> ( -. u R v /\ -. v R u ) ) )   &    |- ( ph -> C e. A )   &    |- ( ph -> C e. B )   &    |- ( ( ph /\ y e. B ) -> -. C R y )   =>    |- ( ph -> sup ( B , A , R ) = C )
Theorem	supsnti 7296*	The supremum of a singleton. (Contributed by Jim Kingdon, 26-Nov-2021.)
|- ( ( ph /\ ( u e. A /\ v e. A ) ) -> ( u = v <-> ( -. u R v /\ -. v R u ) ) )   &    |- ( ph -> B e. A )   =>    |- ( ph -> sup ( { B } , A , R ) = B )
Theorem	isotilem 7297*	Lemma for isoti 7298. (Contributed by Jim Kingdon, 26-Nov-2021.)
|- ( F Isom R , S ( A , B ) -> ( A. x e. B A. y e. B ( x = y <-> ( -. x S y /\ -. y S x ) ) -> A. u e. A A. v e. A ( u = v <-> ( -. u R v /\ -. v R u ) ) ) )
Theorem	isoti 7298*	An isomorphism preserves tightness. (Contributed by Jim Kingdon, 26-Nov-2021.)
|- ( F Isom R , S ( A , B ) -> ( A. u e. A A. v e. A ( u = v <-> ( -. u R v /\ -. v R u ) ) <-> A. u e. B A. v e. B ( u = v <-> ( -. u S v /\ -. v S u ) ) ) )
Theorem	supisolem 7299*	Lemma for supisoti 7301. (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 7300*	Lemma for supisoti 7301. (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 ) ) )