HomeHome Intuitionistic Logic Explorer
Theorem List (p. 119 of 132)
< Previous  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 11801-11900   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremphicl2 11801 Bounds and closure for the value of the Euler  phi function. (Contributed by Mario Carneiro, 23-Feb-2014.)
 |-  ( N  e.  NN  ->  ( phi `  N )  e.  ( 1 ... N ) )
 
Theoremphicl 11802 Closure for the value of the Euler 
phi function. (Contributed by Mario Carneiro, 28-Feb-2014.)
 |-  ( N  e.  NN  ->  ( phi `  N )  e.  NN )
 
Theoremphibndlem 11803* Lemma for phibnd 11804. (Contributed by Mario Carneiro, 23-Feb-2014.)
 |-  ( N  e.  ( ZZ>=
 `  2 )  ->  { x  e.  (
 1 ... N )  |  ( x  gcd  N )  =  1 }  C_  ( 1 ... ( N  -  1 ) ) )
 
Theoremphibnd 11804 A slightly tighter bound on the value of the Euler  phi function. (Contributed by Mario Carneiro, 23-Feb-2014.)
 |-  ( N  e.  ( ZZ>=
 `  2 )  ->  ( phi `  N )  <_  ( N  -  1
 ) )
 
Theoremphicld 11805 Closure for the value of the Euler 
phi function. (Contributed by Mario Carneiro, 29-May-2016.)
 |-  ( ph  ->  N  e.  NN )   =>    |-  ( ph  ->  ( phi `  N )  e. 
 NN )
 
Theoremphi1 11806 Value of the Euler  phi function at 1. (Contributed by Mario Carneiro, 23-Feb-2014.)
 |-  ( phi `  1
 )  =  1
 
Theoremdfphi2 11807* Alternate definition of the Euler 
phi function. (Contributed by Mario Carneiro, 23-Feb-2014.) (Revised by Mario Carneiro, 2-May-2016.)
 |-  ( N  e.  NN  ->  ( phi `  N )  =  ( `  { x  e.  ( 0..^ N )  |  ( x  gcd  N )  =  1 } ) )
 
Theoremhashdvds 11808* The number of numbers in a given residue class in a finite set of integers. (Contributed by Mario Carneiro, 12-Mar-2014.) (Proof shortened by Mario Carneiro, 7-Jun-2016.)
 |-  ( ph  ->  N  e.  NN )   &    |-  ( ph  ->  A  e.  ZZ )   &    |-  ( ph  ->  B  e.  ( ZZ>=
 `  ( A  -  1 ) ) )   &    |-  ( ph  ->  C  e.  ZZ )   =>    |-  ( ph  ->  ( ` 
 { x  e.  ( A ... B )  |  N  ||  ( x  -  C ) } )  =  ( ( |_ `  (
 ( B  -  C )  /  N ) )  -  ( |_ `  (
 ( ( A  -  1 )  -  C )  /  N ) ) ) )
 
Theoremphiprmpw 11809 Value of the Euler  phi function at a prime power. Theorem 2.5(a) in [ApostolNT] p. 28. (Contributed by Mario Carneiro, 24-Feb-2014.)
 |-  ( ( P  e.  Prime  /\  K  e.  NN )  ->  ( phi `  ( P ^ K ) )  =  ( ( P ^ ( K  -  1 ) )  x.  ( P  -  1
 ) ) )
 
