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	php5fin 6901	A finite set is not equinumerous to a set which adds one element. (Contributed by Jim Kingdon, 13-Sep-2021.)
|- ( ( A e. Fin /\ B e. ( _V \ A ) ) -> -. A ~~ ( A u. { B } ) )
Theorem	fisbth 6902	Schroeder-Bernstein Theorem for finite sets. (Contributed by Jim Kingdon, 12-Sep-2021.)
|- ( ( ( A e. Fin /\ B e. Fin ) /\ ( A ~<_ B /\ B ~<_ A ) ) -> A ~~ B )
Theorem	0fin 6903	The empty set is finite. (Contributed by FL, 14-Jul-2008.)
|- (/) e. Fin
Theorem	fin0 6904*	A nonempty finite set has at least one element. (Contributed by Jim Kingdon, 10-Sep-2021.)
|- ( A e. Fin -> ( A =/= (/) <-> E. x x e. A ) )
Theorem	fin0or 6905*	A finite set is either empty or inhabited. (Contributed by Jim Kingdon, 30-Sep-2021.)
|- ( A e. Fin -> ( A = (/) \/ E. x x e. A ) )
Theorem	diffitest 6906*	If subtracting any set from a finite set gives a finite set, any proposition of the form -. ph is decidable. This is not a proof of full excluded middle, but it is close enough to show we won't be able to prove A e. Fin -> ( A \ B ) e. Fin. (Contributed by Jim Kingdon, 8-Sep-2021.)
|- A. a e. Fin A. b ( a \ b ) e. Fin   =>    |- ( -. ph \/ -. -. ph )
Theorem	findcard 6907*	Schema for induction on the cardinality of a finite set. The inductive hypothesis is that the result is true on the given set with any one element removed. The result is then proven to be true for all finite sets. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( x = (/) -> ( ph <-> ps ) )   &    |- ( x = ( y \ { z } ) -> ( ph <-> ch ) )   &    |- ( x = y -> ( ph <-> th ) )   &    |- ( x = A -> ( ph <-> ta ) )   &    |- ps   &    |- ( y e. Fin -> ( A. z e. y ch -> th ) )   =>    |- ( A e. Fin -> ta )
Theorem	findcard2 6908*	Schema for induction on the cardinality of a finite set. The inductive step shows that the result is true if one more element is added to the set. The result is then proven to be true for all finite sets. (Contributed by Jeff Madsen, 8-Jul-2010.)
|- ( x = (/) -> ( ph <-> ps ) )   &    |- ( x = y -> ( ph <-> ch ) )   &    |- ( x = ( y u. { z } ) -> ( ph <-> th ) )   &    |- ( x = A -> ( ph <-> ta ) )   &    |- ps   &    |- ( y e. Fin -> ( ch -> th ) )   =>    |- ( A e. Fin -> ta )
Theorem	findcard2s 6909*	Variation of findcard2 6908 requiring that the element added in the induction step not be a member of the original set. (Contributed by Paul Chapman, 30-Nov-2012.)
|- ( x = (/) -> ( ph <-> ps ) )   &    |- ( x = y -> ( ph <-> ch ) )   &    |- ( x = ( y u. { z } ) -> ( ph <-> th ) )   &    |- ( x = A -> ( ph <-> ta ) )   &    |- ps   &    |- ( ( y e. Fin /\ -. z e. y ) -> ( ch -> th ) )   =>    |- ( A e. Fin -> ta )
Theorem	findcard2d 6910*	Deduction version of findcard2 6908. If you also need y e. Fin (which doesn't come for free due to ssfiexmid 6895), use findcard2sd 6911 instead. (Contributed by SO, 16-Jul-2018.)
|- ( x = (/) -> ( ps <-> ch ) )   &    |- ( x = y -> ( ps <-> th ) )   &    |- ( x = ( y u. { z } ) -> ( ps <-> ta ) )   &    |- ( x = A -> ( ps <-> et ) )   &    |- ( ph -> ch )   &    |- ( ( ph /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( th -> ta ) )   &    |- ( ph -> A e. Fin )   =>    |- ( ph -> et )
Theorem	findcard2sd 6911*	Deduction form of finite set induction . (Contributed by Jim Kingdon, 14-Sep-2021.)
|- ( x = (/) -> ( ps <-> ch ) )   &    |- ( x = y -> ( ps <-> th ) )   &    |- ( x = ( y u. { z } ) -> ( ps <-> ta ) )   &    |- ( x = A -> ( ps <-> et ) )   &    |- ( ph -> ch )   &    |- ( ( ( ph /\ y e. Fin ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( th -> ta ) )   &    |- ( ph -> A e. Fin )   =>    |- ( ph -> et )
Theorem	diffisn 6912	Subtracting a singleton from a finite set produces a finite set. (Contributed by Jim Kingdon, 11-Sep-2021.)
|- ( ( A e. Fin /\ B e. A ) -> ( A \ { B } ) e. Fin )
Theorem	diffifi 6913	Subtracting one finite set from another produces a finite set. (Contributed by Jim Kingdon, 8-Sep-2021.)
|- ( ( A e. Fin /\ B e. Fin /\ B C_ A ) -> ( A \ B ) e. Fin )
Theorem	infnfi 6914	An infinite set is not finite. (Contributed by Jim Kingdon, 20-Feb-2022.)
|- ( om ~<_ A -> -. A e. Fin )
Theorem	ominf 6915	The set of natural numbers is not finite. Although we supply this theorem because we can, the more natural way to express " om is infinite" is om ~<_ om which is an instance of domrefg 6786. (Contributed by NM, 2-Jun-1998.)
|- -. om e. Fin
Theorem	isinfinf 6916*	An infinite set contains subsets of arbitrarily large finite cardinality. (Contributed by Jim Kingdon, 15-Jun-2022.)
|- ( om ~<_ A -> A. n e. om E. x ( x C_ A /\ x ~~ n ) )
Theorem	ac6sfi 6917*	Existence of a choice function for finite sets. (Contributed by Jeff Hankins, 26-Jun-2009.) (Proof shortened by Mario Carneiro, 29-Jan-2014.)
|- ( y = ( f ` x ) -> ( ph <-> ps ) )   =>    |- ( ( A e. Fin /\ A. x e. A E. y e. B ph ) -> E. f ( f : A --> B /\ A. x e. A ps ) )
Theorem	tridc 6918*	A trichotomous order is decidable. (Contributed by Jim Kingdon, 5-Sep-2022.)
|- ( ph -> R Po A )   &    |- ( ph -> A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) )   &    |- ( ph -> B e. A )   &    |- ( ph -> C e. A )   =>    |- ( ph -> DECID B R C )
Theorem	fimax2gtrilemstep 6919*	Lemma for fimax2gtri 6920. The induction step. (Contributed by Jim Kingdon, 5-Sep-2022.)
|- ( ph -> R Po A )   &    |- ( ph -> A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) )   &    |- ( ph -> A e. Fin )   &    |- ( ph -> A =/= (/) )   &    |- ( ph -> U e. Fin )   &    |- ( ph -> U C_ A )   &    |- ( ph -> Z e. A )   &    |- ( ph -> V e. A )   &    |- ( ph -> -. V e. U )   &    |- ( ph -> A. y e. U -. Z R y )   =>    |- ( ph -> E. x e. A A. y e. ( U u. { V } ) -. x R y )
Theorem	fimax2gtri 6920*	A finite set has a maximum under a trichotomous order. (Contributed by Jim Kingdon, 5-Sep-2022.)
|- ( ph -> R Po A )   &    |- ( ph -> A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) )   &    |- ( ph -> A e. Fin )   &    |- ( ph -> A =/= (/) )   =>    |- ( ph -> E. x e. A A. y e. A -. x R y )
Theorem	finexdc 6921*	Decidability of existence, over a finite set and defined by a decidable proposition. (Contributed by Jim Kingdon, 12-Jul-2022.)
|- ( ( A e. Fin /\ A. x e. A DECID ph ) -> DECID E. x e. A ph )
Theorem	dfrex2fin 6922*	Relationship between universal and existential quantifiers over a finite set. Remark in Section 2.2.1 of [Pierik], p. 8. Although Pierik does not mention the decidability condition explicitly, it does say "only finitely many x to check" which means there must be some way of checking each value of x. (Contributed by Jim Kingdon, 11-Jul-2022.)
|- ( ( A e. Fin /\ A. x e. A DECID ph ) -> ( E. x e. A ph <-> -. A. x e. A -. ph ) )
Theorem	infm 6923*	An infinite set is inhabited. (Contributed by Jim Kingdon, 18-Feb-2022.)
|- ( om ~<_ A -> E. x x e. A )
Theorem	infn0 6924	An infinite set is not empty. (Contributed by NM, 23-Oct-2004.)
|- ( om ~<_ A -> A =/= (/) )
Theorem	inffiexmid 6925*	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 6926	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 6927	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 6928	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 6929	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 6930	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 6931	Reformulation of ss1o0el1 4212 using 1o instead of { (/) }. (Contributed by BJ, 9-Aug-2024.)
|- ( A C_ 1o -> ( (/) e. A <-> A = 1o ) )
Theorem	pw1dc1 6932	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 6933	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 6934*	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 6935	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 6936*	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 6937	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 6938	The B e. V condition in unsnfi 6937. This is intended to show that unsnfi 6937 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 6939	The -. B e. A condition in unsnfi 6937. This is intended to show that unsnfi 6937 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 6940	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 6941*	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 6942*	Union of complementary parts into whole. This is a case where we can strengthen undifss 3518 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 6943	Union of complementary parts into whole. This is a case where we can strengthen undifss 3518 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 6944	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 6945	A pair is finite if it consists of two unequal sets. For the case where A = B, see snfig 6833. For the cases where one or both is a proper class, see prprc1 3715, prprc2 3716, or prprc 3717. (Contributed by Jim Kingdon, 31-May-2022.)
|- ( ( A e. V /\ B e. W /\ A =/= B ) -> { A , B } e. Fin )
Theorem	tpfidisj 6946	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 6947*	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 6948	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 6949	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 6950	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 6951	Corollary of the Pigeonhole Principle using equality. Strengthening of phpm 6884 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 6952*	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 6953*	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	infidc 6954*	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 6955	An ordinal which is a singleton is { (/) }. (Contributed by Jim Kingdon, 19-Oct-2021.)
|- ( ( A e. V /\ { A } e. On ) -> A = (/) )
Theorem	fnfi 6956	A version of fnex 5755 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 6957	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 6958	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 6959	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 6960	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 6961	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 6962	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 6963	A one-to-one function whose domain is a set is finite if and only if its range is finite. See also f1vrnfibi 6964. (Contributed by AV, 10-Jan-2020.)
|- ( ( A e. V /\ F : A -1-1-> B ) -> ( F e. Fin <-> ran F e. Fin ) )
Theorem	f1vrnfibi 6964	A one-to-one function which is a set is finite if and only if its range is finite. See also f1dmvrnfibi 6963. (Contributed by AV, 10-Jan-2020.)
|- ( ( F e. V /\ F : A -1-1-> B ) -> ( F e. Fin <-> ran F e. Fin ) )
Theorem	iunfidisj 6965*	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 6966	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 6967	A set with one element is a singleton. (Contributed by FL, 18-Aug-2008.)
|- ( ( A e. B /\ B ~~ 1o ) -> B = { A } )
Theorem	en1eqsnbi 6968	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 6969*	A case where the antecedent of snexg 4199 is not needed. The class { x | ph } is from dcextest 4595. (Contributed by Mario Carneiro and Jim Kingdon, 4-Jul-2022.)
|- { { x | ph } } e. _V
Theorem	preimaf1ofi 6970	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 6971*	Lemma for fidcenum 6975. 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 6972*	Lemma for fidcenum 6975. Induction step for fidcenumlemrk 6973. (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 6973*	Lemma for fidcenum 6975. (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 6974*	Lemma for fidcenum 6975. 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 6975*	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 6976*	Lemma for isbth 6986. (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 6977*	Lemma for isbth 6986. (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 6978*	Lemma for isbth 6986. (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 6979*	Lemma for isbth 6986. (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 6980*	Lemma for isbth 6986. (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 6981*	Lemma for isbth 6986. (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 6982*	Lemma for isbth 6986. (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 6983*	Lemma for isbth 6986. (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 6984*	Lemma for isbth 6986. (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 6985*	Lemma for isbth 6986. (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 6986	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 6976 through sbthlemi10 6985; this final piece mainly changes bound variables to eliminate the hypotheses of sbthlemi10 6985. 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 15176. (Contributed by NM, 8-Jun-1998.)
|- ( (EXMID /\ ( A ~<_ B /\ B ~<_ A ) ) -> A ~~ B )
2.6.33  Finite intersections
Syntax	cfi 6987	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 6988*	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 6991). (Contributed by FL, 27-Apr-2008.)
|- fi = ( x e. _V |-> { z | E. y e. ( ~P x i^i Fin ) z = |^| y } )
Theorem	fival 6989*	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 6990*	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 6991*	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 6992	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 6993	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 6994	The set of finite intersections of the empty set. (Contributed by Mario Carneiro, 30-Aug-2015.)
|- ( fi ` (/) ) = (/)
Theorem	fieq0 6995	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 6996	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 6997	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 6998	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 6999*	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 7000*	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 )