P. 71 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 7001-7100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	infm 7001*	An infinite set is inhabited. (Contributed by Jim Kingdon, 18-Feb-2022.)
|- ( om ~<_ A -> E. x x e. A )
Theorem	infn0 7002	An infinite set is not empty. (Contributed by NM, 23-Oct-2004.)
|- ( om ~<_ A -> A =/= (/) )
Theorem	inffiexmid 7003*	If any given set is either finite or infinite, excluded middle follows. (Contributed by Jim Kingdon, 15-Jun-2022.)
|- ( x e. Fin \/ om ~<_ x )   =>    |- ( ph \/ -. ph )
Theorem	en2eqpr 7004	Building a set with two elements. (Contributed by FL, 11-Aug-2008.) (Revised by Mario Carneiro, 10-Sep-2015.)
|- ( ( C ~~ 2o /\ A e. C /\ B e. C ) -> ( A =/= B -> C = { A , B } ) )
Theorem	exmidpw 7005	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 7006	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 7007	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 7008	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	exmidpw2en 7009	The power set of a set being equinumerous to set exponentiation with a base of ordinal 2o is equivalent to excluded middle. This is Metamath 100 proof #52. The forward direction uses excluded middle expressed as EXMID to show this equinumerosity. The reverse direction is the one which establishes that power set being equinumerous to set exponentiation implies excluded middle. This resolves the question of whether we will be able to prove this equinumerosity theorem in the negative. (Contributed by Jim Kingdon, 13-Aug-2022.)
|- (EXMID <-> A. x ~P x ~~ ( 2o ^m x ) )
Theorem	ss1o0el1o 7010	Reformulation of ss1o0el1 4241 using 1o instead of { (/) }. (Contributed by BJ, 9-Aug-2024.)
|- ( A C_ 1o -> ( (/) e. A <-> A = 1o ) )
Theorem	pw1dc1 7011	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 7012	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 7013*	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 7014	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 7015*	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 7016	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 7017	The B e. V condition in unsnfi 7016. This is intended to show that unsnfi 7016 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 7018	The -. B e. A condition in unsnfi 7016. This is intended to show that unsnfi 7016 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 7019	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 7020*	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 7021*	Union of complementary parts into whole. This is a case where we can strengthen undifss 3541 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 7022	Union of complementary parts into whole. This is a case where we can strengthen undifss 3541 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 7023	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 7024	A pair is finite if it consists of two unequal sets. For the case where A = B, see snfig 6906. For the cases where one or both is a proper class, see prprc1 3741, prprc2 3742, or prprc 3743. (Contributed by Jim Kingdon, 31-May-2022.)
|- ( ( A e. V /\ B e. W /\ A =/= B ) -> { A , B } e. Fin )
Theorem	prfidceq 7025*	A pair is finite if it consists of elements of a class with decidable equality. (Contributed by Jim Kingdon, 13-Oct-2025.)
|- ( ph -> A e. C )   &    |- ( ph -> B e. C )   &    |- ( ph -> A. x e. C A. y e. C DECID x = y )   =>    |- ( ph -> { A , B } e. Fin )
Theorem	tpfidisj 7026	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	tpfidceq 7027*	A triple is finite if it consists of elements of a class with decidable equality. (Contributed by Jim Kingdon, 13-Oct-2025.)
|- ( ph -> A e. D )   &    |- ( ph -> B e. D )   &    |- ( ph -> C e. D )   &    |- ( ph -> A. x e. D A. y e. D DECID x = y )   =>    |- ( ph -> { A , B , C } e. Fin )
Theorem	fiintim 7028*	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 7029	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 7030	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 7031	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 7032	Corollary of the Pigeonhole Principle using equality. Strengthening of phpm 6962 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 7033*	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 7034*	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	opabfi 7035*	Finiteness of an ordered pair abstraction which is a decidable subset of finite sets. (Contributed by Jim Kingdon, 16-Sep-2025.)
|- S = { <. x , y >. | ( ( x e. A /\ y e. B ) /\ ps ) }   &    |- ( ph -> A e. Fin )   &    |- ( ph -> B e. Fin )   &    |- ( ph -> A. x e. A A. y e. B DECID ps )   =>    |- ( ph -> S e. Fin )
Theorem	infidc 7036*	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 7037	An ordinal which is a singleton is { (/) }. (Contributed by Jim Kingdon, 19-Oct-2021.)
|- ( ( A e. V /\ { A } e. On ) -> A = (/) )
Theorem	fnfi 7038	A version of fnex 5806 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 7039	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 7040	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 7041	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 7042	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 7043	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 7044	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 7045	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 7046	A one-to-one function whose domain is a set is finite if and only if its range is finite. See also f1vrnfibi 7047. (Contributed by AV, 10-Jan-2020.)
|- ( ( A e. V /\ F : A -1-1-> B ) -> ( F e. Fin <-> ran F e. Fin ) )
Theorem	f1vrnfibi 7047	A one-to-one function which is a set is finite if and only if its range is finite. See also f1dmvrnfibi 7046. (Contributed by AV, 10-Jan-2020.)
|- ( ( F e. V /\ F : A -1-1-> B ) -> ( F e. Fin <-> ran F e. Fin ) )
Theorem	iunfidisj 7048*	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 7049	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 7050	A set with one element is a singleton. (Contributed by FL, 18-Aug-2008.)
|- ( ( A e. B /\ B ~~ 1o ) -> B = { A } )
Theorem	en1eqsnbi 7051	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 7052*	A case where the antecedent of snexg 4228 is not needed. The class { x | ph } is from dcextest 4629. (Contributed by Mario Carneiro and Jim Kingdon, 4-Jul-2022.)
|- { { x | ph } } e. _V
Theorem	preimaf1ofi 7053	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 7054*	Lemma for fidcenum 7058. 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 7055*	Lemma for fidcenum 7058. Induction step for fidcenumlemrk 7056. (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 7056*	Lemma for fidcenum 7058. (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 7057*	Lemma for fidcenum 7058. 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 7058*	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 7059*	Lemma for isbth 7069. (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 7060*	Lemma for isbth 7069. (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 7061*	Lemma for isbth 7069. (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 7062*	Lemma for isbth 7069. (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 7063*	Lemma for isbth 7069. (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 7064*	Lemma for isbth 7069. (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 7065*	Lemma for isbth 7069. (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 7066*	Lemma for isbth 7069. (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 7067*	Lemma for isbth 7069. (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 7068*	Lemma for isbth 7069. (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 7069	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 7059 through sbthlemi10 7068; this final piece mainly changes bound variables to eliminate the hypotheses of sbthlemi10 7068. 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 15962. (Contributed by NM, 8-Jun-1998.)
|- ( (EXMID /\ ( A ~<_ B /\ B ~<_ A ) ) -> A ~~ B )
2.6.33  Finite intersections
Syntax	cfi 7070	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 7071*	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 7074). (Contributed by FL, 27-Apr-2008.)
|- fi = ( x e. _V |-> { z | E. y e. ( ~P x i^i Fin ) z = |^| y } )
Theorem	fival 7072*	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 7073*	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 7074*	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 7075	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 7076	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 7077	The set of finite intersections of the empty set. (Contributed by Mario Carneiro, 30-Aug-2015.)
|- ( fi ` (/) ) = (/)
Theorem	fieq0 7078	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 7079	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 7080	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 7081	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 7082*	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 7083*	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 7084	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 7085	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 7086*	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 7087	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 7088	Equality theorem for supremum. (Contributed by NM, 22-May-1999.)
|- ( B = C -> sup ( B , A , R ) = sup ( C , A , R ) )
Theorem	supeq1d 7089	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 7090	Equality inference for supremum. (Contributed by Paul Chapman, 22-Jun-2011.)
|- B = C   =>    |- sup ( B , A , R ) = sup ( C , A , R )
Theorem	supeq2 7091	Equality theorem for supremum. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( B = C -> sup ( A , B , R ) = sup ( A , C , R ) )
Theorem	supeq3 7092	Equality theorem for supremum. (Contributed by Scott Fenton, 13-Jun-2018.)
|- ( R = S -> sup ( A , B , R ) = sup ( A , B , S ) )
Theorem	supeq123d 7093	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 7094	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 7095*	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 8152) 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 7096*	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 7097*	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 7098*	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 7099*	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 7100*	A supremum belongs to its base class (closure law). See also supubti 7101 and suplubti 7102. (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 )