P. 73 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 7201-7300   *Has distinct variable group(s)

Type	Label	Description
Statement
Definition	df-case 7201	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 7199. 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 7202	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 7203	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 7204	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 7205	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 7206	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 7207	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 7208	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 7209	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 7210	Dominance law for disjoint union. (Contributed by Jim Kingdon, 25-Jul-2022.)
|- ( ( A ~<_ B /\ C ~<_ D ) -> ( A ⊔ C ) ~<_ ( B ⊔ D ) )
Theorem	omp1eomlem 7211*	Lemma for omp1eom 7212. (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 7212	Adding one to om. (Contributed by Jim Kingdon, 10-Jul-2023.)
|- ( om ⊔ 1o ) ~~ om
Theorem	endjusym 7213	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 7214	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 7215	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 7216*	Lemma for difinfsn 7217. 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 7217*	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 7218*	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 7219	Syntax for the domain-disjoint-union of two relations.
class ( R ⊔d S )
Definition	df-djud 7220	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 7199 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 7201, 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 7221	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 7222	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 7223	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 7224	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 7225*	Lemma for ctm 7226. 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 7226*	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 7227*	Lemma for ctssdc 7230. 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 7228*	A mapping from a decidable subset of the natural numbers onto a countable set. This is similar to one direction of ctssdc 7230 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 7229*	Lemma for ctssdc 7230. 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 7230*	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 7267. (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 7231*	Lemma for enumct 7232. 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 7232*	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 7233*	A finite set is countable. (Contributed by Jim Kingdon, 17-Mar-2023.)
|- ( A e. Fin -> E. g g : om -onto-> ( A ⊔ 1o ) )
Theorem	omct 7234	om is countable. (Contributed by Jim Kingdon, 23-Dec-2023.)
|- E. f f : om -onto-> ( om ⊔ 1o )
Theorem	ctfoex 7235*	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 7236	Set of nonincreasing sequences in 2o ^m om.
class ℕ∞
Definition	df-nninf 7237*	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 9379 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 6529) 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 7238	ℕ∞ is a set. (Contributed by Jim Kingdon, 10-Aug-2022.)
|- ℕ∞ e. _V
Theorem	nninff 7239	An element of ℕ∞ is a sequence of zeroes and ones. (Contributed by Jim Kingdon, 4-Aug-2022.)
|- ( A e. ℕ∞ -> A : om --> 2o )
Theorem	nninfninc 7240	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 7241	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 4730 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 7242	Obsolete version of infnninf 7241 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 7243*	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 7244. (Contributed by Jim Kingdon, 14-Jul-2022.)
|- ( N e. om -> ( i e. om |-> if ( i e. N , 1o , (/) ) ) e. ℕ∞ )
Theorem	nnnninf2 7244*	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 7245*	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 7246*	Mapping of a natural number to an element of ℕ∞. Similar to nnnninfeq 7245 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 7247*	Lemma for nninfisol 7250. 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 7248*	Lemma for nninfisol 7250. 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 7249*	Lemma for nninfisol 7250. 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 7250*	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). By contrast, the point at infinity being isolated is equivalent to the Weak Limited Principle of Omniscience (WLPO) (nninfinfwlpo 7297). (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 7251	Extend class definition to include the class of omniscient sets.
class Omni
Definition	df-omni 7252*	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 7253*	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 7254*	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 7255	Lemma for enomni 7256. One direction of the biconditional. (Contributed by Jim Kingdon, 13-Jul-2022.)
|- ( A ~~ B -> ( A e. Omni -> B e. Omni ) )
Theorem	enomni 7256	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 6529 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 ) )
Theorem	finomni 7257	A finite set is omniscient. Remark right after Definition 3.1 of [Pierik], p. 14. (Contributed by Jim Kingdon, 28-Jun-2022.)
|- ( A e. Fin -> A e. Omni )
Theorem	exmidomniim 7258	Given excluded middle, every set is omniscient. Remark following Definition 3.1 of [Pierik], p. 14. This is one direction of the biconditional exmidomni 7259. (Contributed by Jim Kingdon, 29-Jun-2022.)
|- (EXMID -> A. x x e. Omni )
Theorem	exmidomni 7259	Excluded middle is equivalent to every set being omniscient. (Contributed by BJ and Jim Kingdon, 30-Jun-2022.)
|- (EXMID <-> A. x x e. Omni )
Theorem	exmidlpo 7260	Excluded middle implies the Limited Principle of Omniscience (LPO). (Contributed by Jim Kingdon, 29-Mar-2023.)
|- (EXMID -> om e. Omni )
Theorem	fodjuomnilemdc 7261*	Lemma for fodjuomni 7266. Decidability of a condition we use in various lemmas. (Contributed by Jim Kingdon, 27-Jul-2022.)
|- ( ph -> F : O -onto-> ( A ⊔ B ) )   =>    |- ( ( ph /\ X e. O ) -> DECID E. z e. A ( F ` X ) = (inl ` z ) )
Theorem	fodjuf 7262*	Lemma for fodjuomni 7266 and fodjumkv 7277. Domain and range of P. (Contributed by Jim Kingdon, 27-Jul-2022.) (Revised by Jim Kingdon, 25-Mar-2023.)
|- ( ph -> F : O -onto-> ( A ⊔ B ) )   &    |- P = ( y e. O |-> if ( E. z e. A ( F ` y ) = (inl ` z ) , (/) , 1o ) )   &    |- ( ph -> O e. V )   =>    |- ( ph -> P e. ( 2o ^m O ) )
Theorem	fodjum 7263*	Lemma for fodjuomni 7266 and fodjumkv 7277. A condition which shows that A is inhabited. (Contributed by Jim Kingdon, 27-Jul-2022.) (Revised by Jim Kingdon, 25-Mar-2023.)
|- ( ph -> F : O -onto-> ( A ⊔ B ) )   &    |- P = ( y e. O |-> if ( E. z e. A ( F ` y ) = (inl ` z ) , (/) , 1o ) )   &    |- ( ph -> E. w e. O ( P ` w ) = (/) )   =>    |- ( ph -> E. x x e. A )
Theorem	fodju0 7264*	Lemma for fodjuomni 7266 and fodjumkv 7277. A condition which shows that A is empty. (Contributed by Jim Kingdon, 27-Jul-2022.) (Revised by Jim Kingdon, 25-Mar-2023.)
|- ( ph -> F : O -onto-> ( A ⊔ B ) )   &    |- P = ( y e. O |-> if ( E. z e. A ( F ` y ) = (inl ` z ) , (/) , 1o ) )   &    |- ( ph -> A. w e. O ( P ` w ) = 1o )   =>    |- ( ph -> A = (/) )
Theorem	fodjuomnilemres 7265*	Lemma for fodjuomni 7266. The final result with P expressed as a local definition. (Contributed by Jim Kingdon, 29-Jul-2022.)
|- ( ph -> O e. Omni )   &    |- ( ph -> F : O -onto-> ( A ⊔ B ) )   &    |- P = ( y e. O |-> if ( E. z e. A ( F ` y ) = (inl ` z ) , (/) , 1o ) )   =>    |- ( ph -> ( E. x x e. A \/ A = (/) ) )
Theorem	fodjuomni 7266*	A condition which ensures A is either inhabited or empty. Lemma 3.2 of [PradicBrown2022], p. 4. (Contributed by Jim Kingdon, 27-Jul-2022.)
|- ( ph -> O e. Omni )   &    |- ( ph -> F : O -onto-> ( A ⊔ B ) )   =>    |- ( ph -> ( E. x x e. A \/ A = (/) ) )
Theorem	ctssexmid 7267*	The decidability condition in ctssdc 7230 is needed. More specifically, ctssdc 7230 minus that condition, plus the Limited Principle of Omniscience (LPO), implies excluded middle. (Contributed by Jim Kingdon, 15-Aug-2023.)
|- ( ( y C_ om /\ E. f f : y -onto-> x ) -> E. f f : om -onto-> ( x ⊔ 1o ) )   &    |- om e. Omni   =>    |- ( ph \/ -. ph )
2.6.39  Markov's principle
Syntax	cmarkov 7268	Extend class definition to include the class of Markov sets.
class Markov
Definition	df-markov 7269*	A Markov set is one where if a predicate (here represented by a function f) on that set does not hold (where hold means is equal to 1o) for all elements, then there exists an element where it fails (is equal to (/)). Generalization of definition 2.5 of [Pierik], p. 9. In particular, om e. Markov is known as Markov's Principle (MP). (Contributed by Jim Kingdon, 18-Mar-2023.)
|- Markov = { y | A. f ( f : y --> 2o -> ( -. A. x e. y ( f ` x ) = 1o -> E. x e. y ( f ` x ) = (/) ) ) }
Theorem	ismkv 7270*	The predicate of being Markov. (Contributed by Jim Kingdon, 18-Mar-2023.)
|- ( A e. V -> ( A e. Markov <-> A. f ( f : A --> 2o -> ( -. A. x e. A ( f ` x ) = 1o -> E. x e. A ( f ` x ) = (/) ) ) ) )
Theorem	ismkvmap 7271*	The predicate of being Markov stated in terms of set exponentiation. (Contributed by Jim Kingdon, 18-Mar-2023.)
|- ( A e. V -> ( A e. Markov <-> A. f e. ( 2o ^m A ) ( -. A. x e. A ( f ` x ) = 1o -> E. x e. A ( f ` x ) = (/) ) ) )
Theorem	ismkvnex 7272*	The predicate of being Markov stated in terms of double negation and comparison with 1o. (Contributed by Jim Kingdon, 29-Nov-2023.)
|- ( A e. V -> ( A e. Markov <-> A. f e. ( 2o ^m A ) ( -. -. E. x e. A ( f ` x ) = 1o -> E. x e. A ( f ` x ) = 1o ) ) )
Theorem	omnimkv 7273	An omniscient set is Markov. In particular, the case where A is om means that the Limited Principle of Omniscience (LPO) implies Markov's Principle (MP). (Contributed by Jim Kingdon, 18-Mar-2023.)
|- ( A e. Omni -> A e. Markov )
Theorem	exmidmp 7274	Excluded middle implies Markov's Principle (MP). (Contributed by Jim Kingdon, 4-Apr-2023.)
|- (EXMID -> om e. Markov )
Theorem	mkvprop 7275*	Markov's Principle expressed in terms of propositions (or more precisely, the A = om case is Markov's Principle). (Contributed by Jim Kingdon, 19-Mar-2023.)
|- ( ( A e. Markov /\ A. n e. A DECID ph /\ -. A. n e. A -. ph ) -> E. n e. A ph )
Theorem	fodjumkvlemres 7276*	Lemma for fodjumkv 7277. The final result with P expressed as a local definition. (Contributed by Jim Kingdon, 25-Mar-2023.)
|- ( ph -> M e. Markov )   &    |- ( ph -> F : M -onto-> ( A ⊔ B ) )   &    |- P = ( y e. M |-> if ( E. z e. A ( F ` y ) = (inl ` z ) , (/) , 1o ) )   =>    |- ( ph -> ( A =/= (/) -> E. x x e. A ) )
Theorem	fodjumkv 7277*	A condition which ensures that a nonempty set is inhabited. (Contributed by Jim Kingdon, 25-Mar-2023.)
|- ( ph -> M e. Markov )   &    |- ( ph -> F : M -onto-> ( A ⊔ B ) )   =>    |- ( ph -> ( A =/= (/) -> E. x x e. A ) )
Theorem	enmkvlem 7278	Lemma for enmkv 7279. One direction of the biconditional. (Contributed by Jim Kingdon, 25-Jun-2024.)
|- ( A ~~ B -> ( A e. Markov -> B e. Markov ) )
Theorem	enmkv 7279	Being Markov is invariant with respect to equinumerosity. For example, this means that we can express the Markov's Principle as either om e. Markov or NN0 e. Markov. The former is a better match to conventional notation in the sense that df2o3 6529 says that 2o = { (/) , 1o } whereas the corresponding relationship does not exist between 2 and { 0 , 1 }. (Contributed by Jim Kingdon, 24-Jun-2024.)
|- ( A ~~ B -> ( A e. Markov <-> B e. Markov ) )
2.6.40  Weakly omniscient sets
Syntax	cwomni 7280	Extend class definition to include the class of weakly omniscient sets.
class WOmni
Definition	df-womni 7281*	A weakly 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 not. Generalization of definition 2.4 of [Pierik], p. 9. In particular, om e. WOmni is known as the Weak Limited Principle of Omniscience (WLPO). The term WLPO is common in the literature; there appears to be no widespread term for what we are calling a weakly omniscient set. (Contributed by Jim Kingdon, 9-Jun-2024.)
|- WOmni = { y | A. f ( f : y --> 2o -> DECID A. x e. y ( f ` x ) = 1o ) }
Theorem	iswomni 7282*	The predicate of being weakly omniscient. (Contributed by Jim Kingdon, 9-Jun-2024.)
|- ( A e. V -> ( A e. WOmni <-> A. f ( f : A --> 2o -> DECID A. x e. A ( f ` x ) = 1o ) ) )
Theorem	iswomnimap 7283*	The predicate of being weakly omniscient stated in terms of set exponentiation. (Contributed by Jim Kingdon, 9-Jun-2024.)
|- ( A e. V -> ( A e. WOmni <-> A. f e. ( 2o ^m A )DECID A. x e. A ( f ` x ) = 1o ) )
Theorem	omniwomnimkv 7284	A set is omniscient if and only if it is weakly omniscient and Markov. The case A = om says that LPO <-> WLPO /\ MP which is a remark following Definition 2.5 of [Pierik], p. 9. (Contributed by Jim Kingdon, 9-Jun-2024.)
|- ( A e. Omni <-> ( A e. WOmni /\ A e. Markov ) )
Theorem	lpowlpo 7285	LPO implies WLPO. Easy corollary of the more general omniwomnimkv 7284. There is an analogue in terms of analytic omniscience principles at tridceq 16136. (Contributed by Jim Kingdon, 24-Jul-2024.)
|- ( om e. Omni -> om e. WOmni )
Theorem	enwomnilem 7286	Lemma for enwomni 7287. One direction of the biconditional. (Contributed by Jim Kingdon, 20-Jun-2024.)
|- ( A ~~ B -> ( A e. WOmni -> B e. WOmni ) )
Theorem	enwomni 7287	Weak omniscience is invariant with respect to equinumerosity. For example, this means that we can express the Weak Limited Principle of Omniscience as either om e. WOmni or NN0 e. WOmni. The former is a better match to conventional notation in the sense that df2o3 6529 says that 2o = { (/) , 1o } whereas the corresponding relationship does not exist between 2 and { 0 , 1 }. (Contributed by Jim Kingdon, 20-Jun-2024.)
|- ( A ~~ B -> ( A e. WOmni <-> B e. WOmni ) )
Theorem	nninfdcinf 7288*	The Weak Limited Principle of Omniscience (WLPO) implies that it is decidable whether an element of ℕ∞ equals the point at infinity. (Contributed by Jim Kingdon, 3-Dec-2024.)
|- ( ph -> om e. WOmni )   &    |- ( ph -> N e. ℕ∞ )   =>    |- ( ph -> DECID N = ( i e. om |-> 1o ) )
Theorem	nninfwlporlemd 7289*	Given two countably infinite sequences of zeroes and ones, they are equal if and only if a sequence formed by pointwise comparing them is all ones. (Contributed by Jim Kingdon, 6-Dec-2024.)
|- ( ph -> X : om --> 2o )   &    |- ( ph -> Y : om --> 2o )   &    |- D = ( i e. om |-> if ( ( X ` i ) = ( Y ` i ) , 1o , (/) ) )   =>    |- ( ph -> ( X = Y <-> D = ( i e. om |-> 1o ) ) )
Theorem	nninfwlporlem 7290*	Lemma for nninfwlpor 7291. The result. (Contributed by Jim Kingdon, 7-Dec-2024.)
|- ( ph -> X : om --> 2o )   &    |- ( ph -> Y : om --> 2o )   &    |- D = ( i e. om |-> if ( ( X ` i ) = ( Y ` i ) , 1o , (/) ) )   &    |- ( ph -> om e. WOmni )   =>    |- ( ph -> DECID X = Y )
Theorem	nninfwlpor 7291*	The Weak Limited Principle of Omniscience (WLPO) implies that equality for ℕ∞ is decidable. (Contributed by Jim Kingdon, 7-Dec-2024.)
|- ( om e. WOmni -> A. x e. ℕ∞ A. y e. ℕ∞ DECID x = y )
Theorem	nninfwlpoimlemg 7292*	Lemma for nninfwlpoim 7296. (Contributed by Jim Kingdon, 8-Dec-2024.)
|- ( ph -> F : om --> 2o )   &    |- G = ( i e. om |-> if ( E. x e. suc i ( F ` x ) = (/) , (/) , 1o ) )   =>    |- ( ph -> G e. ℕ∞ )
Theorem	nninfwlpoimlemginf 7293*	Lemma for nninfwlpoim 7296. (Contributed by Jim Kingdon, 8-Dec-2024.)
|- ( ph -> F : om --> 2o )   &    |- G = ( i e. om |-> if ( E. x e. suc i ( F ` x ) = (/) , (/) , 1o ) )   =>    |- ( ph -> ( G = ( i e. om |-> 1o ) <-> A. n e. om ( F ` n ) = 1o ) )
Theorem	nninfwlpoimlemdc 7294*	Lemma for nninfwlpoim 7296. (Contributed by Jim Kingdon, 8-Dec-2024.)
|- ( ph -> F : om --> 2o )   &    |- G = ( i e. om |-> if ( E. x e. suc i ( F ` x ) = (/) , (/) , 1o ) )   &    |- ( ph -> A. x e. ℕ∞ A. y e. ℕ∞ DECID x = y )   =>    |- ( ph -> DECID A. n e. om ( F ` n ) = 1o )
Theorem	nninfinfwlpolem 7295*	Lemma for nninfinfwlpo 7297. (Contributed by Jim Kingdon, 8-Dec-2024.)
|- ( ph -> F : om --> 2o )   &    |- G = ( i e. om |-> if ( E. x e. suc i ( F ` x ) = (/) , (/) , 1o ) )   &    |- ( ph -> A. x e. ℕ∞ DECID x = ( i e. om |-> 1o ) )   =>    |- ( ph -> DECID A. n e. om ( F ` n ) = 1o )
Theorem	nninfwlpoim 7296*	Decidable equality for ℕ∞ implies the Weak Limited Principle of Omniscience (WLPO). (Contributed by Jim Kingdon, 9-Dec-2024.)
|- ( A. x e. ℕ∞ A. y e. ℕ∞ DECID x = y -> om e. WOmni )
Theorem	nninfinfwlpo 7297*	The point at infinity in ℕ∞ being isolated is equivalent to the Weak Limited Principle of Omniscience (WLPO). By isolated, we mean that the equality of that point with every other element of ℕ∞ is decidable. From an online post by Martin Escardo. By contrast, elements of ℕ∞ corresponding to natural numbers are isolated (nninfisol 7250). (Contributed by Jim Kingdon, 25-Nov-2025.)
|- ( A. x e. ℕ∞ DECID x = ( i e. om |-> 1o ) <-> om e. WOmni )
Theorem	nninfwlpo 7298*	Decidability of equality for ℕ∞ is equivalent to the Weak Limited Principle of Omniscience (WLPO). (Contributed by Jim Kingdon, 3-Dec-2024.)
|- ( A. x e. ℕ∞ A. y e. ℕ∞ DECID x = y <-> om e. WOmni )
2.6.41  Cardinal numbers
Syntax	ccrd 7299	Extend class definition to include the cardinal size function.
class card
Syntax	wacn 7300	The axiom of choice for limited-length sequences.
class AC A