Theoremphiprm 11810 Value of the Euler  phi function at a prime. (Contributed by Mario Carneiro, 28-Feb-2014.)
 |-  ( P  e.  Prime  ->  ( phi `  P )  =  ( P  -  1
 ) )
 
Theoremcrth 11811* The Chinese Remainder Theorem: the function that maps  x to its remainder classes  mod  M and  mod  N is 1-1 and onto when  M and  N are coprime. (Contributed by Mario Carneiro, 24-Feb-2014.) (Proof shortened by Mario Carneiro, 2-May-2016.)
 |-  S  =  ( 0..^ ( M  x.  N ) )   &    |-  T  =  ( ( 0..^ M )  X.  ( 0..^ N ) )   &    |-  F  =  ( x  e.  S  |->  <.
 ( x  mod  M ) ,  ( x  mod  N ) >. )   &    |-  ( ph  ->  ( M  e.  NN  /\  N  e.  NN  /\  ( M  gcd  N )  =  1 )
 )   =>    |-  ( ph  ->  F : S -1-1-onto-> T )
 
Theoremphimullem 11812* Lemma for phimul 11813. (Contributed by Mario Carneiro, 24-Feb-2014.)
 |-  S  =  ( 0..^ ( M  x.  N ) )   &    |-  T  =  ( ( 0..^ M )  X.  ( 0..^ N ) )   &    |-  F  =  ( x  e.  S  |->  <.
 ( x  mod  M ) ,  ( x  mod  N ) >. )   &    |-  ( ph  ->  ( M  e.  NN  /\  N  e.  NN  /\  ( M  gcd  N )  =  1 )
 )   &    |-  U  =  { y  e.  ( 0..^ M )  |  ( y  gcd  M )  =  1 }   &    |-  V  =  { y  e.  ( 0..^ N )  |  ( y  gcd  N )  =  1 }   &    |-  W  =  { y  e.  S  |  ( y 
 gcd  ( M  x.  N ) )  =  1 }   =>    |-  ( ph  ->  ( phi `  ( M  x.  N ) )  =  ( ( phi `  M )  x.  ( phi `  N ) ) )
 
Theoremphimul 11813 The Euler  phi function is a multiplicative function, meaning that it distributes over multiplication at relatively prime arguments. Theorem 2.5(c) in [ApostolNT] p. 28. (Contributed by Mario Carneiro, 24-Feb-2014.)
 |-  ( ( M  e.  NN  /\  N  e.  NN  /\  ( M  gcd  N )  =  1 )  ->  ( phi `  ( M  x.  N ) )  =  ( ( phi `  M )  x.  ( phi `  N ) ) )
 
Theoremhashgcdlem 11814* A correspondence between elements of specific GCD and relative primes in a smaller ring. (Contributed by Stefan O'Rear, 12-Sep-2015.)
 |-  A  =  { y  e.  ( 0..^ ( M 
 /  N ) )  |  ( y  gcd  ( M  /  N ) )  =  1 }   &    |-  B  =  { z  e.  ( 0..^ M )  |  ( z  gcd  M )  =  N }   &    |-  F  =  ( x  e.  A  |->  ( x  x.  N ) )   =>    |-  ( ( M  e.  NN  /\  N  e.  NN  /\  N  ||  M )  ->  F : A -1-1-onto-> B )
 
Theoremhashgcdeq 11815* Number of initial positive integers with specified divisors. (Contributed by Stefan O'Rear, 12-Sep-2015.)
 |-  ( ( M  e.  NN  /\  N  e.  NN )  ->  ( `  { x  e.  ( 0..^ M )  |  ( x  gcd  M )  =  N }
 )  =  if ( N  ||  M ,  ( phi `  ( M  /  N ) ) ,  0 ) )
 
5.3  Cardinality of real and complex number subsets
 
5.3.1  Countability of integers and rationals
 
Theoremoddennn 11816 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
 
Theoremevenennn 11817 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
 
Theoremxpnnen 11818 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
 
Theoremxpomen 11819 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
 
Theoremxpct 11820 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 )
 
Theoremunennn 11821 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 )
 
Theoremznnen 11822 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
 
Theoremennnfonelemdc 11823* Lemma for ennnfone 11849. A direct consequence of fidcenumlemrk 6810. (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 ) )
 
Theoremennnfonelemk 11824* Lemma for ennnfone 11849. (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 )
 
Theoremennnfonelemj0 11825* Lemma for ennnfone 11849. 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 } )
 
Theoremennnfonelemjn 11826* Lemma for ennnfone 11849. 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 )
 
Theoremennnfonelemg 11827* Lemma for ennnfone 11849. 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 } )
 
Theoremennnfonelemh 11828* Lemma for ennnfone 11849. (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 ) )
 
Theoremennnfonelem0 11829* Lemma for ennnfone 11849. 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 )  =  (/) )
 
Theoremennnfonelemp1 11830* Lemma for ennnfone 11849. 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 ) ) >. } ) ) )
 
Theoremennnfonelem1 11831* Lemma for ennnfone 11849. 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 `
  (/) ) >. } )
 
