P. 113 of Theorem List - Intuitionistic Logic Explorer

Type

Label

Description

Statement

Theorem

hashen 11201

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 11202*

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 11203*

There is no bijection between a finite set and an infinite set. By infnfi 7189 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 11204

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 11205

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 11206

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 11207

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 11208

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 11209

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 11210

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 11211

Two ways of saying a finite set is not empty. Also, "A is inhabited" would be equivalent by fin0 7179. (Contributed by Alexander van der Vekens, 23-Sep-2018.) (Intuitionized by Jim Kingdon, 23-Feb-2022.)

|- ( A e. Fin -> ( 0 < (♯ ` A ) <-> A =/= (/) ) )

Theorem

hashnncl 11212

Positive natural closure of the hash function. (Contributed by Mario Carneiro, 16-Jan-2015.)

|- ( A e. Fin -> ( (♯ ` A ) e. NN <-> A =/= (/) ) )

Theorem

hash0 11213

The empty set has size zero. (Contributed by Mario Carneiro, 8-Jul-2014.)

|- (♯ ` (/) ) = 0

Theorem

fihashelne0d 11214

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 11215

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 11216

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 11217

A set equinumerous to the ordinal one has size 1 . (Contributed by Jim Kingdon, 11-Mar-2026.)

|- ( A ~~ 1o -> (♯ ` A ) = 1 )

Theorem

fihashfn 11218

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 11219

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 11220

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 11221

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 11222

Lemma for hashun 11223. 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 11223

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 11224

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 11225

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 11226

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 11227

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 11228

There is (at least) one set with two different elements: the unordered pair containing 0 and 1. In contrast to pr0hash2ex 11234, 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 11229

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 11230

Size of a natural number ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.)

|- (♯ ` 1o ) = 1

Theorem

hash2 11231

Size of a natural number ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.)

|- (♯ ` 2o ) = 2

Theorem

hash3 11232

Size of a natural number ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.)

|- (♯ ` 3o ) = 3

Theorem

hash4 11233

Size of a natural number ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.)

|- (♯ ` 4o ) = 4

Theorem

pr0hash2ex 11234

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 11235

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 11236

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 11237

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 11238

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 11239

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 11240

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 11241

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 11242

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 11243

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 11244

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 11245

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 11246

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 11247

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 7310. For the number of subsets (which need not be finite) of a set, see pw1mapen 16940. (Contributed by Jim Kingdon, 5-Jun-2026.)

|- ( A e. Fin -> (♯ ` ( ~P A i^i Fin ) ) = ( 2 ^ (♯ ` A ) ) )

Theorem

fimaxq 11248*

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 11249*

