P. 113 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 11201-11300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bcval5 11201	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 11202	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 11203	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 11204	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 11205	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 11206	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	bcm1n 11207	The proportion of one binomial coefficient to another with N decreased by 1. (Contributed by Thierry Arnoux, 9-Nov-2016.)
|- ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> ( ( ( N - 1 ) _C K ) / ( N _C K ) ) = ( ( N - K ) / N ) )
Theorem	bcn2m1 11208	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 11209	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 11210	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 11211	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 11212	The value of four choose three. (Contributed by Scott Fenton, 11-Jun-2016.)
|- ( 4 _C 3 ) = 4
Theorem	4bc2eq6 11213	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 11214	Extend the definition of a class to include the set size function.
class ♯
Definition	df-ihash 11215*	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 7213), 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 7217). Note that we use the sharp sign (♯) for this function and we use the different character octothorpe (#) for the apartness relation (see df-ap 8910). 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 11216*	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 11217	The value of the ♯ function on an infinite set. (Contributed by Jim Kingdon, 20-Feb-2022.)
|- ( om ~<_ A -> (♯ ` A ) = +oo )
Theorem	hashennnuni 11218*	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 11219*	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 11220	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 11221	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 11222	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 11223	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 11224*	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 11225*	There is no bijection between a finite set and an infinite set. By infnfi 7199 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 11226	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 11227	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 11228	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 11229	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 11230	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 11231	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 11232	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 11233	Two ways of saying a finite set is not empty. Also, "A is inhabited" would be equivalent by fin0 7189. (Contributed by Alexander van der Vekens, 23-Sep-2018.) (Intuitionized by Jim Kingdon, 23-Feb-2022.)
|- ( A e. Fin -> ( 0 < (♯ ` A ) <-> A =/= (/) ) )
Theorem	hashnncl 11234	Positive natural closure of the hash function. (Contributed by Mario Carneiro, 16-Jan-2015.)
|- ( A e. Fin -> ( (♯ ` A ) e. NN <-> A =/= (/) ) )
Theorem	hash0 11235	The empty set has size zero. (Contributed by Mario Carneiro, 8-Jul-2014.)
|- (♯ ` (/) ) = 0
Theorem	fihashelne0d 11236	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 11237	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 11238	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 11239	A set equinumerous to the ordinal one has size 1 . (Contributed by Jim Kingdon, 11-Mar-2026.)
|- ( A ~~ 1o -> (♯ ` A ) = 1 )
Theorem	fihashfn 11240	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 11241	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 11242	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 11243	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 11244	Lemma for hashun 11245. 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 11245	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 11246	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 11247	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 11248	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 11249	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 11250	There is (at least) one set with two different elements: the unordered pair containing 0 and 1. In contrast to pr0hash2ex 11256, 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 11251	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 11252	Size of a natural number ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.)
|- (♯ ` 1o ) = 1
Theorem	hash2 11253	Size of a natural number ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.)
|- (♯ ` 2o ) = 2
Theorem	hash3 11254	Size of a natural number ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.)
|- (♯ ` 3o ) = 3
Theorem	hash4 11255	Size of a natural number ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.)
|- (♯ ` 4o ) = 4
Theorem	pr0hash2ex 11256	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 11257	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 11258	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 11259	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 11260	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 11261	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 11262	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 11263	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 11264	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 11265	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 11266	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 11267	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	hashmap 11268	The size of the set exponential of two finite sets is the exponential of their sizes. (This is the original motivation behind the notation for set exponentiation.) (Contributed by Mario Carneiro, 5-Aug-2014.) (Proof shortened by AV, 18-Jul-2022.)
|- ( ( A e. Fin /\ B e. Fin ) -> (♯ ` ( A ^m B ) ) = ( (♯ ` A ) ^ (♯ ` B ) ) )
Theorem	hashpwfi 11269	The number of finite subsets of a finite set is two raised to the power of the size of the set. For a similar theorem with set size expressed using equinumerosity, see 2omapfi 7320. For the number of subsets (which need not be finite) of a set, see pw1mapen 17026. (Contributed by Jim Kingdon, 5-Jun-2026.)
|- ( A e. Fin -> (♯ ` ( ~P A i^i Fin ) ) = ( 2 ^ (♯ ` A ) ) )
Theorem	fimaxq 11270*	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 11271*	Lemma for fiubz 11272 and fiubnn 11273. 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 11272*	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 11273*	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 11274	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 11275	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 11276	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 11277	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 11278	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	sseqn 11279*	Two ways to express the subsets of a class of a given size. It might seem that { x e. ~P A | (♯ ` x ) = N } would suffice, but that would require the converse of hashcl 11220 or something similar. Although each side of the equality would be well defined if we changed N e. NN0 to N e. ZZ, they would give different results for the (degenerate) case of a negative size, as shown at ssenneg 11280 and sshashneg 11281. (Contributed by Jim Kingdon, 22-May-2026.)
|- ( N e. NN0 -> { x e. ~P A | x ~~ ( 1 ... N ) } = { x e. ( ~P A i^i Fin ) | (♯ ` x ) = N } )
Theorem	ssenneg 11280*	Subsets of a class of a negative size (a degenerate case). Together with sshashneg 11281 this shows that sseqn 11279 could not be extended beyond N e. NN0. (Contributed by Jim Kingdon, 22-May-2026.)
|- ( ( N e. ZZ /\ N < 0 ) -> { x e. ~P A | x ~~ ( 1 ... N ) } = { (/) } )
Theorem	sshashneg 11281*	Subsets of a class of a negative size (a degenerate case). Together with ssenneg 11280 this shows that sseqn 11279 could not be extended beyond N e. NN0. (Contributed by Jim Kingdon, 22-May-2026.)
|- ( ( N e. ZZ /\ N < 0 ) -> { x e. ( ~P A i^i Fin ) | (♯ ` x ) = N } = (/) )
Theorem	hashfibclem 11282*	Lemma for hashfibc 11283: inductive step. (Contributed by Mario Carneiro, 13-Jul-2014.)
|- ( ph -> A e. Fin )   &    |- ( ph -> -. z e. A )   &    |- ( ph -> A. j e. ZZ ( (♯ ` A ) _C j ) = (♯ ` { x e. ( ~P A i^i Fin ) | (♯ ` x ) = j } ) )   &    |- ( ph -> K e. ZZ )   =>    |- ( ph -> ( (♯ ` ( A u. { z } ) ) _C K ) = (♯ ` { x e. ( ~P ( A u. { z } ) i^i Fin ) | (♯ ` x ) = K } ) )
Theorem	hashfibc 11283*	The binomial coefficient counts the number of subsets of a finite set of a given size. This is Metamath 100 proof #58 (formula for the number of combinations). For more on the notation for subsets of a given size, see sseqn 11279. (Contributed by Mario Carneiro, 13-Jul-2014.)
|- ( ( A e. Fin /\ K e. ZZ ) -> ( (♯ ` A ) _C K ) = (♯ ` { x e. ( ~P A i^i Fin ) | (♯ ` x ) = K } ) )
Theorem	hashfacen 11284*	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	hashf1lem1 11285*	Lemma for hashf1 11287. (Contributed by Mario Carneiro, 17-Apr-2015.) (Proof shortened by AV, 14-Aug-2024.)
|- ( ph -> A e. Fin )   &    |- ( ph -> B e. Fin )   &    |- ( ph -> -. z e. A )   &    |- ( ph -> ( (♯ ` A ) + 1 ) <_ (♯ ` B ) )   &    |- ( ph -> F : A -1-1-> B )   =>    |- ( ph -> { f | ( ( f |` A ) = F /\ f : ( A u. { z } ) -1-1-> B ) } ~~ ( B \ ran F ) )
Theorem	hashf1lem2 11286*	Lemma for hashf1 11287. (Contributed by Mario Carneiro, 17-Apr-2015.)
|- ( ph -> A e. Fin )   &    |- ( ph -> B e. Fin )   &    |- ( ph -> -. z e. A )   &    |- ( ph -> ( (♯ ` A ) + 1 ) <_ (♯ ` B ) )   =>    |- ( ph -> (♯ ` { f | f : ( A u. { z } ) -1-1-> B } ) = ( ( (♯ ` B ) - (♯ ` A ) ) x. (♯ ` { f | f : A -1-1-> B } ) ) )
Theorem	hashf1 11287*	The permutation number | A | ! x. ( | B | _C | A | ) = | B | ! / ( | B | - | A | ) ! counts the number of injections from A to B. (Contributed by Mario Carneiro, 21-Jan-2015.)
|- ( ( A e. Fin /\ B e. Fin ) -> (♯ ` { f | f : A -1-1-> B } ) = ( ( ! ` (♯ ` A ) ) x. ( (♯ ` B ) _C (♯ ` A ) ) ) )
Theorem	hashfac 11288*	A factorial counts the number of bijections on a finite set. (Contributed by Mario Carneiro, 21-Jan-2015.) (Proof shortened by Mario Carneiro, 17-Apr-2015.)
|- ( A e. Fin -> (♯ ` { f | f : A -1-1-onto-> A } ) = ( ! ` (♯ ` A ) ) )
Theorem	leisorel 11289	Version of isorel 6014 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 ) ) )
Theorem	zfz1isolemsplit 11290	Lemma for zfz1iso 11293. Removing one element from an integer range. (Contributed by Jim Kingdon, 8-Sep-2022.)
|- ( ph -> X e. Fin )   &    |- ( ph -> M e. X )   =>    |- ( ph -> ( 1 ... (♯ ` X ) ) = ( ( 1 ... (♯ ` ( X \ { M } ) ) ) u. { (♯ ` X ) } ) )
Theorem	zfz1isolemiso 11291*	Lemma for zfz1iso 11293. Adding one element to the order isomorphism. (Contributed by Jim Kingdon, 8-Sep-2022.)
|- ( ph -> X e. Fin )   &    |- ( ph -> X C_ ZZ )   &    |- ( ph -> M e. X )   &    |- ( ph -> A. z e. X z <_ M )   &    |- ( ph -> G Isom < , < ( ( 1 ... (♯ ` ( X \ { M } ) ) ) , ( X \ { M } ) ) )   &    |- ( ph -> A e. ( 1 ... (♯ ` X ) ) )   &    |- ( ph -> B e. ( 1 ... (♯ ` X ) ) )   =>    |- ( ph -> ( A < B <-> ( ( G u. { <. (♯ ` X ) , M >. } ) ` A ) < ( ( G u. { <. (♯ ` X ) , M >. } ) ` B ) ) )
Theorem	zfz1isolem1 11292*	Lemma for zfz1iso 11293. Existence of an order isomorphism given the existence of shorter isomorphisms. (Contributed by Jim Kingdon, 7-Sep-2022.)
|- ( ph -> K e. om )   &    |- ( ph -> A. y ( ( ( y C_ ZZ /\ y e. Fin ) /\ y ~~ K ) -> E. f f Isom < , < ( ( 1 ... (♯ ` y ) ) , y ) ) )   &    |- ( ph -> X C_ ZZ )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> X ~~ suc K )   &    |- ( ph -> M e. X )   &    |- ( ph -> A. z e. X z <_ M )   =>    |- ( ph -> E. f f Isom < , < ( ( 1 ... (♯ ` X ) ) , X ) )
Theorem	zfz1iso 11293*	A finite set of integers has an order isomorphism to a one-based finite sequence. (Contributed by Jim Kingdon, 3-Sep-2022.)
|- ( ( A C_ ZZ /\ A e. Fin ) -> E. f f Isom < , < ( ( 1 ... (♯ ` A ) ) , A ) )
Theorem	seq3coll 11294*	The function F contains a sparse set of nonzero values to be summed. The function G is an order isomorphism from the set of nonzero values of F to a 1-based finite sequence, and H collects these nonzero values together. Under these conditions, the sum over the values in H yields the same result as the sum over the original set F. (Contributed by Mario Carneiro, 2-Apr-2014.) (Revised by Jim Kingdon, 9-Apr-2023.)
|- ( ( ph /\ k e. S ) -> ( Z .+ k ) = k )   &    |- ( ( ph /\ k e. S ) -> ( k .+ Z ) = k )   &    |- ( ( ph /\ ( k e. S /\ n e. S ) ) -> ( k .+ n ) e. S )   &    |- ( ph -> Z e. S )   &    |- ( ph -> G Isom < , < ( ( 1 ... (♯ ` A ) ) , A ) )   &    |- ( ph -> N e. ( 1 ... (♯ ` A ) ) )   &    |- ( ph -> A C_ ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) e. S )   &    |- ( ( ph /\ k e. ( ZZ>= ` 1 ) ) -> ( H ` k ) e. S )   &    |- ( ( ph /\ k e. ( ( M ... ( G ` (♯ ` A ) ) ) \ A ) ) -> ( F ` k ) = Z )   &    |- ( ( ph /\ n e. ( 1 ... (♯ ` A ) ) ) -> ( H ` n ) = ( F ` ( G ` n ) ) )   =>    |- ( ph -> ( seq M ( .+ , F ) ` ( G ` N ) ) = ( seq 1 ( .+ , H ) ` N ) )
4.6.10.1  Proper unordered pairs and triples (sets of size 2 and 3)
Theorem	hash2en 11295	Two equivalent ways to say a set has two elements. (Contributed by Jim Kingdon, 4-Dec-2025.)
|- ( V ~~ 2o <-> ( V e. Fin /\ (♯ ` V ) = 2 ) )
Theorem	hashdmprop2dom 11296	A class which contains two ordered pairs with different first components has at least two elements. (Contributed by AV, 12-Nov-2021.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. Y )   &    |- ( ph -> F e. Z )   &    |- ( ph -> A =/= B )   &    |- ( ph -> { <. A , C >. , <. B , D >. } C_ F )   =>    |- ( ph -> 2o ~<_ dom F )
Theorem	hashtpgim 11297	The size of an unordered triple of three different elements. (Contributed by Alexander van der Vekens, 10-Nov-2017.) (Revised by AV, 18-Sep-2021.) (Revised by Jim Kingdon, 17-Apr-2026.)
|- ( ( A e. U /\ B e. V /\ C e. W ) -> ( ( A =/= B /\ B =/= C /\ C =/= A ) -> (♯ ` { A , B , C } ) = 3 ) )
Theorem	hashtpglem 11298	Lemma for hashtpg 11299. This is one of the three not-equal conclusions required for the reverse direction. (Contributed by Jim Kingdon, 18-Apr-2026.)
|- ( ph -> A e. U )   &    |- ( ph -> B e. V )   &    |- ( ph -> C e. W )   &    |- ( ph -> (♯ ` { A , B , C } ) = 3 )   =>    |- ( ph -> B =/= C )
Theorem	hashtpg 11299	The size of an unordered triple of three different elements. (Contributed by Alexander van der Vekens, 10-Nov-2017.) (Revised by AV, 18-Sep-2021.)
|- ( ( A e. U /\ B e. V /\ C e. W ) -> ( ( A =/= B /\ B =/= C /\ C =/= A ) <-> (♯ ` { A , B , C } ) = 3 ) )
4.6.10.2  Functions with a domain containing at least two different elements
Theorem	fundm2domnop0 11300	A function with a domain containing (at least) two different elements is not an ordered pair. This theorem (which requires that ( G \ { (/) } ) needs to be a function instead of G) is useful for proofs for extensible structures, see structn0fun 13365. (Contributed by AV, 12-Oct-2020.) (Revised by AV, 7-Jun-2021.) (Proof shortened by AV, 15-Nov-2021.)
|- ( ( Fun ( G \ { (/) } ) /\ 2o ~<_ dom G ) -> -. G e. ( _V X. _V ) )