Theoremennnfonelemom 11832* Lemma for ennnfone 11849. 
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 )
 
Theoremennnfonelemhdmp1 11833* Lemma for ennnfone 11849. 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 ) )
 
Theoremennnfonelemss 11834* Lemma for ennnfone 11849. 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 ) ) )
 
Theoremennnfoneleminc 11835* Lemma for ennnfone 11849. 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 ) )
 
Theoremennnfonelemkh 11836* Lemma for ennnfone 11849. 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 ) )
 
Theoremennnfonelemhf1o 11837* Lemma for ennnfone 11849. 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 ) ) )
 
Theoremennnfonelemex 11838* Lemma for ennnfone 11849. 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 ) )
 
Theoremennnfonelemhom 11839* Lemma for ennnfone 11849. 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 ) )
 
Theoremennnfonelemrnh 11840* Lemma for ennnfone 11849. A consequence of ennnfonelemss 11834. (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 ) )
 
Theoremennnfonelemfun 11841* Lemma for ennnfone 11849. 
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 )
 
Theoremennnfonelemf1 11842* Lemma for ennnfone 11849. 
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 )
 
Theoremennnfonelemrn 11843* Lemma for ennnfone 11849. 
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 )
 
Theoremennnfonelemdm 11844* Lemma for ennnfone 11849. 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 )
 
Theoremennnfonelemen 11845* Lemma for ennnfone 11849. 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 )
 
Theoremennnfonelemnn0 11846* Lemma for ennnfone 11849. A version of ennnfonelemen 11845 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 )
 
Theoremennnfonelemr 11847* Lemma for ennnfone 11849. 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 )
 
Theoremennnfonelemim 11848* Lemma for ennnfone 11849. 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 ) ) ) )
 
Theoremennnfone 11849* 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 6962), 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 )
 ) ) )
 
Theoremexmidunben 11850* 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 )
 
Theoremctinfomlemom 11851* Lemma for ctinfom 11852. 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 ) ) )
 
Theoremctinfom 11852* A condition for a set being countably infinite. Restates ennnfone 11849 in terms of  om and function image. Like ennnfone 11849 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 ) ) ) )
 
Theoreminffinp1 11853* 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 )
 
Theoremctinf 11854* 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 ) )
 
Theoremqnnen 11855 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
 
Theoremenctlem 11856* Lemma for enct 11857. 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 ) ) )
 
Theoremenct 11857* 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 )
 ) )
 
Theoremctiunctlemu1st 11858* Lemma for ctiunct 11864. (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 )
 
Theoremctiunctlemu2nd 11859* Lemma for ctiunct 11864. (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 )
 
Theoremctiunctlemuom 11860 Lemma for ctiunct 11864. (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 )
 
Theoremctiunctlemudc 11861* Lemma for ctiunct 11864. (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 )
 
Theoremctiunctlemf 11862* Lemma for ctiunct 11864. (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 )
 
Theoremctiunctlemfo 11863* Lemma for ctiunct 11864. (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 )
 
Theoremctiunct 11864* 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.

The "countably many countable sets" version could be expressed as  ( ph  /\  x  e.  A )  ->  E. g g : om -onto-> ( B 1o ) and countable choice would be needed to derive the current hypothesis from that.

Compare with the case of two sets instead of countably many, as seen at unct 11865, in which case we express countability using  E..

The proof proceeds by mapping a natural number to a pair of natural numbers (by xpomen 11819) 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 6964 and ctssdc 6966.

(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 ) )
 
Theoremunct 11865* The union of two countable sets is countable. (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 ) )
 
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 11894 and strslfv 11914. Using extractors makes it easier to change numeric indices and also makes the components' purpose clearer.

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-ress 11878. 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.

 
Syntaxcstr 11866 Extend class notation with the class of structures with components numbered below  A.
 class Struct
 
Syntaxcnx 11867 Extend class notation with the structure component index extractor.
 class  ndx
 
Syntaxcsts 11868 Set components of a structure.
 class sSet
 
