P. 70 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 6901-7000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	exmidpw 6901	Excluded middle is equivalent to the power set of 1o having two elements. Remark of [PradicBrown2022], p. 2. (Contributed by Jim Kingdon, 30-Jun-2022.)
|- (EXMID <-> ~P 1o ~~ 2o )
Theorem	exmidpweq 6902	Excluded middle is equivalent to the power set of 1o being 2o. (Contributed by Jim Kingdon, 28-Jul-2024.)
|- (EXMID <-> ~P 1o = 2o )
Theorem	pw1fin 6903	Excluded middle is equivalent to the power set of 1o being finite. (Contributed by SN and Jim Kingdon, 7-Aug-2024.)
|- (EXMID <-> ~P 1o e. Fin )
Theorem	pw1dc0el 6904	Another equivalent of excluded middle, which is a mere reformulation of the definition. (Contributed by BJ, 9-Aug-2024.)
|- (EXMID <-> A. x e. ~P 1oDECID (/) e. x )
Theorem	ss1o0el1o 6905	Reformulation of ss1o0el1 4194 using 1o instead of { (/) }. (Contributed by BJ, 9-Aug-2024.)
|- ( A C_ 1o -> ( (/) e. A <-> A = 1o ) )
Theorem	pw1dc1 6906	If, in the set of truth values (the powerset of 1o), equality to 1o is decidable, then excluded middle holds (and conversely). (Contributed by BJ and Jim Kingdon, 8-Aug-2024.)
|- (EXMID <-> A. x e. ~P 1oDECID x = 1o )
Theorem	fientri3 6907	Trichotomy of dominance for finite sets. (Contributed by Jim Kingdon, 15-Sep-2021.)
|- ( ( A e. Fin /\ B e. Fin ) -> ( A ~<_ B \/ B ~<_ A ) )
Theorem	nnwetri 6908*	A natural number is well-ordered by _E. More specifically, this order both satisfies We and is trichotomous. (Contributed by Jim Kingdon, 25-Sep-2021.)
|- ( A e. om -> ( _E We A /\ A. x e. A A. y e. A ( x _E y \/ x = y \/ y _E x ) ) )
Theorem	onunsnss 6909	Adding a singleton to create an ordinal. (Contributed by Jim Kingdon, 20-Oct-2021.)
|- ( ( B e. V /\ ( A u. { B } ) e. On ) -> B C_ A )
Theorem	unfiexmid 6910*	If the union of any two finite sets is finite, excluded middle follows. Remark 8.1.17 of [AczelRathjen], p. 74. (Contributed by Mario Carneiro and Jim Kingdon, 5-Mar-2022.)
|- ( ( x e. Fin /\ y e. Fin ) -> ( x u. y ) e. Fin )   =>    |- ( ph \/ -. ph )
Theorem	unsnfi 6911	Adding a singleton to a finite set yields a finite set. (Contributed by Jim Kingdon, 3-Feb-2022.)
|- ( ( A e. Fin /\ B e. V /\ -. B e. A ) -> ( A u. { B } ) e. Fin )
Theorem	unsnfidcex 6912	The B e. V condition in unsnfi 6911. This is intended to show that unsnfi 6911 without that condition would not be provable but it probably would need to be strengthened (for example, to imply included middle) to fully show that. (Contributed by Jim Kingdon, 6-Feb-2022.)
|- ( ( A e. Fin /\ -. B e. A /\ ( A u. { B } ) e. Fin ) -> DECID -. B e. _V )
Theorem	unsnfidcel 6913	The -. B e. A condition in unsnfi 6911. This is intended to show that unsnfi 6911 without that condition would not be provable but it probably would need to be strengthened (for example, to imply included middle) to fully show that. (Contributed by Jim Kingdon, 6-Feb-2022.)
|- ( ( A e. Fin /\ B e. V /\ ( A u. { B } ) e. Fin ) -> DECID -. B e. A )
Theorem	unfidisj 6914	The union of two disjoint finite sets is finite. (Contributed by Jim Kingdon, 25-Feb-2022.)
|- ( ( A e. Fin /\ B e. Fin /\ ( A i^i B ) = (/) ) -> ( A u. B ) e. Fin )
Theorem	undifdcss 6915*	Union of complementary parts into whole and decidability. (Contributed by Jim Kingdon, 17-Jun-2022.)
|- ( A = ( B u. ( A \ B ) ) <-> ( B C_ A /\ A. x e. A DECID x e. B ) )
Theorem	undifdc 6916*	Union of complementary parts into whole. This is a case where we can strengthen undifss 3503 from subset to equality. (Contributed by Jim Kingdon, 17-Jun-2022.)
|- ( ( A. x e. A A. y e. A DECID x = y /\ B e. Fin /\ B C_ A ) -> A = ( B u. ( A \ B ) ) )
Theorem	undiffi 6917	Union of complementary parts into whole. This is a case where we can strengthen undifss 3503 from subset to equality. (Contributed by Jim Kingdon, 2-Mar-2022.)
|- ( ( A e. Fin /\ B e. Fin /\ B C_ A ) -> A = ( B u. ( A \ B ) ) )
Theorem	unfiin 6918	The union of two finite sets is finite if their intersection is. (Contributed by Jim Kingdon, 2-Mar-2022.)
|- ( ( A e. Fin /\ B e. Fin /\ ( A i^i B ) e. Fin ) -> ( A u. B ) e. Fin )
Theorem	prfidisj 6919	A pair is finite if it consists of two unequal sets. For the case where A = B, see snfig 6807. For the cases where one or both is a proper class, see prprc1 3699, prprc2 3700, or prprc 3701. (Contributed by Jim Kingdon, 31-May-2022.)
|- ( ( A e. V /\ B e. W /\ A =/= B ) -> { A , B } e. Fin )
Theorem	tpfidisj 6920	A triple is finite if it consists of three unequal sets. (Contributed by Jim Kingdon, 1-Oct-2022.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   &    |- ( ph -> A =/= B )   &    |- ( ph -> A =/= C )   &    |- ( ph -> B =/= C )   =>    |- ( ph -> { A , B , C } e. Fin )
Theorem	fiintim 6921*	If a class is closed under pairwise intersections, then it is closed under nonempty finite intersections. The converse would appear to require an additional condition, such as x and y not being equal, or A having decidable equality. This theorem is applicable to a topology, which (among other axioms) is closed under finite intersections. Some texts use a pairwise intersection and some texts use a finite intersection, but most topology texts assume excluded middle (in which case the two intersection properties would be equivalent). (Contributed by NM, 22-Sep-2002.) (Revised by Jim Kingdon, 14-Jan-2023.)
|- ( A. x e. A A. y e. A ( x i^i y ) e. A -> A. x ( ( x C_ A /\ x =/= (/) /\ x e. Fin ) -> |^| x e. A ) )
Theorem	xpfi 6922	The Cartesian product of two finite sets is finite. Lemma 8.1.16 of [AczelRathjen], p. 74. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Mar-2015.)
|- ( ( A e. Fin /\ B e. Fin ) -> ( A X. B ) e. Fin )
Theorem	3xpfi 6923	The Cartesian product of three finite sets is a finite set. (Contributed by Alexander van der Vekens, 11-Mar-2018.)
|- ( V e. Fin -> ( ( V X. V ) X. V ) e. Fin )
Theorem	fisseneq 6924	A finite set is equal to its subset if they are equinumerous. (Contributed by FL, 11-Aug-2008.)
|- ( ( B e. Fin /\ A C_ B /\ A ~~ B ) -> A = B )
Theorem	phpeqd 6925	Corollary of the Pigeonhole Principle using equality. Strengthening of phpm 6858 expressed without negation. (Contributed by Rohan Ridenour, 3-Aug-2023.)
|- ( ph -> A e. Fin )   &    |- ( ph -> B C_ A )   &    |- ( ph -> A ~~ B )   =>    |- ( ph -> A = B )
Theorem	ssfirab 6926*	A subset of a finite set is finite if it is defined by a decidable property. (Contributed by Jim Kingdon, 27-May-2022.)
|- ( ph -> A e. Fin )   &    |- ( ph -> A. x e. A DECID ps )   =>    |- ( ph -> { x e. A | ps } e. Fin )
Theorem	ssfidc 6927*	A subset of a finite set is finite if membership in the subset is decidable. (Contributed by Jim Kingdon, 27-May-2022.)
|- ( ( A e. Fin /\ B C_ A /\ A. x e. A DECID x e. B ) -> B e. Fin )
Theorem	snon0 6928	An ordinal which is a singleton is { (/) }. (Contributed by Jim Kingdon, 19-Oct-2021.)
|- ( ( A e. V /\ { A } e. On ) -> A = (/) )
Theorem	fnfi 6929	A version of fnex 5733 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 6930	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 6931	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 6932	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	relcnvfi 6933	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 6934	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 6935	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 6936	A one-to-one function whose domain is a set is finite if and only if its range is finite. See also f1vrnfibi 6937. (Contributed by AV, 10-Jan-2020.)
|- ( ( A e. V /\ F : A -1-1-> B ) -> ( F e. Fin <-> ran F e. Fin ) )
Theorem	f1vrnfibi 6937	A one-to-one function which is a set is finite if and only if its range is finite. See also f1dmvrnfibi 6936. (Contributed by AV, 10-Jan-2020.)
|- ( ( F e. V /\ F : A -1-1-> B ) -> ( F e. Fin <-> ran F e. Fin ) )
Theorem	iunfidisj 6938*	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	f1finf1o 6939	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 6940	A set with one element is a singleton. (Contributed by FL, 18-Aug-2008.)
|- ( ( A e. B /\ B ~~ 1o ) -> B = { A } )
Theorem	en1eqsnbi 6941	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 6942*	A case where the antecedent of snexg 4181 is not needed. The class { x | ph } is from dcextest 4576. (Contributed by Mario Carneiro and Jim Kingdon, 4-Jul-2022.)
|- { { x | ph } } e. _V
Theorem	preimaf1ofi 6943	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 6944*	Lemma for fidcenum 6948. 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 6945*	Lemma for fidcenum 6948. Induction step for fidcenumlemrk 6946. (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 6946*	Lemma for fidcenum 6948. (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 6947*	Lemma for fidcenum 6948. 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 6948*	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.32  Schroeder-Bernstein Theorem
Theorem	sbthlem1 6949*	Lemma for isbth 6959. (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 6950*	Lemma for isbth 6959. (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 6951*	Lemma for isbth 6959. (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 6952*	Lemma for isbth 6959. (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 6953*	Lemma for isbth 6959. (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 6954*	Lemma for isbth 6959. (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 6955*	Lemma for isbth 6959. (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 6956*	Lemma for isbth 6959. (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 6957*	Lemma for isbth 6959. (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 6958*	Lemma for isbth 6959. (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 6959	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 6949 through sbthlemi10 6958; this final piece mainly changes bound variables to eliminate the hypotheses of sbthlemi10 6958. 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 14394. (Contributed by NM, 8-Jun-1998.)
|- ( (EXMID /\ ( A ~<_ B /\ B ~<_ A ) ) -> A ~~ B )
2.6.33  Finite intersections
Syntax	cfi 6960	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 6961*	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 6964). (Contributed by FL, 27-Apr-2008.)
|- fi = ( x e. _V |-> { z | E. y e. ( ~P x i^i Fin ) z = |^| y } )
Theorem	fival 6962*	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 6963*	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 6964*	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 6965	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 6966	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 6967	The set of finite intersections of the empty set. (Contributed by Mario Carneiro, 30-Aug-2015.)
|- ( fi ` (/) ) = (/)
Theorem	fieq0 6968	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 6969	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 6970	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 6971	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 6972*	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 6973*	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.34  Supremum and infimum
Syntax	csup 6974	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 6975	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 6976*	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 6977	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 6978	Equality theorem for supremum. (Contributed by NM, 22-May-1999.)
|- ( B = C -> sup ( B , A , R ) = sup ( C , A , R ) )
Theorem	supeq1d 6979	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 6980	Equality inference for supremum. (Contributed by Paul Chapman, 22-Jun-2011.)
|- B = C   =>    |- sup ( B , A , R ) = sup ( C , A , R )
Theorem	supeq2 6981	Equality theorem for supremum. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( B = C -> sup ( A , B , R ) = sup ( A , C , R ) )
Theorem	supeq3 6982	Equality theorem for supremum. (Contributed by Scott Fenton, 13-Jun-2018.)
|- ( R = S -> sup ( A , B , R ) = sup ( A , B , S ) )
Theorem	supeq123d 6983	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 6984	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 6985*	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 8014) 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 6986*	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 6987*	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 6988*	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 6989*	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 6990*	A supremum belongs to its base class (closure law). See also supubti 6991 and suplubti 6992. (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 6991*	A supremum is an upper bound. See also supclti 6990 and suplubti 6992. This proof demonstrates how to expand an iota-based definition (df-iota 5173) using riotacl2 5837. (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 6992*	A supremum is the least upper bound. See also supclti 6990 and supubti 6991. (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 6993*	Bidirectional form of suplubti 6992. (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 6994*	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 6995	The supremum under an empty base set is always the empty set. (Contributed by AV, 4-Sep-2020.)
|- sup ( B , (/) , R ) = (/)
Theorem	supmaxti 6996*	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 6997*	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 6998*	Lemma for isoti 6999. (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 6999*	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 7000*	Lemma for supisoti 7002. (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 ) ) ) )