P. 72 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 7101-7200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	djueq1 7101	Equality theorem for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.)
|- ( A = B -> ( A ⊔ C ) = ( B ⊔ C ) )
Theorem	djueq2 7102	Equality theorem for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.)
|- ( A = B -> ( C ⊔ A ) = ( C ⊔ B ) )
Theorem	nfdju 7103	Bound-variable hypothesis builder for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/_ x ( A ⊔ B )
Theorem	djuex 7104	The disjoint union of sets is a set. See also the more precise djuss 7131. (Contributed by AV, 28-Jun-2022.)
|- ( ( A e. V /\ B e. W ) -> ( A ⊔ B ) e. _V )
Theorem	djuexb 7105	The disjoint union of two classes is a set iff both classes are sets. (Contributed by Jim Kingdon, 6-Sep-2023.)
|- ( ( A e. _V /\ B e. _V ) <-> ( A ⊔ B ) e. _V )
2.6.36.2  Left and right injections of a disjoint union In this section, we define the left and right injections of a disjoint union and prove their main properties. These injections are restrictions of the "template" functions inl and inr, which appear in most applications in the form (inl |` A ) and (inr |` B ).
Syntax	cinl 7106	Extend class notation to include left injection of a disjoint union.
class inl
Syntax	cinr 7107	Extend class notation to include right injection of a disjoint union.
class inr
Definition	df-inl 7108	Left injection of a disjoint union. (Contributed by Mario Carneiro, 21-Jun-2022.)
|- inl = ( x e. _V |-> <. (/) , x >. )
Definition	df-inr 7109	Right injection of a disjoint union. (Contributed by Mario Carneiro, 21-Jun-2022.)
|- inr = ( x e. _V |-> <. 1o , x >. )
Theorem	djulclr 7110	Left closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.) (Revised by BJ, 6-Jul-2022.)
|- ( C e. A -> ( (inl |` A ) ` C ) e. ( A ⊔ B ) )
Theorem	djurclr 7111	Right closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.) (Revised by BJ, 6-Jul-2022.)
|- ( C e. B -> ( (inr |` B ) ` C ) e. ( A ⊔ B ) )
Theorem	djulcl 7112	Left closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.)
|- ( C e. A -> (inl ` C ) e. ( A ⊔ B ) )
Theorem	djurcl 7113	Right closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.)
|- ( C e. B -> (inr ` C ) e. ( A ⊔ B ) )
Theorem	djuf1olem 7114*	Lemma for djulf1o 7119 and djurf1o 7120. (Contributed by BJ and Jim Kingdon, 4-Jul-2022.)
|- X e. _V   &    |- F = ( x e. A |-> <. X , x >. )   =>    |- F : A -1-1-onto-> ( { X } X. A )
Theorem	djuf1olemr 7115*	Lemma for djulf1or 7117 and djurf1or 7118. For a version of this lemma with F defined on A and no restriction in the conclusion, see djuf1olem 7114. (Contributed by BJ and Jim Kingdon, 4-Jul-2022.)
|- X e. _V   &    |- F = ( x e. _V |-> <. X , x >. )   =>    |- ( F |` A ) : A -1-1-onto-> ( { X } X. A )
Theorem	djulclb 7116	Left biconditional closure of disjoint union. (Contributed by Jim Kingdon, 2-Jul-2022.)
|- ( C e. V -> ( C e. A <-> (inl ` C ) e. ( A ⊔ B ) ) )
Theorem	djulf1or 7117	The left injection function on all sets is one to one and onto. (Contributed by BJ and Jim Kingdon, 22-Jun-2022.)
|- (inl |` A ) : A -1-1-onto-> ( { (/) } X. A )
Theorem	djurf1or 7118	The right injection function on all sets is one to one and onto. (Contributed by BJ and Jim Kingdon, 22-Jun-2022.)
|- (inr |` A ) : A -1-1-onto-> ( { 1o } X. A )
Theorem	djulf1o 7119	The left injection function on all sets is one to one and onto. (Contributed by Jim Kingdon, 22-Jun-2022.)
|- inl : _V -1-1-onto-> ( { (/) } X. _V )
Theorem	djurf1o 7120	The right injection function on all sets is one to one and onto. (Contributed by Jim Kingdon, 22-Jun-2022.)
|- inr : _V -1-1-onto-> ( { 1o } X. _V )
Theorem	inresflem 7121*	Lemma for inlresf1 7122 and inrresf1 7123. (Contributed by BJ, 4-Jul-2022.)
|- F : A -1-1-onto-> ( { X } X. A )   &    |- ( x e. A -> ( F ` x ) e. B )   =>    |- F : A -1-1-> B
Theorem	inlresf1 7122	The left injection restricted to the left class of a disjoint union is an injective function from the left class into the disjoint union. (Contributed by AV, 28-Jun-2022.)
|- (inl |` A ) : A -1-1-> ( A ⊔ B )
Theorem	inrresf1 7123	The right injection restricted to the right class of a disjoint union is an injective function from the right class into the disjoint union. (Contributed by AV, 28-Jun-2022.)
|- (inr |` B ) : B -1-1-> ( A ⊔ B )
Theorem	djuinr 7124	The ranges of any left and right injections are disjoint. Remark: the extra generality offered by the two restrictions makes the theorem more readily usable (e.g., by djudom 7154 and djufun 7165) while the simpler statement |- ( ran inl i^i ran inr ) = (/) is easily recovered from it by substituting _V for both A and B as done in casefun 7146). (Contributed by BJ and Jim Kingdon, 21-Jun-2022.)
|- ( ran (inl |` A ) i^i ran (inr |` B ) ) = (/)
Theorem	djuin 7125	The images of any classes under right and left injection produce disjoint sets. (Contributed by Jim Kingdon, 21-Jun-2022.) (Proof shortened by BJ, 9-Jul-2023.)
|- ( (inl " A ) i^i (inr " B ) ) = (/)
Theorem	inl11 7126	Left injection is one-to-one. (Contributed by Jim Kingdon, 12-Jul-2023.)
|- ( ( A e. V /\ B e. W ) -> ( (inl ` A ) = (inl ` B ) <-> A = B ) )
Theorem	djuunr 7127	The disjoint union of two classes is the union of the images of those two classes under right and left injection. (Contributed by Jim Kingdon, 22-Jun-2022.) (Proof shortened by BJ, 6-Jul-2022.)
|- ( ran (inl |` A ) u. ran (inr |` B ) ) = ( A ⊔ B )
Theorem	djuun 7128	The disjoint union of two classes is the union of the images of those two classes under right and left injection. (Contributed by Jim Kingdon, 22-Jun-2022.) (Proof shortened by BJ, 9-Jul-2023.)
|- ( (inl " A ) u. (inr " B ) ) = ( A ⊔ B )
Theorem	eldju 7129*	Element of a disjoint union. (Contributed by BJ and Jim Kingdon, 23-Jun-2022.)
|- ( C e. ( A ⊔ B ) <-> ( E. x e. A C = ( (inl |` A ) ` x ) \/ E. x e. B C = ( (inr |` B ) ` x ) ) )
Theorem	djur 7130*	A member of a disjoint union can be mapped from one of the classes which produced it. (Contributed by Jim Kingdon, 23-Jun-2022.) Upgrade implication to biconditional and shorten proof. (Revised by BJ, 14-Jul-2023.)
|- ( C e. ( A ⊔ B ) <-> ( E. x e. A C = (inl ` x ) \/ E. x e. B C = (inr ` x ) ) )
2.6.36.3  Universal property of the disjoint union
Theorem	djuss 7131	A disjoint union is a subset of a Cartesian product. (Contributed by AV, 25-Jun-2022.)
|- ( A ⊔ B ) C_ ( { (/) , 1o } X. ( A u. B ) )
Theorem	eldju1st 7132	The first component of an element of a disjoint union is either (/) or 1o. (Contributed by AV, 26-Jun-2022.)
|- ( X e. ( A ⊔ B ) -> ( ( 1st ` X ) = (/) \/ ( 1st ` X ) = 1o ) )
Theorem	eldju2ndl 7133	The second component of an element of a disjoint union is an element of the left class of the disjoint union if its first component is the empty set. (Contributed by AV, 26-Jun-2022.)
|- ( ( X e. ( A ⊔ B ) /\ ( 1st ` X ) = (/) ) -> ( 2nd ` X ) e. A )
Theorem	eldju2ndr 7134	The second component of an element of a disjoint union is an element of the right class of the disjoint union if its first component is not the empty set. (Contributed by AV, 26-Jun-2022.)
|- ( ( X e. ( A ⊔ B ) /\ ( 1st ` X ) =/= (/) ) -> ( 2nd ` X ) e. B )
Theorem	1stinl 7135	The first component of the value of a left injection is the empty set. (Contributed by AV, 27-Jun-2022.)
|- ( X e. V -> ( 1st ` (inl ` X ) ) = (/) )
Theorem	2ndinl 7136	The second component of the value of a left injection is its argument. (Contributed by AV, 27-Jun-2022.)
|- ( X e. V -> ( 2nd ` (inl ` X ) ) = X )
Theorem	1stinr 7137	The first component of the value of a right injection is 1o. (Contributed by AV, 27-Jun-2022.)
|- ( X e. V -> ( 1st ` (inr ` X ) ) = 1o )
Theorem	2ndinr 7138	The second component of the value of a right injection is its argument. (Contributed by AV, 27-Jun-2022.)
|- ( X e. V -> ( 2nd ` (inr ` X ) ) = X )
Theorem	djune 7139	Left and right injection never produce equal values. (Contributed by Jim Kingdon, 2-Jul-2022.)
|- ( ( A e. V /\ B e. W ) -> (inl ` A ) =/= (inr ` B ) )
Theorem	updjudhf 7140*	The mapping of an element of the disjoint union to the value of the corresponding function is a function. (Contributed by AV, 26-Jun-2022.)
|- ( ph -> F : A --> C )   &    |- ( ph -> G : B --> C )   &    |- H = ( x e. ( A ⊔ B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) )   =>    |- ( ph -> H : ( A ⊔ B ) --> C )
Theorem	updjudhcoinlf 7141*	The composition of the mapping of an element of the disjoint union to the value of the corresponding function and the left injection equals the first function. (Contributed by AV, 27-Jun-2022.)
|- ( ph -> F : A --> C )   &    |- ( ph -> G : B --> C )   &    |- H = ( x e. ( A ⊔ B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) )   =>    |- ( ph -> ( H o. (inl |` A ) ) = F )
Theorem	updjudhcoinrg 7142*	The composition of the mapping of an element of the disjoint union to the value of the corresponding function and the right injection equals the second function. (Contributed by AV, 27-Jun-2022.)
|- ( ph -> F : A --> C )   &    |- ( ph -> G : B --> C )   &    |- H = ( x e. ( A ⊔ B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) )   =>    |- ( ph -> ( H o. (inr |` B ) ) = G )
Theorem	updjud 7143*	Universal property of the disjoint union. (Proposed by BJ, 25-Jun-2022.) (Contributed by AV, 28-Jun-2022.)
|- ( ph -> F : A --> C )   &    |- ( ph -> G : B --> C )   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. W )   =>    |- ( ph -> E! h ( h : ( A ⊔ B ) --> C /\ ( h o. (inl |` A ) ) = F /\ ( h o. (inr |` B ) ) = G ) )
Syntax	cdjucase 7144	Syntax for the "case" construction.
class case ( R , S )
Definition	df-case 7145	The "case" construction: if F : A --> X and G : B --> X are functions, then case ( F , G ) : ( A ⊔ B ) --> X is the natural function obtained by a definition by cases, hence the name. It is the unique function whose existence is asserted by the universal property of disjoint unions updjud 7143. The definition is adapted to make sense also for binary relations (where the universal property also holds). (Contributed by MC and BJ, 10-Jul-2022.)
|- case ( R , S ) = ( ( R o. `'inl ) u. ( S o. `'inr ) )
Theorem	casefun 7146	The "case" construction of two functions is a function. (Contributed by BJ, 10-Jul-2022.)
|- ( ph -> Fun F )   &    |- ( ph -> Fun G )   =>    |- ( ph -> Fun case ( F , G ) )
Theorem	casedm 7147	The domain of the "case" construction is the disjoint union of the domains. TODO (although less important): |- ran case ( F , G ) = ( ran F u. ran G ). (Contributed by BJ, 10-Jul-2022.)
|- dom case ( F , G ) = ( dom F ⊔ dom G )
Theorem	caserel 7148	The "case" construction of two relations is a relation, with bounds on its domain and codomain. Typically, the "case" construction is used when both relations have a common codomain. (Contributed by BJ, 10-Jul-2022.)
|- case ( R , S ) C_ ( ( dom R ⊔ dom S ) X. ( ran R u. ran S ) )
Theorem	casef 7149	The "case" construction of two functions is a function on the disjoint union of their domains. (Contributed by BJ, 10-Jul-2022.)
|- ( ph -> F : A --> X )   &    |- ( ph -> G : B --> X )   =>    |- ( ph -> case ( F , G ) : ( A ⊔ B ) --> X )
Theorem	caseinj 7150	The "case" construction of two injective relations with disjoint ranges is an injective relation. (Contributed by BJ, 10-Jul-2022.)
|- ( ph -> Fun `' R )   &    |- ( ph -> Fun `' S )   &    |- ( ph -> ( ran R i^i ran S ) = (/) )   =>    |- ( ph -> Fun `'case ( R , S ) )
Theorem	casef1 7151	The "case" construction of two injective functions with disjoint ranges is an injective function. (Contributed by BJ, 10-Jul-2022.)
|- ( ph -> F : A -1-1-> X )   &    |- ( ph -> G : B -1-1-> X )   &    |- ( ph -> ( ran F i^i ran G ) = (/) )   =>    |- ( ph -> case ( F , G ) : ( A ⊔ B ) -1-1-> X )
Theorem	caseinl 7152	Applying the "case" construction to a left injection. (Contributed by Jim Kingdon, 15-Mar-2023.)
|- ( ph -> F Fn B )   &    |- ( ph -> Fun G )   &    |- ( ph -> A e. B )   =>    |- ( ph -> (case ( F , G ) ` (inl ` A ) ) = ( F ` A ) )
Theorem	caseinr 7153	Applying the "case" construction to a right injection. (Contributed by Jim Kingdon, 12-Jul-2023.)
|- ( ph -> Fun F )   &    |- ( ph -> G Fn B )   &    |- ( ph -> A e. B )   =>    |- ( ph -> (case ( F , G ) ` (inr ` A ) ) = ( G ` A ) )
2.6.36.4  Dominance and equinumerosity properties of disjoint union
Theorem	djudom 7154	Dominance law for disjoint union. (Contributed by Jim Kingdon, 25-Jul-2022.)
|- ( ( A ~<_ B /\ C ~<_ D ) -> ( A ⊔ C ) ~<_ ( B ⊔ D ) )
Theorem	omp1eomlem 7155*	Lemma for omp1eom 7156. (Contributed by Jim Kingdon, 11-Jul-2023.)
|- F = ( x e. om |-> if ( x = (/) , (inr ` x ) , (inl ` U. x ) ) )   &    |- S = ( x e. om |-> suc x )   &    |- G = case ( S , ( _I |` 1o ) )   =>    |- F : om -1-1-onto-> ( om ⊔ 1o )
Theorem	omp1eom 7156	Adding one to om. (Contributed by Jim Kingdon, 10-Jul-2023.)
|- ( om ⊔ 1o ) ~~ om
Theorem	endjusym 7157	Reversing right and left operands of a disjoint union produces an equinumerous result. (Contributed by Jim Kingdon, 10-Jul-2023.)
|- ( ( A e. V /\ B e. W ) -> ( A ⊔ B ) ~~ ( B ⊔ A ) )
Theorem	eninl 7158	Equinumerosity of a set and its image under left injection. (Contributed by Jim Kingdon, 30-Jul-2023.)
|- ( A e. V -> (inl " A ) ~~ A )
Theorem	eninr 7159	Equinumerosity of a set and its image under right injection. (Contributed by Jim Kingdon, 30-Jul-2023.)
|- ( A e. V -> (inr " A ) ~~ A )
Theorem	difinfsnlem 7160*	Lemma for difinfsn 7161. The case where we need to swap B and (inr ` (/) ) in building the mapping G. (Contributed by Jim Kingdon, 9-Aug-2023.)
|- ( ph -> A. x e. A A. y e. A DECID x = y )   &    |- ( ph -> B e. A )   &    |- ( ph -> F : ( om ⊔ 1o ) -1-1-> A )   &    |- ( ph -> ( F ` (inr ` (/) ) ) =/= B )   &    |- G = ( n e. om |-> if ( ( F ` (inl ` n ) ) = B , ( F ` (inr ` (/) ) ) , ( F ` (inl ` n ) ) ) )   =>    |- ( ph -> G : om -1-1-> ( A \ { B } ) )
Theorem	difinfsn 7161*	An infinite set minus one element is infinite. We require that the set has decidable equality. (Contributed by Jim Kingdon, 8-Aug-2023.)
|- ( ( A. x e. A A. y e. A DECID x = y /\ om ~<_ A /\ B e. A ) -> om ~<_ ( A \ { B } ) )
Theorem	difinfinf 7162*	An infinite set minus a finite subset is infinite. We require that the set has decidable equality. (Contributed by Jim Kingdon, 8-Aug-2023.)
|- ( ( ( A. x e. A A. y e. A DECID x = y /\ om ~<_ A ) /\ ( B C_ A /\ B e. Fin ) ) -> om ~<_ ( A \ B ) )
2.6.36.5  Older definition temporarily kept for comparison, to be deleted
Syntax	cdjud 7163	Syntax for the domain-disjoint-union of two relations.
class ( R ⊔d S )
Definition	df-djud 7164	The "domain-disjoint-union" of two relations: if R C_ ( A X. X ) and S C_ ( B X. X ) are two binary relations, then ( R ⊔d S ) is the binary relation from ( A ⊔ B ) to X having the universal property of disjoint unions (see updjud 7143 in the case of functions). Remark: the restrictions to dom R (resp. dom S) are not necessary since extra stuff would be thrown away in the post-composition with R (resp. S), as in df-case 7145, but they are explicitly written for clarity. (Contributed by MC and BJ, 10-Jul-2022.)
|- ( R ⊔d S ) = ( ( R o. `' (inl |` dom R ) ) u. ( S o. `' (inr |` dom S ) ) )
Theorem	djufun 7165	The "domain-disjoint-union" of two functions is a function. (Contributed by BJ, 10-Jul-2022.)
|- ( ph -> Fun F )   &    |- ( ph -> Fun G )   =>    |- ( ph -> Fun ( F ⊔d G ) )
Theorem	djudm 7166	The domain of the "domain-disjoint-union" is the disjoint union of the domains. Remark: its range is the (standard) union of the ranges. (Contributed by BJ, 10-Jul-2022.)
|- dom ( F ⊔d G ) = ( dom F ⊔ dom G )
Theorem	djuinj 7167	The "domain-disjoint-union" of two injective relations with disjoint ranges is an injective relation. (Contributed by BJ, 10-Jul-2022.)
|- ( ph -> Fun `' R )   &    |- ( ph -> Fun `' S )   &    |- ( ph -> ( ran R i^i ran S ) = (/) )   =>    |- ( ph -> Fun `' ( R ⊔d S ) )
2.6.36.6  Countable sets
Theorem	0ct 7168	The empty set is countable. Remark of [BauerSwan], p. 14:3 which also has the definition of countable used here. (Contributed by Jim Kingdon, 13-Mar-2023.)
|- E. f f : om -onto-> ( (/) ⊔ 1o )
Theorem	ctmlemr 7169*	Lemma for ctm 7170. One of the directions of the biconditional. (Contributed by Jim Kingdon, 16-Mar-2023.)
|- ( E. x x e. A -> ( E. f f : om -onto-> A -> E. f f : om -onto-> ( A ⊔ 1o ) ) )
Theorem	ctm 7170*	Two equivalent definitions of countable for an inhabited set. Remark of [BauerSwan], p. 14:3. (Contributed by Jim Kingdon, 13-Mar-2023.)
|- ( E. x x e. A -> ( E. f f : om -onto-> ( A ⊔ 1o ) <-> E. f f : om -onto-> A ) )
Theorem	ctssdclemn0 7171*	Lemma for ctssdc 7174. The -. (/) e. S case. (Contributed by Jim Kingdon, 16-Aug-2023.)
|- ( ph -> S C_ om )   &    |- ( ph -> A. n e. om DECID n e. S )   &    |- ( ph -> F : S -onto-> A )   &    |- ( ph -> -. (/) e. S )   =>    |- ( ph -> E. g g : om -onto-> ( A ⊔ 1o ) )
Theorem	ctssdccl 7172*	A mapping from a decidable subset of the natural numbers onto a countable set. This is similar to one direction of ctssdc 7174 but expressed in terms of classes rather than E.. (Contributed by Jim Kingdon, 30-Oct-2023.)
|- ( ph -> F : om -onto-> ( A ⊔ 1o ) )   &    |- S = { x e. om | ( F ` x ) e. (inl " A ) }   &    |- G = ( `'inl o. F )   =>    |- ( ph -> ( S C_ om /\ G : S -onto-> A /\ A. n e. om DECID n e. S ) )
Theorem	ctssdclemr 7173*	Lemma for ctssdc 7174. Showing that our usual definition of countable implies the alternate one. (Contributed by Jim Kingdon, 16-Aug-2023.)
|- ( E. f f : om -onto-> ( A ⊔ 1o ) -> E. s ( s C_ om /\ E. f f : s -onto-> A /\ A. n e. om DECID n e. s ) )
Theorem	ctssdc 7174*	A set is countable iff there is a surjection from a decidable subset of the natural numbers onto it. The decidability condition is needed as shown at ctssexmid 7211. (Contributed by Jim Kingdon, 15-Aug-2023.)
|- ( E. s ( s C_ om /\ E. f f : s -onto-> A /\ A. n e. om DECID n e. s ) <-> E. f f : om -onto-> ( A ⊔ 1o ) )
Theorem	enumctlemm 7175*	Lemma for enumct 7176. The case where N is greater than zero. (Contributed by Jim Kingdon, 13-Mar-2023.)
|- ( ph -> F : N -onto-> A )   &    |- ( ph -> N e. om )   &    |- ( ph -> (/) e. N )   &    |- G = ( k e. om |-> if ( k e. N , ( F ` k ) , ( F ` (/) ) ) )   =>    |- ( ph -> G : om -onto-> A )
Theorem	enumct 7176*	A finitely enumerable set is countable. Lemma 8.1.14 of [AczelRathjen], p. 73 (except that our definition of countable does not require the set to be inhabited). "Finitely enumerable" is defined as E. n e. om E. f f : n -onto-> A per Definition 8.1.4 of [AczelRathjen], p. 71 and "countable" is defined as E. g g : om -onto-> ( A ⊔ 1o ) per [BauerSwan], p. 14:3. (Contributed by Jim Kingdon, 13-Mar-2023.)
|- ( E. n e. om E. f f : n -onto-> A -> E. g g : om -onto-> ( A ⊔ 1o ) )
Theorem	finct 7177*	A finite set is countable. (Contributed by Jim Kingdon, 17-Mar-2023.)
|- ( A e. Fin -> E. g g : om -onto-> ( A ⊔ 1o ) )
Theorem	omct 7178	om is countable. (Contributed by Jim Kingdon, 23-Dec-2023.)
|- E. f f : om -onto-> ( om ⊔ 1o )
Theorem	ctfoex 7179*	A countable class is a set. (Contributed by Jim Kingdon, 25-Dec-2023.)
|- ( E. f f : om -onto-> ( A ⊔ 1o ) -> A e. _V )
2.6.37  The one-point compactification of the natural numbers This section introduces the one-point compactification of the set of natural numbers, introduced by Escardo as the set of nonincreasing sequences on om with values in 2o. The topological results justifying its name will be proved later.
Syntax	xnninf 7180	Set of nonincreasing sequences in 2o ^m om.
class ℕ∞
Definition	df-nninf 7181*	Define the set of nonincreasing sequences in 2o ^m om. Definition in Section 3.1 of [Pierik], p. 15. If we assumed excluded middle, this would be essentially the same as NN0* as defined at df-xnn0 9307 but in its absence the relationship between the two is more complicated. This definition would function much the same whether we used om or NN0, but the former allows us to take advantage of 2o = { (/) , 1o } (df2o3 6485) so we adopt it. (Contributed by Jim Kingdon, 14-Jul-2022.)
|- ℕ∞ = { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }
Theorem	nninfex 7182	ℕ∞ is a set. (Contributed by Jim Kingdon, 10-Aug-2022.)
|- ℕ∞ e. _V
Theorem	nninff 7183	An element of ℕ∞ is a sequence of zeroes and ones. (Contributed by Jim Kingdon, 4-Aug-2022.)
|- ( A e. ℕ∞ -> A : om --> 2o )
Theorem	nninfninc 7184	All values beyond a zero in an ℕ∞ sequence are zero. This is another way of stating that elements of ℕ∞ are nonincreasing. (Contributed by Jim Kingdon, 12-Jul-2025.)
|- ( ph -> A e. ℕ∞ )   &    |- ( ph -> X e. om )   &    |- ( ph -> Y e. om )   &    |- ( ph -> X C_ Y )   &    |- ( ph -> ( A ` X ) = (/) )   =>    |- ( ph -> ( A ` Y ) = (/) )
Theorem	infnninf 7185	The point at infinity in ℕ∞ is the constant sequence equal to 1o. Note that with our encoding of functions, that constant function can also be expressed as ( om X. { 1o } ), as fconstmpt 4707 shows. (Contributed by Jim Kingdon, 14-Jul-2022.) Use maps-to notation. (Revised by BJ, 10-Aug-2024.)
|- ( i e. om |-> 1o ) e. ℕ∞
Theorem	infnninfOLD 7186	Obsolete version of infnninf 7185 as of 10-Aug-2024. (Contributed by Jim Kingdon, 14-Jul-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( om X. { 1o } ) e. ℕ∞
Theorem	nnnninf 7187*	Elements of ℕ∞ corresponding to natural numbers. The natural number N corresponds to a sequence of N ones followed by zeroes. This can be strengthened to include infinity, see nnnninf2 7188. (Contributed by Jim Kingdon, 14-Jul-2022.)
|- ( N e. om -> ( i e. om |-> if ( i e. N , 1o , (/) ) ) e. ℕ∞ )
Theorem	nnnninf2 7188*	Canonical embedding of suc om into ℕ∞. (Contributed by BJ, 10-Aug-2024.)
|- ( N e. suc om -> ( i e. om |-> if ( i e. N , 1o , (/) ) ) e. ℕ∞ )
Theorem	nnnninfeq 7189*	Mapping of a natural number to an element of ℕ∞. (Contributed by Jim Kingdon, 4-Aug-2022.)
|- ( ph -> P e. ℕ∞ )   &    |- ( ph -> N e. om )   &    |- ( ph -> A. x e. N ( P ` x ) = 1o )   &    |- ( ph -> ( P ` N ) = (/) )   =>    |- ( ph -> P = ( i e. om |-> if ( i e. N , 1o , (/) ) ) )
Theorem	nnnninfeq2 7190*	Mapping of a natural number to an element of ℕ∞. Similar to nnnninfeq 7189 but if we have information about a single 1o digit, that gives information about all previous digits. (Contributed by Jim Kingdon, 4-Aug-2022.)
|- ( ph -> P e. ℕ∞ )   &    |- ( ph -> N e. om )   &    |- ( ph -> ( P ` U. N ) = 1o )   &    |- ( ph -> ( P ` N ) = (/) )   =>    |- ( ph -> P = ( i e. om |-> if ( i e. N , 1o , (/) ) ) )
Theorem	nninfisollem0 7191*	Lemma for nninfisol 7194. The case where N is zero. (Contributed by Jim Kingdon, 13-Sep-2024.)
|- ( ph -> X e. ℕ∞ )   &    |- ( ph -> ( X ` N ) = (/) )   &    |- ( ph -> N e. om )   &    |- ( ph -> N = (/) )   =>    |- ( ph -> DECID ( i e. om |-> if ( i e. N , 1o , (/) ) ) = X )
Theorem	nninfisollemne 7192*	Lemma for nninfisol 7194. A case where N is a successor and N and X are not equal. (Contributed by Jim Kingdon, 13-Sep-2024.)
|- ( ph -> X e. ℕ∞ )   &    |- ( ph -> ( X ` N ) = (/) )   &    |- ( ph -> N e. om )   &    |- ( ph -> N =/= (/) )   &    |- ( ph -> ( X ` U. N ) = (/) )   =>    |- ( ph -> DECID ( i e. om |-> if ( i e. N , 1o , (/) ) ) = X )
Theorem	nninfisollemeq 7193*	Lemma for nninfisol 7194. The case where N is a successor and N and X are equal. (Contributed by Jim Kingdon, 13-Sep-2024.)
|- ( ph -> X e. ℕ∞ )   &    |- ( ph -> ( X ` N ) = (/) )   &    |- ( ph -> N e. om )   &    |- ( ph -> N =/= (/) )   &    |- ( ph -> ( X ` U. N ) = 1o )   =>    |- ( ph -> DECID ( i e. om |-> if ( i e. N , 1o , (/) ) ) = X )
Theorem	nninfisol 7194*	Finite elements of ℕ∞ are isolated. That is, given a natural number and any element of ℕ∞, it is decidable whether the natural number (when converted to an element of ℕ∞) is equal to the given element of ℕ∞. Stated in an online post by Martin Escardo. One way to understand this theorem is that you do not need to look at an unbounded number of elements of the sequence X to decide whether it is equal to N (in fact, you only need to look at two elements and N tells you where to look). (Contributed by BJ and Jim Kingdon, 12-Sep-2024.)
|- ( ( N e. om /\ X e. ℕ∞ ) -> DECID ( i e. om |-> if ( i e. N , 1o , (/) ) ) = X )
2.6.38  Omniscient sets
Syntax	comni 7195	Extend class definition to include the class of omniscient sets.
class Omni
Definition	df-omni 7196*	An omniscient set is one where we can decide whether a predicate (here represented by a function f) holds (is equal to 1o) for all elements or fails to hold (is equal to (/)) for some element. Definition 3.1 of [Pierik], p. 14. In particular, om e. Omni is known as the Limited Principle of Omniscience (LPO). (Contributed by Jim Kingdon, 28-Jun-2022.)
|- Omni = { y | A. f ( f : y --> 2o -> ( E. x e. y ( f ` x ) = (/) \/ A. x e. y ( f ` x ) = 1o ) ) }
Theorem	isomni 7197*	The predicate of being omniscient. (Contributed by Jim Kingdon, 28-Jun-2022.)
|- ( A e. V -> ( A e. Omni <-> A. f ( f : A --> 2o -> ( E. x e. A ( f ` x ) = (/) \/ A. x e. A ( f ` x ) = 1o ) ) ) )
Theorem	isomnimap 7198*	The predicate of being omniscient stated in terms of set exponentiation. (Contributed by Jim Kingdon, 13-Jul-2022.)
|- ( A e. V -> ( A e. Omni <-> A. f e. ( 2o ^m A ) ( E. x e. A ( f ` x ) = (/) \/ A. x e. A ( f ` x ) = 1o ) ) )
Theorem	enomnilem 7199	Lemma for enomni 7200. One direction of the biconditional. (Contributed by Jim Kingdon, 13-Jul-2022.)
|- ( A ~~ B -> ( A e. Omni -> B e. Omni ) )
Theorem	enomni 7200	Omniscience is invariant with respect to equinumerosity. For example, this means that we can express the Limited Principle of Omniscience as either om e. Omni or NN0 e. Omni. The former is a better match to conventional notation in the sense that df2o3 6485 says that 2o = { (/) , 1o } whereas the corresponding relationship does not exist between 2 and { 0 , 1 }. (Contributed by Jim Kingdon, 13-Jul-2022.)
|- ( A ~~ B -> ( A e. Omni <-> B e. Omni ) )