Lemma for fiubz 11250 and fiubnn 11251. 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 11250*

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 11251*

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 11252

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 11253

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 11254

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 11255

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 11256

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 11257*

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 11198 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 11258 and sshashneg 11259. (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 11258*

Subsets of a class of a negative size (a degenerate case). Together with sshashneg 11259 this shows that sseqn 11257 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 11259*

Subsets of a class of a negative size (a degenerate case). Together with ssenneg 11258 this shows that sseqn 11257 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 11260*

Lemma for hashfibc 11261: 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 11261*

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 11257. (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 11262*

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 11263*

Lemma for hashf1 11265. (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 11264*

Lemma for hashf1 11265. (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 11265*

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 11266*

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 11267

Version of isorel 6004 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 11268

Lemma for zfz1iso 11271. 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 11269*

Lemma for zfz1iso 11271. 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 11270*

Lemma for zfz1iso 11271. 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 11271*

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 11272*

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 11273

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 11274

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 11275

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 11276

Lemma for hashtpg 11277. 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 11277

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 11278

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 13343. (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 ) )

Theorem

fundm2domnop 11279

A function with a domain containing (at least) two different elements is not an ordered pair. (Contributed by AV, 12-Oct-2020.) (Proof shortened by AV, 9-Jun-2021.)

|- ( ( Fun G /\ 2o ~<_ dom G ) -> -. G e. ( _V X. _V ) )

Theorem

fun2dmnop0 11280

A function with a domain containing (at least) two different elements is not an ordered pair. This stronger version of fun2dmnop 11281 (with the less restrictive requirement that ( G \ { (/) } ) needs to be a function instead of G) is useful for proofs for extensible structures, see structn0fun 13343. (Contributed by AV, 21-Sep-2020.) (Revised by AV, 7-Jun-2021.)

|- A e. _V   &    |- B e. _V   =>    |- ( ( Fun ( G \ { (/) } ) /\ A =/= B /\ { A , B } C_ dom G ) -> -. G e. ( _V X. _V ) )

Theorem

fun2dmnop 11281

A function with a domain containing (at least) two different elements is not an ordered pair. (Contributed by AV, 21-Sep-2020.) (Proof shortened by AV, 9-Jun-2021.)

|- A e. _V   &    |- B e. _V   =>    |- ( ( Fun G /\ A =/= B /\ { A , B } C_ dom G ) -> -. G e. ( _V X. _V ) )

4.7  Words over a set

This section is about words (or strings) over a set (alphabet) defined as finite sequences of symbols (or characters) being elements of the alphabet. Although it is often required that the underlying set/alphabet be nonempty, finite and not a proper class, these restrictions are not made in the current definition df-word 11283. Note that the empty word (/) (i.e., the empty set) is the only word over an empty alphabet, see 0wrd0 11308. The set Word S of words over S is the free monoid over S, where the monoid law is concatenation and the monoid unit is the empty word. Besides the definition of words themselves, several operations on words are defined in this section:

Name	Reference	Explanation	Example	Remarks
Length (or size) of a word	df-ihash 11193: (♯ ` W )	Operation which determines the number of the symbols within the word.	W : ( 0..^ N ) --> S -> ( W e. Word S /\ (♯ ` W ) = N	This is not a special definition for words, but for arbitrary sets.
First symbol of a word	df-fv 5380: ( W ` 0 )	Operation which extracts the first symbol of a word. The result is the symbol at the first place in the sequence representing the word.	W : ( 0..^ 1 ) --> S -> ( W e. Word S /\ ( W ` 0 ) e. S	This is not a special definition for words, but for arbitrary functions with a half-open range of nonnegative integers as domain.
Last symbol of a word	df-lsw 11328: (lastS ` W )	Operation which extracts the last symbol of a word. The result is the symbol at the last place in the sequence representing the word.	W : ( 0..^ 3 ) --> S -> ( W e. Word S /\ (lastS ` W ) = ( W ` 2 )	Note that the index of the last symbol is less by 1 than the length of the word.
Subword (or substring) of a word	df-substr 11396: ( W substr <. I , J >. )	Operation which extracts a portion of a word. The result is a consecutive, reindexed part of the sequence representing the word.	W : ( 0..^ 3 ) --> S -> ( W e. Word S /\ ( W substr <. 1 , 2 >. ) e. Word S /\ (♯ ` ( W substr <. 1 , 2 >. ) ) = 1	Note that the last index of the range defining the subword is greater by 1 than the index of the last symbol of the subword in the sequence of the original word.
Concatenation of two words	df-concat 11337: ( W ++ U )	Operation combining two words to one new word. The result is a combined, reindexed sequence build from the sequences representing the two words.	( W e. Word S /\ U e. Word S ) -> (♯ ` ( W ++ U ) ) = ( (♯ ` W ) + (♯ ` U ) )	Note that the index of the first symbol of the second concatenated word is the length of the first word in the concatenation.
Singleton word	df-s1 11362: <" S ">	Constructor building a word of length 1 from a symbol.	(♯ ` <" S "> ) = 1

Conventions:

• Words are usually represented by class variable W, or if two words are involved, by W and U or by A and B.
• The alphabets are usually represented by class variable V (because any arbitrary set can be an alphabet), sometimes also by S (especially as codomain of the function representing a word, because the alphabet is the set of symbols).
• The symbols are usually represented by class variables S or A, or if two symbols are involved, by S and T or by A and B.
• The indices of the sequence representing a word are usually represented by class variable I, if two indices are involved (especially for subwords) by I and J, or by M and N.
• The length of a word is usually represented by class variables N or L.
• The number of positions by which to cyclically shift a word is usually represented by class variables N or L.

4.7.1  Definitions and basic theorems

Syntax

cword 11282

Syntax for the Word operator.

class Word S

Definition

df-word 11283*

Define the class of words over a set. A word (sometimes also called a string) is a finite sequence of symbols from a set (alphabet) S. Definition in Section 9.1 of [AhoHopUll] p. 318. The domain is forced to be an initial segment of NN0 so that two words with the same symbols in the same order be equal. The set Word S is sometimes denoted by S*, using the Kleene star, although the Kleene star, or Kleene closure, is sometimes reserved to denote an operation on languages. The set Word S equipped with concatenation is the free monoid over S, and the monoid unit is the empty word. (Contributed by FL, 14-Jan-2014.) (Revised by Stefan O'Rear, 14-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)

|- Word S = { w | E. l e. NN0 w : ( 0..^ l ) --> S }

Theorem

iswrd 11284*

Property of being a word over a set with an existential quantifier over the length. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) (Proof shortened by AV, 13-May-2020.)

|- ( W e. Word S <-> E. l e. NN0 W : ( 0..^ l ) --> S )

Theorem

wrdval 11285*

Value of the set of words over a set. (Contributed by Stefan O'Rear, 10-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)

|- ( S e. V -> Word S = U_ l e. NN0 ( S ^m ( 0..^ l ) ) )

Theorem

lencl 11286

The length of a word is a nonnegative integer. This corresponds to the definition in Section 9.1 of [AhoHopUll] p. 318. (Contributed by Stefan O'Rear, 27-Aug-2015.)

|- ( W e. Word S -> (♯ ` W ) e. NN0 )

Theorem

iswrdinn0 11287

A zero-based sequence is a word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) (Revised by Jim Kingdon, 16-Aug-2025.)

|- ( ( W : ( 0..^ L ) --> S /\ L e. NN0 ) -> W e. Word S )

Theorem

wrdf 11288

A word is a zero-based sequence with a recoverable upper limit. (Contributed by Stefan O'Rear, 15-Aug-2015.)

|- ( W e. Word S -> W : ( 0..^ (♯ ` W ) ) --> S )

Theorem

iswrdiz 11289

A zero-based sequence is a word. In iswrdinn0 11287 we can specify a length as an nonnegative integer. However, it will occasionally be helpful to allow a negative length, as well as zero, to specify an empty sequence. (Contributed by Jim Kingdon, 18-Aug-2025.)

|- ( ( W : ( 0..^ L ) --> S /\ L e. ZZ ) -> W e. Word S )

Theorem

wrddm 11290

The indices of a word (i.e. its domain regarded as function) are elements of an open range of nonnegative integers (of length equal to the length of the word). (Contributed by AV, 2-May-2020.)

|- ( W e. Word S -> dom W = ( 0..^ (♯ ` W ) ) )

Theorem

sswrd 11291

The set of words respects ordering on the base set. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) (Proof shortened by AV, 13-May-2020.)

|- ( S C_ T -> Word S C_ Word T )

Theorem

snopiswrd 11292

A singleton of an ordered pair (with 0 as first component) is a word. (Contributed by AV, 23-Nov-2018.) (Proof shortened by AV, 18-Apr-2021.)

|- ( S e. V -> { <. 0 , S >. } e. Word V )

Theorem

wrdexg 11293

The set of words over a set is a set. (Contributed by Mario Carneiro, 26-Feb-2016.) (Proof shortened by JJ, 18-Nov-2022.)

|- ( S e. V -> Word S e. _V )

Theorem

wrdexb 11294

The set of words over a set is a set, bidirectional version. (Contributed by Mario Carneiro, 26-Feb-2016.) (Proof shortened by AV, 23-Nov-2018.)

|- ( S e. _V <-> Word S e. _V )

Theorem

wrdexi 11295

The set of words over a set is a set, inference form. (Contributed by AV, 23-May-2021.)

|- S e. _V   =>    |- Word S e. _V

Theorem

wrdsymbcl 11296

A symbol within a word over an alphabet belongs to the alphabet. (Contributed by Alexander van der Vekens, 28-Jun-2018.)

|- ( ( W e. Word V /\ I e. ( 0..^ (♯ ` W ) ) ) -> ( W ` I ) e. V )

Theorem

wrdfn 11297

A word is a function with a zero-based sequence of integers as domain. (Contributed by Alexander van der Vekens, 13-Apr-2018.)

|- ( W e. Word S -> W Fn ( 0..^ (♯ ` W ) ) )

Theorem

wrdv 11298

A word over an alphabet is a word over the universal class. (Contributed by AV, 8-Feb-2021.) (Proof shortened by JJ, 18-Nov-2022.)

|- ( W e. Word V -> W e. Word _V )

Theorem

wrdlndm 11299

The length of a word is not in the domain of the word (regarded as a function). (Contributed by AV, 3-Mar-2021.) (Proof shortened by JJ, 18-Nov-2022.)

|- ( W e. Word V -> (♯ ` W ) e/ dom W )

Theorem

iswrdsymb 11300*

An arbitrary word is a word over an alphabet if all of its symbols belong to the alphabet. (Contributed by AV, 23-Jan-2021.)

|- ( ( W e. Word _V /\ A. i e. ( 0..^ (♯ ` W ) ) ( W ` i ) e. V ) -> W e. Word V )