Syntaxcslot 11869 Extend class notation with the slot function.
 class Slot  A
 
Syntaxcbs 11870 Extend class notation with the class of all base set extractors.
 class  Base
 
Syntaxcress 11871 Extend class notation with the extensible structure builder restriction operator.
 classs
 
Definitiondf-struct 11872* Define a structure with components in  M ... N. This is not a requirement for groups, posets, etc., but it is a useful assumption for component extraction theorems.

As mentioned in the section header, an "extensible structure should be implemented as a function (a set of ordered pairs)". The current definition, however, is less restrictive: it allows for classes which contain the empty set 
(/) to be extensible structures. Because of 0nelfun 5111, such classes cannot be functions. Without the empty set, however, a structure must be a function, see structn0fun 11883:  F Struct  X  ->  Fun  ( F  \  { (/)
} ).

Allowing an extensible structure to contain the empty set ensures that expressions like  { <. A ,  B >. ,  <. C ,  D >. } are structures without asserting or implying that  A,  B,  C and  D are sets (if  A or  B is a proper class, then  <. A ,  B >.  =  (/), see opprc 3696). (Contributed by Mario Carneiro, 29-Aug-2015.)

 |- Struct  =  { <. f ,  x >.  |  ( x  e.  (  <_  i^i  ( NN 
 X.  NN ) )  /\  Fun  ( f  \  { (/)
 } )  /\  dom  f  C_  ( ... `  x ) ) }
 
Definitiondf-ndx 11873 Define the structure component index extractor. See theorem ndxarg 11893 to understand its purpose. The restriction to  NN ensures that  ndx is a set. The restriction to some set is necessary since  _I is a proper class. In principle, we could have chosen  CC or (if we revise all structure component definitions such as df-base 11876) another set such as the set of finite ordinals 
om (df-iom 4475). (Contributed by NM, 4-Sep-2011.)
 |- 
 ndx  =  (  _I  |` 
 NN )
 
Definitiondf-slot 11874* Define the slot extractor for extensible structures. The class Slot  A is a function whose argument can be any set, although it is meaningful only if that set is a member of an extensible structure (such as a partially ordered set or a group).

Note that Slot  A is implemented as "evaluation at  A". That is,  (Slot  A `  S ) is defined to be  ( S `  A ), where  A will typically be a small nonzero natural number. Each extensible structure  S is a function defined on specific natural number "slots", and this function extracts the value at a particular slot.

The special "structure"  ndx, defined as the identity function restricted to  NN, can be used to extract the number  A from a slot, since  (Slot  A `  ndx )  =  A (see ndxarg 11893). This is typically used to refer to the number of a slot when defining structures without having to expose the detail of what that number is (for instance, we use the expression  ( Base `  ndx ) in theorems and proofs instead of its value 1).

The class Slot cannot be defined as  ( x  e.  _V  |->  ( f  e. 
_V  |->  ( f `  x ) ) ) because each Slot  A is a function on the proper class  _V so is itself a proper class, and the values of functions are sets (fvex 5409). It is necessary to allow proper classes as values of Slot  A since for instance the class of all (base sets of) groups is proper. (Contributed by Mario Carneiro, 22-Sep-2015.)

 |- Slot  A  =  ( x  e.  _V  |->  ( x `  A ) )
 
Theoremsloteq 11875 Equality theorem for the Slot construction. The converse holds if  A (or  B) is a set. (Contributed by BJ, 27-Dec-2021.)
 |-  ( A  =  B  -> Slot 
 A  = Slot  B )
 
Definitiondf-base 11876 Define the base set (also called underlying set, ground set, carrier set, or carrier) extractor for extensible structures. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
 |- 
 Base  = Slot  1
 
Definitiondf-sets 11877* Set a component of an extensible structure. This function is useful for taking an existing structure and "overriding" one of its components. For example, df-ress 11878 adjusts the base set to match its second argument, which has the effect of making subgroups, subspaces, subrings etc. from the original structures. (Contributed by Mario Carneiro, 1-Dec-2014.)
 |- sSet  =  ( s  e.  _V ,  e  e.  _V  |->  ( ( s  |`  ( _V  \  dom  { e } ) )  u. 
 { e } )
 )
 
Definitiondf-ress 11878* Define a multifunction restriction operator for extensible structures, which 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.

(Credit for this operator goes to Mario Carneiro.)

(Contributed by Stefan O'Rear, 29-Nov-2014.)

 |-s  =  ( w  e.  _V ,  x  e.  _V  |->  if ( ( Base `  w )  C_  x ,  w ,  ( w sSet  <. ( Base ` 
 ndx ) ,  ( x  i^i  ( Base `  w ) ) >. ) ) )
 
Theorembrstruct 11879 The structure relation is a relation. (Contributed by Mario Carneiro, 29-Aug-2015.)
 |- 
 Rel Struct
 
Theoremisstruct2im 11880 The property of being a structure with components in  ( 1st `  X
) ... ( 2nd `  X
). (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 18-Jan-2023.)
 |-  ( F Struct  X  ->  ( X  e.  (  <_  i^i  ( NN  X.  NN ) )  /\  Fun  ( F  \  { (/) } )  /\  dom  F  C_  ( ... `  X ) ) )
 
Theoremisstruct2r 11881 The property of being a structure with components in  ( 1st `  X
) ... ( 2nd `  X
). (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 18-Jan-2023.)
 |-  ( ( ( X  e.  (  <_  i^i  ( NN  X.  NN )
 )  /\  Fun  ( F 
 \  { (/) } )
 )  /\  ( F  e.  V  /\  dom  F  C_  ( ... `  X ) ) )  ->  F Struct  X )
 
