P. 131 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 13001-13100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	3exp3 13001	Three to the third power is 27. (Contributed by Mario Carneiro, 20-Apr-2015.)
|- ( 3 ^ 3 ) = ; 2 7
Theorem	2expltfac 13002	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 13003	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 13004	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 13005	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 13006	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 13007	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 13008	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 13009	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 13010*	Lemma for ennnfone 13036. A direct consequence of fidcenumlemrk 7144. (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 13011*	Lemma for ennnfone 13036. (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 13012*	Lemma for ennnfone 13036. 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 13013*	Lemma for ennnfone 13036. 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 13014*	Lemma for ennnfone 13036. 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 13015*	Lemma for ennnfone 13036. (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 13016*	Lemma for ennnfone 13036. 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 13017*	Lemma for ennnfone 13036. 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 13018*	Lemma for ennnfone 13036. 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 13019*	Lemma for ennnfone 13036. 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 13020*	Lemma for ennnfone 13036. 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 13021*	Lemma for ennnfone 13036. 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 13022*	Lemma for ennnfone 13036. 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 13023*	Lemma for ennnfone 13036. 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 13024*	Lemma for ennnfone 13036. 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 13025*	Lemma for ennnfone 13036. 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 13026*	Lemma for ennnfone 13036. 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 13027*	Lemma for ennnfone 13036. A consequence of ennnfonelemss 13021. (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 13028*	Lemma for ennnfone 13036. 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 13029*	Lemma for ennnfone 13036. 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 13030*	Lemma for ennnfone 13036. 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 13031*	Lemma for ennnfone 13036. 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 13032*	Lemma for ennnfone 13036. 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 13033*	Lemma for ennnfone 13036. A version of ennnfonelemen 13032 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 13034*	Lemma for ennnfone 13036. 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 13035*	Lemma for ennnfone 13036. 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 13036*	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 7299), 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 13037*	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 13038*	Lemma for ctinfom 13039. 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 13039*	A condition for a set being countably infinite. Restates ennnfone 13036 in terms of om and function image. Like ennnfone 13036 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 13040*	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 13041*	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 13042	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 13043*	Lemma for enct 13044. 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 13044*	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 13045*	Lemma for ctiunct 13051. (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 13046*	Lemma for ctiunct 13051. (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 13047	Lemma for ctiunct 13051. (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 13048*	Lemma for ctiunct 13051. (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 13049*	Lemma for ctiunct 13051. (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 13050*	Lemma for ctiunct 13051. (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 13051*	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 13055 (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 13053, 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 13006) 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 7301 and ctssdc 7303. (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 13052*	Variation of ctiunct 13051 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 13053*	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 13054*	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 13055*	The union of a countably infinite collection of countable sets is countable. Theorem 8.1.28 of [AczelRathjen], p. 78. Compare with ctiunct 13051 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 13056*	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 13057*	Lemma for ssnnct 13058. 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 13058*	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 13059*	Lemma for nninfdc 13064. (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 13060*	Lemma for nninfdc 13064. 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 13061*	Lemma for nninfdc 13064. 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 13062*	Lemma for nninfdc 13064. The function from nninfdclemf 13060 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 13063*	Lemma for nninfdc 13064. The function from nninfdclemf 13060 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 13064*	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 13065*	An unbounded decidable set of positive integers is infinite. (Contributed by NM, 5-May-2005.) (Revised by Jim Kingdon, 30-Sep-2024.)
|- ( ( A C_ NN /\ A. x e. NN DECID x e. A /\ A. m e. NN E. n e. A m < n ) -> A ~~ NN )
Theorem	prminf 13066	There are an infinite number of primes. Theorem 1.7 in [ApostolNT] p. 16. (Contributed by Paul Chapman, 28-Nov-2012.)
|- Prime ~~ NN
Theorem	infpn2 13067*	There exist infinitely many prime numbers: the set of all primes S is unbounded by infpn 12924, so by unbendc 13065 it is infinite. This is Metamath 100 proof #11. (Contributed by NM, 5-May-2005.)
|- S = { n e. NN | ( 1 < n /\ A. m e. NN ( ( n / m ) e. NN -> ( m = 1 \/ m = n ) ) ) }   =>    |- S ~~ NN
PART 6  BASIC STRUCTURES
6.1  Extensible structures
6.1.1  Basic definitions An "extensible structure" (or "structure" in short, at least in this section) is used to define a specific group, ring, poset, and so on. An extensible structure can contain many components. For example, a group will have at least two components (base set and operation), although it can be further specialized by adding other components such as a multiplicative operation for rings (and still remain a group per our definition). Thus, every ring is also a group. This extensible structure approach allows theorems from more general structures (such as groups) to be reused for more specialized structures (such as rings) without having to reprove anything. Structures are common in mathematics, but in informal (natural language) proofs the details are assumed in ways that we must make explicit. An extensible structure is implemented as a function (a set of ordered pairs) on a finite (and not necessarily sequential) subset of NN. The function's argument is the index of a structure component (such as 1 for the base set of a group), and its value is the component (such as the base set). By convention, we normally avoid direct reference to the hard-coded numeric index and instead use structure component extractors such as ndxid 13096 and strslfv 13117. Using extractors makes it easier to change numeric indices and also makes the components' purpose clearer. See the comment of basendx 13127 for more details on numeric indices versus the structure component extractors. There are many other possible ways to handle structures. We chose this extensible structure approach because this approach (1) results in simpler notation than other approaches we are aware of, and (2) is easier to do proofs with. We cannot use an approach that uses "hidden" arguments; Metamath does not support hidden arguments, and in any case we want nothing hidden. It would be possible to use a categorical approach (e.g., something vaguely similar to Lean's mathlib). However, instances (the chain of proofs that an X is a Y via a bunch of forgetful functors) can cause serious performance problems for automated tooling, and the resulting proofs would be painful to look at directly (in the case of Lean, they are long past the level where people would find it acceptable to look at them directly). Metamath is working under much stricter conditions than this, and it has still managed to achieve about the same level of flexibility through this "extensible structure" approach. To create a substructure of a given extensible structure, you can simply use the multifunction restriction operator for extensible structures ↾s as defined in df-iress 13080. This can be used to turn statements about rings into statements about subrings, modules into submodules, etc. This definition knows nothing about individual structures and merely truncates the Base set while leaving operators alone. Individual kinds of structures will need to handle this behavior by ignoring operators' values outside the range, defining a function using the base set and applying that, or explicitly truncating the slot before use. Extensible structures only work well when they represent concrete categories, where there is a "base set", morphisms are functions, and subobjects are subsets with induced operations. In short, they primarily work well for "sets with (some) extra structure". Extensible structures may not suffice for more complicated situations. For example, in manifolds, ↾s would not work. That said, extensible structures are sufficient for many of the structures that set.mm currently considers, and offer a good compromise for a goal-oriented formalization.
Syntax	cstr 13068	Extend class notation with the class of structures with components numbered below A.
class Struct
Syntax	cnx 13069	Extend class notation with the structure component index extractor.
class ndx
Syntax	csts 13070	Set components of a structure.
class sSet
Syntax	cslot 13071	Extend class notation with the slot function.
class Slot A
Syntax	cbs 13072	Extend class notation with the class of all base set extractors.
class Base
Syntax	cress 13073	Extend class notation with the extensible structure builder restriction operator.
class ↾s
Definition	df-struct 13074*	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 5342, such classes cannot be functions. Without the empty set, however, a structure must be a function, see structn0fun 13085: 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 3881). (Contributed by Mario Carneiro, 29-Aug-2015.)
|- Struct = { <. f , x >. | ( x e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( f \ { (/) } ) /\ dom f C_ ( ... ` x ) ) }
Definition	df-ndx 13075	Define the structure component index extractor. See Theorem ndxarg 13095 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 13078) another set such as the set of finite ordinals om (df-iom 4687). (Contributed by NM, 4-Sep-2011.)
|- ndx = ( _I |` NN )
Definition	df-slot 13076*	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 13095). 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 5655). 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 ) )
Theorem	sloteq 13077	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 )
Definition	df-base 13078	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
Definition	df-sets 13079*	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-iress 13080 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 } ) )
Definition	df-iress 13080*	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, as well as the 2023 modification for iset.mm, goes to Mario Carneiro.) (Contributed by Stefan O'Rear, 29-Nov-2014.) (Revised by Jim Kingdon, 7-Oct-2023.)
|- ↾s = ( w e. _V , x e. _V |-> ( w sSet <. ( Base ` ndx ) , ( x i^i ( Base ` w ) ) >. ) )
Theorem	brstruct 13081	The structure relation is a relation. (Contributed by Mario Carneiro, 29-Aug-2015.)
|- Rel Struct
Theorem	isstruct2im 13082	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 ) ) )
Theorem	isstruct2r 13083	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 )
Theorem	structex 13084	A structure is a set. (Contributed by AV, 10-Nov-2021.)
|- ( G Struct X -> G e. _V )
Theorem	structn0fun 13085	A structure without the empty set is a function. (Contributed by AV, 13-Nov-2021.)
|- ( F Struct X -> Fun ( F \ { (/) } ) )
Theorem	isstructim 13086	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 ) ) )
Theorem	isstructr 13087	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 >. )
Theorem	structcnvcnv 13088	Two ways to express the relational part of a structure. (Contributed by Mario Carneiro, 29-Aug-2015.)
|- ( F Struct X -> `' `' F = ( F \ { (/) } ) )
Theorem	structfung 13089	The converse of the converse of a structure is a function. Closed form of structfun 13090. (Contributed by AV, 12-Nov-2021.)
|- ( F Struct X -> Fun `' `' F )
Theorem	structfun 13090	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
Theorem	structfn 13091	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 ) )
Theorem	strnfvnd 13092	Deduction version of strnfvn 13093. (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 ) )
Theorem	strnfvn 13093	Value of a structure component extractor E. Normally, E is a defined constant symbol such as Base (df-base 13078) 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 13117. (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 )
Theorem	strfvssn 13094	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 )
Theorem	ndxarg 13095	Get the numeric argument from a defined structure component extractor such as df-base 13078. (Contributed by Mario Carneiro, 6-Oct-2013.)
|- E = Slot N   &    |- N e. NN   =>    |- ( E ` ndx ) = N
Theorem	ndxid 13096	A structure component extractor is defined by its own index. This theorem, together with strslfv 13117 below, is useful for avoiding direct reference to the hard-coded numeric index in component extractor definitions, such as the 1 in df-base 13078, 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 )
Theorem	ndxslid 13097	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 13117. (Contributed by Jim Kingdon, 29-Jan-2023.)
|- E = Slot N   &    |- N e. NN   =>    |- ( E = Slot ( E ` ndx ) /\ ( E ` ndx ) e. NN )
Theorem	slotslfn 13098	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
Theorem	slotex 13099	Existence of slot value. A corollary of slotslfn 13098. (Contributed by Jim Kingdon, 12-Feb-2023.)
|- ( E = Slot ( E ` ndx ) /\ ( E ` ndx ) e. NN )   =>    |- ( A e. V -> ( E ` A ) e. _V )
Theorem	strndxid 13100	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 ) )