P. 111 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 11001-11100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	facwordi 11001	Ordering property of factorial. (Contributed by NM, 9-Dec-2005.)
|- ( ( M e. NN0 /\ N e. NN0 /\ M <_ N ) -> ( ! ` M ) <_ ( ! ` N ) )
Theorem	faclbnd 11002	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 11003	A lower bound for the factorial function. (Contributed by NM, 17-Dec-2005.)
|- ( N e. NN0 -> ( ( 2 ^ N ) / 2 ) <_ ( ! ` N ) )
Theorem	faclbnd3 11004	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 11005	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 11006	An upper bound for the factorial function. (Contributed by Mario Carneiro, 15-Apr-2016.)
|- ( N e. NN0 -> ( ! ` N ) <_ ( N ^ N ) )
Theorem	facavg 11007	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 11008	Extend class notation to include the binomial coefficient operation (combinatorial choose operation).
class _C
Definition	df-bc 11009*	Define the binomial coefficient operation. For example, ( 5 _C 3 ) = 1 0 (ex-bc 16325). 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 11010	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 11011 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 11011	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 11012	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 11013	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 11014	Closure of the binomial coefficient in the positive reals. (This is mostly a lemma before we have bccl2 11029.) (Contributed by Mario Carneiro, 10-Mar-2014.)
|- ( K e. ( 0 ... N ) -> ( N _C K ) e. RR+ )
Theorem	bccmpl 11015	"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 11016	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 11017	The binomial coefficient " 0 choose K " is 0 for a positive integer K. Note that ( 0 _C 0 ) = 1 (see bcn0 11016). (Contributed by Alexander van der Vekens, 1-Jan-2018.)
|- ( K e. NN -> ( 0 _C K ) = 0 )
Theorem	bcnn 11018	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 11019	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 11020	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 11021	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 11022	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 11023	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 11024	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 11025	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 11026	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 11027	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 11028	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 11029	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 11030	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 11031	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 11032	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 11033	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 11034	The value of four choose three. (Contributed by Scott Fenton, 11-Jun-2016.)
|- ( 4 _C 3 ) = 4
Theorem	4bc2eq6 11035	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 11036	Extend the definition of a class to include the set size function.
class ♯
Definition	df-ihash 11037*	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. Since we don't know that an arbitrary set is either finite or infinite (by inffiexmid 7097), the behavior beyond finite sets is not as useful as it might appear. For example, we wouldn't expect to be able to define this function in a meaningful way on ~P 1o, which cannot be shown to be finite (per pw1fin 7101). Note that we use the sharp sign (♯) for this function and we use the different character octothorpe (#) for the apartness relation (see df-ap 8761). 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 11038*	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 11039	The value of the ♯ function on an infinite set. (Contributed by Jim Kingdon, 20-Feb-2022.)
|- ( om ~<_ A -> (♯ ` A ) = +oo )
Theorem	hashennnuni 11040*	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 11041*	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 11042	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 11043	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 11044	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 11045	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 11046*	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 11047*	There is no bijection between a finite set and an infinite set. By infnfi 7083 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 11048	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 11049	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 11050	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 11051	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 11052	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 11053	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 11054	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 11055	Two ways of saying a finite set is not empty. Also, "A is inhabited" would be equivalent by fin0 7073. (Contributed by Alexander van der Vekens, 23-Sep-2018.) (Intuitionized by Jim Kingdon, 23-Feb-2022.)
|- ( A e. Fin -> ( 0 < (♯ ` A ) <-> A =/= (/) ) )
Theorem	hashnncl 11056	Positive natural closure of the hash function. (Contributed by Mario Carneiro, 16-Jan-2015.)
|- ( A e. Fin -> ( (♯ ` A ) e. NN <-> A =/= (/) ) )
Theorem	hash0 11057	The empty set has size zero. (Contributed by Mario Carneiro, 8-Jul-2014.)
|- (♯ ` (/) ) = 0
Theorem	fihashelne0d 11058	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 11059	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 11060	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	en1hash 11061	A set equinumerous to the ordinal one has size 1 . (Contributed by Jim Kingdon, 11-Mar-2026.)
|- ( A ~~ 1o -> (♯ ` A ) = 1 )
Theorem	fihashfn 11062	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 11063	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 11064	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 11065	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 11066	Lemma for hashun 11067. 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 11067	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	fihashgt0 11068	The cardinality of a finite nonempty set is greater than zero. (Contributed by Thierry Arnoux, 2-Mar-2017.)
|- ( ( A e. Fin /\ A =/= (/) ) -> 0 < (♯ ` A ) )
Theorem	1elfz0hash 11069	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 11070	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 11071	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 11072	There is (at least) one set with two different elements: the unordered pair containing 0 and 1. In contrast to pr0hash2ex 11078, 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 11073	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 11074	Size of a natural number ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.)
|- (♯ ` 1o ) = 1
Theorem	hash2 11075	Size of a natural number ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.)
|- (♯ ` 2o ) = 2
Theorem	hash3 11076	Size of a natural number ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.)
|- (♯ ` 3o ) = 3
Theorem	hash4 11077	Size of a natural number ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.)
|- (♯ ` 4o ) = 4
Theorem	pr0hash2ex 11078	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 11079	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 11080	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 11081	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 11082	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 11083	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 11084	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 11085	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 11086	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 11087	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 11088	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 11089	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 11090*	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 11091*	Lemma for fiubz 11092 and fiubnn 11093. 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 11092*	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 11093*	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 11094	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 11095	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 11096	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 11097	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 11098	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 11099*	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 } )
Theorem	leisorel 11100	Version of isorel 5948 for strictly increasing functions on the reals. (Contributed by Mario Carneiro, 6-Apr-2015.) (Revised by Mario Carneiro, 9-Sep-2015.)
|- ( ( F Isom < , < ( A , B ) /\ ( A C_ RR* /\ B C_ RR* ) /\ ( C e. A /\ D e. A ) ) -> ( C <_ D <-> ( F ` C ) <_ ( F ` D ) ) )