P. 108 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 10701-10800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	facne0 10701	The factorial function is nonzero. (Contributed by NM, 26-Apr-2005.)
|- ( N e. NN0 -> ( ! ` N ) =/= 0 )
Theorem	facdiv 10702	A positive integer divides the factorial of an equal or larger number. (Contributed by NM, 2-May-2005.)
|- ( ( M e. NN0 /\ N e. NN /\ N <_ M ) -> ( ( ! ` M ) / N ) e. NN )
Theorem	facndiv 10703	No positive integer (greater than one) divides the factorial plus one of an equal or larger number. (Contributed by NM, 3-May-2005.)
|- ( ( ( M e. NN0 /\ N e. NN ) /\ ( 1 < N /\ N <_ M ) ) -> -. ( ( ( ! ` M ) + 1 ) / N ) e. ZZ )
Theorem	facwordi 10704	Ordering property of factorial. (Contributed by NM, 9-Dec-2005.)
|- ( ( M e. NN0 /\ N e. NN0 /\ M <_ N ) -> ( ! ` M ) <_ ( ! ` N ) )
Theorem	faclbnd 10705	A lower bound for the factorial function. (Contributed by NM, 17-Dec-2005.)
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( M ^ ( N + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` N ) ) )
Theorem	faclbnd2 10706	A lower bound for the factorial function. (Contributed by NM, 17-Dec-2005.)
|- ( N e. NN0 -> ( ( 2 ^ N ) / 2 ) <_ ( ! ` N ) )
Theorem	faclbnd3 10707	A lower bound for the factorial function. (Contributed by NM, 19-Dec-2005.)
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( M ^ N ) <_ ( ( M ^ M ) x. ( ! ` N ) ) )
Theorem	faclbnd6 10708	Geometric lower bound for the factorial function, where N is usually held constant. (Contributed by Paul Chapman, 28-Dec-2007.)
|- ( ( N e. NN0 /\ M e. NN0 ) -> ( ( ! ` N ) x. ( ( N + 1 ) ^ M ) ) <_ ( ! ` ( N + M ) ) )
Theorem	facubnd 10709	An upper bound for the factorial function. (Contributed by Mario Carneiro, 15-Apr-2016.)
|- ( N e. NN0 -> ( ! ` N ) <_ ( N ^ N ) )
Theorem	facavg 10710	The product of two factorials is greater than or equal to the factorial of (the floor of) their average. (Contributed by NM, 9-Dec-2005.)
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( ! ` ( |_ ` ( ( M + N ) / 2 ) ) ) <_ ( ( ! ` M ) x. ( ! ` N ) ) )
4.6.9  The binomial coefficient operation
Syntax	cbc 10711	Extend class notation to include the binomial coefficient operation (combinatorial choose operation).
class _C
Definition	df-bc 10712*	Define the binomial coefficient operation. For example, ( 5 _C 3 ) = 1 0 (ex-bc 14137). In the literature, this function is often written as a column vector of the two arguments, or with the arguments as subscripts before and after the letter "C". ( N _C K ) is read " N choose K." Definition of binomial coefficient in [Gleason] p. 295. As suggested by Gleason, we define it to be 0 when 0 <_ k <_ n does not hold. (Contributed by NM, 10-Jul-2005.)
|- _C = ( n e. NN0 , k e. ZZ |-> if ( k e. ( 0 ... n ) , ( ( ! ` n ) / ( ( ! ` ( n - k ) ) x. ( ! ` k ) ) ) , 0 ) )
Theorem	bcval 10713	Value of the binomial coefficient, N choose K. Definition of binomial coefficient in [Gleason] p. 295. As suggested by Gleason, we define it to be 0 when 0 <_ K <_ N does not hold. See bcval2 10714 for the value in the standard domain. (Contributed by NM, 10-Jul-2005.) (Revised by Mario Carneiro, 7-Nov-2013.)
|- ( ( N e. NN0 /\ K e. ZZ ) -> ( N _C K ) = if ( K e. ( 0 ... N ) , ( ( ! ` N ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) , 0 ) )
Theorem	bcval2 10714	Value of the binomial coefficient, N choose K, in its standard domain. (Contributed by NM, 9-Jun-2005.) (Revised by Mario Carneiro, 7-Nov-2013.)
|- ( K e. ( 0 ... N ) -> ( N _C K ) = ( ( ! ` N ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) )
Theorem	bcval3 10715	Value of the binomial coefficient, N choose K, outside of its standard domain. Remark in [Gleason] p. 295. (Contributed by NM, 14-Jul-2005.) (Revised by Mario Carneiro, 8-Nov-2013.)
|- ( ( N e. NN0 /\ K e. ZZ /\ -. K e. ( 0 ... N ) ) -> ( N _C K ) = 0 )
Theorem	bcval4 10716	Value of the binomial coefficient, N choose K, outside of its standard domain. Remark in [Gleason] p. 295. (Contributed by NM, 14-Jul-2005.) (Revised by Mario Carneiro, 7-Nov-2013.)
|- ( ( N e. NN0 /\ K e. ZZ /\ ( K < 0 \/ N < K ) ) -> ( N _C K ) = 0 )
Theorem	bcrpcl 10717	Closure of the binomial coefficient in the positive reals. (This is mostly a lemma before we have bccl2 10732.) (Contributed by Mario Carneiro, 10-Mar-2014.)
|- ( K e. ( 0 ... N ) -> ( N _C K ) e. RR+ )
Theorem	bccmpl 10718	"Complementing" its second argument doesn't change a binary coefficient. (Contributed by NM, 21-Jun-2005.) (Revised by Mario Carneiro, 5-Mar-2014.)
|- ( ( N e. NN0 /\ K e. ZZ ) -> ( N _C K ) = ( N _C ( N - K ) ) )
Theorem	bcn0 10719	N choose 0 is 1. Remark in [Gleason] p. 296. (Contributed by NM, 17-Jun-2005.) (Revised by Mario Carneiro, 8-Nov-2013.)
|- ( N e. NN0 -> ( N _C 0 ) = 1 )
Theorem	bc0k 10720	The binomial coefficient " 0 choose K " is 0 for a positive integer K. Note that ( 0 _C 0 ) = 1 (see bcn0 10719). (Contributed by Alexander van der Vekens, 1-Jan-2018.)
|- ( K e. NN -> ( 0 _C K ) = 0 )
Theorem	bcnn 10721	N choose N is 1. Remark in [Gleason] p. 296. (Contributed by NM, 17-Jun-2005.) (Revised by Mario Carneiro, 8-Nov-2013.)
|- ( N e. NN0 -> ( N _C N ) = 1 )
Theorem	bcn1 10722	Binomial coefficient: N choose 1. (Contributed by NM, 21-Jun-2005.) (Revised by Mario Carneiro, 8-Nov-2013.)
|- ( N e. NN0 -> ( N _C 1 ) = N )
Theorem	bcnp1n 10723	Binomial coefficient: N + 1 choose N. (Contributed by NM, 20-Jun-2005.) (Revised by Mario Carneiro, 8-Nov-2013.)
|- ( N e. NN0 -> ( ( N + 1 ) _C N ) = ( N + 1 ) )
Theorem	bcm1k 10724	The proportion of one binomial coefficient to another with K decreased by 1. (Contributed by Mario Carneiro, 10-Mar-2014.)
|- ( K e. ( 1 ... N ) -> ( N _C K ) = ( ( N _C ( K - 1 ) ) x. ( ( N - ( K - 1 ) ) / K ) ) )
Theorem	bcp1n 10725	The proportion of one binomial coefficient to another with N increased by 1. (Contributed by Mario Carneiro, 10-Mar-2014.)
|- ( K e. ( 0 ... N ) -> ( ( N + 1 ) _C K ) = ( ( N _C K ) x. ( ( N + 1 ) / ( ( N + 1 ) - K ) ) ) )
Theorem	bcp1nk 10726	The proportion of one binomial coefficient to another with N and K increased by 1. (Contributed by Mario Carneiro, 16-Jan-2015.)
|- ( K e. ( 0 ... N ) -> ( ( N + 1 ) _C ( K + 1 ) ) = ( ( N _C K ) x. ( ( N + 1 ) / ( K + 1 ) ) ) )
Theorem	bcval5 10727	Write out the top and bottom parts of the binomial coefficient ( N _C K ) = ( N x. ( N - 1 ) x. ... x. ( ( N - K ) + 1 ) ) / K ! explicitly. In this form, it is valid even for N < K, although it is no longer valid for nonpositive K. (Contributed by Mario Carneiro, 22-May-2014.) (Revised by Jim Kingdon, 23-Apr-2023.)
|- ( ( N e. NN0 /\ K e. NN ) -> ( N _C K ) = ( ( seq ( ( N - K ) + 1 ) ( x. , _I ) ` N ) / ( ! ` K ) ) )
Theorem	bcn2 10728	Binomial coefficient: N choose 2. (Contributed by Mario Carneiro, 22-May-2014.)
|- ( N e. NN0 -> ( N _C 2 ) = ( ( N x. ( N - 1 ) ) / 2 ) )
Theorem	bcp1m1 10729	Compute the binomial coefficient of ( N + 1 ) over ( N - 1 ) (Contributed by Scott Fenton, 11-May-2014.) (Revised by Mario Carneiro, 22-May-2014.)
|- ( N e. NN0 -> ( ( N + 1 ) _C ( N - 1 ) ) = ( ( ( N + 1 ) x. N ) / 2 ) )
Theorem	bcpasc 10730	Pascal's rule for the binomial coefficient, generalized to all integers K. Equation 2 of [Gleason] p. 295. (Contributed by NM, 13-Jul-2005.) (Revised by Mario Carneiro, 10-Mar-2014.)
|- ( ( N e. NN0 /\ K e. ZZ ) -> ( ( N _C K ) + ( N _C ( K - 1 ) ) ) = ( ( N + 1 ) _C K ) )
Theorem	bccl 10731	A binomial coefficient, in its extended domain, is a nonnegative integer. (Contributed by NM, 10-Jul-2005.) (Revised by Mario Carneiro, 9-Nov-2013.)
|- ( ( N e. NN0 /\ K e. ZZ ) -> ( N _C K ) e. NN0 )
Theorem	bccl2 10732	A binomial coefficient, in its standard domain, is a positive integer. (Contributed by NM, 3-Jan-2006.) (Revised by Mario Carneiro, 10-Mar-2014.)
|- ( K e. ( 0 ... N ) -> ( N _C K ) e. NN )
Theorem	bcn2m1 10733	Compute the binomial coefficient " N choose 2 " from " ( N - 1 ) choose 2 ": (N-1) + ( (N-1) 2 ) = ( N 2 ). (Contributed by Alexander van der Vekens, 7-Jan-2018.)
|- ( N e. NN -> ( ( N - 1 ) + ( ( N - 1 ) _C 2 ) ) = ( N _C 2 ) )
Theorem	bcn2p1 10734	Compute the binomial coefficient " ( N + 1 ) choose 2 " from " N choose 2 ": N + ( N 2 ) = ( (N+1) 2 ). (Contributed by Alexander van der Vekens, 8-Jan-2018.)
|- ( N e. NN0 -> ( N + ( N _C 2 ) ) = ( ( N + 1 ) _C 2 ) )
Theorem	permnn 10735	The number of permutations of N - R objects from a collection of N objects is a positive integer. (Contributed by Jason Orendorff, 24-Jan-2007.)
|- ( R e. ( 0 ... N ) -> ( ( ! ` N ) / ( ! ` R ) ) e. NN )
Theorem	bcnm1 10736	The binomial coefficent of ( N - 1 ) is N. (Contributed by Scott Fenton, 16-May-2014.)
|- ( N e. NN0 -> ( N _C ( N - 1 ) ) = N )
Theorem	4bc3eq4 10737	The value of four choose three. (Contributed by Scott Fenton, 11-Jun-2016.)
|- ( 4 _C 3 ) = 4
Theorem	4bc2eq6 10738	The value of four choose two. (Contributed by Scott Fenton, 9-Jan-2017.)
|- ( 4 _C 2 ) = 6
4.6.10  The ` # ` (set size) function
Syntax	chash 10739	Extend the definition of a class to include the set size function.
class ♯
Definition	df-ihash 10740*	Define the set size function ♯, which gives the cardinality of a finite set as a member of NN0, and assigns all infinite sets the value +oo. For example, (♯ ` { 0 , 1 , 2 } ) = 3. Note that we use the sharp sign (♯) for this function and we use the different character octothorpe (#) for the apartness relation (see df-ap 8529). We adopt the former notation from Corollary 8.2.4 of [AczelRathjen], p. 80 (although that work only defines it for finite sets). This definition (in terms of U. and ~<_) is not taken directly from the literature, but for finite sets should be equivalent to the conventional definition that the size of a finite set is the unique natural number which is equinumerous to the given set. (Contributed by Jim Kingdon, 19-Feb-2022.)
|- ♯ = ( (frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 ) u. { <. om , +oo >. } ) o. ( x e. _V |-> U. { y e. ( om u. { om } ) | y ~<_ x } ) )
Theorem	hashinfuni 10741*	The ordinal size of an infinite set is om. (Contributed by Jim Kingdon, 20-Feb-2022.)
|- ( om ~<_ A -> U. { y e. ( om u. { om } ) | y ~<_ A } = om )
Theorem	hashinfom 10742	The value of the ♯ function on an infinite set. (Contributed by Jim Kingdon, 20-Feb-2022.)
|- ( om ~<_ A -> (♯ ` A ) = +oo )
Theorem	hashennnuni 10743*	The ordinal size of a set equinumerous to an element of om is that element of om. (Contributed by Jim Kingdon, 20-Feb-2022.)
|- ( ( N e. om /\ N ~~ A ) -> U. { y e. ( om u. { om } ) | y ~<_ A } = N )
Theorem	hashennn 10744*	The size of a set equinumerous to an element of om. (Contributed by Jim Kingdon, 21-Feb-2022.)
|- ( ( N e. om /\ N ~~ A ) -> (♯ ` A ) = (frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 ) ` N ) )
Theorem	hashcl 10745	Closure of the ♯ function. (Contributed by Paul Chapman, 26-Oct-2012.) (Revised by Mario Carneiro, 13-Jul-2014.)
|- ( A e. Fin -> (♯ ` A ) e. NN0 )
Theorem	hashfiv01gt1 10746	The size of a finite set is either 0 or 1 or greater than 1. (Contributed by Jim Kingdon, 21-Feb-2022.)
|- ( M e. Fin -> ( (♯ ` M ) = 0 \/ (♯ ` M ) = 1 \/ 1 < (♯ ` M ) ) )
Theorem	hashfz1 10747	The set ( 1 ... N ) has N elements. (Contributed by Paul Chapman, 22-Jun-2011.) (Revised by Mario Carneiro, 15-Sep-2013.)
|- ( N e. NN0 -> (♯ ` ( 1 ... N ) ) = N )
Theorem	hashen 10748	Two finite sets have the same number of elements iff they are equinumerous. (Contributed by Paul Chapman, 22-Jun-2011.) (Revised by Mario Carneiro, 15-Sep-2013.)
|- ( ( A e. Fin /\ B e. Fin ) -> ( (♯ ` A ) = (♯ ` B ) <-> A ~~ B ) )
Theorem	hasheqf1o 10749*	The size of two finite sets is equal if and only if there is a bijection mapping one of the sets onto the other. (Contributed by Alexander van der Vekens, 17-Dec-2017.)
|- ( ( A e. Fin /\ B e. Fin ) -> ( (♯ ` A ) = (♯ ` B ) <-> E. f f : A -1-1-onto-> B ) )
Theorem	fiinfnf1o 10750*	There is no bijection between a finite set and an infinite set. By infnfi 6889 the theorem would also hold if "infinite" were expressed as om ~<_ B. (Contributed by Alexander van der Vekens, 25-Dec-2017.)
|- ( ( A e. Fin /\ -. B e. Fin ) -> -. E. f f : A -1-1-onto-> B )
Theorem	fihasheqf1oi 10751	The size of two finite sets is equal if there is a bijection mapping one of the sets onto the other. (Contributed by Jim Kingdon, 21-Feb-2022.)
|- ( ( A e. Fin /\ F : A -1-1-onto-> B ) -> (♯ ` A ) = (♯ ` B ) )
Theorem	fihashf1rn 10752	The size of a finite set which is a one-to-one function is equal to the size of the function's range. (Contributed by Jim Kingdon, 21-Feb-2022.)
|- ( ( A e. Fin /\ F : A -1-1-> B ) -> (♯ ` F ) = (♯ ` ran F ) )
Theorem	fihasheqf1od 10753	The size of two finite sets is equal if there is a bijection mapping one of the sets onto the other. (Contributed by Jim Kingdon, 21-Feb-2022.)
|- ( ph -> A e. Fin )   &    |- ( ph -> F : A -1-1-onto-> B )   =>    |- ( ph -> (♯ ` A ) = (♯ ` B ) )
Theorem	fz1eqb 10754	Two possibly-empty 1-based finite sets of sequential integers are equal iff their endpoints are equal. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Mario Carneiro, 29-Mar-2014.)
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( ( 1 ... M ) = ( 1 ... N ) <-> M = N ) )
Theorem	filtinf 10755	The size of an infinite set is greater than the size of a finite set. (Contributed by Jim Kingdon, 21-Feb-2022.)
|- ( ( A e. Fin /\ om ~<_ B ) -> (♯ ` A ) < (♯ ` B ) )
Theorem	isfinite4im 10756	A finite set is equinumerous to the range of integers from one up to the hash value of the set. (Contributed by Jim Kingdon, 22-Feb-2022.)
|- ( A e. Fin -> ( 1 ... (♯ ` A ) ) ~~ A )
Theorem	fihasheq0 10757	Two ways of saying a finite set is empty. (Contributed by Paul Chapman, 26-Oct-2012.) (Revised by Mario Carneiro, 27-Jul-2014.) (Intuitionized by Jim Kingdon, 23-Feb-2022.)
|- ( A e. Fin -> ( (♯ ` A ) = 0 <-> A = (/) ) )
Theorem	fihashneq0 10758	Two ways of saying a finite set is not empty. Also, "A is inhabited" would be equivalent by fin0 6879. (Contributed by Alexander van der Vekens, 23-Sep-2018.) (Intuitionized by Jim Kingdon, 23-Feb-2022.)
|- ( A e. Fin -> ( 0 < (♯ ` A ) <-> A =/= (/) ) )
Theorem	hashnncl 10759	Positive natural closure of the hash function. (Contributed by Mario Carneiro, 16-Jan-2015.)
|- ( A e. Fin -> ( (♯ ` A ) e. NN <-> A =/= (/) ) )
Theorem	hash0 10760	The empty set has size zero. (Contributed by Mario Carneiro, 8-Jul-2014.)
|- (♯ ` (/) ) = 0
Theorem	fihashelne0d 10761	A finite set with an element has nonzero size. (Contributed by Rohan Ridenour, 3-Aug-2023.)
|- ( ph -> B e. A )   &    |- ( ph -> A e. Fin )   =>    |- ( ph -> -. (♯ ` A ) = 0 )
Theorem	hashsng 10762	The size of a singleton. (Contributed by Paul Chapman, 26-Oct-2012.) (Proof shortened by Mario Carneiro, 13-Feb-2013.)
|- ( A e. V -> (♯ ` { A } ) = 1 )
Theorem	fihashen1 10763	A finite set has size 1 if and only if it is equinumerous to the ordinal 1. (Contributed by AV, 14-Apr-2019.) (Intuitionized by Jim Kingdon, 23-Feb-2022.)
|- ( A e. Fin -> ( (♯ ` A ) = 1 <-> A ~~ 1o ) )
Theorem	fihashfn 10764	A function on a finite set is equinumerous to its domain. (Contributed by Mario Carneiro, 12-Mar-2015.) (Intuitionized by Jim Kingdon, 24-Feb-2022.)
|- ( ( F Fn A /\ A e. Fin ) -> (♯ ` F ) = (♯ ` A ) )
Theorem	fseq1hash 10765	The value of the size function on a finite 1-based sequence. (Contributed by Paul Chapman, 26-Oct-2012.) (Proof shortened by Mario Carneiro, 12-Mar-2015.)
|- ( ( N e. NN0 /\ F Fn ( 1 ... N ) ) -> (♯ ` F ) = N )
Theorem	omgadd 10766	Mapping ordinal addition to integer addition. (Contributed by Jim Kingdon, 24-Feb-2022.)
|- G = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   =>    |- ( ( A e. om /\ B e. om ) -> ( G ` ( A +o B ) ) = ( ( G ` A ) + ( G ` B ) ) )
Theorem	fihashdom 10767	Dominance relation for the size function. (Contributed by Jim Kingdon, 24-Feb-2022.)
|- ( ( A e. Fin /\ B e. Fin ) -> ( (♯ ` A ) <_ (♯ ` B ) <-> A ~<_ B ) )
Theorem	hashunlem 10768	Lemma for hashun 10769. Ordinal size of the union. (Contributed by Jim Kingdon, 25-Feb-2022.)
|- ( ph -> A e. Fin )   &    |- ( ph -> B e. Fin )   &    |- ( ph -> ( A i^i B ) = (/) )   &    |- ( ph -> N e. om )   &    |- ( ph -> M e. om )   &    |- ( ph -> A ~~ N )   &    |- ( ph -> B ~~ M )   =>    |- ( ph -> ( A u. B ) ~~ ( N +o M ) )
Theorem	hashun 10769	The size of the union of disjoint finite sets is the sum of their sizes. (Contributed by Paul Chapman, 30-Nov-2012.) (Revised by Mario Carneiro, 15-Sep-2013.)
|- ( ( A e. Fin /\ B e. Fin /\ ( A i^i B ) = (/) ) -> (♯ ` ( A u. B ) ) = ( (♯ ` A ) + (♯ ` B ) ) )
Theorem	1elfz0hash 10770	1 is an element of the finite set of sequential nonnegative integers bounded by the size of a nonempty finite set. (Contributed by AV, 9-May-2020.)
|- ( ( A e. Fin /\ A =/= (/) ) -> 1 e. ( 0 ... (♯ ` A ) ) )
Theorem	hashunsng 10771	The size of the union of a finite set with a disjoint singleton is one more than the size of the set. (Contributed by Paul Chapman, 30-Nov-2012.)
|- ( B e. V -> ( ( A e. Fin /\ -. B e. A ) -> (♯ ` ( A u. { B } ) ) = ( (♯ ` A ) + 1 ) ) )
Theorem	hashprg 10772	The size of an unordered pair. (Contributed by Mario Carneiro, 27-Sep-2013.) (Revised by Mario Carneiro, 5-May-2016.) (Revised by AV, 18-Sep-2021.)
|- ( ( A e. V /\ B e. W ) -> ( A =/= B <-> (♯ ` { A , B } ) = 2 ) )
Theorem	prhash2ex 10773	There is (at least) one set with two different elements: the unordered pair containing 0 and 1. In contrast to pr0hash2ex 10779, numbers are used instead of sets because their representation is shorter (and more comprehensive). (Contributed by AV, 29-Jan-2020.)
|- (♯ ` { 0 , 1 } ) = 2
Theorem	hashp1i 10774	Size of a natural number ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.)
|- A e. om   &    |- B = suc A   &    |- (♯ ` A ) = M   &    |- ( M + 1 ) = N   =>    |- (♯ ` B ) = N
Theorem	hash1 10775	Size of a natural number ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.)
|- (♯ ` 1o ) = 1
Theorem	hash2 10776	Size of a natural number ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.)
|- (♯ ` 2o ) = 2
Theorem	hash3 10777	Size of a natural number ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.)
|- (♯ ` 3o ) = 3
Theorem	hash4 10778	Size of a natural number ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.)
|- (♯ ` 4o ) = 4
Theorem	pr0hash2ex 10779	There is (at least) one set with two different elements: the unordered pair containing the empty set and the singleton containing the empty set. (Contributed by AV, 29-Jan-2020.)
|- (♯ ` { (/) , { (/) } } ) = 2
Theorem	fihashss 10780	The size of a subset is less than or equal to the size of its superset. (Contributed by Alexander van der Vekens, 14-Jul-2018.)
|- ( ( A e. Fin /\ B e. Fin /\ B C_ A ) -> (♯ ` B ) <_ (♯ ` A ) )
Theorem	fiprsshashgt1 10781	The size of a superset of a proper unordered pair is greater than 1. (Contributed by AV, 6-Feb-2021.)
|- ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ C e. Fin ) -> ( { A , B } C_ C -> 2 <_ (♯ ` C ) ) )
Theorem	fihashssdif 10782	The size of the difference of a finite set and a finite subset is the set's size minus the subset's. (Contributed by Jim Kingdon, 31-May-2022.)
|- ( ( A e. Fin /\ B e. Fin /\ B C_ A ) -> (♯ ` ( A \ B ) ) = ( (♯ ` A ) - (♯ ` B ) ) )
Theorem	hashdifsn 10783	The size of the difference of a finite set and a singleton subset is the set's size minus 1. (Contributed by Alexander van der Vekens, 6-Jan-2018.)
|- ( ( A e. Fin /\ B e. A ) -> (♯ ` ( A \ { B } ) ) = ( (♯ ` A ) - 1 ) )
Theorem	hashdifpr 10784	The size of the difference of a finite set and a proper ordered pair subset is the set's size minus 2. (Contributed by AV, 16-Dec-2020.)
|- ( ( A e. Fin /\ ( B e. A /\ C e. A /\ B =/= C ) ) -> (♯ ` ( A \ { B , C } ) ) = ( (♯ ` A ) - 2 ) )
Theorem	hashfz 10785	Value of the numeric cardinality of a nonempty integer range. (Contributed by Stefan O'Rear, 12-Sep-2014.) (Proof shortened by Mario Carneiro, 15-Apr-2015.)
|- ( B e. ( ZZ>= ` A ) -> (♯ ` ( A ... B ) ) = ( ( B - A ) + 1 ) )
Theorem	hashfzo 10786	Cardinality of a half-open set of integers. (Contributed by Stefan O'Rear, 15-Aug-2015.)
|- ( B e. ( ZZ>= ` A ) -> (♯ ` ( A..^ B ) ) = ( B - A ) )
Theorem	hashfzo0 10787	Cardinality of a half-open set of integers based at zero. (Contributed by Stefan O'Rear, 15-Aug-2015.)
|- ( B e. NN0 -> (♯ ` ( 0..^ B ) ) = B )
Theorem	hashfzp1 10788	Value of the numeric cardinality of a (possibly empty) integer range. (Contributed by AV, 19-Jun-2021.)
|- ( B e. ( ZZ>= ` A ) -> (♯ ` ( ( A + 1 ) ... B ) ) = ( B - A ) )
Theorem	hashfz0 10789	Value of the numeric cardinality of a nonempty range of nonnegative integers. (Contributed by Alexander van der Vekens, 21-Jul-2018.)
|- ( B e. NN0 -> (♯ ` ( 0 ... B ) ) = ( B + 1 ) )
Theorem	hashxp 10790	The size of the Cartesian product of two finite sets is the product of their sizes. (Contributed by Paul Chapman, 30-Nov-2012.)
|- ( ( A e. Fin /\ B e. Fin ) -> (♯ ` ( A X. B ) ) = ( (♯ ` A ) x. (♯ ` B ) ) )
Theorem	fimaxq 10791*	A finite set of rational numbers has a maximum. (Contributed by Jim Kingdon, 6-Sep-2022.)
|- ( ( A C_ QQ /\ A e. Fin /\ A =/= (/) ) -> E. x e. A A. y e. A y <_ x )
Theorem	fiubm 10792*	Lemma for fiubz 10793 and fiubnn 10794. A general form of those theorems. (Contributed by Jim Kingdon, 29-Oct-2024.)
|- ( ph -> A C_ B )   &    |- ( ph -> B C_ QQ )   &    |- ( ph -> C e. B )   &    |- ( ph -> A e. Fin )   =>    |- ( ph -> E. x e. B A. y e. A y <_ x )
Theorem	fiubz 10793*	A finite set of integers has an upper bound which is an integer. (Contributed by Jim Kingdon, 29-Oct-2024.)
|- ( ( A C_ ZZ /\ A e. Fin ) -> E. x e. ZZ A. y e. A y <_ x )
Theorem	fiubnn 10794*	A finite set of natural numbers has an upper bound which is a a natural number. (Contributed by Jim Kingdon, 29-Oct-2024.)
|- ( ( A C_ NN /\ A e. Fin ) -> E. x e. NN A. y e. A y <_ x )
Theorem	resunimafz0 10795	The union of a restriction by an image over an open range of nonnegative integers and a singleton of an ordered pair is a restriction by an image over an interval of nonnegative integers. (Contributed by Mario Carneiro, 8-Apr-2015.) (Revised by AV, 20-Feb-2021.)
|- ( ph -> Fun I )   &    |- ( ph -> F : ( 0..^ (♯ ` F ) ) --> dom I )   &    |- ( ph -> N e. ( 0..^ (♯ ` F ) ) )   =>    |- ( ph -> ( I |` ( F " ( 0 ... N ) ) ) = ( ( I |` ( F " ( 0..^ N ) ) ) u. { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } ) )
Theorem	fnfz0hash 10796	The size of a function on a finite set of sequential nonnegative integers. (Contributed by Alexander van der Vekens, 25-Jun-2018.)
|- ( ( N e. NN0 /\ F Fn ( 0 ... N ) ) -> (♯ ` F ) = ( N + 1 ) )
Theorem	ffz0hash 10797	The size of a function on a finite set of sequential nonnegative integers equals the upper bound of the sequence increased by 1. (Contributed by Alexander van der Vekens, 15-Mar-2018.) (Proof shortened by AV, 11-Apr-2021.)
|- ( ( N e. NN0 /\ F : ( 0 ... N ) --> B ) -> (♯ ` F ) = ( N + 1 ) )
Theorem	ffzo0hash 10798	The size of a function on a half-open range of nonnegative integers. (Contributed by Alexander van der Vekens, 25-Mar-2018.)
|- ( ( N e. NN0 /\ F Fn ( 0..^ N ) ) -> (♯ ` F ) = N )
Theorem	fnfzo0hash 10799	The size of a function on a half-open range of nonnegative integers equals the upper bound of this range. (Contributed by Alexander van der Vekens, 26-Jan-2018.) (Proof shortened by AV, 11-Apr-2021.)
|- ( ( N e. NN0 /\ F : ( 0..^ N ) --> B ) -> (♯ ` F ) = N )
Theorem	hashfacen 10800*	The number of bijections between two sets is a cardinal invariant. (Contributed by Mario Carneiro, 21-Jan-2015.)
|- ( ( A ~~ B /\ C ~~ D ) -> { f | f : A -1-1-onto-> C } ~~ { f | f : B -1-1-onto-> D } )