P. 134 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 13301-13400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ballotfilemimin 13301*	( I ` C ) is the first tie. (Contributed by Thierry Arnoux, 1-Dec-2016.) (Revised by AV, 6-Oct-2020.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   =>    |- ( C e. ( O \ E ) -> -. E. k e. ( 1 ... ( ( I ` C ) - 1 ) ) ( ( F ` C ) ` k ) = 0 )
Theorem	ballotfilemic 13302*	If the first vote is for B, the vote on the first tie is for A. (Contributed by Thierry Arnoux, 1-Dec-2016.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   =>    |- ( ( C e. ( O \ E ) /\ -. 1 e. C ) -> ( I ` C ) e. C )
Theorem	ballotfilem1c 13303*	If the first vote is for A, the vote on the first tie is for B. (Contributed by Thierry Arnoux, 4-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   =>    |- ( ( C e. ( O \ E ) /\ 1 e. C ) -> -. ( I ` C ) e. C )
Theorem	ballotfilemsval 13304*	Value of S. (Contributed by Thierry Arnoux, 12-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   =>    |- ( C e. ( O \ E ) -> ( S ` C ) = ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` C ) , ( ( ( I ` C ) + 1 ) - i ) , i ) ) )
Theorem	ballotfilemsv 13305*	Value of S evaluated at J for a given counting C. (Contributed by Thierry Arnoux, 12-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   =>    |- ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( M + N ) ) ) -> ( ( S ` C ) ` J ) = if ( J <_ ( I ` C ) , ( ( ( I ` C ) + 1 ) - J ) , J ) )
Theorem	ballotfilemsgt1 13306*	S maps values less than ( I ` C ) to values greater than 1. (Contributed by Thierry Arnoux, 28-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   =>    |- ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( M + N ) ) /\ J < ( I ` C ) ) -> 1 < ( ( S ` C ) ` J ) )
Theorem	ballotfilemsdom 13307*	Domain of S for a given counting C. (Contributed by Thierry Arnoux, 12-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   =>    |- ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( M + N ) ) ) -> ( ( S ` C ) ` J ) e. ( 1 ... ( M + N ) ) )
Theorem	ballotfilemsel1i 13308*	The range ( 1 ... ( I ` C ) ) is invariant under ( S ` C ). (Contributed by Thierry Arnoux, 28-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   =>    |- ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) -> ( ( S ` C ) ` J ) e. ( 1 ... ( I ` C ) ) )
Theorem	ballotfilemsf1o 13309*	The defined S is a bijection, and an involution. (Contributed by Thierry Arnoux, 14-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   =>    |- ( C e. ( O \ E ) -> ( ( S ` C ) : ( 1 ... ( M + N ) ) -1-1-onto-> ( 1 ... ( M + N ) ) /\ `' ( S ` C ) = ( S ` C ) ) )
Theorem	ballotfilemsi 13310*	The image by S of the first tie pick is the first pick. (Contributed by Thierry Arnoux, 14-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   =>    |- ( C e. ( O \ E ) -> ( ( S ` C ) ` ( I ` C ) ) = 1 )
Theorem	ballotfilemsima 13311*	The image by S of an interval before the first pick. (Contributed by Thierry Arnoux, 5-May-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   =>    |- ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) -> ( ( S ` C ) " ( 1 ... J ) ) = ( ( ( S ` C ) ` J ) ... ( I ` C ) ) )
Theorem	ballotfilemieq 13312*	If two countings share the same first tie, they also have the same swap function. (Contributed by Thierry Arnoux, 18-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   =>    |- ( ( C e. ( O \ E ) /\ D e. ( O \ E ) /\ ( I ` C ) = ( I ` D ) ) -> ( S ` C ) = ( S ` D ) )
Theorem	ballotfilemrval 13313*	Value of R. (Contributed by Thierry Arnoux, 14-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   &    |- R = ( c e. ( O \ E ) |-> ( ( S ` c ) " c ) )   =>    |- ( C e. ( O \ E ) -> ( R ` C ) = ( ( S ` C ) " C ) )
Theorem	ballotfilemscr 13314*	The image of ( R ` C ) by ( S ` C ). (Contributed by Thierry Arnoux, 21-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   &    |- R = ( c e. ( O \ E ) |-> ( ( S ` c ) " c ) )   =>    |- ( C e. ( O \ E ) -> ( ( S ` C ) " ( R ` C ) ) = C )
Theorem	ballotfilemrv 13315*	Value of R evaluated at J. (Contributed by Thierry Arnoux, 17-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   &    |- R = ( c e. ( O \ E ) |-> ( ( S ` c ) " c ) )   =>    |- ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( M + N ) ) ) -> ( J e. ( R ` C ) <-> if ( J <_ ( I ` C ) , ( ( ( I ` C ) + 1 ) - J ) , J ) e. C ) )
Theorem	ballotfilemrv1 13316*	Value of R before the tie. (Contributed by Thierry Arnoux, 11-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   &    |- R = ( c e. ( O \ E ) |-> ( ( S ` c ) " c ) )   =>    |- ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( M + N ) ) /\ J <_ ( I ` C ) ) -> ( J e. ( R ` C ) <-> ( ( ( I ` C ) + 1 ) - J ) e. C ) )
Theorem	ballotfilemrv2 13317*	Value of R after the tie. (Contributed by Thierry Arnoux, 11-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   &    |- R = ( c e. ( O \ E ) |-> ( ( S ` c ) " c ) )   =>    |- ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( M + N ) ) /\ ( I ` C ) < J ) -> ( J e. ( R ` C ) <-> J e. C ) )
Theorem	ballotfilemro 13318*	Range of R is included in O. (Contributed by Thierry Arnoux, 17-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   &    |- R = ( c e. ( O \ E ) |-> ( ( S ` c ) " c ) )   =>    |- ( C e. ( O \ E ) -> ( R ` C ) e. O )
Theorem	ballotfilemgval 13319*	Expand the value of .^. (Contributed by Thierry Arnoux, 21-Apr-2017.) (Revised by Jim Kingdon, 15-Jun-2026.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   &    |- R = ( c e. ( O \ E ) |-> ( ( S ` c ) " c ) )   &    |- .^ = ( u e. O , v e. Fin |-> ( (♯ ` ( v i^i u ) ) - (♯ ` ( v \ u ) ) ) )   &    |- ( ph -> U e. O )   &    |- ( ph -> J e. ZZ )   &    |- ( ph -> K e. ZZ )   &    |- ( ph -> V = ( J ... K ) )   =>    |- ( ph -> ( U .^ V ) = ( (♯ ` ( V i^i U ) ) - (♯ ` ( V \ U ) ) ) )
Theorem	ballotfilemgun 13320*	A property of the defined .^ operator. (Contributed by Thierry Arnoux, 26-Apr-2017.) (Revised by Jim Kingdon, 15-Jun-2026.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   &    |- R = ( c e. ( O \ E ) |-> ( ( S ` c ) " c ) )   &    |- .^ = ( u e. O , v e. Fin |-> ( (♯ ` ( v i^i u ) ) - (♯ ` ( v \ u ) ) ) )   &    |- ( ph -> U e. O )   &    |- ( ph -> L e. ( J ... K ) )   =>    |- ( ph -> ( U .^ ( J ... K ) ) = ( ( U .^ ( J ... ( L - 1 ) ) ) + ( U .^ ( L ... K ) ) ) )
Theorem	ballotfilemfg 13321*	Express the value of ( F ` C ) in terms of .^. (Contributed by Thierry Arnoux, 21-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   &    |- R = ( c e. ( O \ E ) |-> ( ( S ` c ) " c ) )   &    |- .^ = ( u e. O , v e. Fin |-> ( (♯ ` ( v i^i u ) ) - (♯ ` ( v \ u ) ) ) )   =>    |- ( ( C e. ( O \ E ) /\ J e. ( 0 ... ( M + N ) ) ) -> ( ( F ` C ) ` J ) = ( C .^ ( 1 ... J ) ) )
Theorem	ballotfilemfrc 13322*	Express the value of ( F ` ( R ` C ) ) in terms of the newly defined .^. (Contributed by Thierry Arnoux, 21-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   &    |- R = ( c e. ( O \ E ) |-> ( ( S ` c ) " c ) )   &    |- .^ = ( u e. O , v e. Fin |-> ( (♯ ` ( v i^i u ) ) - (♯ ` ( v \ u ) ) ) )   =>    |- ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) -> ( ( F ` ( R ` C ) ) ` J ) = ( C .^ ( ( ( S ` C ) ` J ) ... ( I ` C ) ) ) )
Theorem	ballotfilemfrci 13323*	Reverse counting preserves a tie at the first tie. (Contributed by Thierry Arnoux, 21-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   &    |- R = ( c e. ( O \ E ) |-> ( ( S ` c ) " c ) )   &    |- .^ = ( u e. O , v e. Fin |-> ( (♯ ` ( v i^i u ) ) - (♯ ` ( v \ u ) ) ) )   =>    |- ( C e. ( O \ E ) -> ( ( F ` ( R ` C ) ) ` ( I ` C ) ) = 0 )
Theorem	ballotfilemfrceq 13324*	Value of F for a reverse counting ( R ` C ). (Contributed by Thierry Arnoux, 27-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   &    |- R = ( c e. ( O \ E ) |-> ( ( S ` c ) " c ) )   &    |- .^ = ( u e. O , v e. Fin |-> ( (♯ ` ( v i^i u ) ) - (♯ ` ( v \ u ) ) ) )   =>    |- ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) -> ( ( F ` C ) ` ( ( ( S ` C ) ` J ) - 1 ) ) = -u ( ( F ` ( R ` C ) ) ` J ) )
Theorem	ballotfilemfrcn0 13325*	Value of F for a reversed counting ( R ` C ), before the first tie, cannot be zero. (Contributed by Thierry Arnoux, 25-Apr-2017.) (Revised by AV, 6-Oct-2020.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   &    |- R = ( c e. ( O \ E ) |-> ( ( S ` c ) " c ) )   =>    |- ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( M + N ) ) /\ J < ( I ` C ) ) -> ( ( F ` ( R ` C ) ) ` J ) =/= 0 )
Theorem	ballotfilemrc 13326*	Range of R. (Contributed by Thierry Arnoux, 19-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   &    |- R = ( c e. ( O \ E ) |-> ( ( S ` c ) " c ) )   =>    |- ( C e. ( O \ E ) -> ( R ` C ) e. ( O \ E ) )
Theorem	ballotfilemirc 13327*	Applying R does not change first ties. (Contributed by Thierry Arnoux, 19-Apr-2017.) (Revised by AV, 6-Oct-2020.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   &    |- R = ( c e. ( O \ E ) |-> ( ( S ` c ) " c ) )   =>    |- ( C e. ( O \ E ) -> ( I ` ( R ` C ) ) = ( I ` C ) )
Theorem	ballotfilemrinv0 13328*	Lemma for ballotfilemrinv 13329. (Contributed by Thierry Arnoux, 18-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   &    |- R = ( c e. ( O \ E ) |-> ( ( S ` c ) " c ) )   =>    |- ( ( C e. ( O \ E ) /\ D = ( ( S ` C ) " C ) ) -> ( D e. ( O \ E ) /\ C = ( ( S ` D ) " D ) ) )
Theorem	ballotfilemrinv 13329*	R is its own inverse : it is an involution. (Contributed by Thierry Arnoux, 10-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   &    |- R = ( c e. ( O \ E ) |-> ( ( S ` c ) " c ) )   =>    |- `' R = R
Theorem	ballotfilem1ri 13330*	When the vote on the first tie is for A, the first vote is also for A on the reverse counting. (Contributed by Thierry Arnoux, 18-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   &    |- R = ( c e. ( O \ E ) |-> ( ( S ` c ) " c ) )   =>    |- ( C e. ( O \ E ) -> ( 1 e. ( R ` C ) <-> ( I ` C ) e. C ) )
Theorem	ballotfilem7 13331*	R is a bijection between two subsets of ( O \ E ): one where a vote for A is picked first, and one where a vote for B is picked first. (Contributed by Thierry Arnoux, 12-Dec-2016.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   &    |- R = ( c e. ( O \ E ) |-> ( ( S ` c ) " c ) )   =>    |- ( R |` { c e. ( O \ E ) | 1 e. c } ) : { c e. ( O \ E ) | 1 e. c } -1-1-onto-> { c e. ( O \ E ) | -. 1 e. c }
Theorem	ballotfilem8 13332*	There are as many countings with ties starting with a ballot for A as there are starting with a ballot for B. (Contributed by Thierry Arnoux, 7-Dec-2016.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   &    |- R = ( c e. ( O \ E ) |-> ( ( S ` c ) " c ) )   =>    |- (♯ ` { c e. ( O \ E ) | 1 e. c } ) = (♯ ` { c e. ( O \ E ) | -. 1 e. c } )
Theorem	ballotfilemth 13333*	Lemma for ballotfi 13334. The result, with several additional hypotheses which are for use during the proof. (Contributed by Thierry Arnoux, 7-Dec-2016.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   &    |- R = ( c e. ( O \ E ) |-> ( ( S ` c ) " c ) )   =>    |- ( P ` E ) = ( ( M - N ) / ( M + N ) )
Theorem	ballotfi 13334*	Bertrand's ballot problem : the probability that A is ahead throughout the counting. The proof formalized here is a proof "by reflection", as opposed to other known proofs "by induction" or "by permutation". This is Metamath 100 proof #30. (Contributed by Thierry Arnoux, 7-Dec-2016.) (Revised by Jim Kingdon, 17-Jun-2026.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   =>    |- ( P ` E ) = ( ( M - N ) / ( M + N ) )
5.3  Cardinality of real and complex number subsets
5.3.1  Countability of integers and rationals
Theorem	oddennn 13335	There are as many odd positive integers as there are positive integers. (Contributed by Jim Kingdon, 11-May-2022.)
|- { z e. NN | -. 2 || z } ~~ NN
Theorem	evenennn 13336	There are as many even positive integers as there are positive integers. (Contributed by Jim Kingdon, 12-May-2022.)
|- { z e. NN | 2 || z } ~~ NN
Theorem	xpnnen 13337	The Cartesian product of the set of positive integers with itself is equinumerous to the set of positive integers. (Contributed by NM, 1-Aug-2004.)
|- ( NN X. NN ) ~~ NN
Theorem	xpomen 13338	The Cartesian product of omega (the set of ordinal natural numbers) with itself is equinumerous to omega. Exercise 1 of [Enderton] p. 133. (Contributed by NM, 23-Jul-2004.)
|- ( om X. om ) ~~ om
Theorem	xpct 13339	The cartesian product of two sets dominated by om is dominated by om. (Contributed by Thierry Arnoux, 24-Sep-2017.)
|- ( ( A ~<_ om /\ B ~<_ om ) -> ( A X. B ) ~<_ om )
Theorem	unennn 13340	The union of two disjoint countably infinite sets is countably infinite. (Contributed by Jim Kingdon, 13-May-2022.)
|- ( ( A ~~ NN /\ B ~~ NN /\ ( A i^i B ) = (/) ) -> ( A u. B ) ~~ NN )
Theorem	znnen 13341	The set of integers and the set of positive integers are equinumerous. Corollary 8.1.23 of [AczelRathjen], p. 75. (Contributed by NM, 31-Jul-2004.)
|- ZZ ~~ NN
Theorem	ennnfonelemdc 13342*	Lemma for ennnfone 13368. A direct consequence of fidcenumlemrk 7271. (Contributed by Jim Kingdon, 15-Jul-2023.)
|- ( ph -> A. x e. A A. y e. A DECID x = y )   &    |- ( ph -> F : om -onto-> A )   &    |- ( ph -> P e. om )   =>    |- ( ph -> DECID ( F ` P ) e. ( F " P ) )
Theorem	ennnfonelemk 13343*	Lemma for ennnfone 13368. (Contributed by Jim Kingdon, 15-Jul-2023.)
|- ( ph -> F : om -onto-> A )   &    |- ( ph -> K e. om )   &    |- ( ph -> N e. om )   &    |- ( ph -> A. j e. suc N ( F ` K ) =/= ( F ` j ) )   =>    |- ( ph -> N e. K )
Theorem	ennnfonelemj0 13344*	Lemma for ennnfone 13368. Initial state for J. (Contributed by Jim Kingdon, 20-Jul-2023.)
|- ( ph -> A. x e. A A. y e. A DECID x = y )   &    |- ( ph -> F : om -onto-> A )   &    |- ( ph -> A. n e. om E. k e. om A. j e. suc n ( F ` k ) =/= ( F ` j ) )   &    |- G = ( x e. ( A ^pm om ) , y e. om |-> if ( ( F ` y ) e. ( F " y ) , x , ( x u. { <. dom x , ( F ` y ) >. } ) ) )   &    |- N = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   &    |- J = ( x e. NN0 |-> if ( x = 0 , (/) , ( `' N ` ( x - 1 ) ) ) )   &    |- H = seq 0 ( G , J )   =>    |- ( ph -> ( J ` 0 ) e. { g e. ( A ^pm om ) | dom g e. om } )
Theorem	ennnfonelemjn 13345*	Lemma for ennnfone 13368. Non-initial state for J. (Contributed by Jim Kingdon, 20-Jul-2023.)
|- ( ph -> A. x e. A A. y e. A DECID x = y )   &    |- ( ph -> F : om -onto-> A )   &    |- ( ph -> A. n e. om E. k e. om A. j e. suc n ( F ` k ) =/= ( F ` j ) )   &    |- G = ( x e. ( A ^pm om ) , y e. om |-> if ( ( F ` y ) e. ( F " y ) , x , ( x u. { <. dom x , ( F ` y ) >. } ) ) )   &    |- N = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   &    |- J = ( x e. NN0 |-> if ( x = 0 , (/) , ( `' N ` ( x - 1 ) ) ) )   &    |- H = seq 0 ( G , J )   =>    |- ( ( ph /\ f e. ( ZZ>= ` ( 0 + 1 ) ) ) -> ( J ` f ) e. om )
Theorem	ennnfonelemg 13346*	Lemma for ennnfone 13368. Closure for G. (Contributed by Jim Kingdon, 20-Jul-2023.)
|- ( ph -> A. x e. A A. y e. A DECID x = y )   &    |- ( ph -> F : om -onto-> A )   &    |- ( ph -> A. n e. om E. k e. om A. j e. suc n ( F ` k ) =/= ( F ` j ) )   &    |- G = ( x e. ( A ^pm om ) , y e. om |-> if ( ( F ` y ) e. ( F " y ) , x , ( x u. { <. dom x , ( F ` y ) >. } ) ) )   &    |- N = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   &    |- J = ( x e. NN0 |-> if ( x = 0 , (/) , ( `' N ` ( x - 1 ) ) ) )   &    |- H = seq 0 ( G , J )   =>    |- ( ( ph /\ ( f e. { g e. ( A ^pm om ) | dom g e. om } /\ j e. om ) ) -> ( f G j ) e. { g e. ( A ^pm om ) | dom g e. om } )
Theorem	ennnfonelemh 13347*	Lemma for ennnfone 13368. (Contributed by Jim Kingdon, 8-Jul-2023.)
|- ( ph -> A. x e. A A. y e. A DECID x = y )   &    |- ( ph -> F : om -onto-> A )   &    |- ( ph -> A. n e. om E. k e. om A. j e. suc n ( F ` k ) =/= ( F ` j ) )   &    |- G = ( x e. ( A ^pm om ) , y e. om |-> if ( ( F ` y ) e. ( F " y ) , x , ( x u. { <. dom x , ( F ` y ) >. } ) ) )   &    |- N = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   &    |- J = ( x e. NN0 |-> if ( x = 0 , (/) , ( `' N ` ( x - 1 ) ) ) )   &    |- H = seq 0 ( G , J )   =>    |- ( ph -> H : NN0 --> ( A ^pm om ) )
Theorem	ennnfonelem0 13348*	Lemma for ennnfone 13368. Initial value. (Contributed by Jim Kingdon, 15-Jul-2023.)
|- ( ph -> A. x e. A A. y e. A DECID x = y )   &    |- ( ph -> F : om -onto-> A )   &    |- ( ph -> A. n e. om E. k e. om A. j e. suc n ( F ` k ) =/= ( F ` j ) )   &    |- G = ( x e. ( A ^pm om ) , y e. om |-> if ( ( F ` y ) e. ( F " y ) , x , ( x u. { <. dom x , ( F ` y ) >. } ) ) )   &    |- N = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   &    |- J = ( x e. NN0 |-> if ( x = 0 , (/) , ( `' N ` ( x - 1 ) ) ) )   &    |- H = seq 0 ( G , J )   =>    |- ( ph -> ( H ` 0 ) = (/) )
Theorem	ennnfonelemp1 13349*	Lemma for ennnfone 13368. Value of H at a successor. (Contributed by Jim Kingdon, 23-Jul-2023.)
|- ( ph -> A. x e. A A. y e. A DECID x = y )   &    |- ( ph -> F : om -onto-> A )   &    |- ( ph -> A. n e. om E. k e. om A. j e. suc n ( F ` k ) =/= ( F ` j ) )   &    |- G = ( x e. ( A ^pm om ) , y e. om |-> if ( ( F ` y ) e. ( F " y ) , x , ( x u. { <. dom x , ( F ` y ) >. } ) ) )   &    |- N = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   &    |- J = ( x e. NN0 |-> if ( x = 0 , (/) , ( `' N ` ( x - 1 ) ) ) )   &    |- H = seq 0 ( G , J )   &    |- ( ph -> P e. NN0 )   =>    |- ( ph -> ( H ` ( P + 1 ) ) = if ( ( F ` ( `' N ` P ) ) e. ( F " ( `' N ` P ) ) , ( H ` P ) , ( ( H ` P ) u. { <. dom ( H ` P ) , ( F ` ( `' N ` P ) ) >. } ) ) )
Theorem	ennnfonelem1 13350*	Lemma for ennnfone 13368. Second value. (Contributed by Jim Kingdon, 19-Jul-2023.)
|- ( ph -> A. x e. A A. y e. A DECID x = y )   &    |- ( ph -> F : om -onto-> A )   &    |- ( ph -> A. n e. om E. k e. om A. j e. suc n ( F ` k ) =/= ( F ` j ) )   &    |- G = ( x e. ( A ^pm om ) , y e. om |-> if ( ( F ` y ) e. ( F " y ) , x , ( x u. { <. dom x , ( F ` y ) >. } ) ) )   &    |- N = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   &    |- J = ( x e. NN0 |-> if ( x = 0 , (/) , ( `' N ` ( x - 1 ) ) ) )   &    |- H = seq 0 ( G , J )   =>    |- ( ph -> ( H ` 1 ) = { <. (/) , ( F ` (/) ) >. } )
Theorem	ennnfonelemom 13351*	Lemma for ennnfone 13368. H yields finite sequences. (Contributed by Jim Kingdon, 19-Jul-2023.)
|- ( ph -> A. x e. A A. y e. A DECID x = y )   &    |- ( ph -> F : om -onto-> A )   &    |- ( ph -> A. n e. om E. k e. om A. j e. suc n ( F ` k ) =/= ( F ` j ) )   &    |- G = ( x e. ( A ^pm om ) , y e. om |-> if ( ( F ` y ) e. ( F " y ) , x , ( x u. { <. dom x , ( F ` y ) >. } ) ) )   &    |- N = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   &    |- J = ( x e. NN0 |-> if ( x = 0 , (/) , ( `' N ` ( x - 1 ) ) ) )   &    |- H = seq 0 ( G , J )   &    |- ( ph -> P e. NN0 )   =>    |- ( ph -> dom ( H ` P ) e. om )
Theorem	ennnfonelemhdmp1 13352*	Lemma for ennnfone 13368. Domain at a successor where we need to add an element to the sequence. (Contributed by Jim Kingdon, 23-Jul-2023.)
|- ( ph -> A. x e. A A. y e. A DECID x = y )   &    |- ( ph -> F : om -onto-> A )   &    |- ( ph -> A. n e. om E. k e. om A. j e. suc n ( F ` k ) =/= ( F ` j ) )   &    |- G = ( x e. ( A ^pm om ) , y e. om |-> if ( ( F ` y ) e. ( F " y ) , x , ( x u. { <. dom x , ( F ` y ) >. } ) ) )   &    |- N = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   &    |- J = ( x e. NN0 |-> if ( x = 0 , (/) , ( `' N ` ( x - 1 ) ) ) )   &    |- H = seq 0 ( G , J )   &    |- ( ph -> P e. NN0 )   &    |- ( ph -> -. ( F ` ( `' N ` P ) ) e. ( F " ( `' N ` P ) ) )   =>    |- ( ph -> dom ( H ` ( P + 1 ) ) = suc dom ( H ` P ) )
Theorem	ennnfonelemss 13353*	Lemma for ennnfone 13368. We only add elements to H as the index increases. (Contributed by Jim Kingdon, 15-Jul-2023.)
|- ( ph -> A. x e. A A. y e. A DECID x = y )   &    |- ( ph -> F : om -onto-> A )   &    |- ( ph -> A. n e. om E. k e. om A. j e. suc n ( F ` k ) =/= ( F ` j ) )   &    |- G = ( x e. ( A ^pm om ) , y e. om |-> if ( ( F ` y ) e. ( F " y ) , x , ( x u. { <. dom x , ( F ` y ) >. } ) ) )   &    |- N = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   &    |- J = ( x e. NN0 |-> if ( x = 0 , (/) , ( `' N ` ( x - 1 ) ) ) )   &    |- H = seq 0 ( G , J )   &    |- ( ph -> P e. NN0 )   =>    |- ( ph -> ( H ` P ) C_ ( H ` ( P + 1 ) ) )
Theorem	ennnfoneleminc 13354*	Lemma for ennnfone 13368. We only add elements to H as the index increases. (Contributed by Jim Kingdon, 21-Jul-2023.)
|- ( ph -> A. x e. A A. y e. A DECID x = y )   &    |- ( ph -> F : om -onto-> A )   &    |- ( ph -> A. n e. om E. k e. om A. j e. suc n ( F ` k ) =/= ( F ` j ) )   &    |- G = ( x e. ( A ^pm om ) , y e. om |-> if ( ( F ` y ) e. ( F " y ) , x , ( x u. { <. dom x , ( F ` y ) >. } ) ) )   &    |- N = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   &    |- J = ( x e. NN0 |-> if ( x = 0 , (/) , ( `' N ` ( x - 1 ) ) ) )   &    |- H = seq 0 ( G , J )   &    |- ( ph -> P e. NN0 )   &    |- ( ph -> Q e. NN0 )   &    |- ( ph -> P <_ Q )   =>    |- ( ph -> ( H ` P ) C_ ( H ` Q ) )
Theorem	ennnfonelemkh 13355*	Lemma for ennnfone 13368. Because we add zero or one entries for each new index, the length of each sequence is no greater than its index. (Contributed by Jim Kingdon, 19-Jul-2023.)
|- ( ph -> A. x e. A A. y e. A DECID x = y )   &    |- ( ph -> F : om -onto-> A )   &    |- ( ph -> A. n e. om E. k e. om A. j e. suc n ( F ` k ) =/= ( F ` j ) )   &    |- G = ( x e. ( A ^pm om ) , y e. om |-> if ( ( F ` y ) e. ( F " y ) , x , ( x u. { <. dom x , ( F ` y ) >. } ) ) )   &    |- N = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   &    |- J = ( x e. NN0 |-> if ( x = 0 , (/) , ( `' N ` ( x - 1 ) ) ) )   &    |- H = seq 0 ( G , J )   &    |- ( ph -> P e. NN0 )   =>    |- ( ph -> dom ( H ` P ) C_ ( `' N ` P ) )
Theorem	ennnfonelemhf1o 13356*	Lemma for ennnfone 13368. Each of the functions in H is one to one and onto an image of F. (Contributed by Jim Kingdon, 17-Jul-2023.)
|- ( ph -> A. x e. A A. y e. A DECID x = y )   &    |- ( ph -> F : om -onto-> A )   &    |- ( ph -> A. n e. om E. k e. om A. j e. suc n ( F ` k ) =/= ( F ` j ) )   &    |- G = ( x e. ( A ^pm om ) , y e. om |-> if ( ( F ` y ) e. ( F " y ) , x , ( x u. { <. dom x , ( F ` y ) >. } ) ) )   &    |- N = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   &    |- J = ( x e. NN0 |-> if ( x = 0 , (/) , ( `' N ` ( x - 1 ) ) ) )   &    |- H = seq 0 ( G , J )   &    |- ( ph -> P e. NN0 )   =>    |- ( ph -> ( H ` P ) : dom ( H ` P ) -1-1-onto-> ( F " ( `' N ` P ) ) )
Theorem	ennnfonelemex 13357*	Lemma for ennnfone 13368. Extending the sequence ( H ` P ) to include an additional element. (Contributed by Jim Kingdon, 19-Jul-2023.)
|- ( ph -> A. x e. A A. y e. A DECID x = y )   &    |- ( ph -> F : om -onto-> A )   &    |- ( ph -> A. n e. om E. k e. om A. j e. suc n ( F ` k ) =/= ( F ` j ) )   &    |- G = ( x e. ( A ^pm om ) , y e. om |-> if ( ( F ` y ) e. ( F " y ) , x , ( x u. { <. dom x , ( F ` y ) >. } ) ) )   &    |- N = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   &    |- J = ( x e. NN0 |-> if ( x = 0 , (/) , ( `' N ` ( x - 1 ) ) ) )   &    |- H = seq 0 ( G , J )   &    |- ( ph -> P e. NN0 )   =>    |- ( ph -> E. i e. NN0 dom ( H ` P ) e. dom ( H ` i ) )
Theorem	ennnfonelemhom 13358*	Lemma for ennnfone 13368. The sequences in H increase in length without bound if you go out far enough. (Contributed by Jim Kingdon, 19-Jul-2023.)
|- ( ph -> A. x e. A A. y e. A DECID x = y )   &    |- ( ph -> F : om -onto-> A )   &    |- ( ph -> A. n e. om E. k e. om A. j e. suc n ( F ` k ) =/= ( F ` j ) )   &    |- G = ( x e. ( A ^pm om ) , y e. om |-> if ( ( F ` y ) e. ( F " y ) , x , ( x u. { <. dom x , ( F ` y ) >. } ) ) )   &    |- N = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   &    |- J = ( x e. NN0 |-> if ( x = 0 , (/) , ( `' N ` ( x - 1 ) ) ) )   &    |- H = seq 0 ( G , J )   &    |- ( ph -> M e. om )   =>    |- ( ph -> E. i e. NN0 M e. dom ( H ` i ) )
Theorem	ennnfonelemrnh 13359*	Lemma for ennnfone 13368. A consequence of ennnfonelemss 13353. (Contributed by Jim Kingdon, 16-Jul-2023.)
|- ( ph -> A. x e. A A. y e. A DECID x = y )   &    |- ( ph -> F : om -onto-> A )   &    |- ( ph -> A. n e. om E. k e. om A. j e. suc n ( F ` k ) =/= ( F ` j ) )   &    |- G = ( x e. ( A ^pm om ) , y e. om |-> if ( ( F ` y ) e. ( F " y ) , x , ( x u. { <. dom x , ( F ` y ) >. } ) ) )   &    |- N = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   &    |- J = ( x e. NN0 |-> if ( x = 0 , (/) , ( `' N ` ( x - 1 ) ) ) )   &    |- H = seq 0 ( G , J )   &    |- ( ph -> X e. ran H )   &    |- ( ph -> Y e. ran H )   =>    |- ( ph -> ( X C_ Y \/ Y C_ X ) )
Theorem	ennnfonelemfun 13360*	Lemma for ennnfone 13368. L is a function. (Contributed by Jim Kingdon, 16-Jul-2023.)
|- ( ph -> A. x e. A A. y e. A DECID x = y )   &    |- ( ph -> F : om -onto-> A )   &    |- ( ph -> A. n e. om E. k e. om A. j e. suc n ( F ` k ) =/= ( F ` j ) )   &    |- G = ( x e. ( A ^pm om ) , y e. om |-> if ( ( F ` y ) e. ( F " y ) , x , ( x u. { <. dom x , ( F ` y ) >. } ) ) )   &    |- N = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   &    |- J = ( x e. NN0 |-> if ( x = 0 , (/) , ( `' N ` ( x - 1 ) ) ) )   &    |- H = seq 0 ( G , J )   &    |- L = U_ i e. NN0 ( H ` i )   =>    |- ( ph -> Fun L )
Theorem	ennnfonelemf1 13361*	Lemma for ennnfone 13368. L is one-to-one. (Contributed by Jim Kingdon, 16-Jul-2023.)
|- ( ph -> A. x e. A A. y e. A DECID x = y )   &    |- ( ph -> F : om -onto-> A )   &    |- ( ph -> A. n e. om E. k e. om A. j e. suc n ( F ` k ) =/= ( F ` j ) )   &    |- G = ( x e. ( A ^pm om ) , y e. om |-> if ( ( F ` y ) e. ( F " y ) , x , ( x u. { <. dom x , ( F ` y ) >. } ) ) )   &    |- N = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   &    |- J = ( x e. NN0 |-> if ( x = 0 , (/) , ( `' N ` ( x - 1 ) ) ) )   &    |- H = seq 0 ( G , J )   &    |- L = U_ i e. NN0 ( H ` i )   =>    |- ( ph -> L : dom L -1-1-> A )
Theorem	ennnfonelemrn 13362*	Lemma for ennnfone 13368. L is onto A. (Contributed by Jim Kingdon, 16-Jul-2023.)
|- ( ph -> A. x e. A A. y e. A DECID x = y )   &    |- ( ph -> F : om -onto-> A )   &    |- ( ph -> A. n e. om E. k e. om A. j e. suc n ( F ` k ) =/= ( F ` j ) )   &    |- G = ( x e. ( A ^pm om ) , y e. om |-> if ( ( F ` y ) e. ( F " y ) , x , ( x u. { <. dom x , ( F ` y ) >. } ) ) )   &    |- N = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   &    |- J = ( x e. NN0 |-> if ( x = 0 , (/) , ( `' N ` ( x - 1 ) ) ) )   &    |- H = seq 0 ( G , J )   &    |- L = U_ i e. NN0 ( H ` i )   =>    |- ( ph -> ran L = A )
Theorem	ennnfonelemdm 13363*	Lemma for ennnfone 13368. The function L is defined everywhere. (Contributed by Jim Kingdon, 16-Jul-2023.)
|- ( ph -> A. x e. A A. y e. A DECID x = y )   &    |- ( ph -> F : om -onto-> A )   &    |- ( ph -> A. n e. om E. k e. om A. j e. suc n ( F ` k ) =/= ( F ` j ) )   &    |- G = ( x e. ( A ^pm om ) , y e. om |-> if ( ( F ` y ) e. ( F " y ) , x , ( x u. { <. dom x , ( F ` y ) >. } ) ) )   &    |- N = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   &    |- J = ( x e. NN0 |-> if ( x = 0 , (/) , ( `' N ` ( x - 1 ) ) ) )   &    |- H = seq 0 ( G , J )   &    |- L = U_ i e. NN0 ( H ` i )   =>    |- ( ph -> dom L = om )
Theorem	ennnfonelemen 13364*	Lemma for ennnfone 13368. The result. (Contributed by Jim Kingdon, 16-Jul-2023.)
|- ( ph -> A. x e. A A. y e. A DECID x = y )   &    |- ( ph -> F : om -onto-> A )   &    |- ( ph -> A. n e. om E. k e. om A. j e. suc n ( F ` k ) =/= ( F ` j ) )   &    |- G = ( x e. ( A ^pm om ) , y e. om |-> if ( ( F ` y ) e. ( F " y ) , x , ( x u. { <. dom x , ( F ` y ) >. } ) ) )   &    |- N = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   &    |- J = ( x e. NN0 |-> if ( x = 0 , (/) , ( `' N ` ( x - 1 ) ) ) )   &    |- H = seq 0 ( G , J )   &    |- L = U_ i e. NN0 ( H ` i )   =>    |- ( ph -> A ~~ NN )
Theorem	ennnfonelemnn0 13365*	Lemma for ennnfone 13368. A version of ennnfonelemen 13364 expressed in terms of NN0 instead of om. (Contributed by Jim Kingdon, 27-Oct-2022.)
|- ( ph -> A. x e. A A. y e. A DECID x = y )   &    |- ( ph -> F : NN0 -onto-> A )   &    |- ( ph -> A. n e. NN0 E. k e. NN0 A. j e. ( 0 ... n ) ( F ` k ) =/= ( F ` j ) )   &    |- N = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   =>    |- ( ph -> A ~~ NN )
Theorem	ennnfonelemr 13366*	Lemma for ennnfone 13368. The interesting direction, expressed in deduction form. (Contributed by Jim Kingdon, 27-Oct-2022.)
|- ( ph -> A. x e. A A. y e. A DECID x = y )   &    |- ( ph -> F : NN0 -onto-> A )   &    |- ( ph -> A. n e. NN0 E. k e. NN0 A. j e. ( 0 ... n ) ( F ` k ) =/= ( F ` j ) )   =>    |- ( ph -> A ~~ NN )
Theorem	ennnfonelemim 13367*	Lemma for ennnfone 13368. The trivial direction. (Contributed by Jim Kingdon, 27-Oct-2022.)
|- ( A ~~ NN -> ( A. x e. A A. y e. A DECID x = y /\ E. f ( f : NN0 -onto-> A /\ A. n e. NN0 E. k e. NN0 A. j e. ( 0 ... n ) ( f ` k ) =/= ( f ` j ) ) ) )
Theorem	ennnfone 13368*	A condition for a set being countably infinite. Corollary 8.1.13 of [AczelRathjen], p. 73. Roughly speaking, the condition says that A is countable (that's the f : NN0 -onto-> A part, as seen in theorems like ctm 7450), infinite (that's the part about being able to find an element of A distinct from any mapping of a natural number via f), and has decidable equality. (Contributed by Jim Kingdon, 27-Oct-2022.)
|- ( A ~~ NN <-> ( A. x e. A A. y e. A DECID x = y /\ E. f ( f : NN0 -onto-> A /\ A. n e. NN0 E. k e. NN0 A. j e. ( 0 ... n ) ( f ` k ) =/= ( f ` j ) ) ) )
Theorem	exmidunben 13369*	If any unbounded set of positive integers is equinumerous to NN, then the Limited Principle of Omniscience (LPO) implies excluded middle. (Contributed by Jim Kingdon, 29-Jul-2023.)
|- ( ( A. x ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) -> x ~~ NN ) /\ om e. Omni ) -> EXMID )
Theorem	ctinfomlemom 13370*	Lemma for ctinfom 13371. Converting between om and NN0. (Contributed by Jim Kingdon, 10-Aug-2023.)
|- N = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   &    |- G = ( F o. `' N )   &    |- ( ph -> F : om -onto-> A )   &    |- ( ph -> A. n e. om E. k e. om -. ( F ` k ) e. ( F " n ) )   =>    |- ( ph -> ( G : NN0 -onto-> A /\ A. m e. NN0 E. j e. NN0 A. i e. ( 0 ... m ) ( G ` j ) =/= ( G ` i ) ) )
Theorem	ctinfom 13371*	A condition for a set being countably infinite. Restates ennnfone 13368 in terms of om and function image. Like ennnfone 13368 the condition can be summarized as A being countable, infinite, and having decidable equality. (Contributed by Jim Kingdon, 7-Aug-2023.)
|- ( A ~~ NN <-> ( A. x e. A A. y e. A DECID x = y /\ E. f ( f : om -onto-> A /\ A. n e. om E. k e. om -. ( f ` k ) e. ( f " n ) ) ) )
Theorem	inffinp1 13372*	An infinite set contains an element not contained in a given finite subset. (Contributed by Jim Kingdon, 7-Aug-2023.)
|- ( ph -> A. x e. A A. y e. A DECID x = y )   &    |- ( ph -> om ~<_ A )   &    |- ( ph -> B C_ A )   &    |- ( ph -> B e. Fin )   =>    |- ( ph -> E. x e. A -. x e. B )
Theorem	ctinf 13373*	A set is countably infinite if and only if it has decidable equality, is countable, and is infinite. (Contributed by Jim Kingdon, 7-Aug-2023.)
|- ( A ~~ NN <-> ( A. x e. A A. y e. A DECID x = y /\ E. f f : om -onto-> A /\ om ~<_ A ) )
Theorem	qnnen 13374	The rational numbers are countably infinite. Corollary 8.1.23 of [AczelRathjen], p. 75. This is Metamath 100 proof #3. (Contributed by Jim Kingdon, 11-Aug-2023.)
|- QQ ~~ NN
Theorem	enctlem 13375*	Lemma for enct 13376. One direction of the biconditional. (Contributed by Jim Kingdon, 23-Dec-2023.)
|- ( A ~~ B -> ( E. f f : om -onto-> ( A ⊔ 1o ) -> E. g g : om -onto-> ( B ⊔ 1o ) ) )
Theorem	enct 13376*	Countability is invariant relative to equinumerosity. (Contributed by Jim Kingdon, 23-Dec-2023.)
|- ( A ~~ B -> ( E. f f : om -onto-> ( A ⊔ 1o ) <-> E. g g : om -onto-> ( B ⊔ 1o ) ) )
Theorem	ctiunctlemu1st 13377*	Lemma for ctiunct 13383. (Contributed by Jim Kingdon, 28-Oct-2023.)
|- ( ph -> S C_ om )   &    |- ( ph -> A. n e. om DECID n e. S )   &    |- ( ph -> F : S -onto-> A )   &    |- ( ( ph /\ x e. A ) -> T C_ om )   &    |- ( ( ph /\ x e. A ) -> A. n e. om DECID n e. T )   &    |- ( ( ph /\ x e. A ) -> G : T -onto-> B )   &    |- ( ph -> J : om -1-1-onto-> ( om X. om ) )   &    |- U = { z e. om | ( ( 1st ` ( J ` z ) ) e. S /\ ( 2nd ` ( J ` z ) ) e. [_ ( F ` ( 1st ` ( J ` z ) ) ) / x ]_ T ) }   &    |- ( ph -> N e. U )   =>    |- ( ph -> ( 1st ` ( J ` N ) ) e. S )
Theorem	ctiunctlemu2nd 13378*	Lemma for ctiunct 13383. (Contributed by Jim Kingdon, 28-Oct-2023.)
|- ( ph -> S C_ om )   &    |- ( ph -> A. n e. om DECID n e. S )   &    |- ( ph -> F : S -onto-> A )   &    |- ( ( ph /\ x e. A ) -> T C_ om )   &    |- ( ( ph /\ x e. A ) -> A. n e. om DECID n e. T )   &    |- ( ( ph /\ x e. A ) -> G : T -onto-> B )   &    |- ( ph -> J : om -1-1-onto-> ( om X. om ) )   &    |- U = { z e. om | ( ( 1st ` ( J ` z ) ) e. S /\ ( 2nd ` ( J ` z ) ) e. [_ ( F ` ( 1st ` ( J ` z ) ) ) / x ]_ T ) }   &    |- ( ph -> N e. U )   =>    |- ( ph -> ( 2nd ` ( J ` N ) ) e. [_ ( F ` ( 1st ` ( J ` N ) ) ) / x ]_ T )
Theorem	ctiunctlemuom 13379	Lemma for ctiunct 13383. (Contributed by Jim Kingdon, 28-Oct-2023.)
|- ( ph -> S C_ om )   &    |- ( ph -> A. n e. om DECID n e. S )   &    |- ( ph -> F : S -onto-> A )   &    |- ( ( ph /\ x e. A ) -> T C_ om )   &    |- ( ( ph /\ x e. A ) -> A. n e. om DECID n e. T )   &    |- ( ( ph /\ x e. A ) -> G : T -onto-> B )   &    |- ( ph -> J : om -1-1-onto-> ( om X. om ) )   &    |- U = { z e. om | ( ( 1st ` ( J ` z ) ) e. S /\ ( 2nd ` ( J ` z ) ) e. [_ ( F ` ( 1st ` ( J ` z ) ) ) / x ]_ T ) }   =>    |- ( ph -> U C_ om )
Theorem	ctiunctlemudc 13380*	Lemma for ctiunct 13383. (Contributed by Jim Kingdon, 28-Oct-2023.)
|- ( ph -> S C_ om )   &    |- ( ph -> A. n e. om DECID n e. S )   &    |- ( ph -> F : S -onto-> A )   &    |- ( ( ph /\ x e. A ) -> T C_ om )   &    |- ( ( ph /\ x e. A ) -> A. n e. om DECID n e. T )   &    |- ( ( ph /\ x e. A ) -> G : T -onto-> B )   &    |- ( ph -> J : om -1-1-onto-> ( om X. om ) )   &    |- U = { z e. om | ( ( 1st ` ( J ` z ) ) e. S /\ ( 2nd ` ( J ` z ) ) e. [_ ( F ` ( 1st ` ( J ` z ) ) ) / x ]_ T ) }   =>    |- ( ph -> A. n e. om DECID n e. U )
Theorem	ctiunctlemf 13381*	Lemma for ctiunct 13383. (Contributed by Jim Kingdon, 28-Oct-2023.)
|- ( ph -> S C_ om )   &    |- ( ph -> A. n e. om DECID n e. S )   &    |- ( ph -> F : S -onto-> A )   &    |- ( ( ph /\ x e. A ) -> T C_ om )   &    |- ( ( ph /\ x e. A ) -> A. n e. om DECID n e. T )   &    |- ( ( ph /\ x e. A ) -> G : T -onto-> B )   &    |- ( ph -> J : om -1-1-onto-> ( om X. om ) )   &    |- U = { z e. om | ( ( 1st ` ( J ` z ) ) e. S /\ ( 2nd ` ( J ` z ) ) e. [_ ( F ` ( 1st ` ( J ` z ) ) ) / x ]_ T ) }   &    |- H = ( n e. U |-> ( [_ ( F ` ( 1st ` ( J ` n ) ) ) / x ]_ G ` ( 2nd ` ( J ` n ) ) ) )   =>    |- ( ph -> H : U --> U_ x e. A B )
Theorem	ctiunctlemfo 13382*	Lemma for ctiunct 13383. (Contributed by Jim Kingdon, 28-Oct-2023.)
|- ( ph -> S C_ om )   &    |- ( ph -> A. n e. om DECID n e. S )   &    |- ( ph -> F : S -onto-> A )   &    |- ( ( ph /\ x e. A ) -> T C_ om )   &    |- ( ( ph /\ x e. A ) -> A. n e. om DECID n e. T )   &    |- ( ( ph /\ x e. A ) -> G : T -onto-> B )   &    |- ( ph -> J : om -1-1-onto-> ( om X. om ) )   &    |- U = { z e. om | ( ( 1st ` ( J ` z ) ) e. S /\ ( 2nd ` ( J ` z ) ) e. [_ ( F ` ( 1st ` ( J ` z ) ) ) / x ]_ T ) }   &    |- H = ( n e. U |-> ( [_ ( F ` ( 1st ` ( J ` n ) ) ) / x ]_ G ` ( 2nd ` ( J ` n ) ) ) )   &    |- F/_ x H   &    |- F/_ x U   =>    |- ( ph -> H : U -onto-> U_ x e. A B )
Theorem	ctiunct 13383*	A sequence of enumerations gives an enumeration of the union. We refer to "sequence of enumerations" rather than "countably many countable sets" because the hypothesis provides more than countability for each B ( x ): it refers to B ( x ) together with the G ( x ) which enumerates it. Theorem 8.1.19 of [AczelRathjen], p. 74. For "countably many countable sets" the key hypothesis would be ( ph /\ x e. A ) -> E. g g : om -onto-> ( B ⊔ 1o ). This is almost omiunct 13387 (which uses countable choice) although that is for a countably infinite collection not any countable collection. Compare with the case of two sets instead of countably many, as seen at unct 13385, which says that the union of two countable sets is countable . The proof proceeds by mapping a natural number to a pair of natural numbers (by xpomen 13338) and using the first number to map to an element x of A and the second number to map to an element of B(x) . In this way we are able to map to every element of U_ x e. A B. Although it would be possible to work directly with countability expressed as F : om -onto-> ( A ⊔ 1o ), we instead use functions from subsets of the natural numbers via ctssdccl 7452 and ctssdc 7454. (Contributed by Jim Kingdon, 31-Oct-2023.)
|- ( ph -> F : om -onto-> ( A ⊔ 1o ) )   &    |- ( ( ph /\ x e. A ) -> G : om -onto-> ( B ⊔ 1o ) )   =>    |- ( ph -> E. h h : om -onto-> ( U_ x e. A B ⊔ 1o ) )
Theorem	ctiunctal 13384*	Variation of ctiunct 13383 which allows x to be present in ph. (Contributed by Jim Kingdon, 5-May-2024.)
|- ( ph -> F : om -onto-> ( A ⊔ 1o ) )   &    |- ( ph -> A. x e. A G : om -onto-> ( B ⊔ 1o ) )   =>    |- ( ph -> E. h h : om -onto-> ( U_ x e. A B ⊔ 1o ) )
Theorem	unct 13385*	The union of two countable sets is countable. Corollary 8.1.20 of [AczelRathjen], p. 75. (Contributed by Jim Kingdon, 1-Nov-2023.)
|- ( ( E. f f : om -onto-> ( A ⊔ 1o ) /\ E. g g : om -onto-> ( B ⊔ 1o ) ) -> E. h h : om -onto-> ( ( A u. B ) ⊔ 1o ) )
Theorem	omctfn 13386*	Using countable choice to find a sequence of enumerations for a collection of countable sets. Lemma 8.1.27 of [AczelRathjen], p. 77. (Contributed by Jim Kingdon, 19-Apr-2024.)
|- ( ph -> CCHOICE )   &    |- ( ( ph /\ x e. om ) -> E. g g : om -onto-> ( B ⊔ 1o ) )   =>    |- ( ph -> E. f ( f Fn om /\ A. x e. om ( f ` x ) : om -onto-> ( B ⊔ 1o ) ) )
Theorem	omiunct 13387*	The union of a countably infinite collection of countable sets is countable. Theorem 8.1.28 of [AczelRathjen], p. 78. Compare with ctiunct 13383 which has a stronger hypothesis but does not require countable choice. (Contributed by Jim Kingdon, 5-May-2024.)
|- ( ph -> CCHOICE )   &    |- ( ( ph /\ x e. om ) -> E. g g : om -onto-> ( B ⊔ 1o ) )   =>    |- ( ph -> E. h h : om -onto-> ( U_ x e. om B ⊔ 1o ) )
Theorem	ssomct 13388*	A decidable subset of om is countable. (Contributed by Jim Kingdon, 19-Sep-2024.)
|- ( ( A C_ om /\ A. x e. om DECID x e. A ) -> E. f f : om -onto-> ( A ⊔ 1o ) )
Theorem	ssnnctlemct 13389*	Lemma for ssnnct 13390. The result. (Contributed by Jim Kingdon, 29-Sep-2024.)
|- G = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 1 )   =>    |- ( ( A C_ NN /\ A. x e. NN DECID x e. A ) -> E. f f : om -onto-> ( A ⊔ 1o ) )
Theorem	ssnnct 13390*	A decidable subset of NN is countable. (Contributed by Jim Kingdon, 29-Sep-2024.)
|- ( ( A C_ NN /\ A. x e. NN DECID x e. A ) -> E. f f : om -onto-> ( A ⊔ 1o ) )
Theorem	nninfdclemcl 13391*	Lemma for nninfdc 13396. (Contributed by Jim Kingdon, 25-Sep-2024.)
|- ( ph -> A C_ NN )   &    |- ( ph -> A. x e. NN DECID x e. A )   &    |- ( ph -> A. m e. NN E. n e. A m < n )   &    |- ( ph -> P e. A )   &    |- ( ph -> Q e. A )   =>    |- ( ph -> ( P ( y e. NN , z e. NN |-> inf ( ( A i^i ( ZZ>= ` ( y + 1 ) ) ) , RR , < ) ) Q ) e. A )
Theorem	nninfdclemf 13392*	Lemma for nninfdc 13396. A function from the natural numbers into A. (Contributed by Jim Kingdon, 23-Sep-2024.)
|- ( ph -> A C_ NN )   &    |- ( ph -> A. x e. NN DECID x e. A )   &    |- ( ph -> A. m e. NN E. n e. A m < n )   &    |- ( ph -> ( J e. A /\ 1 < J ) )   &    |- F = seq 1 ( ( y e. NN , z e. NN |-> inf ( ( A i^i ( ZZ>= ` ( y + 1 ) ) ) , RR , < ) ) , ( i e. NN |-> J ) )   =>    |- ( ph -> F : NN --> A )
Theorem	nninfdclemp1 13393*	Lemma for nninfdc 13396. Each element of the sequence F is greater than the previous element. (Contributed by Jim Kingdon, 26-Sep-2024.)
|- ( ph -> A C_ NN )   &    |- ( ph -> A. x e. NN DECID x e. A )   &    |- ( ph -> A. m e. NN E. n e. A m < n )   &    |- ( ph -> ( J e. A /\ 1 < J ) )   &    |- F = seq 1 ( ( y e. NN , z e. NN |-> inf ( ( A i^i ( ZZ>= ` ( y + 1 ) ) ) , RR , < ) ) , ( i e. NN |-> J ) )   &    |- ( ph -> U e. NN )   =>    |- ( ph -> ( F ` U ) < ( F ` ( U + 1 ) ) )
Theorem	nninfdclemlt 13394*	Lemma for nninfdc 13396. The function from nninfdclemf 13392 is strictly monotonic. (Contributed by Jim Kingdon, 24-Sep-2024.)
|- ( ph -> A C_ NN )   &    |- ( ph -> A. x e. NN DECID x e. A )   &    |- ( ph -> A. m e. NN E. n e. A m < n )   &    |- ( ph -> ( J e. A /\ 1 < J ) )   &    |- F = seq 1 ( ( y e. NN , z e. NN |-> inf ( ( A i^i ( ZZ>= ` ( y + 1 ) ) ) , RR , < ) ) , ( i e. NN |-> J ) )   &    |- ( ph -> U e. NN )   &    |- ( ph -> V e. NN )   &    |- ( ph -> U < V )   =>    |- ( ph -> ( F ` U ) < ( F ` V ) )
Theorem	nninfdclemf1 13395*	Lemma for nninfdc 13396. The function from nninfdclemf 13392 is one-to-one. (Contributed by Jim Kingdon, 23-Sep-2024.)
|- ( ph -> A C_ NN )   &    |- ( ph -> A. x e. NN DECID x e. A )   &    |- ( ph -> A. m e. NN E. n e. A m < n )   &    |- ( ph -> ( J e. A /\ 1 < J ) )   &    |- F = seq 1 ( ( y e. NN , z e. NN |-> inf ( ( A i^i ( ZZ>= ` ( y + 1 ) ) ) , RR , < ) ) , ( i e. NN |-> J ) )   =>    |- ( ph -> F : NN -1-1-> A )
Theorem	nninfdc 13396*	An unbounded decidable set of positive integers is infinite. (Contributed by Jim Kingdon, 23-Sep-2024.)
|- ( ( A C_ NN /\ A. x e. NN DECID x e. A /\ A. m e. NN E. n e. A m < n ) -> om ~<_ A )
Theorem	unbendc 13397*	An unbounded decidable set of positive integers is infinite. (Contributed by NM, 5-May-2005.) (Revised by Jim Kingdon, 30-Sep-2024.)
|- ( ( A C_ NN /\ A. x e. NN DECID x e. A /\ A. m e. NN E. n e. A m < n ) -> A ~~ NN )
Theorem	prminf 13398	There are an infinite number of primes. Theorem 1.7 in [ApostolNT] p. 16. (Contributed by Paul Chapman, 28-Nov-2012.)
|- Prime ~~ NN
Theorem	infpn2 13399*	There exist infinitely many prime numbers: the set of all primes S is unbounded by infpn 13163, so by unbendc 13397 it is infinite. This is Metamath 100 proof #11. (Contributed by NM, 5-May-2005.)
|- S = { n e. NN | ( 1 < n /\ A. m e. NN ( ( n / m ) e. NN -> ( m = 1 \/ m = n ) ) ) }   =>    |- S ~~ NN
PART 6  BASIC STRUCTURES
6.1  Extensible structures
6.1.1  Basic definitions An "extensible structure" (or "structure" in short, at least in this section) is used to define a specific group, ring, poset, and so on. An extensible structure can contain many components. For example, a group will have at least two components (base set and operation), although it can be further specialized by adding other components such as a multiplicative operation for rings (and still remain a group per our definition). Thus, every ring is also a group. This extensible structure approach allows theorems from more general structures (such as groups) to be reused for more specialized structures (such as rings) without having to reprove anything. Structures are common in mathematics, but in informal (natural language) proofs the details are assumed in ways that we must make explicit. An extensible structure is implemented as a function (a set of ordered pairs) on a finite (and not necessarily sequential) subset of NN. The function's argument is the index of a structure component (such as 1 for the base set of a group), and its value is the component (such as the base set). By convention, we normally avoid direct reference to the hard-coded numeric index and instead use structure component extractors such as ndxid 13428 and strslfv 13449. Using extractors makes it easier to change numeric indices and also makes the components' purpose clearer. See the comment of basendx 13459 for more details on numeric indices versus the structure component extractors. There are many other possible ways to handle structures. We chose this extensible structure approach because this approach (1) results in simpler notation than other approaches we are aware of, and (2) is easier to do proofs with. We cannot use an approach that uses "hidden" arguments; Metamath does not support hidden arguments, and in any case we want nothing hidden. It would be possible to use a categorical approach (e.g., something vaguely similar to Lean's mathlib). However, instances (the chain of proofs that an X is a Y via a bunch of forgetful functors) can cause serious performance problems for automated tooling, and the resulting proofs would be painful to look at directly (in the case of Lean, they are long past the level where people would find it acceptable to look at them directly). Metamath is working under much stricter conditions than this, and it has still managed to achieve about the same level of flexibility through this "extensible structure" approach. To create a substructure of a given extensible structure, you can simply use the multifunction restriction operator for extensible structures ↾s as defined in df-iress 13412. This can be used to turn statements about rings into statements about subrings, modules into submodules, etc. This definition knows nothing about individual structures and merely truncates the Base set while leaving operators alone. Individual kinds of structures will need to handle this behavior by ignoring operators' values outside the range, defining a function using the base set and applying that, or explicitly truncating the slot before use. Extensible structures only work well when they represent concrete categories, where there is a "base set", morphisms are functions, and subobjects are subsets with induced operations. In short, they primarily work well for "sets with (some) extra structure". Extensible structures may not suffice for more complicated situations. For example, in manifolds, ↾s would not work. That said, extensible structures are sufficient for many of the structures that set.mm currently considers, and offer a good compromise for a goal-oriented formalization.
Syntax	cstr 13400	Extend class notation with the class of structures with components numbered below A.
class Struct