P. 129 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 12801-12900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	4sqlem13m 12801*	Lemma for 4sq 12808. (Contributed by Mario Carneiro, 16-Jul-2014.) (Revised by AV, 14-Sep-2020.)
|- S = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }   &    |- ( ph -> N e. NN )   &    |- ( ph -> P = ( ( 2 x. N ) + 1 ) )   &    |- ( ph -> P e. Prime )   &    |- ( ph -> ( 0 ... ( 2 x. N ) ) C_ S )   &    |- T = { i e. NN | ( i x. P ) e. S }   &    |- M = inf ( T , RR , < )   =>    |- ( ph -> ( E. j j e. T /\ M < P ) )
Theorem	4sqlem14 12802*	Lemma for 4sq 12808. (Contributed by Mario Carneiro, 16-Jul-2014.) (Revised by AV, 14-Sep-2020.)
|- S = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }   &    |- ( ph -> N e. NN )   &    |- ( ph -> P = ( ( 2 x. N ) + 1 ) )   &    |- ( ph -> P e. Prime )   &    |- ( ph -> ( 0 ... ( 2 x. N ) ) C_ S )   &    |- T = { i e. NN | ( i x. P ) e. S }   &    |- M = inf ( T , RR , < )   &    |- ( ph -> M e. ( ZZ>= ` 2 ) )   &    |- ( ph -> A e. ZZ )   &    |- ( ph -> B e. ZZ )   &    |- ( ph -> C e. ZZ )   &    |- ( ph -> D e. ZZ )   &    |- E = ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- F = ( ( ( B + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- G = ( ( ( C + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- H = ( ( ( D + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- R = ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) / M )   &    |- ( ph -> ( M x. P ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) )   =>    |- ( ph -> R e. NN0 )
Theorem	4sqlem15 12803*	Lemma for 4sq 12808. (Contributed by Mario Carneiro, 16-Jul-2014.) (Revised by AV, 14-Sep-2020.)
|- S = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }   &    |- ( ph -> N e. NN )   &    |- ( ph -> P = ( ( 2 x. N ) + 1 ) )   &    |- ( ph -> P e. Prime )   &    |- ( ph -> ( 0 ... ( 2 x. N ) ) C_ S )   &    |- T = { i e. NN | ( i x. P ) e. S }   &    |- M = inf ( T , RR , < )   &    |- ( ph -> M e. ( ZZ>= ` 2 ) )   &    |- ( ph -> A e. ZZ )   &    |- ( ph -> B e. ZZ )   &    |- ( ph -> C e. ZZ )   &    |- ( ph -> D e. ZZ )   &    |- E = ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- F = ( ( ( B + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- G = ( ( ( C + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- H = ( ( ( D + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- R = ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) / M )   &    |- ( ph -> ( M x. P ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) )   =>    |- ( ( ph /\ R = M ) -> ( ( ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( E ^ 2 ) ) = 0 /\ ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( F ^ 2 ) ) = 0 ) /\ ( ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( G ^ 2 ) ) = 0 /\ ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( H ^ 2 ) ) = 0 ) ) )
Theorem	4sqlem16 12804*	Lemma for 4sq 12808. (Contributed by Mario Carneiro, 16-Jul-2014.) (Revised by AV, 14-Sep-2020.)
|- S = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }   &    |- ( ph -> N e. NN )   &    |- ( ph -> P = ( ( 2 x. N ) + 1 ) )   &    |- ( ph -> P e. Prime )   &    |- ( ph -> ( 0 ... ( 2 x. N ) ) C_ S )   &    |- T = { i e. NN | ( i x. P ) e. S }   &    |- M = inf ( T , RR , < )   &    |- ( ph -> M e. ( ZZ>= ` 2 ) )   &    |- ( ph -> A e. ZZ )   &    |- ( ph -> B e. ZZ )   &    |- ( ph -> C e. ZZ )   &    |- ( ph -> D e. ZZ )   &    |- E = ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- F = ( ( ( B + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- G = ( ( ( C + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- H = ( ( ( D + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- R = ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) / M )   &    |- ( ph -> ( M x. P ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) )   =>    |- ( ph -> ( R <_ M /\ ( ( R = 0 \/ R = M ) -> ( M ^ 2 ) || ( M x. P ) ) ) )
Theorem	4sqlem17 12805*	Lemma for 4sq 12808. (Contributed by Mario Carneiro, 16-Jul-2014.) (Revised by AV, 14-Sep-2020.)
|- S = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }   &    |- ( ph -> N e. NN )   &    |- ( ph -> P = ( ( 2 x. N ) + 1 ) )   &    |- ( ph -> P e. Prime )   &    |- ( ph -> ( 0 ... ( 2 x. N ) ) C_ S )   &    |- T = { i e. NN | ( i x. P ) e. S }   &    |- M = inf ( T , RR , < )   &    |- ( ph -> M e. ( ZZ>= ` 2 ) )   &    |- ( ph -> A e. ZZ )   &    |- ( ph -> B e. ZZ )   &    |- ( ph -> C e. ZZ )   &    |- ( ph -> D e. ZZ )   &    |- E = ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- F = ( ( ( B + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- G = ( ( ( C + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- H = ( ( ( D + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- R = ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) / M )   &    |- ( ph -> ( M x. P ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) )   =>    |- -. ph
Theorem	4sqlem18 12806*	Lemma for 4sq 12808. Inductive step, odd prime case. (Contributed by Mario Carneiro, 16-Jul-2014.) (Revised by AV, 14-Sep-2020.)
|- S = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }   &    |- ( ph -> N e. NN )   &    |- ( ph -> P = ( ( 2 x. N ) + 1 ) )   &    |- ( ph -> P e. Prime )   &    |- ( ph -> ( 0 ... ( 2 x. N ) ) C_ S )   &    |- T = { i e. NN | ( i x. P ) e. S }   &    |- M = inf ( T , RR , < )   =>    |- ( ph -> P e. S )
Theorem	4sqlem19 12807*	Lemma for 4sq 12808. The proof is by strong induction - we show that if all the integers less than k are in S, then k is as well. In this part of the proof we do the induction argument and dispense with all the cases except the odd prime case, which is sent to 4sqlem18 12806. If k is 0 , 1 , 2, we show k e. S directly; otherwise if k is composite, k is the product of two numbers less than it (and hence in S by assumption), so by mul4sq 12792 k e. S. (Contributed by Mario Carneiro, 14-Jul-2014.) (Revised by Mario Carneiro, 20-Jun-2015.)
|- S = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }   =>    |- NN0 = S
Theorem	4sq 12808*	Lagrange's four-square theorem, or Bachet's conjecture: every nonnegative integer is expressible as a sum of four squares. This is Metamath 100 proof #19. (Contributed by Mario Carneiro, 16-Jul-2014.)
|- ( A e. NN0 <-> E. a e. ZZ E. b e. ZZ E. c e. ZZ E. d e. ZZ A = ( ( ( a ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) )
5.2.13  Decimal arithmetic (cont.)
Theorem	dec2dvds 12809	Divisibility by two is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- A e. NN0   &    |- B e. NN0   &    |- ( B x. 2 ) = C   &    |- D = ( C + 1 )   =>    |- -. 2 || ; A D
Theorem	dec5dvds 12810	Divisibility by five is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- A e. NN0   &    |- B e. NN   &    |- B < 5   =>    |- -. 5 || ; A B
Theorem	dec5dvds2 12811	Divisibility by five is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- A e. NN0   &    |- B e. NN   &    |- B < 5   &    |- ( 5 + B ) = C   =>    |- -. 5 || ; A C
Theorem	dec5nprm 12812	A decimal number greater than 10 and ending with five is not a prime number. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- A e. NN   =>    |- -. ; A 5 e. Prime
Theorem	dec2nprm 12813	A decimal number greater than 10 and ending with an even digit is not a prime number. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- A e. NN   &    |- B e. NN0   &    |- ( B x. 2 ) = C   =>    |- -. ; A C e. Prime
Theorem	modxai 12814	Add exponents in a power mod calculation. (Contributed by Mario Carneiro, 21-Feb-2014.) (Revised by Mario Carneiro, 5-Feb-2015.)
|- N e. NN   &    |- A e. NN   &    |- B e. NN0   &    |- D e. ZZ   &    |- K e. NN0   &    |- M e. NN0   &    |- C e. NN0   &    |- L e. NN0   &    |- ( ( A ^ B ) mod N ) = ( K mod N )   &    |- ( ( A ^ C ) mod N ) = ( L mod N )   &    |- ( B + C ) = E   &    |- ( ( D x. N ) + M ) = ( K x. L )   =>    |- ( ( A ^ E ) mod N ) = ( M mod N )
Theorem	mod2xi 12815	Double exponents in a power mod calculation. (Contributed by Mario Carneiro, 21-Feb-2014.)
|- N e. NN   &    |- A e. NN   &    |- B e. NN0   &    |- D e. ZZ   &    |- K e. NN0   &    |- M e. NN0   &    |- ( ( A ^ B ) mod N ) = ( K mod N )   &    |- ( 2 x. B ) = E   &    |- ( ( D x. N ) + M ) = ( K x. K )   =>    |- ( ( A ^ E ) mod N ) = ( M mod N )
Theorem	modxp1i 12816	Add one to an exponent in a power mod calculation. (Contributed by Mario Carneiro, 21-Feb-2014.)
|- N e. NN   &    |- A e. NN   &    |- B e. NN0   &    |- D e. ZZ   &    |- K e. NN0   &    |- M e. NN0   &    |- ( ( A ^ B ) mod N ) = ( K mod N )   &    |- ( B + 1 ) = E   &    |- ( ( D x. N ) + M ) = ( K x. A )   =>    |- ( ( A ^ E ) mod N ) = ( M mod N )
Theorem	modsubi 12817	Subtract from within a mod calculation. (Contributed by Mario Carneiro, 18-Feb-2014.)
|- N e. NN   &    |- A e. NN   &    |- B e. NN0   &    |- M e. NN0   &    |- ( A mod N ) = ( K mod N )   &    |- ( M + B ) = K   =>    |- ( ( A - B ) mod N ) = ( M mod N )
Theorem	gcdi 12818	Calculate a GCD via Euclid's algorithm. (Contributed by Mario Carneiro, 19-Feb-2014.)
|- K e. NN0   &    |- R e. NN0   &    |- N e. NN0   &    |- ( N gcd R ) = G   &    |- ( ( K x. N ) + R ) = M   =>    |- ( M gcd N ) = G
Theorem	gcdmodi 12819	Calculate a GCD via Euclid's algorithm. Theorem 5.6 in [ApostolNT] p. 109. (Contributed by Mario Carneiro, 19-Feb-2014.)
|- K e. NN0   &    |- R e. NN0   &    |- N e. NN   &    |- ( K mod N ) = ( R mod N )   &    |- ( N gcd R ) = G   =>    |- ( K gcd N ) = G
Theorem	numexp0 12820	Calculate an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.)
|- A e. NN0   =>    |- ( A ^ 0 ) = 1
Theorem	numexp1 12821	Calculate an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.)
|- A e. NN0   =>    |- ( A ^ 1 ) = A
Theorem	numexpp1 12822	Calculate an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.)
|- A e. NN0   &    |- M e. NN0   &    |- ( M + 1 ) = N   &    |- ( ( A ^ M ) x. A ) = C   =>    |- ( A ^ N ) = C
Theorem	numexp2x 12823	Double an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.)
|- A e. NN0   &    |- M e. NN0   &    |- ( 2 x. M ) = N   &    |- ( A ^ M ) = D   &    |- ( D x. D ) = C   =>    |- ( A ^ N ) = C
Theorem	decsplit0b 12824	Split a decimal number into two parts. Base case: N = 0. (Contributed by Mario Carneiro, 16-Jul-2015.) (Revised by AV, 8-Sep-2021.)
|- A e. NN0   =>    |- ( ( A x. (; 1 0 ^ 0 ) ) + B ) = ( A + B )
Theorem	decsplit0 12825	Split a decimal number into two parts. Base case: N = 0. (Contributed by Mario Carneiro, 16-Jul-2015.) (Revised by AV, 8-Sep-2021.)
|- A e. NN0   =>    |- ( ( A x. (; 1 0 ^ 0 ) ) + 0 ) = A
Theorem	decsplit1 12826	Split a decimal number into two parts. Base case: N = 1. (Contributed by Mario Carneiro, 16-Jul-2015.) (Revised by AV, 8-Sep-2021.)
|- A e. NN0   =>    |- ( ( A x. (; 1 0 ^ 1 ) ) + B ) = ; A B
Theorem	decsplit 12827	Split a decimal number into two parts. Inductive step. (Contributed by Mario Carneiro, 16-Jul-2015.) (Revised by AV, 8-Sep-2021.)
|- A e. NN0   &    |- B e. NN0   &    |- D e. NN0   &    |- M e. NN0   &    |- ( M + 1 ) = N   &    |- ( ( A x. (; 1 0 ^ M ) ) + B ) = C   =>    |- ( ( A x. (; 1 0 ^ N ) ) + ; B D ) = ; C D
Theorem	karatsuba 12828	The Karatsuba multiplication algorithm. If X and Y are decomposed into two groups of digits of length M (only the lower group is known to be this size but the algorithm is most efficient when the partition is chosen near the middle of the digit string), then X Y can be written in three groups of digits, where each group needs only one multiplication. Thus, we can halve both inputs with only three multiplications on the smaller operands, yielding an asymptotic improvement of n^(log2 3) instead of n^2 for the "naive" algorithm decmul1c 9588. (Contributed by Mario Carneiro, 16-Jul-2015.) (Revised by AV, 9-Sep-2021.)
|- A e. NN0   &    |- B e. NN0   &    |- C e. NN0   &    |- D e. NN0   &    |- S e. NN0   &    |- M e. NN0   &    |- ( A x. C ) = R   &    |- ( B x. D ) = T   &    |- ( ( A + B ) x. ( C + D ) ) = ( ( R + S ) + T )   &    |- ( ( A x. (; 1 0 ^ M ) ) + B ) = X   &    |- ( ( C x. (; 1 0 ^ M ) ) + D ) = Y   &    |- ( ( R x. (; 1 0 ^ M ) ) + S ) = W   &    |- ( ( W x. (; 1 0 ^ M ) ) + T ) = Z   =>    |- ( X x. Y ) = Z
Theorem	2exp4 12829	Two to the fourth power is 16. (Contributed by Mario Carneiro, 20-Apr-2015.)
|- ( 2 ^ 4 ) = ; 1 6
Theorem	2exp5 12830	Two to the fifth power is 32. (Contributed by AV, 16-Aug-2021.)
|- ( 2 ^ 5 ) = ; 3 2
Theorem	2exp6 12831	Two to the sixth power is 64. (Contributed by Mario Carneiro, 20-Apr-2015.) (Proof shortened by OpenAI, 25-Mar-2020.)
|- ( 2 ^ 6 ) = ; 6 4
Theorem	2exp7 12832	Two to the seventh power is 128. (Contributed by AV, 16-Aug-2021.)
|- ( 2 ^ 7 ) = ;; 1 2 8
Theorem	2exp8 12833	Two to the eighth power is 256. (Contributed by Mario Carneiro, 20-Apr-2015.)
|- ( 2 ^ 8 ) = ;; 2 5 6
Theorem	2exp11 12834	Two to the eleventh power is 2048. (Contributed by AV, 16-Aug-2021.)
|- ( 2 ^; 1 1 ) = ;;; 2 0 4 8
Theorem	2exp16 12835	Two to the sixteenth power is 65536. (Contributed by Mario Carneiro, 20-Apr-2015.)
|- ( 2 ^; 1 6 ) = ;;;; 6 5 5 3 6
Theorem	3exp3 12836	Three to the third power is 27. (Contributed by Mario Carneiro, 20-Apr-2015.)
|- ( 3 ^ 3 ) = ; 2 7
Theorem	2expltfac 12837	The factorial grows faster than two to the power N. (Contributed by Mario Carneiro, 15-Sep-2016.)
|- ( N e. ( ZZ>= ` 4 ) -> ( 2 ^ N ) < ( ! ` N ) )
5.3  Cardinality of real and complex number subsets
5.3.1  Countability of integers and rationals
Theorem	oddennn 12838	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 12839	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 12840	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 12841	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 12842	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 12843	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 12844	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 12845*	Lemma for ennnfone 12871. A direct consequence of fidcenumlemrk 7071. (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 12846*	Lemma for ennnfone 12871. (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 12847*	Lemma for ennnfone 12871. 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 12848*	Lemma for ennnfone 12871. 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 12849*	Lemma for ennnfone 12871. 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 12850*	Lemma for ennnfone 12871. (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 12851*	Lemma for ennnfone 12871. 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 12852*	Lemma for ennnfone 12871. 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 12853*	Lemma for ennnfone 12871. 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 12854*	Lemma for ennnfone 12871. 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 12855*	Lemma for ennnfone 12871. 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 12856*	Lemma for ennnfone 12871. 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 12857*	Lemma for ennnfone 12871. 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 12858*	Lemma for ennnfone 12871. 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 12859*	Lemma for ennnfone 12871. 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 12860*	Lemma for ennnfone 12871. 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 12861*	Lemma for ennnfone 12871. 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 12862*	Lemma for ennnfone 12871. A consequence of ennnfonelemss 12856. (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 12863*	Lemma for ennnfone 12871. 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 12864*	Lemma for ennnfone 12871. 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 12865*	Lemma for ennnfone 12871. 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 12866*	Lemma for ennnfone 12871. 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 12867*	Lemma for ennnfone 12871. 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 12868*	Lemma for ennnfone 12871. A version of ennnfonelemen 12867 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 12869*	Lemma for ennnfone 12871. 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 12870*	Lemma for ennnfone 12871. 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 12871*	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 7226), 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 12872*	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 12873*	Lemma for ctinfom 12874. 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 12874*	A condition for a set being countably infinite. Restates ennnfone 12871 in terms of om and function image. Like ennnfone 12871 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 12875*	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 12876*	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 12877	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 12878*	Lemma for enct 12879. 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 12879*	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 12880*	Lemma for ctiunct 12886. (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 12881*	Lemma for ctiunct 12886. (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 12882	Lemma for ctiunct 12886. (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 12883*	Lemma for ctiunct 12886. (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 12884*	Lemma for ctiunct 12886. (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 12885*	Lemma for ctiunct 12886. (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 12886*	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 12890 (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 12888, 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 12841) 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 7228 and ctssdc 7230. (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 12887*	Variation of ctiunct 12886 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 12888*	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 12889*	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 12890*	The union of a countably infinite collection of countable sets is countable. Theorem 8.1.28 of [AczelRathjen], p. 78. Compare with ctiunct 12886 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 12891*	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 12892*	Lemma for ssnnct 12893. 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 12893*	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 12894*	Lemma for nninfdc 12899. (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 12895*	Lemma for nninfdc 12899. 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 12896*	Lemma for nninfdc 12899. 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 12897*	Lemma for nninfdc 12899. The function from nninfdclemf 12895 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 12898*	Lemma for nninfdc 12899. The function from nninfdclemf 12895 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 12899*	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 12900*	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 )