P. 171 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 17001-17100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bj-omssonALT 17001	Alternate proof of bj-omsson 17000. (Contributed by BJ, 27-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
|- om C_ On
Theorem	bj-nn0suc 17002*	Proof of (biconditional form of) nn0suc 4751 from the core axioms of CZF. See also bj-nn0sucALT 17016. As a characterization of the elements of om, this could be labeled "elom". (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.)
|- ( A e. om <-> ( A = (/) \/ E. x e. om A = suc x ) )
14.3.11  CZF: Set induction In this section, we add the axiom of set induction to the core axioms of CZF.
14.3.11.1  Set induction In this section, we prove some variants of the axiom of set induction.
Theorem	setindft 17003*	Axiom of set-induction with a disjoint variable condition replaced with a nonfreeness hypothesis. (Contributed by BJ, 22-Nov-2019.)
|- ( A. x F/ y ph -> ( A. x ( A. y e. x [ y / x ] ph -> ph ) -> A. x ph ) )
Theorem	setindf 17004*	Axiom of set-induction with a disjoint variable condition replaced with a nonfreeness hypothesis. (Contributed by BJ, 22-Nov-2019.)
|- F/ y ph   =>    |- ( A. x ( A. y e. x [ y / x ] ph -> ph ) -> A. x ph )
Theorem	setindis 17005*	Axiom of set induction using implicit substitutions. (Contributed by BJ, 22-Nov-2019.)
|- F/ x ps   &    |- F/ x ch   &    |- F/ y ph   &    |- F/ y ps   &    |- ( x = z -> ( ph -> ps ) )   &    |- ( x = y -> ( ch -> ph ) )   =>    |- ( A. y ( A. z e. y ps -> ch ) -> A. x ph )
Axiom	ax-bdsetind 17006*	Axiom of bounded set induction. (Contributed by BJ, 28-Nov-2019.)
|- BOUNDED ph   =>    |- ( A. a ( A. y e. a [ y / a ] ph -> ph ) -> A. a ph )
Theorem	bdsetindis 17007*	Axiom of bounded set induction using implicit substitutions. (Contributed by BJ, 22-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED ph   &    |- F/ x ps   &    |- F/ x ch   &    |- F/ y ph   &    |- F/ y ps   &    |- ( x = z -> ( ph -> ps ) )   &    |- ( x = y -> ( ch -> ph ) )   =>    |- ( A. y ( A. z e. y ps -> ch ) -> A. x ph )
Theorem	bj-inf2vnlem1 17008*	Lemma for bj-inf2vn 17012. Remark: unoptimized proof (have to use more deduction style). (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.)
|- ( A. x ( x e. A <-> ( x = (/) \/ E. y e. A x = suc y ) ) -> Ind A )
Theorem	bj-inf2vnlem2 17009*	Lemma for bj-inf2vnlem3 17010 and bj-inf2vnlem4 17011. Remark: unoptimized proof (have to use more deduction style). (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.)
|- ( A. x e. A ( x = (/) \/ E. y e. A x = suc y ) -> (Ind Z -> A. u ( A. t e. u ( t e. A -> t e. Z ) -> ( u e. A -> u e. Z ) ) ) )
Theorem	bj-inf2vnlem3 17010*	Lemma for bj-inf2vn 17012. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.)
|- BOUNDED A   &    |- BOUNDED Z   =>    |- ( A. x e. A ( x = (/) \/ E. y e. A x = suc y ) -> (Ind Z -> A C_ Z ) )
Theorem	bj-inf2vnlem4 17011*	Lemma for bj-inf2vn2 17013. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.)
|- ( A. x e. A ( x = (/) \/ E. y e. A x = suc y ) -> (Ind Z -> A C_ Z ) )
Theorem	bj-inf2vn 17012*	A sufficient condition for om to be a set. See bj-inf2vn2 17013 for the unbounded version from full set induction. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.)
|- BOUNDED A   =>    |- ( A e. V -> ( A. x ( x e. A <-> ( x = (/) \/ E. y e. A x = suc y ) ) -> A = om ) )
Theorem	bj-inf2vn2 17013*	A sufficient condition for om to be a set; unbounded version of bj-inf2vn 17012. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.)
|- ( A e. V -> ( A. x ( x e. A <-> ( x = (/) \/ E. y e. A x = suc y ) ) -> A = om ) )
Axiom	ax-inf2 17014*	Another axiom of infinity in a constructive setting (see ax-infvn 16979). (Contributed by BJ, 14-Nov-2019.) (New usage is discouraged.)
|- E. a A. x ( x e. a <-> ( x = (/) \/ E. y e. a x = suc y ) )
Theorem	bj-omex2 17015	Using bounded set induction and the strong axiom of infinity, om is a set, that is, we recover ax-infvn 16979 (see bj-2inf 16976 for the equivalence of the latter with bj-omex 16980). (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- om e. _V
Theorem	bj-nn0sucALT 17016*	Alternate proof of bj-nn0suc 17002, also constructive but from ax-inf2 17014, hence requiring ax-bdsetind 17006. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( A e. om <-> ( A = (/) \/ E. x e. om A = suc x ) )
14.3.11.2  Full induction In this section, using the axiom of set induction, we prove full induction on the set of natural numbers.
Theorem	bj-findis 17017*	Principle of induction, using implicit substitutions (the biconditional versions of the hypotheses are implicit substitutions, and we have weakened them to implications). Constructive proof (from CZF). See bj-bdfindis 16985 for a bounded version not requiring ax-setind 4684. See finds 4747 for a proof in IZF. From this version, it is easy to prove of finds 4747, finds2 4748, finds1 4749. (Contributed by BJ, 22-Dec-2019.) (Proof modification is discouraged.)
|- F/ x ps   &    |- F/ x ch   &    |- F/ x th   &    |- ( x = (/) -> ( ps -> ph ) )   &    |- ( x = y -> ( ph -> ch ) )   &    |- ( x = suc y -> ( th -> ph ) )   =>    |- ( ( ps /\ A. y e. om ( ch -> th ) ) -> A. x e. om ph )
Theorem	bj-findisg 17018*	Version of bj-findis 17017 using a class term in the consequent. Constructive proof (from CZF). See the comment of bj-findis 17017 for explanations. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.)
|- F/ x ps   &    |- F/ x ch   &    |- F/ x th   &    |- ( x = (/) -> ( ps -> ph ) )   &    |- ( x = y -> ( ph -> ch ) )   &    |- ( x = suc y -> ( th -> ph ) )   &    |- F/_ x A   &    |- F/ x ta   &    |- ( x = A -> ( ph -> ta ) )   =>    |- ( ( ps /\ A. y e. om ( ch -> th ) ) -> ( A e. om -> ta ) )
Theorem	bj-findes 17019	Principle of induction, using explicit substitutions. Constructive proof (from CZF). See the comment of bj-findis 17017 for explanations. From this version, it is easy to prove findes 4750. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.)
|- ( ( [. (/) / x ]. ph /\ A. x e. om ( ph -> [. suc x / x ]. ph ) ) -> A. x e. om ph )
14.3.12  CZF: Strong collection In this section, we state the axiom scheme of strong collection, which is part of CZF set theory.
Axiom	ax-strcoll 17020*	Axiom scheme of strong collection. It is stated with all possible disjoint variable conditions, to show that this weak form is sufficient. The antecedent means that ph represents a multivalued function on a, or equivalently a collection of nonempty classes indexed by a, and the axiom asserts the existence of a set b which "collects" at least one element in the image of each x e. a and which is made only of such elements. That second conjunct is what makes it "strong", compared to the axiom scheme of collection ax-coll 4246. (Contributed by BJ, 5-Oct-2019.)
|- A. a ( A. x e. a E. y ph -> E. b ( A. x e. a E. y e. b ph /\ A. y e. b E. x e. a ph ) )
Theorem	strcoll2 17021*	Version of ax-strcoll 17020 with one disjoint variable condition removed and without initial universal quantifier. (Contributed by BJ, 5-Oct-2019.)
|- ( A. x e. a E. y ph -> E. b ( A. x e. a E. y e. b ph /\ A. y e. b E. x e. a ph ) )
Theorem	strcollnft 17022*	Closed form of strcollnf 17023. (Contributed by BJ, 21-Oct-2019.)
|- ( A. x A. y F/ b ph -> ( A. x e. a E. y ph -> E. b ( A. x e. a E. y e. b ph /\ A. y e. b E. x e. a ph ) ) )
Theorem	strcollnf 17023*	Version of ax-strcoll 17020 with one disjoint variable condition removed, the other disjoint variable condition replaced with a nonfreeness hypothesis, and without initial universal quantifier. Version of strcoll2 17021 with the disjoint variable condition on b , ph replaced with a nonfreeness hypothesis. This proof aims to demonstrate a standard technique, but strcoll2 17021 will generally suffice: since the theorem asserts the existence of a set b, supposing that that setvar does not occur in the already defined ph is not a big constraint. (Contributed by BJ, 21-Oct-2019.)
|- F/ b ph   =>    |- ( A. x e. a E. y ph -> E. b ( A. x e. a E. y e. b ph /\ A. y e. b E. x e. a ph ) )
Theorem	strcollnfALT 17024*	Alternate proof of strcollnf 17023, not using strcollnft 17022. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ b ph   =>    |- ( A. x e. a E. y ph -> E. b ( A. x e. a E. y e. b ph /\ A. y e. b E. x e. a ph ) )
14.3.13  CZF: Subset collection In this section, we state the axiom scheme of subset collection, which is part of CZF set theory.
Axiom	ax-sscoll 17025*	Axiom scheme of subset collection. It is stated with all possible disjoint variable conditions, to show that this weak form is sufficient. The antecedent means that ph represents a multivalued function from a to b, or equivalently a collection of nonempty subsets of b indexed by a, and the consequent asserts the existence of a subset of c which "collects" at least one element in the image of each x e. a and which is made only of such elements. The axiom asserts the existence, for any sets a , b, of a set c such that that implication holds for any value of the parameter z of ph. (Contributed by BJ, 5-Oct-2019.)
|- A. a A. b E. c A. z ( A. x e. a E. y e. b ph -> E. d e. c ( A. x e. a E. y e. d ph /\ A. y e. d E. x e. a ph ) )
Theorem	sscoll2 17026*	Version of ax-sscoll 17025 with two disjoint variable conditions removed and without initial universal quantifiers. (Contributed by BJ, 5-Oct-2019.)
|- E. c A. z ( A. x e. a E. y e. b ph -> E. d e. c ( A. x e. a E. y e. d ph /\ A. y e. d E. x e. a ph ) )
14.3.14  Real numbers
Axiom	ax-ddkcomp 17027	Axiom of Dedekind completeness for Dedekind real numbers: every inhabited upper-bounded located set of reals has a real upper bound. Ideally, this axiom should be "proved" as "axddkcomp" for the real numbers constructed from IZF, and then Axiom ax-ddkcomp 17027 should be used in place of construction specific results. In particular, axcaucvg 8267 should be proved from it. (Contributed by BJ, 24-Oct-2021.)
|- ( ( ( A C_ RR /\ E. x x e. A ) /\ E. x e. RR A. y e. A y < x /\ A. x e. RR A. y e. RR ( x < y -> ( E. z e. A x < z \/ A. z e. A z < y ) ) ) -> E. x e. RR ( A. y e. A y <_ x /\ ( ( B e. R /\ A. y e. A y <_ B ) -> x <_ B ) ) )
14.4  Mathbox for Jim Kingdon
14.4.1  Propositional and predicate logic
Theorem	nnnotnotr 17028	Double negation of double negation elimination. Suggested by an online post by Martin Escardo. Although this statement resembles nnexmid 862, it can be proved with reference only to implication and negation (that is, without use of disjunction). (Contributed by Jim Kingdon, 21-Oct-2024.)
|- -. -. ( -. -. ph -> ph )
14.4.2  The sizes of sets
Theorem	ss1oel2o 17029	Any subset of ordinal one being an element of ordinal two is equivalent to excluded middle. A variation of exmid01 4335 which more directly illustrates the contrast with el2oss1o 6716. (Contributed by Jim Kingdon, 8-Aug-2022.)
|- (EXMID <-> A. x ( x C_ 1o -> x e. 2o ) )
Theorem	3dom 17030*	A set that dominates ordinal 3 has at least 3 different members. (Contributed by Jim Kingdon, 12-Feb-2026.)
|- ( 3o ~<_ A -> E. x e. A E. y e. A E. z e. A ( x =/= y /\ x =/= z /\ y =/= z ) )
Theorem	pw1ndom3lem 17031	Lemma for pw1ndom3 17032. (Contributed by Jim Kingdon, 14-Feb-2026.)
|- ( ph -> X e. ~P 1o )   &    |- ( ph -> Y e. ~P 1o )   &    |- ( ph -> Z e. ~P 1o )   &    |- ( ph -> X =/= Y )   &    |- ( ph -> X =/= Z )   &    |- ( ph -> Y =/= Z )   =>    |- ( ph -> X = (/) )
Theorem	pw1ndom3 17032	The powerset of 1o does not dominate 3o. This is another way of saying that ~P 1o does not have three elements (like pwntru 4336). (Contributed by Steven Nguyen and Jim Kingdon, 14-Feb-2026.)
|- -. 3o ~<_ ~P 1o
Theorem	pw1ninf 17033	The powerset of 1o is not infinite. Since we cannot prove it is finite (see pw1fin 7217), this provides a concrete example of a set which we cannot show to be finite or infinite, as seen another way at inffiexmid 7213. (Contributed by Jim Kingdon, 14-Feb-2026.)
|- -. om ~<_ ~P 1o
Theorem	nnti 17034	Ordering on a natural number generates a tight apartness. (Contributed by Jim Kingdon, 7-Aug-2022.)
|- ( ph -> A e. om )   =>    |- ( ( ph /\ ( u e. A /\ v e. A ) ) -> ( u = v <-> ( -. u _E v /\ -. v _E u ) ) )
Theorem	012of 17035	Mapping zero and one between NN0 and om style integers. (Contributed by Jim Kingdon, 28-Jun-2024.)
|- G = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   =>    |- ( `' G |` { 0 , 1 } ) : { 0 , 1 } --> 2o
Theorem	2o01f 17036	Mapping zero and one between om and NN0 style integers. (Contributed by Jim Kingdon, 28-Jun-2024.)
|- G = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   =>    |- ( G |` 2o ) : 2o --> { 0 , 1 }
Theorem	pw1map 17037*	Mapping between ( ~P 1o ^m A ) and subsets of A. (Contributed by Jim Kingdon, 9-Jan-2026.)
|- F = ( s e. ( ~P 1o ^m A ) |-> { z e. A | ( s ` z ) = 1o } )   =>    |- ( A e. V -> F : ( ~P 1o ^m A ) -1-1-onto-> ~P A )
Theorem	pw1mapen 17038	Equinumerosity of ( ~P 1o ^m A ) and the set of subsets of A. (Contributed by Jim Kingdon, 10-Jan-2026.)
|- ( A e. V -> ( ~P 1o ^m A ) ~~ ~P A )
14.4.3  The power set of a singleton
Theorem	pwtrufal 17039	A subset of the singleton { (/) } cannot be anything other than (/) or { (/) }. Removing the double negation would change the meaning, as seen at exmid01 4335. If we view a subset of a singleton as a truth value (as seen in theorems like exmidexmid 4333), then this theorem states there are no truth values other than true and false, as described in section 1.1 of [Bauer], p. 481. (Contributed by Mario Carneiro and Jim Kingdon, 11-Sep-2023.)
|- ( A C_ { (/) } -> -. -. ( A = (/) \/ A = { (/) } ) )
Theorem	pwle2 17040*	An exercise related to N copies of a singleton and the power set of a singleton (where the latter can also be thought of as representing truth values). Posed as an exercise by Martin Escardo online. (Contributed by Jim Kingdon, 3-Sep-2023.)
|- T = U_ x e. N ( { x } X. 1o )   =>    |- ( ( N e. om /\ G : T -1-1-> ~P 1o ) -> N C_ 2o )
Theorem	pwf1oexmid 17041*	An exercise related to N copies of a singleton and the power set of a singleton (where the latter can also be thought of as representing truth values). Posed as an exercise by Martin Escardo online. (Contributed by Jim Kingdon, 3-Sep-2023.)
|- T = U_ x e. N ( { x } X. 1o )   =>    |- ( ( N e. om /\ G : T -1-1-> ~P 1o ) -> ( ran G = ~P 1o <-> ( N = 2o /\ EXMID ) ) )
Theorem	subctctexmid 17042*	If every subcountable set is countable and Markov's principle holds, excluded middle follows. Proposition 2.6 of [BauerSwan], p. 14:4. The proof is taken from that paper. (Contributed by Jim Kingdon, 29-Nov-2023.)
|- ( ph -> A. x ( E. s ( s C_ om /\ E. f f : s -onto-> x ) -> E. g g : om -onto-> ( x ⊔ 1o ) ) )   &    |- ( ph -> om e. Markov )   =>    |- ( ph -> EXMID )
Theorem	domomsubct 17043*	A set dominated by om is subcountable. (Contributed by Jim Kingdon, 11-Nov-2025.)
|- ( A ~<_ om -> E. s ( s C_ om /\ E. f f : s -onto-> A ) )
Theorem	sssneq 17044*	Any two elements of a subset of a singleton are equal. (Contributed by Jim Kingdon, 28-May-2024.)
|- ( A C_ { B } -> A. y e. A A. z e. A y = z )
Theorem	pw1nct 17045*	A condition which ensures that the powerset of a singleton is not countable. The antecedent here can be referred to as the uniformity principle. Based on Mastodon posts by Andrej Bauer and Rahul Chhabra. (Contributed by Jim Kingdon, 29-May-2024.)
|- ( A. r ( r C_ ( ~P 1o X. om ) -> ( A. p e. ~P 1o E. n e. om p r n -> E. m e. om A. q e. ~P 1o q r m ) ) -> -. E. f f : om -onto-> ( ~P 1o ⊔ 1o ) )
Theorem	rabid1o 17046*	Converting between propositions and corresponding subsets of a singleton. (Contributed by Jim Kingdon, 31-Jul-2026.)
|- ( { x e. 1o | ph } = 1o <-> ph )
Theorem	pw1dceq 17047*	The powerset of 1o having decidable equality is equivalent to excluded middle. (Contributed by Jim Kingdon, 12-Feb-2026.)
|- (EXMID <-> A. x e. ~P 1o A. y e. ~P 1oDECID x = y )
Theorem	exmidnotnotr 17048	Excluded middle is equivalent to double negation elimination. Read an element of ~P 1o as being a truth value and x = 1o being that x is true. For a similar theorem, but expressed in terms of formulas rather than subsets of 1o, see dcfromnotnotr 1497. (Contributed by Jim Kingdon, 22-Apr-2026.)
|- (EXMID <-> A. x e. ~P 1o ( -. -. x = 1o -> x = 1o ) )
Theorem	exmidcon 17049*	Excluded middle is equivalent to the form of contraposition which removes negation. Read an element of ~P 1o as being a truth value and x = 1o being that x is true. For a similar theorem, but expressed in terms of formulas rather than subsets of 1o, see dcfromcon 1498. (Contributed by Jim Kingdon, 22-Apr-2026.)
|- (EXMID <-> A. x e. ~P 1o A. y e. ~P 1o ( ( -. y = 1o -> -. x = 1o ) -> ( x = 1o -> y = 1o ) ) )
Theorem	exmidpeirce 17050*	Excluded middle is equivalent to Peirce's law. Read an element of ~P 1o as being a truth value and x = 1o being that x is true. For a similar theorem, but expressed in terms of formulas rather than subsets of 1o, see dcfrompeirce 1499. (Contributed by Jim Kingdon, 23-Apr-2026.)
|- (EXMID <-> A. x e. ~P 1o A. y e. ~P 1o ( ( ( x = 1o -> y = 1o ) -> x = 1o ) -> x = 1o ) )
Theorem	stnot 17051*	A proposition is double negation stable if and only if it is equivalent to a negated proposition. Here by "proposition" we mean a subset of a singleton (which is a choice which allows us to quantify over them). Posed as an exercise online by Yannick Forster. (Contributed by Jim Kingdon, 24-Jul-2026.)
|- ( A e. ~P 1o -> ( ( -. -. A = 1o -> A = 1o ) <-> E. y e. ~P 1o ( A = 1o <-> -. y = 1o ) ) )
14.4.4  Weak excluded middle
Syntax	wwem 17052	Formula for an abbreviation of weak excluded middle.
wff WEXMID
Definition	df-wexmid 17053	Weak excluded middle is the principle that any negated proposition is decidable. (Contributed by Jim Kingdon, 30-Jul-2026.)
|- (WEXMID <-> A. p e. ~P 1o ( -. p = 1o \/ -. -. p = 1o ) )
Theorem	wexmiddc 17054	Weak excluded middle expressed using WEXMID implies decidability of a negated proposition. (Contributed by Jim Kingdon, 30-Jul-2026.)
|- (WEXMID -> DECID -. ph )
Theorem	wexmiddiffilem 17055*	Lemma for wexmiddiffi 17056. The reverse direction, using different notation. (Contributed by Jim Kingdon, 29-Jul-2026.)
|- ( A. x A. y ( x e. Fin -> ( x \ y ) e. Fin ) -> ( -. ph \/ -. -. ph ) )
Theorem	wexmiddiffi 17056*	Being able to subtract an arbitrary set from a finite set and get a finite set is equivalent to weak excluded middle. By adding additional conditions we can get a theorem which does not need weak excluded middle, at diffifi 7198. (Contributed by Jim Kingdon, 29-Jul-2026.)
|- (WEXMID <-> A. x A. y ( x e. Fin -> ( x \ y ) e. Fin ) )
Theorem	wexmiddifxylem 17057*	Lemma for wexmiddifxylem 17057. Showing weak excluded middle given a suitable finite set. (Contributed by Jim Kingdon, 1-Aug-2026.)
|- ( ( { 1o } \ { { x e. 1o | ph } } ) e. Fin -> DECID -. ph )
Theorem	wexmiddifxy 17058*	Being able to subtract an arbitrary finite set from a finite set and get a finite set is equivalent to weak excluded middle. By adding additional conditions we can get a theorem which does not need weak excluded middle, at diffifi 7198. (Contributed by Jim Kingdon, 1-Aug-2026.)
|- (WEXMID <-> A. x A. y ( ( x e. Fin /\ y e. Fin ) -> ( x \ y ) e. Fin ) )
14.4.5  Omniscience of NN+oo
Theorem	0nninf 17059	The zero element of ℕ∞ (the constant sequence equal to (/)). (Contributed by Jim Kingdon, 14-Jul-2022.)
|- ( om X. { (/) } ) e. ℕ∞
Theorem	nnsf 17060*	Domain and range of S. Part of Definition 3.3 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 30-Jul-2022.)
|- S = ( p e. ℕ∞ |-> ( i e. om |-> if ( i = (/) , 1o , ( p ` U. i ) ) ) )   =>    |- S :ℕ∞ -->ℕ∞
Theorem	peano4nninf 17061*	The successor function on ℕ∞ is one to one. Half of Lemma 3.4 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 31-Jul-2022.)
|- S = ( p e. ℕ∞ |-> ( i e. om |-> if ( i = (/) , 1o , ( p ` U. i ) ) ) )   =>    |- S :ℕ∞ -1-1->ℕ∞
Theorem	peano3nninf 17062*	The successor function on ℕ∞ is never zero. Half of Lemma 3.4 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 1-Aug-2022.)
|- S = ( p e. ℕ∞ |-> ( i e. om |-> if ( i = (/) , 1o , ( p ` U. i ) ) ) )   =>    |- ( A e. ℕ∞ -> ( S ` A ) =/= ( x e. om |-> (/) ) )
Theorem	nninfalllem1 17063*	Lemma for nninfall 17064. (Contributed by Jim Kingdon, 1-Aug-2022.)
|- ( ph -> Q e. ( 2o ^m ℕ∞ ) )   &    |- ( ph -> ( Q ` ( x e. om |-> 1o ) ) = 1o )   &    |- ( ph -> A. n e. om ( Q ` ( i e. om |-> if ( i e. n , 1o , (/) ) ) ) = 1o )   &    |- ( ph -> P e. ℕ∞ )   &    |- ( ph -> ( Q ` P ) = (/) )   =>    |- ( ph -> A. n e. om ( P ` n ) = 1o )
Theorem	nninfall 17064*	Given a decidable predicate on ℕ∞, showing it holds for natural numbers and the point at infinity suffices to show it holds everywhere. The sense in which Q is a decidable predicate is that it assigns a value of either (/) or 1o (which can be thought of as false and true) to every element of ℕ∞. Lemma 3.5 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 1-Aug-2022.)
|- ( ph -> Q e. ( 2o ^m ℕ∞ ) )   &    |- ( ph -> ( Q ` ( x e. om |-> 1o ) ) = 1o )   &    |- ( ph -> A. n e. om ( Q ` ( i e. om |-> if ( i e. n , 1o , (/) ) ) ) = 1o )   =>    |- ( ph -> A. p e. ℕ∞ ( Q ` p ) = 1o )
Theorem	nninfsellemdc 17065*	Lemma for nninfself 17068. Showing that the selection function is well defined. (Contributed by Jim Kingdon, 8-Aug-2022.)
|- ( ( Q e. ( 2o ^m ℕ∞ ) /\ N e. om ) -> DECID A. k e. suc N ( Q ` ( i e. om |-> if ( i e. k , 1o , (/) ) ) ) = 1o )
Theorem	nninfsellemcl 17066*	Lemma for nninfself 17068. (Contributed by Jim Kingdon, 8-Aug-2022.)
|- ( ( Q e. ( 2o ^m ℕ∞ ) /\ N e. om ) -> if ( A. k e. suc N ( Q ` ( i e. om |-> if ( i e. k , 1o , (/) ) ) ) = 1o , 1o , (/) ) e. 2o )
Theorem	nninfsellemsuc 17067*	Lemma for nninfself 17068. (Contributed by Jim Kingdon, 6-Aug-2022.)
|- ( ( Q e. ( 2o ^m ℕ∞ ) /\ J e. om ) -> if ( A. k e. suc suc J ( Q ` ( i e. om |-> if ( i e. k , 1o , (/) ) ) ) = 1o , 1o , (/) ) C_ if ( A. k e. suc J ( Q ` ( i e. om |-> if ( i e. k , 1o , (/) ) ) ) = 1o , 1o , (/) ) )
Theorem	nninfself 17068*	Domain and range of the selection function for ℕ∞. (Contributed by Jim Kingdon, 6-Aug-2022.)
|- E = ( q e. ( 2o ^m ℕ∞ ) |-> ( n e. om |-> if ( A. k e. suc n ( q ` ( i e. om |-> if ( i e. k , 1o , (/) ) ) ) = 1o , 1o , (/) ) ) )   =>    |- E : ( 2o ^m ℕ∞ ) -->ℕ∞
Theorem	nninfsellemeq 17069*	Lemma for nninfsel 17072. (Contributed by Jim Kingdon, 9-Aug-2022.)
|- E = ( q e. ( 2o ^m ℕ∞ ) |-> ( n e. om |-> if ( A. k e. suc n ( q ` ( i e. om |-> if ( i e. k , 1o , (/) ) ) ) = 1o , 1o , (/) ) ) )   &    |- ( ph -> Q e. ( 2o ^m ℕ∞ ) )   &    |- ( ph -> ( Q ` ( E ` Q ) ) = 1o )   &    |- ( ph -> N e. om )   &    |- ( ph -> A. k e. N ( Q ` ( i e. om |-> if ( i e. k , 1o , (/) ) ) ) = 1o )   &    |- ( ph -> ( Q ` ( i e. om |-> if ( i e. N , 1o , (/) ) ) ) = (/) )   =>    |- ( ph -> ( E ` Q ) = ( i e. om |-> if ( i e. N , 1o , (/) ) ) )
Theorem	nninfsellemqall 17070*	Lemma for nninfsel 17072. (Contributed by Jim Kingdon, 9-Aug-2022.)
|- E = ( q e. ( 2o ^m ℕ∞ ) |-> ( n e. om |-> if ( A. k e. suc n ( q ` ( i e. om |-> if ( i e. k , 1o , (/) ) ) ) = 1o , 1o , (/) ) ) )   &    |- ( ph -> Q e. ( 2o ^m ℕ∞ ) )   &    |- ( ph -> ( Q ` ( E ` Q ) ) = 1o )   &    |- ( ph -> N e. om )   =>    |- ( ph -> ( Q ` ( i e. om |-> if ( i e. N , 1o , (/) ) ) ) = 1o )
Theorem	nninfsellemeqinf 17071*	Lemma for nninfsel 17072. (Contributed by Jim Kingdon, 9-Aug-2022.)
|- E = ( q e. ( 2o ^m ℕ∞ ) |-> ( n e. om |-> if ( A. k e. suc n ( q ` ( i e. om |-> if ( i e. k , 1o , (/) ) ) ) = 1o , 1o , (/) ) ) )   &    |- ( ph -> Q e. ( 2o ^m ℕ∞ ) )   &    |- ( ph -> ( Q ` ( E ` Q ) ) = 1o )   =>    |- ( ph -> ( E ` Q ) = ( i e. om |-> 1o ) )
Theorem	nninfsel 17072*	E is a selection function for ℕ∞. Theorem 3.6 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 9-Aug-2022.)
|- E = ( q e. ( 2o ^m ℕ∞ ) |-> ( n e. om |-> if ( A. k e. suc n ( q ` ( i e. om |-> if ( i e. k , 1o , (/) ) ) ) = 1o , 1o , (/) ) ) )   &    |- ( ph -> Q e. ( 2o ^m ℕ∞ ) )   &    |- ( ph -> ( Q ` ( E ` Q ) ) = 1o )   =>    |- ( ph -> A. p e. ℕ∞ ( Q ` p ) = 1o )
Theorem	nninfomnilem 17073*	Lemma for nninfomni 17074. (Contributed by Jim Kingdon, 10-Aug-2022.)
|- E = ( q e. ( 2o ^m ℕ∞ ) |-> ( n e. om |-> if ( A. k e. suc n ( q ` ( i e. om |-> if ( i e. k , 1o , (/) ) ) ) = 1o , 1o , (/) ) ) )   =>    |- ℕ∞ e. Omni
Theorem	nninfomni 17074	ℕ∞ is omniscient. Corollary 3.7 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 10-Aug-2022.)
|- ℕ∞ e. Omni
Theorem	nninffeq 17075*	Equality of two functions on ℕ∞ which agree at every integer and at the point at infinity. From an online post by Martin Escardo. Remark: the last two hypotheses can be grouped into one, |- ( ph -> A. n e. suc om ... ). (Contributed by Jim Kingdon, 4-Aug-2023.)
|- ( ph -> F :ℕ∞ --> NN0 )   &    |- ( ph -> G :ℕ∞ --> NN0 )   &    |- ( ph -> ( F ` ( x e. om |-> 1o ) ) = ( G ` ( x e. om |-> 1o ) ) )   &    |- ( ph -> A. n e. om ( F ` ( i e. om |-> if ( i e. n , 1o , (/) ) ) ) = ( G ` ( i e. om |-> if ( i e. n , 1o , (/) ) ) ) )   =>    |- ( ph -> F = G )
Theorem	nnnninfen 17076	Equinumerosity of the natural numbers and ℕ∞ is equivalent to the Limited Principle of Omniscience (LPO). Remark in Section 1.1 of [Pradic2025], p. 2. (Contributed by Jim Kingdon, 8-Jul-2025.)
|- ( om ~~ ℕ∞ <-> om e. Omni )
Theorem	nnnninfex 17077*	If an element of ℕ∞ has a value of zero somewhere, then it is the mapping of a natural number. (Contributed by Jim Kingdon, 4-Aug-2022.)
|- ( ph -> P e. ℕ∞ )   &    |- ( ph -> N e. om )   &    |- ( ph -> ( P ` N ) = (/) )   =>    |- ( ph -> E. n e. om P = ( i e. om |-> if ( i e. n , 1o , (/) ) ) )
Theorem	nninfnfiinf 17078*	An element of ℕ∞ which is not finite is infinite. (Contributed by Jim Kingdon, 30-Nov-2025.)
|- ( ( A e. ℕ∞ /\ -. E. n e. om A = ( i e. om |-> if ( i e. n , 1o , (/) ) ) ) -> A = ( i e. om |-> 1o ) )
14.4.6  Schroeder-Bernstein Theorem
Theorem	exmidsbthrlem 17079*	Lemma for exmidsbthr 17080. (Contributed by Jim Kingdon, 11-Aug-2022.)
|- S = ( p e. ℕ∞ |-> ( i e. om |-> if ( i = (/) , 1o , ( p ` U. i ) ) ) )   =>    |- ( A. x A. y ( ( x ~<_ y /\ y ~<_ x ) -> x ~~ y ) -> EXMID )
Theorem	exmidsbthr 17080*	The Schroeder-Bernstein Theorem implies excluded middle. Theorem 1 of [PradicBrown2022], p. 1. (Contributed by Jim Kingdon, 11-Aug-2022.)
|- ( A. x A. y ( ( x ~<_ y /\ y ~<_ x ) -> x ~~ y ) -> EXMID )
Theorem	exmidsbth 17081*	The Schroeder-Bernstein Theorem is equivalent to excluded middle. This is Metamath 100 proof #25. The forward direction (isbth 7284) is the proof of the Schroeder-Bernstein Theorem from the Metamath Proof Explorer database (in which excluded middle holds), but adapted to use EXMID as an antecedent rather than being unconditionally true, as in the non-intuitionistic proof at https://us.metamath.org/mpeuni/sbth.html 7284. The reverse direction (exmidsbthr 17080) is the one which establishes that Schroeder-Bernstein implies excluded middle. This resolves the question of whether we will be able to prove Schroeder-Bernstein from our axioms in the negative. (Contributed by Jim Kingdon, 13-Aug-2022.)
|- (EXMID <-> A. x A. y ( ( x ~<_ y /\ y ~<_ x ) -> x ~~ y ) )
Theorem	sbthomlem 17082	Lemma for sbthom 17083. (Contributed by Mario Carneiro and Jim Kingdon, 13-Jul-2023.)
|- ( ph -> om e. Omni )   &    |- ( ph -> Y C_ { (/) } )   &    |- ( ph -> F : om -1-1-onto-> ( Y ⊔ om ) )   =>    |- ( ph -> ( Y = (/) \/ Y = { (/) } ) )
Theorem	sbthom 17083	Schroeder-Bernstein is not possible even for om. We know by exmidsbth 17081 that full Schroeder-Bernstein will not be provable but what about the case where one of the sets is om? That case plus the Limited Principle of Omniscience (LPO) implies excluded middle, so we will not be able to prove it. (Contributed by Mario Carneiro and Jim Kingdon, 10-Jul-2023.)
|- ( ( A. x ( ( x ~<_ om /\ om ~<_ x ) -> x ~~ om ) /\ om e. Omni ) -> EXMID )
14.4.7  Real and complex numbers
Theorem	qdencn 17084*	The set of complex numbers whose real and imaginary parts are rational is dense in the complex plane. This is a two dimensional analogue to qdenre 11970 (and also would hold for RR X. RR with the usual metric; this is not about complex numbers in particular). (Contributed by Jim Kingdon, 18-Oct-2021.)
|- Q = { z e. CC | ( ( Re ` z ) e. QQ /\ ( Im ` z ) e. QQ ) }   =>    |- ( ( A e. CC /\ B e. RR+ ) -> E. x e. Q ( abs ` ( x - A ) ) < B )
Theorem	refeq 17085*	Equality of two real functions which agree at negative numbers, positive numbers, and zero. This holds even without real trichotomy. From an online post by Martin Escardo. (Contributed by Jim Kingdon, 9-Jul-2023.)
|- ( ph -> F : RR --> RR )   &    |- ( ph -> G : RR --> RR )   &    |- ( ph -> A. x e. RR ( x < 0 -> ( F ` x ) = ( G ` x ) ) )   &    |- ( ph -> A. x e. RR ( 0 < x -> ( F ` x ) = ( G ` x ) ) )   &    |- ( ph -> ( F ` 0 ) = ( G ` 0 ) )   =>    |- ( ph -> F = G )
Theorem	repiecelem 17086*	Lemma for repiecele0 17087, repiecege0 17088, and repiecef 17089. The function H is defined everywhere. (Contributed by Jim Kingdon, 27-Apr-2026.)
|- ( ph -> F : ( -oo (,] 0 ) --> RR )   &    |- ( ph -> G : ( 0 [,) +oo ) --> RR )   &    |- ( ph -> ( F ` 0 ) = ( G ` 0 ) )   &    |- H = ( x e. RR |-> ( ( ( F ` inf ( { x , 0 } , RR , < ) ) + ( G ` sup ( { x , 0 } , RR , < ) ) ) - ( F ` 0 ) ) )   =>    |- ( ( ph /\ A e. RR ) -> ( ( ( F ` inf ( { A , 0 } , RR , < ) ) + ( G ` sup ( { A , 0 } , RR , < ) ) ) - ( F ` 0 ) ) e. RR )
Theorem	repiecele0 17087*	Piecewise definition on the reals agrees with the nonpositive part of the definition. See repiecef 17089 for more on this construction. (Contributed by Jim Kingdon, 27-Apr-2026.)
|- ( ph -> F : ( -oo (,] 0 ) --> RR )   &    |- ( ph -> G : ( 0 [,) +oo ) --> RR )   &    |- ( ph -> ( F ` 0 ) = ( G ` 0 ) )   &    |- H = ( x e. RR |-> ( ( ( F ` inf ( { x , 0 } , RR , < ) ) + ( G ` sup ( { x , 0 } , RR , < ) ) ) - ( F ` 0 ) ) )   =>    |- ( ( ph /\ A e. RR /\ A <_ 0 ) -> ( H ` A ) = ( F ` A ) )
Theorem	repiecege0 17088*	Piecewise definition on the reals agrees with the nonnegative part of the definition. See repiecef 17089 for more on this construction. (Contributed by Jim Kingdon, 27-Apr-2026.)
|- ( ph -> F : ( -oo (,] 0 ) --> RR )   &    |- ( ph -> G : ( 0 [,) +oo ) --> RR )   &    |- ( ph -> ( F ` 0 ) = ( G ` 0 ) )   &    |- H = ( x e. RR |-> ( ( ( F ` inf ( { x , 0 } , RR , < ) ) + ( G ` sup ( { x , 0 } , RR , < ) ) ) - ( F ` 0 ) ) )   =>    |- ( ( ph /\ A e. RR /\ 0 <_ A ) -> ( H ` A ) = ( G ` A ) )
Theorem	repiecef 17089*	Piecewise definition on the reals yields a function. The function agrees with F and G on their respective parts of the real line; see repiecele0 17087 and repiecege0 17088. From an online post by James E Hanson. The construction was published in Martín Hötzel Escardó, "Effective and sequential definition by cases on the reals via infinite signed-digit numerals", Electronic Notes in Theoretical Computer Science 10 (1998), page 2, https://martinescardo.github.io/papers/lexnew.pdf. 17088 (Contributed by Jim Kingdon, 27-Apr-2026.)
|- ( ph -> F : ( -oo (,] 0 ) --> RR )   &    |- ( ph -> G : ( 0 [,) +oo ) --> RR )   &    |- ( ph -> ( F ` 0 ) = ( G ` 0 ) )   &    |- H = ( x e. RR |-> ( ( ( F ` inf ( { x , 0 } , RR , < ) ) + ( G ` sup ( { x , 0 } , RR , < ) ) ) - ( F ` 0 ) ) )   =>    |- ( ph -> H : RR --> RR )
Theorem	triap 17090	Two ways of stating real number trichotomy. See also cndcap 17121 which is similar but for complex number apartness. (Contributed by Jim Kingdon, 23-Aug-2023.)
|- ( ( A e. RR /\ B e. RR ) -> ( ( A < B \/ A = B \/ B < A ) <-> DECID A # B ) )
Theorem	isomninnlem 17091*	Lemma for isomninn 17092. The result, with a hypothesis to provide a convenient notation. (Contributed by Jim Kingdon, 30-Aug-2023.)
|- G = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   =>    |- ( A e. V -> ( A e. Omni <-> A. f e. ( { 0 , 1 } ^m A ) ( E. x e. A ( f ` x ) = 0 \/ A. x e. A ( f ` x ) = 1 ) ) )
Theorem	isomninn 17092*	Omniscience stated in terms of natural numbers. Similar to isomnimap 7477 but it will sometimes be more convenient to use 0 and 1 rather than (/) and 1o. (Contributed by Jim Kingdon, 30-Aug-2023.)
|- ( A e. V -> ( A e. Omni <-> A. f e. ( { 0 , 1 } ^m A ) ( E. x e. A ( f ` x ) = 0 \/ A. x e. A ( f ` x ) = 1 ) ) )
Theorem	cvgcmp2nlemabs 17093*	Lemma for cvgcmp2n 17094. The partial sums get closer to each other as we go further out. The proof proceeds by rewriting ( seq 1 ( + , G ) ` N ) as the sum of ( seq 1 ( + , G ) ` M ) and a term which gets smaller as M gets large. (Contributed by Jim Kingdon, 25-Aug-2023.)
|- ( ( ph /\ k e. NN ) -> ( G ` k ) e. RR )   &    |- ( ( ph /\ k e. NN ) -> 0 <_ ( G ` k ) )   &    |- ( ( ph /\ k e. NN ) -> ( G ` k ) <_ ( 1 / ( 2 ^ k ) ) )   &    |- ( ph -> M e. NN )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   =>    |- ( ph -> ( abs ` ( ( seq 1 ( + , G ) ` N ) - ( seq 1 ( + , G ) ` M ) ) ) < ( 2 / M ) )
Theorem	cvgcmp2n 17094*	A comparison test for convergence of a real infinite series. (Contributed by Jim Kingdon, 25-Aug-2023.)
|- ( ( ph /\ k e. NN ) -> ( G ` k ) e. RR )   &    |- ( ( ph /\ k e. NN ) -> 0 <_ ( G ` k ) )   &    |- ( ( ph /\ k e. NN ) -> ( G ` k ) <_ ( 1 / ( 2 ^ k ) ) )   =>    |- ( ph -> seq 1 ( + , G ) e. dom ~~> )
Theorem	iooref1o 17095	A one-to-one mapping from the real numbers onto the open unit interval. (Contributed by Jim Kingdon, 27-Jun-2024.)
|- F = ( x e. RR |-> ( 1 / ( 1 + ( exp ` x ) ) ) )   =>    |- F : RR -1-1-onto-> ( 0 (,) 1 )
Theorem	iooreen 17096	An open interval is equinumerous to the real numbers. (Contributed by Jim Kingdon, 27-Jun-2024.)
|- ( 0 (,) 1 ) ~~ RR
14.4.8  Analytic omniscience principles Omniscience principles refer to several propositions, most of them weaker than full excluded middle, which do not follow from the axioms of IZF set theory. They are: (0) the Principle of Omniscience (PO), which is another name for excluded middle (see exmidomni 7482), (1) the Limited Principle of Omniscience (LPO) is om e. Omni (see df-omni 7475), (2) the Weak Limited Principle of Omniscience (WLPO) is om e. WOmni (see df-womni 7504), (3) Markov's Principle (MP) is om e. Markov (see df-markov 7492), (4) the Lesser Limited Principle of Omniscience (LLPO) is not yet defined in iset.mm. They also have analytic counterparts each of which follows from the corresponding omniscience principle: (1) Analytic LPO is real number trichotomy, A. x e. RR A. y e. RR ( x < y \/ x = y \/ y < x ) (see trilpo 17104), (2) Analytic WLPO is decidability of real number equality, A. x e. RR A. y e. RRDECID x = y (see redcwlpo 17117), (3) Analytic MP is A. x e. RR A. y e. RR ( x =/= y -> x # y ) (see neapmkv 17130), (4) Analytic LLPO is real number dichotomy, A. x e. RR A. y e. RR ( x <_ y \/ y <_ x ) (most relevant current theorem is maxclpr 11990).
Theorem	trilpolemclim 17097*	Lemma for trilpo 17104. Convergence of the series. (Contributed by Jim Kingdon, 24-Aug-2023.)
|- ( ph -> F : NN --> { 0 , 1 } )   &    |- G = ( n e. NN |-> ( ( 1 / ( 2 ^ n ) ) x. ( F ` n ) ) )   =>    |- ( ph -> seq 1 ( + , G ) e. dom ~~> )
Theorem	trilpolemcl 17098*	Lemma for trilpo 17104. The sum exists. (Contributed by Jim Kingdon, 23-Aug-2023.)
|- ( ph -> F : NN --> { 0 , 1 } )   &    |- A = sum_ i e. NN ( ( 1 / ( 2 ^ i ) ) x. ( F ` i ) )   =>    |- ( ph -> A e. RR )
Theorem	trilpolemisumle 17099*	Lemma for trilpo 17104. An upper bound for the sum of the digits beyond a certain point. (Contributed by Jim Kingdon, 28-Aug-2023.)
|- ( ph -> F : NN --> { 0 , 1 } )   &    |- A = sum_ i e. NN ( ( 1 / ( 2 ^ i ) ) x. ( F ` i ) )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. NN )   =>    |- ( ph -> sum_ i e. Z ( ( 1 / ( 2 ^ i ) ) x. ( F ` i ) ) <_ sum_ i e. Z ( 1 / ( 2 ^ i ) ) )
Theorem	trilpolemgt1 17100*	Lemma for trilpo 17104. The 1 < A case. (Contributed by Jim Kingdon, 23-Aug-2023.)
|- ( ph -> F : NN --> { 0 , 1 } )   &    |- A = sum_ i e. NN ( ( 1 / ( 2 ^ i ) ) x. ( F ` i ) )   =>    |- ( ph -> -. 1 < A )