Theoremstructex 11882 A structure is a set. (Contributed by AV, 10-Nov-2021.)
 |-  ( G Struct  X  ->  G  e.  _V )
 
Theoremstructn0fun 11883 A structure without the empty set is a function. (Contributed by AV, 13-Nov-2021.)
 |-  ( F Struct  X  ->  Fun  ( F  \  { (/)
 } ) )
 
Theoremisstructim 11884 The property of being a structure with components in  M ... N. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 18-Jan-2023.)
 |-  ( F Struct  <. M ,  N >.  ->  ( ( M  e.  NN  /\  N  e.  NN  /\  M  <_  N )  /\  Fun  ( F  \  { (/) } )  /\  dom  F  C_  ( M ... N ) ) )
 
Theoremisstructr 11885 The property of being a structure with components in  M ... N. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 18-Jan-2023.)
 |-  ( ( ( M  e.  NN  /\  N  e.  NN  /\  M  <_  N )  /\  ( Fun  ( F  \  { (/)
 } )  /\  F  e.  V  /\  dom  F  C_  ( M ... N ) ) )  ->  F Struct 
 <. M ,  N >. )
 
Theoremstructcnvcnv 11886 Two ways to express the relational part of a structure. (Contributed by Mario Carneiro, 29-Aug-2015.)
 |-  ( F Struct  X  ->  `' `' F  =  ( F  \  { (/) } )
 )
 
Theoremstructfung 11887 The converse of the converse of a structure is a function. Closed form of structfun 11888. (Contributed by AV, 12-Nov-2021.)
 |-  ( F Struct  X  ->  Fun  `' `' F )
 
Theoremstructfun 11888 Convert between two kinds of structure closure. (Contributed by Mario Carneiro, 29-Aug-2015.) (Proof shortened by AV, 12-Nov-2021.)
 |-  F Struct  X   =>    |- 
 Fun  `' `' F
 
Theoremstructfn 11889 Convert between two kinds of structure closure. (Contributed by Mario Carneiro, 29-Aug-2015.)
 |-  F Struct  <. M ,  N >.   =>    |-  ( Fun  `' `' F  /\  dom  F  C_  (
 1 ... N ) )
 
Theoremstrnfvnd 11890 Deduction version of strnfvn 11891. (Contributed by Mario Carneiro, 15-Nov-2014.) (Revised by Jim Kingdon, 19-Jan-2023.)
 |-  E  = Slot  N   &    |-  ( ph  ->  S  e.  V )   &    |-  ( ph  ->  N  e.  NN )   =>    |-  ( ph  ->  ( E `  S )  =  ( S `  N ) )
 
