P. 112 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 11101-11200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	3dec 11101	A "decimal constructor" which is used to build up "decimal integers" or "numeric terms" in base 10 with 3 "digits". (Contributed by AV, 14-Jun-2021.) (Revised by AV, 1-Aug-2021.)
|- A e. NN0   &    |- B e. NN0   =>    |- ;; A B C = ( ( ( (; 1 0 ^ 2 ) x. A ) + (; 1 0 x. B ) ) + C )
Theorem	expcanlem 11102	Lemma for expcan 11103. Proving the order in one direction. (Contributed by Jim Kingdon, 29-Jan-2022.)
|- ( ph -> A e. RR )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> 1 < A )   =>    |- ( ph -> ( ( A ^ M ) <_ ( A ^ N ) -> M <_ N ) )
Theorem	expcan 11103	Cancellation law for exponentiation. (Contributed by NM, 2-Aug-2006.) (Revised by Mario Carneiro, 4-Jun-2014.)
|- ( ( ( A e. RR /\ M e. ZZ /\ N e. ZZ ) /\ 1 < A ) -> ( ( A ^ M ) = ( A ^ N ) <-> M = N ) )
Theorem	expcand 11104	Ordering relationship for exponentiation. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> 1 < A )   &    |- ( ph -> ( A ^ M ) = ( A ^ N ) )   =>    |- ( ph -> M = N )
Theorem	apexp1 11105	Exponentiation and apartness. (Contributed by Jim Kingdon, 9-Jul-2024.)
|- ( ( A e. CC /\ B e. CC /\ N e. NN ) -> ( ( A ^ N ) # ( B ^ N ) -> A # B ) )
4.6.7  Ordered pair theorem for nonnegative integers
Theorem	nn0le2msqd 11106	The square function on nonnegative integers is monotonic. (Contributed by Jim Kingdon, 31-Oct-2021.)
|- ( ph -> A e. NN0 )   &    |- ( ph -> B e. NN0 )   =>    |- ( ph -> ( A <_ B <-> ( A x. A ) <_ ( B x. B ) ) )
Theorem	nn0opthlem1d 11107	A rather pretty lemma for nn0opth2 11111. (Contributed by Jim Kingdon, 31-Oct-2021.)
|- ( ph -> A e. NN0 )   &    |- ( ph -> C e. NN0 )   =>    |- ( ph -> ( A < C <-> ( ( A x. A ) + ( 2 x. A ) ) < ( C x. C ) ) )
Theorem	nn0opthlem2d 11108	Lemma for nn0opth2 11111. (Contributed by Jim Kingdon, 31-Oct-2021.)
|- ( ph -> A e. NN0 )   &    |- ( ph -> B e. NN0 )   &    |- ( ph -> C e. NN0 )   &    |- ( ph -> D e. NN0 )   =>    |- ( ph -> ( ( A + B ) < C -> ( ( C x. C ) + D ) =/= ( ( ( A + B ) x. ( A + B ) ) + B ) ) )
Theorem	nn0opthd 11109	An ordered pair theorem for nonnegative integers. Theorem 17.3 of [Quine] p. 124. We can represent an ordered pair of nonnegative integers A and B by ( ( ( A + B ) x. ( A + B ) ) + B ). If two such ordered pairs are equal, their first elements are equal and their second elements are equal. Contrast this ordered pair representation with the standard one df-op 3703 that works for any set. (Contributed by Jim Kingdon, 31-Oct-2021.)
|- ( ph -> A e. NN0 )   &    |- ( ph -> B e. NN0 )   &    |- ( ph -> C e. NN0 )   &    |- ( ph -> D e. NN0 )   =>    |- ( ph -> ( ( ( ( A + B ) x. ( A + B ) ) + B ) = ( ( ( C + D ) x. ( C + D ) ) + D ) <-> ( A = C /\ B = D ) ) )
Theorem	nn0opth2d 11110	An ordered pair theorem for nonnegative integers. Theorem 17.3 of [Quine] p. 124. See comments for nn0opthd 11109. (Contributed by Jim Kingdon, 31-Oct-2021.)
|- ( ph -> A e. NN0 )   &    |- ( ph -> B e. NN0 )   &    |- ( ph -> C e. NN0 )   &    |- ( ph -> D e. NN0 )   =>    |- ( ph -> ( ( ( ( A + B ) ^ 2 ) + B ) = ( ( ( C + D ) ^ 2 ) + D ) <-> ( A = C /\ B = D ) ) )
Theorem	nn0opth2 11111	An ordered pair theorem for nonnegative integers. Theorem 17.3 of [Quine] p. 124. See nn0opthd 11109. (Contributed by NM, 22-Jul-2004.)
|- ( ( ( A e. NN0 /\ B e. NN0 ) /\ ( C e. NN0 /\ D e. NN0 ) ) -> ( ( ( ( A + B ) ^ 2 ) + B ) = ( ( ( C + D ) ^ 2 ) + D ) <-> ( A = C /\ B = D ) ) )
4.6.8  Factorial function
Syntax	cfa 11112	Extend class notation to include the factorial of nonnegative integers.
class !
Definition	df-fac 11113	Define the factorial function on nonnegative integers. For example, ( ! ` 5 ) = 1 2 0 because 1 x. 2 x. 3 x. 4 x. 5 = 1 2 0 (ex-fac 16622). In the literature, the factorial function is written as a postscript exclamation point. (Contributed by NM, 2-Dec-2004.)
|- ! = ( { <. 0 , 1 >. } u. seq 1 ( x. , _I ) )
Theorem	facnn 11114	Value of the factorial function for positive integers. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.)
|- ( N e. NN -> ( ! ` N ) = ( seq 1 ( x. , _I ) ` N ) )
Theorem	fac0 11115	The factorial of 0. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.)
|- ( ! ` 0 ) = 1
Theorem	fac1 11116	The factorial of 1. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.)
|- ( ! ` 1 ) = 1
Theorem	facp1 11117	The factorial of a successor. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.)
|- ( N e. NN0 -> ( ! ` ( N + 1 ) ) = ( ( ! ` N ) x. ( N + 1 ) ) )
Theorem	fac2 11118	The factorial of 2. (Contributed by NM, 17-Mar-2005.)
|- ( ! ` 2 ) = 2
Theorem	fac3 11119	The factorial of 3. (Contributed by NM, 17-Mar-2005.)
|- ( ! ` 3 ) = 6
Theorem	fac4 11120	The factorial of 4. (Contributed by Mario Carneiro, 18-Jun-2015.)
|- ( ! ` 4 ) = ; 2 4
Theorem	facnn2 11121	Value of the factorial function expressed recursively. (Contributed by NM, 2-Dec-2004.)
|- ( N e. NN -> ( ! ` N ) = ( ( ! ` ( N - 1 ) ) x. N ) )
Theorem	faccl 11122	Closure of the factorial function. (Contributed by NM, 2-Dec-2004.)
|- ( N e. NN0 -> ( ! ` N ) e. NN )
Theorem	faccld 11123	Closure of the factorial function, deduction version of faccl 11122. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- ( ph -> N e. NN0 )   =>    |- ( ph -> ( ! ` N ) e. NN )
Theorem	facne0 11124	The factorial function is nonzero. (Contributed by NM, 26-Apr-2005.)
|- ( N e. NN0 -> ( ! ` N ) =/= 0 )
Theorem	facdiv 11125	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 11126	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 11127	Ordering property of factorial. (Contributed by NM, 9-Dec-2005.)
|- ( ( M e. NN0 /\ N e. NN0 /\ M <_ N ) -> ( ! ` M ) <_ ( ! ` N ) )
Theorem	faclbnd 11128	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 11129	A lower bound for the factorial function. (Contributed by NM, 17-Dec-2005.)
|- ( N e. NN0 -> ( ( 2 ^ N ) / 2 ) <_ ( ! ` N ) )
Theorem	faclbnd3 11130	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 11131	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 11132	An upper bound for the factorial function. (Contributed by Mario Carneiro, 15-Apr-2016.)
|- ( N e. NN0 -> ( ! ` N ) <_ ( N ^ N ) )
Theorem	facavg 11133	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 11134	Extend class notation to include the binomial coefficient operation (combinatorial choose operation).
class _C
Definition	df-bc 11135*	Define the binomial coefficient operation. For example, ( 5 _C 3 ) = 1 0 (ex-bc 16623). 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 11136	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 11137 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 11137	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 11138	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 11139	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 11140	Closure of the binomial coefficient in the positive reals. (This is mostly a lemma before we have bccl2 11155.) (Contributed by Mario Carneiro, 10-Mar-2014.)
|- ( K e. ( 0 ... N ) -> ( N _C K ) e. RR+ )
Theorem	bccmpl 11141	"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 11142	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 11143	The binomial coefficient " 0 choose K " is 0 for a positive integer K. Note that ( 0 _C 0 ) = 1 (see bcn0 11142). (Contributed by Alexander van der Vekens, 1-Jan-2018.)
|- ( K e. NN -> ( 0 _C K ) = 0 )
Theorem	bcnn 11144	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 11145	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 11146	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 11147	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 11148	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 11149	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 11150	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 11151	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 11152	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 11153	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 11154	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 11155	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 11156	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 11157	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 11158	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 11159	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 11160	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 11161	The value of four choose three. (Contributed by Scott Fenton, 11-Jun-2016.)
|- ( 4 _C 3 ) = 4
Theorem	4bc2eq6 11162	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 11163	Extend the definition of a class to include the set size function.
class ♯
Definition	df-ihash 11164*	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 7179), 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 7183). Note that we use the sharp sign (♯) for this function and we use the different character octothorpe (#) for the apartness relation (see df-ap 8873). 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 11165*	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 11166	The value of the ♯ function on an infinite set. (Contributed by Jim Kingdon, 20-Feb-2022.)
|- ( om ~<_ A -> (♯ ` A ) = +oo )
Theorem	hashennnuni 11167*	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 11168*	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 11169	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 11170	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 11171	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 11172	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 11173*	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 11174*	There is no bijection between a finite set and an infinite set. By infnfi 7165 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 11175	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 11176	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 11177	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 11178	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 11179	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 11180	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 11181	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 11182	Two ways of saying a finite set is not empty. Also, "A is inhabited" would be equivalent by fin0 7155. (Contributed by Alexander van der Vekens, 23-Sep-2018.) (Intuitionized by Jim Kingdon, 23-Feb-2022.)
|- ( A e. Fin -> ( 0 < (♯ ` A ) <-> A =/= (/) ) )
Theorem	hashnncl 11183	Positive natural closure of the hash function. (Contributed by Mario Carneiro, 16-Jan-2015.)
|- ( A e. Fin -> ( (♯ ` A ) e. NN <-> A =/= (/) ) )
Theorem	hash0 11184	The empty set has size zero. (Contributed by Mario Carneiro, 8-Jul-2014.)
|- (♯ ` (/) ) = 0
Theorem	fihashelne0d 11185	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 11186	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 11187	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 11188	A set equinumerous to the ordinal one has size 1 . (Contributed by Jim Kingdon, 11-Mar-2026.)
|- ( A ~~ 1o -> (♯ ` A ) = 1 )
Theorem	fihashfn 11189	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 11190	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 11191	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 11192	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 11193	Lemma for hashun 11194. 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 11194	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 11195	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 11196	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 11197	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 11198	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 11199	There is (at least) one set with two different elements: the unordered pair containing 0 and 1. In contrast to pr0hash2ex 11205, 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 11200	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