Theoremstrnfvn 11891 Value of a structure component extractor  E. Normally,  E is a defined constant symbol such as  Base (df-base 11876) and  N is a fixed integer such as  1.  S is a structure, i.e. a specific member of a class of structures.

Note: Normally, this theorem shouldn't be used outside of this section, because it requires hard-coded index values. Instead, use strslfv 11914. (Contributed by NM, 9-Sep-2011.) (Revised by Jim Kingdon, 19-Jan-2023.) (New usage is discouraged.)

 |-  S  e.  _V   &    |-  E  = Slot  N   &    |-  N  e.  NN   =>    |-  ( E `  S )  =  ( S `  N )
 
Theoremstrfvssn 11892 A structure component extractor produces a value which is contained in a set dependent on  S, but not  E. This is sometimes useful for showing sethood. (Contributed by Mario Carneiro, 15-Aug-2015.) (Revised by Jim Kingdon, 19-Jan-2023.)
 |-  E  = Slot  N   &    |-  ( ph  ->  S  e.  V )   &    |-  ( ph  ->  N  e.  NN )   =>    |-  ( ph  ->  ( E `  S )  C_  U.
 ran  S )
 
Theoremndxarg 11893 Get the numeric argument from a defined structure component extractor such as df-base 11876. (Contributed by Mario Carneiro, 6-Oct-2013.)
 |-  E  = Slot  N   &    |-  N  e.  NN   =>    |-  ( E `  ndx )  =  N
 
Theoremndxid 11894 A structure component extractor is defined by its own index. This theorem, together with strslfv 11914 below, is useful for avoiding direct reference to the hard-coded numeric index in component extractor definitions, such as the  1 in df-base 11876, making it easier to change should the need arise.

(Contributed by NM, 19-Oct-2012.) (Revised by Mario Carneiro, 6-Oct-2013.) (Proof shortened by BJ, 27-Dec-2021.)

 |-  E  = Slot  N   &    |-  N  e.  NN   =>    |-  E  = Slot  ( E `
  ndx )
 
Theoremndxslid 11895 A structure component extractor is defined by its own index. That the index is a natural number will also be needed in quite a few contexts so it is included in the conclusion of this theorem which can be used as a hypothesis of theorems like strslfv 11914. (Contributed by Jim Kingdon, 29-Jan-2023.)
 |-  E  = Slot  N   &    |-  N  e.  NN   =>    |-  ( E  = Slot  ( E `  ndx )  /\  ( E `  ndx )  e.  NN )
 
Theoremslotslfn 11896 A slot is a function on sets, treated as structures. (Contributed by Mario Carneiro, 22-Sep-2015.) (Revised by Jim Kingdon, 10-Feb-2023.)
 |-  ( E  = Slot  ( E `  ndx )  /\  ( E `  ndx )  e.  NN )   =>    |-  E  Fn  _V
 
Theoremslotex 11897 Existence of slot value. A corollary of slotslfn 11896. (Contributed by Jim Kingdon, 12-Feb-2023.)
 |-  ( E  = Slot  ( E `  ndx )  /\  ( E `  ndx )  e.  NN )   =>    |-  ( A  e.  V  ->  ( E `  A )  e.  _V )
 
Theoremstrndxid 11898 The value of a structure component extractor is the value of the corresponding slot of the structure. (Contributed by AV, 13-Mar-2020.)
 |-  ( ph  ->  S  e.  V )   &    |-  E  = Slot  N   &    |-  N  e.  NN   =>    |-  ( ph  ->  ( S `  ( E `  ndx ) )  =  ( E `  S ) )
 
Theoremreldmsets 11899 The structure override operator is a proper operator. (Contributed by Stefan O'Rear, 29-Jan-2015.)
 |- 
 Rel  dom sSet
 
Theoremsetsvalg 11900 Value of the structure replacement function. (Contributed by Mario Carneiro, 30-Apr-2015.)
 |-  ( ( S  e.  V  /\  A  e.  W )  ->  ( S sSet  A )  =  ( ( S  |`  ( _V  \  dom  { A } ) )  u.  { A }
 ) )
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13145
  Copyright terms: Public domain < Previous  Next >