Metamath Home Intuitionistic Logic Explorer Home Page First >
Last >
Mirrors  >  Home  >  ILE Home  >  Th. List  >  Recent

Created by Mario Carneiro

Intuitionistic Logic Proof Explorer

Intuitionistic Logic (Wikipedia [accessed 19-Jul-2015], Stanford Encyclopedia of Philosophy [accessed 19-Jul-2015]) can be thought of as a constructive logic in which we must build and exhibit concrete examples of objects before we can accept their existence. Unproved statements in intuitionistic logic are not given an intermediate truth value, instead, they remain of unknown truth value until they are either proved or disproved. Intuitionist logic can also be thought of as a weakening of classical logic such that the law of excluded middle (LEM), (φ ¬ φ), doesn't always hold. Specifically, it holds if we have a proof for φ or we have a proof for ¬ φ, but it doesn't necessarily hold if we don't have a proof of either one. There is also no rule for double negation elimination. Brouwer observed in 1908 that LEM was abstracted from finite situations, then extended without justification to statements about infinite collections.


Contents of this page
  • Overview of intuitionistic logic
  • Overview of this work
  • The axioms
  • Some theorems
  • How to intuitionize classical proofs
  • Metamath Proof Explorer cross reference
  • Bibliography
  • Related pages
  • Table of Contents and Theorem List
  • Most Recent Proofs (this mirror) (latest)
  • Bibliographic Cross-Reference
  • Definition List
  • ASCII Equivalents for Text-Only Browsers
  • Metamath database iset.mm (ASCII file)
  • External links
  • GitHub repository [accessed 06-Jan-2018]

  • Overview of intuitionistic logic

    (Placeholder for future use)


    Overview of this work

    (By Gérard Lang, 7-May-2018)

    Mario Carneiro's work (Metamath database) "iset.mm" provides in Metamath a development of "set.mm" whose eventual aim is to show how many of the theorems of set theory and mathematics that can be derived from classical first-order logic can also be derived from a weaker system called "intuitionistic logic." To achieve this task, iset.mm adds (or substitutes) intuitionistic axioms for a number of the classical logical axioms of set.mm.

    Among these new axioms, the first six (ax-ia1, ax-ia2, ax-ia3, ax-io, ax-in1, and ax-in2), when added to ax-1, ax-2, and ax-mp, allow for the development of intuitionistic propositional logic. We omit the classical axiom ((¬ 𝜑 → ¬ 𝜓) → (𝜓𝜑)) (which is ax-3 in set.mm). Each of our new axioms is a theorem of classical propositional logic, but ax-3 cannot be derived from them. Similarly, other basic classical theorems, like the third middle excluded or the equivalence of a proposition with its double negation, cannot be derived in intuitionistic propositional calculus. Glivenko showed that a proposition φ is a theorem of classical propositional calculus if and only if ¬¬φ is a theorem of intuitionistic propositional calculus.

    The next four new axioms (ax-ial, ax-i5r, ax-ie1, and ax-ie2) together with the set.mm axioms ax-4, ax-5, ax-7, and ax-gen do not mention equality or distinct variables.

    The ax-i9 axiom is just a slight variation of the classical ax-9. The classical axiom ax12 is strengthened into first ax-i12 and then ax-bndl (two results which would be fairly readily equivalent to ax12 classically but which do not follow from ax12, at least not in an obvious way, in intuitionistic logic). The substitution of ax-i9, ax-i12, and ax-bndl for ax-9 and ax12 and the inclusion of ax-8, ax-10, ax-11, ax-13, ax-14, and ax-17 allow for the development of the intuitionistic predicate calculus.

    Each of the new axioms is a theorem of classical first-order logic with equality. But some axioms of classical first-order logic with equality, like ax-3, cannot be derived in the intuitionistic predicate calculus.

    One of the major interests of the intuitionistic predicate calculus is that its use can be considered as a realization of the program of the constructivist philosophical view of mathematics.


    The axioms

    As with the classical axioms we have propositional logic and predicate logic.

    The axioms of intuitionistic propositional logic consist of some of the axioms from classical propositional logic, plus additional axioms for the operation of the 'and', 'or' and 'not' connectives.

    Axioms of intuitionistic propositional calculus
    Axiom Simp ax-1 (φ → (ψφ))
    Axiom Frege ax-2 ((φ → (ψχ)) → ((φψ) → (φχ)))
    Rule of Modus Ponens ax-mp 𝜑   &   𝜑𝜓   ⇒   𝜓
    Left 'and' eliminationax-ia1 ((𝜑𝜓) → 𝜑)
    Right 'and' eliminationax-ia2 ((φ ψ) → ψ)
    'And' introductionax-ia3 (φ → (ψ → (φ ψ)))
    Definition of 'or'ax-io (((φ χ) → ψ) ↔ ((φψ) (χψ)))
    'Not' introductionax-in1 ((φ → ¬ φ) → ¬ φ)
    'Not' eliminationax-in2 φ → (φψ))

    Unlike in classical propositional logic, 'and' and 'or' are not readily defined in terms of implication and 'not'. In particular, φψ is not equivalent to ¬ φψ, nor is φψ equivalent to ¬ φψ, nor is φψ equivalent to ¬ (φ → ¬ ψ).

    The ax-in1 axiom is a form of proof by contradiction which does hold intuitionistically. That is, if φ implies a contradiction (such as its own negation), then one can conclude ¬ φ. By contrast, assuming ¬ φ and then deriving a contradiction only serves to prove ¬ ¬ φ, which in intuitionistic logic is not the same as φ.

    The biconditional can be defined as the conjunction of two implications, as in dfbi2 and df-bi.

    Predicate logic adds set variables (individual variables) and the ability to quantify them with ∀ (for-all) and ∃ (there-exists). Unlike in classical logic, ∃ cannot be defined in terms of ∀. As in classical logic, we also add = for equality (which is key to how we handle substitution in metamath) and ∈ (which for current purposes can just be thought of as an arbitrary predicate, but which will later come to mean set membership).

    Our axioms are based on the classical set.mm predicate logic axioms, but adapted for intuitionistic logic, chiefly by adding additional axioms for ∃ and also changing some aspects of how we handle negations.

    Axioms of intuitionistic predicate logic
    Axiom of Specialization ax-4 (xφφ)
    Axiom of Quantified Implication ax-5 (x(φψ) → (xφxψ))
    The converse of ax-5o ax-i5r ((xφxψ) → x(xφψ))
    Axiom of Quantifier Commutation ax-7 (xyφyxφ)
    Rule of Generalization ax-gen φ   =>    xφ
    x is bound in xφ ax-ial (xφxxφ)
    x is bound in xφ ax-ie1 (xφxxφ)
    Define existential quantification ax-ie2 (x(ψxψ) → (x(φψ) ↔ (xφψ)))
    Axiom of Equality ax-8 (x = y → (x = zy = z))
    Axiom of Existence ax-i9 x x = y
    Axiom of Quantifier Substitution ax-10 (x x = yy y = x)
    Axiom of Variable Substitution ax-11 (x = y → (yφx(x = yφ)))
    Axiom of Quantifier Introduction ax-i12 (z z = x (z z = y z(x = yz x = y)))
    Axiom of Bundling ax-bndl (z z = x (z z = y xz(x = yz x = y)))
    Left Membership Equality ax-13 (x = y → (x zy z))
    Right Membership Equality ax-14 (x = y → (z xz y))
    Distinctness ax-17 (φxφ), where x does not occur in φ

    Set theory uses the formalism of propositional and predicate calculus to assert properties of arbitrary mathematical objects called "sets." A set can be an element of another set, and this relationship is indicated by the e. symbol. Starting with the simplest mathematical object, called the empty set, set theory builds up more and more complex structures whose existence follows from the axioms, eventually resulting in extremely complicated sets that we identify with the real numbers and other familiar mathematical objects. These axioms were developed in response to Russell's Paradox, a discovery that revolutionized the foundations of mathematics and logic.

    In the IZF axioms that follow, all set variables are assumed to be distinct. If you click on their links you will see the explicit distinct variable conditions.

    Intuitionistic Zermelo-Fraenkel Set Theory (IZF)
    Axiom of Extensionality ax-ext (z(z xz y) → x = y)
    Axiom of Collection ax-coll (x 𝑎 yφ𝑏x 𝑎 y 𝑏 φ)
    Axiom of Separation ax-sep yx(x y ↔ (x z φ))
    Axiom of Power Sets ax-pow yz(w(w zw x) → z y)
    Axiom of Pairing ax-pr zw((w = x w = y) → w z)
    Axiom of Union ax-un yz(w(z w w x) → z y)
    Axiom of Set Induction ax-setind (𝑎(y 𝑎 [y / 𝑎]φφ) → 𝑎φ)
    Axiom of Infinity ax-iinf x(∅ x y(y x → suc y x))

    We develop set theory based on the Intuitionistic Zermelo-Fraenkel (IZF) system, mostly following the IZF axioms as laid out in [Crosilla]. The one exception to the statement that we use IZF is that a few sections develop set theory using Constructive Zermelo-Fraenkel (CZF), also described in Crosilla. These sections start at wbd (including the section header right before it) and the biggest complication is the machinery to classify formulas as bounded formulas, for purposes of the Axiom of Restricted Separation ax-bdsep.


    A Theorem Sampler   

    From a psychological point of view, learning constructive mathematics is agonizing, for it requires one to first unlearn certain deeply ingrained intuitions and habits acquired during classical mathematical training.
    —Andrej Bauer

    Listed here are some examples of starting points for your journey through the maze. Some are stated just as they would be in a non-constructive context; others are here to highlight areas which look different constructively. You should study some simple proofs from propositional calculus until you get the hang of it. Then try some predicate calculus and finally set theory.

    The Theorem List shows the complete set of theorems in the database. You may also find the Bibliographic Cross-Reference useful.

    Propositional calculus
  • Law of identity idALT
  • Praeclarum theorema anim12
  • Contraposition introduction con3
  • Double negation introduction notnot
  • Triple negation notnotnot
  • Definition of exclusive or df-xor
  • Negation and the false constant dfnot
  • Predicate calculus
  • Existential and universal quantifier swap 19.12
  • Existentially quantified implication 19.35-1
  • x = x equid
  • Definition of proper substitution df-sb
  • Double existential uniqueness 2eu7
  • Set theory
  • Commutative law for union uncom
  • A basic relationship between class and wff variables abeq2
  • Two ways of saying "is a set" isset
  • The ZF axiom of foundation implies excluded middle regexmid
  • Russell's paradox ru
  • Ordinal trichotomy implies excluded middle ordtriexmid
  • Mathematical (finite) induction findes
  • Peano's postulates for arithmetic: peano1 peano2 peano3 peano4 peano5
  • Two natural numbers are either equal or not equal nndceq (a special case of the law of the excluded middle which we can prove).
  • A natural number is either zero or a successor nn0suc
  • The axiom of choice implies excluded middle acexmid
  • Burali-Forti paradox onprc
  • Transfinite induction tfis3
  • Closure law for ordinal addition oacl
  • Real and complex numbers
  • Archimedean property of real numbers arch
  • Properties of apartness: apirr apsym apcotr apti
  • The square root of 2 is irrational sqrt2irrap (a different statement than "The square root of 2 is not rational" sqrt2irr)
  • Convergence of a sequence of complex numbers climcvg1n given a condition on the rate of convergence
  • Triangle inequality for absolute value abstrii
  • The maximum of two real numbers maxleb

  • How to intuitionize classical proofs   

    For the student or master of classical mathematics, constructive mathematics can be baffling. One can get over some of the intial hurdles of understanding how constructive mathematics works and why it might be interesting by reading [Bauer] but that work does little to explain in concrete terms how to write proofs in intuitionistic logic. Fortunately, metamath helps with one of the biggest hurdles: noticing when one is even using the law of the excluded middle or the axiom of choice. But suppose you have a classical proof from the Metamath Proof Explorer and it fails to verify when you copy it over to the Intuitionistic Logic Explorer. What then? Here are some rules of thumb in converting classical proofs to intuitionistic ones.


    Metamath Proof Explorer cross reference   

    This is a list of theorems from the Metamath Proof Explorer (which assumes the law of the excluded middle throughout) which we do not have in the Intuitionistic Logic Explorer (generally because they are not provable without the law of the excluded middle, although some could be proved but aren't for a variety of reasons), together with the closest replacements.

    set.mm iset.mm notes
    ax-3 , con4d , con34b , necon4d , necon4bd con3 The form of contraposition which removes negation does not hold in intuitionistic logic.
    pm2.18 pm2.01 See for example [Bauer] who uses the terminology "proof of negation" versus "proof by contradiction" to distinguish these.
    pm2.18d , pm2.18i pm2.01d See for example [Bauer] who uses the terminology "proof of negation" versus "proof by contradiction" to distinguish these.
    notnotrd , notnotri , notnotr , notnotb notnot Double negation introduction holds but not double negation elimination.
    mt3d mtod
    nsyl2 nsyl
    mt4d mt2d
    nsyl4 con1dc
    pm2.61 , pm2.61d , pm2.61d1 , pm2.61d2 , pm2.61i , pm2.61ii , pm2.61nii , pm2.61iii , pm2.61ian , pm2.61dan , pm2.61ddan , pm2.61dda , pm2.61ine , pm2.61ne , pm2.61dne , pm2.61dane , pm2.61da2ne , pm2.61da3ne , pm2.61iine none If the proposition being eliminated is decidable (for example due to nndceq, zdceq, zdcle, zdclt, eluzdc, or fzdcel), then case elimination will work using theorems such as exmiddc and mpjaodan
    dfbi1 , dfbi3 df-bi, dfbi2
    impcon4bid, con4bid, notbi, con1bii, con4bii, con2bii con3, condc
    xor3 , nbbn xorbin, xornbi, xor3dc, nbbndc
    biass biassdc
    df-or , pm4.64 , pm2.54 , orri , orrd pm2.53, ori, ord, dfordc
    imor , imori imorr, imorri, imordc
    pm4.63 pm3.2im
    iman imanim, imanst
    annim annimim
    oran , pm4.57 oranim, orandc
    ianor pm3.14, ianordc
    pm4.14 pm4.14dc, pm3.37
    pm4.52 pm4.52im
    pm4.53 pm4.53r
    pm5.17 xorbin The combination of df-xor and xorbin is the forward direction of pm5.17
    biluk bilukdc
    biadan biadani The set.mm proof of biadan depends on biluk
    ecase none This is a form of case elimination.
    ecase3d none This is a form of case elimination.
    dedlem0b dedlemb
    pm4.42 pm4.42r
    3ianor 3ianorr
    df-nan and other theorems using NAND (Sheffer stroke) notation none A quick glance at the internet shows this mostly being used in the presence of excluded middle; in any case it is not currently present in iset.mm
    df-xor df-xor Although the definition of exclusive or is called df-xor in both set.mm and iset.mm (at least currently), the definitions are not equivalent (in the absence of excluded middle).
    xnor none The set.mm proof uses theorems not in iset.mm.
    xorass none The set.mm proof uses theorems not in iset.mm.
    xor2 xoranor, xor2dc
    xornan xor2dc
    xornan2 none See discussion under df-nan
    xorneg2 , xorneg1 , xorneg none The set.mm proofs use theorems not in iset.mm.
    xorexmid none A form of excluded middle
    df-ex exalim
    nfd nfd2 the discrepancy should be fixable once we do some renames to get set.mm and iset.mm more in sync for those theorems which are found in both
    alex alexim
    exnal exnalim
    alexn alexnim
    exanali exanaliim
    19.35 , 19.35ri 19.35-1
    19.30 none
    ax6ev a9ev two names for the same theorem
    19.39 i19.39
    19.24 i19.24
    19.36 , 19.36v 19.36-1
    19.37 , 19.37v 19.37-1
    19.32 19.32r
    19.31 19.31r
    exdistrf exdistrfor
    df-mo df-mo The definitions are different although they currently share the same name.
    exmo exmonim
    mof mo2r, mo3
    df-eu , dfeu eu5 Although this is a definition in set.mm and a theorem in iset.mm it is otherwise the same (with a different name).
    eu6 df-eu Although this is a definition in iset.mm and a theorem in set.mm it is otherwise the same (with a different name).
    nfabd2 nfabd
    nne nner, nnedc
    exmidne dcne
    necon1ad necon1addc
    necon1bd necon1bddc
    necon4ad necon4addc
    necon4bd necon4bddc
    necon1d necon1ddc
    necon4d necon4ddc
    necon1ai necon1aidc
    necon1bi necon1bidc
    necon4ai necon4aidc
    necon1i necon1idc
    necon4i necon4idc
    necon4abid necon4abiddc
    necon4bbid necon4bbiddc
    necon4bid necon4biddc, apcon4bid
    necon1abii necon1abiidc
    necon1bbii necon1bbiidc
    necon1abid necon1abiddc
    necon1bbid necon1bbiddc
    necon2abid necon2abiddc
    necon2bbid necon2bbiddc
    necon2abii necon2abiidc
    necon2bbii necon2bbiidc
    nebi nebidc
    pm2.61ne, pm2.61ine, pm2.61dne, pm2.61dane, pm2.61da2ne, pm2.61da3ne pm2.61dc
    neor pm2.53, ori, ord
    neorian pm3.14
    nnel none The reverse direction could be proved; the forward direction is double negation elimination.
    nfrald nfraldw, nfraldya
    rexnal rexnalim
    rexanali none
    nrexralim none
    dfral2 ralexim
    dfrex2 rexalim, dfrex2dc
    nfrexd nfrexdxy, nfrexdya
    nfral nfralxy, nfralya
    nfra2 nfra1, nfralya
    nfrex nfrexxy, nfrexya
    r19.30 r19.30dc
    r19.35 r19.35-1
    ralcom2 ralcom
    2reuswap 2reuswapdc
    rmo2 rmo2i
    df-pss and all proper subclass theorems none In set.mm, "A is a proper subclass of B" is defined to be (𝐴𝐵𝐴𝐵) and this definition is almost always used in conjunction with excluded middle. A more natural definition might be (𝐴𝐵 ∧ ∃𝑥𝑥 ∈ (𝐵𝐴)), if we need proper subclass at all.
    nss nssr
    ddif ddifnel, ddifss
    df-symdif , dfsymdif2 symdifxor The symmetric difference notation and a number of the theorems could be brought over from set.mm.
    dfss4 ssddif, dfss4st
    dfun3 unssin
    dfin3 inssun
    dfin4 inssddif
    unineq none
    difindi difindiss
    difdif2 difdif2ss
    indm indmss
    undif3 undif3ss
    n0f n0rf
    n0 n0r, notm0, fin0, fin0or
    neq0 neq0r
    reximdva0 reximdva0m
    ssdif0 ssdif0im
    inssdif0 inssdif0im
    abn0 abn0r, abn0m
    rabn0 rabn0m, rabn0r
    csb0 csbconstg, csbprc The set.mm proof uses excluded middle to combine the 𝐴 ∈ V and ¬ 𝐴 ∈ V cases.
    sbcel12 sbcel12g
    sbcne12 sbcne12g
    undif1 undif1ss
    undif2 undif2ss
    inundif inundifss
    undif undifss subset rather than equality, for any sets
    undiffi where both container and subset are finite
    undifdc where the container has decidable equality and the subset is finite
    undifdcss when membership in the subset is decidable
    for any sets implies excluded middle as shown at undifexmid
    forward direction only, for any sets still implies excluded middle as shown at exmidundifim
    ssundif ssundifim
    uneqdifeq uneqdifeqim
    r19.2z r19.2m
    r19.3rz r19.3rm
    r19.28z r19.28m
    r19.9rzv r19.9rmv
    r19.37zv r19.3rmv
    r19.45zv r19.45mv
    r19.44zv r19.44mv
    r19.27z r19.27m
    r19.36zv r19.36av
    dfif2 df-if
    ifsb ifsbdc
    dfif4 none Unused in set.mm
    dfif5 none Unused in set.mm
    ifeq1da ifeq1dadc
    ifnot ifnotdc
    ifan ifandc
    ifor ifordc
    ifeq2da none
    ifclda ifcldadc
    ifeqda none
    elimif , ifval , elif , ifel , ifeqor , 2if2 , ifcomnan , csbif , csbifgOLD none
    ifbothda ifbothdadc
    ifboth ifbothdc
    ifid ifidss, ifiddc
    eqif eqifdc
    ifcl , ifcld ifcldcd, ifcldadc
    ifan ifandc
    dedth , dedth2h , dedth3h , dedth4h , dedth2v , dedth3v , dedth4v , elimhyp , elimhyp2v , elimhyp3v , elimhyp4v , elimel , elimdhyp , keephyp , keephyp2v , keephyp3v , keepel none Even in set.mm, the weak deduction theorem is discouraged in favor of theorems in deduction form.
    ifpr none Should be provable if the condition is decidable.
    difsnid difsnss One direction, for any set
    nndifsnid for a natural number
    dcdifsnid for a set with decidable equality
    fidifsnid for a finite set
    pwpw0 pwpw0ss that pwpw0 is equivalent to excluded middle follows from exmidpw or exmid01
    sssn sssnr One direction, for any classes.
    sssnm When the subset is inhabited.
    for all sets Equivalent to excluded middle by exmidsssn.
    ssunsn2 , ssunsn none
    eqsn eqsnm
    ssunpr none
    sspr ssprr
    sstp sstpr
    prnebg none
    pwsn pwsnss Also see exmidpw
    pwpr pwprss
    pwtp pwtpss
    pwpwpw0 pwpwpw0ss
    iundif2 iundif2ss
    iindif2 iindif2m
    iinin2 iinin2m
    iinin1 iinin1m
    iinvdif iindif2m Unused in set.mm
    riinn0 riinm
    riinrab iinrabm
    iunxdif3 none the set.mm proof relies on inundif
    iinuni iinuniss
    iununi iununir
    rintn0 rintm
    disjor disjnim
    disjors disjnims
    disji none
    disjprg , disjxiun , disjxun none
    disjss3 none Might need to be restated or have decidability conditions added
    trintss trintssm
    ax-rep ax-coll There are a lot of ways to state replacement and most/all of them hold, for example zfrep6 or funimaexg.
    csbexg , csbex csbexga, csbexa set.mm uses case elimination to remove the 𝐴 ∈ V condition.
    intex inteximm, intexr inteximm is the forward direction (but for inhabited rather than non-empty classes) and intexr is the reverse direction.
    intexab intexabim
    intexrab intexrabim
    iinexg iinexgm Changes not empty to inhabited
    intabs none Lightly used in set.mm, and the set.mm proof is not intuitionistic
    reuxfr2d , reuxfr2 , reuxfrd , reuxfr none The set.mm proof of reuxfr2d relies on 2reuswap
    moabex euabex In general, most of the set.mm ∃! theorems still hold, but a decent number of the ∃* ones get caught up on "there are two cases: the set exists or it does not"
    snex snexg, snex

    The iset.mm version of snex has an additional hypothesis.

    We conjecture that the set.mm snex ({𝐴} ∈ V with no condition on whether 𝐴 is a set) is not provable.

    The axioms of set theory allow us to construct rank levels from others, but not to construct something from nothing (except the 0 rank and stuff you can bootstrap from there). A class provides no "data" about where it lives, because it is spread out over the whole universe - you only get the ability to ask yes-no(-maybe) questions about set membership in the class. An assertion that a class exists is a piece of data that gives you a bound on the rank of this set, which can be used to build other existing things like unions and powersets of this class and so on. Anything with unbounded rank cannot be proven to exist.

    So snex, which starts from an arbitrary class and produces evidence that { A } exists, cannot be provable, because the bound here can't depend on A and cannot be upper bounded by anything independent of A either - there are singletons at every rank.

    However, we can refute a singleton being a proper class - see notnotsnex.

    prex prexg
    nssss nssssr
    rmorabex euabex See discussion under moabex
    nnullss mss
    opex opexg, opex The iset.mm version of opex has additional hypotheses
    otex otexg
    opnz opm, opnzi
    df-so df-iso Although we define Or to describe a weakly linear order (such as real numbers), there are some orders which are also trichotomous, for example nntri3or, pitri3or, and nqtri3or.
    sotric sotricim One direction, for any weak linear order.
    sotritric For a trichotomous order.
    nntri2 For the specific order E Or ω
    pitric For the specific order <N Or N
    nqtric For the specific order <Q Or Q
    sotrieq sotritrieq For a trichotomous order
    sotrieq2 see sotrieq and then apply ioran
    issoi issod, ispod Many of the set.mm usages of issoi don't carry over, so there is less need for this convenience theorem.
    isso2i issod Presumably this could be proved if we need it.
    df-fr df-frind
    fri , dffr2 , frc none That any subset of the base set has an element which is minimal accordng to a well-founded relation presumably implies excluded middle (or is otherwise unprovable).
    frss freq2 Because the definition of Fr is different than set.mm, the proof would need to be different.
    frirr frirrg We do not yet have a lot of theorems for the case where 𝐴 is a proper class.
    fr2nr none Shouldn't be hard to prove if we need it (using a proof similar to frirrg and en2lp).
    frminex none Presumably unprovable.
    efrn2lp none Should be easy but lightly used in set.mm
    dfepfr , epfrc none Presumably unprovable.
    df-we df-wetr
    wess none See frss entry. Holds for E (see for example wessep).
    weso wepo
    wecmpep none We does not imply trichotomy in iset.mm
    wefrc , wereu , wereu2 none Presumably not provable
    dmxp dmxpm
    relimasn imasng
    xpnz xpm
    xpeq0 xpeq0r, sqxpeq0
    difxp none The set.mm proof relies on ianor
    rnxp rnxpm
    ssxpb ssxpbm
    xp11 xp11m
    xpcan xpcanm
    xpcan2 xpcan2m
    xpima2 xpima2m
    sossfld , sofld , soex none the set.mm proofs rely on trichotomy
    csbrn csbrng
    dmsnn0 dmsnm
    rnsnn0 rnsnm
    relsn2 relsn2m
    dmsnopss dmsnopg The domain is empty in the ¬ 𝐵 ∈ V case which follows readily from opprc2 and dmsn0. But we presumably cannot combine the 𝐵 ∈ V and ¬ 𝐵 ∈ V cases (set.mm uses excluded middle to do so).
    dmsnsnsn dmsnsnsng
    opswap opswapg
    unixp unixpm
    cnvso cnvsom
    unixp0 unixp0im
    unixpid none We could prove the theorem for the case where A is inhabited
    cnviin cnviinm
    xpco xpcom
    xpcoid xpcom
    tz7.5 none The set.mm proof is not intuitionistic. At a minimum, a change from non-empty to inhabited would be needed, but that's probably not sufficient in light of onintexmid.
    tz7.7 none
    ordelssne none
    ordelpss none
    ordsseleq , onsseleq onelss, eqimss, nnsseleq Taken together, onelss and eqimss represent the reverse direction of the biconditional from ordsseleq . For natural numbers the biconditional is provable.
    ordtri3or nntri3or, exmidontriim Ordinal trichotomy implies the law of the excluded middle as shown in ordtriexmid.
    ordtri2 nntri2 ordtri2 for all ordinals presumably implies excluded middle although we don't have a specific proof analogous to ordtriexmid.
    ordtri3 , ordtri4 , ordtri2or3 , dford2 none Ordinal trichotomy implies the law of the excluded middle as shown in ordtriexmid. We don't have similar proofs for every variation of of trichotomy but most of them are presumably powerful enough to imply excluded middle.
    ordtri1 , ontri1 , onssneli , onssnel2i ssnel, nntri1 ssnel is a trichotomy-like theorem which does hold, although it is an implication whereas ordtri1 is a biconditional. nntri1 is biconditional, but just for natural numbers.
    ordtr2 , ontr2 nntr2 ontr2 implies excluded middle as shown at ontr2exmid
    ordtr3 none This is weak linearity of ordinals, which presumably implies excluded middle by ordsoexmid.
    ord0eln0 , on0eln0 ne0i, nn0eln0
    nsuceq0 nsuceq0g
    ordsssuc trsucss, nnsssuc
    ordequn none If you know which ordinal is larger, you can achieve a similar result via theorems such as oneluni or ssequn1.
    ordun onun2
    ordtri2or none Implies excluded middle as shown at ordtri2orexmid.
    ordtri2or2 nntri2or2 ordtri2or2 implies excluded middle as shown at ordtri2or2exmid.
    onsseli none See entry for ordsseleq
    unizlim none The reverse direction is basically uni0 plus limuni
    on0eqel 0elnn The full on0eqel is conjectured to imply excluded middle by an argument similar to ordtriexmid
    snsn0non none Presumably would be provable (by first proving ¬ ∅ ∈ {{∅}} as in the set.mm proof, and then using that to show that {{∅}} is not a transitive set).
    onxpdisj none Unused in set.mm
    onnev none Presumably provable (see snsn0non entry)
    nfiotad nfiotadw
    nfiota nfiotaw
    iotaex iotacl, euiotaex, riotaexg
    iotan0 iotam
    dffun3 dffun5r
    dffun5 dffun5r
    resasplit resasplitss
    fresaun none The set.mm proof relies on resasplit
    fresaunres2 , fresaunres1 none The set.mm proof relies on resasplit
    fint fintm
    foconst none Although it presumably holds if non-empty is changed to inhabited, it would need a new proof and it is unused in set.mm.
    f1oprswap none The 𝐴𝐵 case is handled (basically) by f1oprg. If there is a proof of the original f1oprswap which does not rely on case elimination, it would look very different from the set.mm proof.
    dffv3 dffv3g
    fvex funfvex when evaluating a function within its domain
    fvexg, fvex when the function is a set and is evaluated at a set
    relrnfvex when evaluating a relation whose range is a set
    mptfvex when the function is defined via maps-to, yields a set for all inputs, and is evaluated at a set
    1stexg, 2ndexg for the functions 1st and 2nd
    slotex for a slot of an extensible structure
    fvexi , fvexd see fvex
    fvif fvifdc
    fvrn0 none The set.mm proof uses case elimination on whether (𝐹𝑋) is the empty set.
    fvssunirn fvssunirng, relfvssunirn
    ndmfv ndmfvg The ¬ 𝐴 ∈ V case is fvprc.
    elfvdm relelfvdm
    elfvex , elfvexd relelfvdm, mptrcl
    dffn5 dffn5im
    fvmpti fvmptg The set.mm proof relies on case elimination on 𝐶 ∈ V
    fvmpt2i fvmpt2 The set.mm proof relies on case elimination on 𝐶 ∈ V
    fvmptss fvmptssdm
    fvmptex none The set.mm proof relies on case elimination
    fvmptnf none The set.mm proof relies on case elimination
    fvmptn none The set.mm proof relies on case elimination
    fvmptss2 fvmpt What fvmptss2 adds is the cases where this is a proper class, or we are out of the domain.
    fvopab4ndm none
    fndmdifeq0 none Although it seems like this might be intuitionizable, it is lightly used in set.mm.
    f0cli ffvelrn
    dff3 dff3im
    dff4 dff4im
    fmptsng , fmptsnd none presumably provable
    fvunsn fvunsng
    fnsnsplit fnsnsplitss Subset rather than equality, for a function on any set.
    fnsnsplitdc For a function on a set with decidable equality.
    fsnunf2 none Apparently would need decidable equality on 𝑆 or some other condition.
    funresdfunsn funresdfunsnss Subset rather than equality, for a function on any set.
    funresdfunsndc For a function on a set with decidable equality.
    mptfvmpt fvmptd3 the set.mm proof relies, in an apparently essential way, on fvexi
    funiunfv fniunfv, funiunfvdm
    funiunfvf funiunfvdmf
    eluniima eluniimadm
    dff14a , dff14b none The set.mm proof depends, in an apparently essential way, on excluded middle.
    fveqf1o none The set.mm proof relies on f1oprswap , which we don't have
    soisores isoresbr
    soisoi none The set.mm proof relies on trichotomy
    isocnv3 none It seems possible that one direction of the biconditional could be proved.
    isomin none
    riotaex riotacl, riotaexg
    nfriotad nfriotadxy
    csbriota , csbriotagOLD csbriotag
    riotaxfrd none Although it may be intuitionizable, it is lightly used in set.mm. The set.mm proof relies on reuxfrd .
    ovex fnovex when the operation is a function evaluated within its domain.
    ovexg when the operation is a set and is evaluated at a set
    relrnfvex when the operation is a relation whose range is a set
    mpofvex When the operation is defined via maps-to, yields a set on any inputs, and is being evaluated at two sets.
    addcl, expcl, etc If there is a closure theorem for a particular operation, that is often the way to intuitionize ovex (check for your particular operation, as these are just a few examples).
    ovrcl elmpocl, relelfvdm
    opabresex2d none it should be possible to update iset.mm to reflect set.mm in this area and related theorems
    0mpo0 mpo0 should be provable
    ovif12 none would be provable under the condition that 𝜑 is decidable
    fnov fnovim
    ov3 ovi3 Although set.mm's ov3 could be proved, it is only used a few places in set.mm, and in iset.mm those places need the modified form found in ovi3.
    oprssdm oprssdmm
    ndmovg , ndmov ndmfvg These theorems are generally used in set.mm for case elimination which is why we just have the general ndmfvg rather than an operation-specific version.
    ndmovcl , ndmovcom , ndmovass , ndmovdistr , ndmovord , and ndmovordi none These theorems are generally used in set.mm for case elimination and the most straightforward way to avoid them is to add conditions that we are evaluating functions within their domains.
    ndmovrcl elmpocl, relelfvdm
    caov4 caov4d Note that caov4d has a closure hypothesis.
    caov411 caov411d Note that caov411d has a closure hypothesis.
    caov42 caov42d Note that caov42d has a closure hypothesis.
    caovdir caovdird caovdird adds some constraints about where the operations are evaluated.
    caovdilem caovdilemd
    caovlem2 caovlem2d
    caovmo caovimo
    mpondm0 none could be proved, but usually is used in conjunction with excluded middle
    elovmporab none could be proved, but unused in set.mm
    elovmporab1 none could be proved
    2mpo0 none Possibly provable, but an inhabited set version would be more likely to be helpful (if anything is).
    relmptopab none Presumably would need a condition that 𝐵 ∈ dom 𝐹
    ofval ofvalg
    offn off the set.mm proof of offn uses ovex and it isn't clear whether anything can be proved with weaker hypotheses than off
    offveq offeq
    caofid0l , caofid0r , caofid1 , caofid2 none Assuming we really need to add conditions that the operations are functions being evaluated within their domains, there would be a fair bit of intuitionizing.
    ordeleqon none
    ssonprc none not provable (we conjecture), but interesting enough to intuitionize anyway. 𝐴 = On → 𝐴𝑉 is provable, and (𝐵 ∈ On ∧ 𝐴𝐵) → 𝐴𝑉 is provable. (One thing we presumably could prove is ( 𝐴 ⊆ On ∧ ∃𝑥𝑥 ∈ (On ∖ 𝐴)) → 𝐴𝑉 which might be easier to understand if we define (or think of) proper subset as meaning that the set difference is inhabited.)
    onint onintss, nnmindc onint implies excluded middle as shown in onintexmid.
    onint0 none Thought to be "trivially not intuitionistic", and it is not clear if there is an alternate way to state it that is true. If the empty set is in A then of course |^| A = (/), but the converse seems difficult. I don't know so much about the structure of the ordinals without linearity,
    onssmin, onminesb, onminsb none Conjectured to not be provable without excluded middle, for the same reason as onint.
    oninton onintonm
    onintrab none The set.mm proof relies on the converse of inteximm.
    onintrab2 onintrab2im The converse would appear to need the converse of inteximm.
    oneqmin none Falls as written because it implies onint, but it might be useful to keep the reverse direction for subsets that do have a minimum.
    onminex none
    onmindif2 none Conjectured to not be provable without excluded middle.
    onmindif2 none Conjectured to not be provable without excluded middle.
    ordpwsuc ordpwsucss See the ordpwsucss comment for discussion of the succcessor-like properites of (𝒫 𝐴 ∩ On). Full ordpwsuc implies excluded middle as seen at ordpwsucexmid.
    ordsucelsuc onsucelsucr, nnsucelsuc The converse of onsucelsucr implies excluded middle, as shown at onsucelsucexmid.
    ordsucsssuc onsucsssucr, nnsucsssuc The converse of onsucsssucr implies excluded middle, as shown at onsucsssucexmid.
    ordsucuniel sucunielr, nnsucuniel Full ordsucuniel implies excluded middle, as shown at ordsucunielexmid.
    ordsucun none yet Conjectured to be provable in the reverse direction, but not the forward direction (implies some order totality).
    ordunpr none Presumably not provable without excluded middle.
    ordunel none Conjectured to not be provable (ordunel implies ordsucun).
    onsucuni, ordsucuni none Conjectured to not be provable without excluded middle.
    orduniorsuc none Presumably not provable.
    ordunisuc onunisuci, unisuc, unisucg
    orduniss2 onuniss2
    0elsuc none This theorem may appear to be innocuous but it implies excluded middle as shown at 0elsucexmid.
    onuniorsuci none Conjectured to not be provable without excluded middle.
    onuninsuci, orduninsuc none Conjectured to be provable in the forward direction but not the reverse one.
    ordunisuc2 ordunisuc2r

    The forward direction is conjectured to imply excluded middle. Here is a sketch of the proposed proof.

    Let om' be the set of all finite iterations of suc' A = (𝒫 𝐴 ∩ On) on . (We can formalize this proof but not until we have om and at least finite induction.) Then om' = U. om' because if x e. om' then x = suc'^n (/) for some n, and then x C_ suc'^n (/) implies x e. suc'^(n+1) (/) e. om' so x e. U. om'.

    Now supposing the theorem, we know that A. x e. om' suc x e. om', so in particular 2o e. om', that is, 2o = suc'^n (/) for some n. (Note that 1o = suc' (/) - see pw0.) For n = 0 and n = 1 this is clearly false, and for n = m+3 we have 1o e. suc' suc' (/) , so 2o C_ suc' suc' (/), so 2o e. suc' suc' suc' (/) C_ suc' suc' suc' suc'^m (/) = 2o, contradicting ordirr.

    Thus 2o = suc' suc' (/) = suc' 1o. Applying this to X = {𝑥 ∈ {∅} ∣ 𝜑} we have X C_ 1o implies X e. suc' 1o = 2o and hence X = (/) \/ X = 1o, and LEM follows (by ordtriexmidlem2 for 𝑋 = ∅ and rabsnt as seen in the onsucsssucexmid proof for 𝑋 = 1o).

    ordzsl, onzsl, dflim3, nlimon none
    dflim4 df-ilim We conjecture that dflim4 is not equivalent to df-ilim.
    limsuc none This would be trivial if dflim4 were the definition of a limit ordinal. With dflim2 as the definition, limsuc might need ordunisuc2 (which we believe is not provable, see ordunisuc2 entry).
    limsssuc none Conjectured to be provable (is this also based on dflim4 being the definition of limit ordinal or is it unrelated?).
    tfinds , tfindsg , tfindsg2 , tfindes , tfinds2 , tfinds3 tfis3 We are unable to separate limit and successor ordinals using case elimination.
    df-om df-iom
    findsg uzind4 findsg presumably could be proved, but there hasn't been a need for it.
    xpexr none
    xpexr2 xpexr2m
    xpexcnv none would be provable if nonempty is changed to inhabited
    1stval 1stvalg
    2ndval 2ndvalg
    1stnpr none May be intuitionizable, but very lightly used in set.mm.
    2ndnpr none May be intuitionizable, but very lightly used in set.mm.
    mptmpoopabbrd none it should be possible to update iset.mm to reflect set.mm in this area and related theorems
    mptmpoopabovd none it should be possible to update iset.mm to reflect set.mm in this area and related theorems
    el2mpocsbcl none the set.mm proof uses excluded middle
    el2mpocl none the set.mm proof uses el2mpocsbcl
    ovmptss none The set.mm proof relies on fvmptss
    mposn none presumably provable
    relmpoopab none The set.mm proof relies on ovmptss
    mpoxeldm none presumably provable
    mpoxneldm none presumably provable
    mpoxopynvov0g none presumably provable
    mpoxopxnop0 none presumably provable
    mpoxopx0ov0 none presumably provable
    mpoxopxprcov0 none presumably provable
    mpoxopynvov0 none
    mpoxopoveqd none unused in set.mm
    brovmpoex none unused in set.mm
    sprmpod none unused in set.mm
    brtpos brtposg
    ottpos ottposg
    ovtpos ovtposg
    df-cur , df-unc and all theorems using the curry and uncurry syntaxes none presumably could be added with only the usual issues around nonempty versus inhabited and the like
    pwuninel pwuninel2 The set.mm proof of pwuninel uses case elimination.
    iunonOLD iunon
    smofvon2 smofvon2dm
    tfr1 tfri1
    tfr2 tfri2
    tfr3 tfri3
    tfr2b , recsfnon , recsval none These transfinite recursion theorems are lightly used in set.mm.
    df-rdg df-irdg This definition combines the successor and limit cases (rather than specifying them as separate cases in a way which relies on excluded middle). In the words of [Crosilla], p. "Set-theoretic principles incompatible with intuitionistic logic", "we can still define many of the familiar set-theoretic operations by transfinite recursion on ordinals (see Aczel and Rathjen 2001, Section 4.2). This is fine as long as the definitions by transfinite recursion do not make case distinctions such as in the classical ordinal cases of successor and limit."
    rdgfnon rdgifnon
    ordge1n0 ordge1n0im, ordgt0ge1
    ondif1 dif1o In set.mm, ondif1 is used for Cantor Normal Form
    ondif2 , dif20el none The set.mm proof is not intuitionistic
    brwitnlem none The set.mm proof is not intuitionistic
    om0r om0, nnm0r
    om00 nnm00
    om00el none
    omopth2 none The set.mm proof relies on ordinal trichotomy.
    omeulem1 , omeu none The set.mm proof relies on ordinal trichotomy, omopth2 , oaord , and other theorems we don't have.
    suc11reg suc11g
    frfnom frecfnom frecfnom adopts the frec notation and adds conditions on the characteristic function and initial value.
    fr0g frec0g frec0g adopts the frec notation and adds a condition on the characteristic function.
    frsuc frecsuc frecsuc adopts the frec notation and adds conditions on the characteristic function and initial value.
    om0x om0
    oa0r none The set.mm proof distinguishes between limit and successor cases using case elimination.
    oaordi nnaordi The set.mm proof of oaordi relies on being able to distinguish between limit ordinals and successor ordinals via case elimination.
    oaord nnaord The set.mm proof of oaord relies on ordinal trichotomy.
    oawordri none Implies excluded middle as shown at oawordriexmid
    oaword oawordi The other direction presumably could be proven but isn't yet.
    oaord1 none yet
    oaword2 none The set.mm proof relies on oawordri and oa0r
    oawordeu none The set.mm proof relies on a number of things we don't have
    oawordex nnawordex The set.mm proof relies on oawordeu
    omwordi nnmword The set.mm proof of omwordi relies on case elimination.
    omword1 nnmword
    oawordex nnawordex
    oarec none the set.mm proof relies on tfinds3
    oaf1o none the set.mm proof uses ontri1 and oawordeu
    oacomf1o , oacomf1olem none the set.mm proof relies on oarec and oaf1o
    swoso none Unused in set.mm.
    ecdmn0 ecdmn0m
    erdisj, qsdisj, qsdisj2, uniinqs none These could presumably be restated to be provable, but they are lightly used in set.mm
    iiner iinerm
    riiner riinerm
    brecop2 none This is a form of reverse closure and uses excluded middle in its proof.
    erov , erov2 none Unused in set.mm.
    eceqoveq none Unused in set.mm.
    ralxpmap none Lightly used in set.mm. The set.mm proof relies on fnsnsplit and undif .
    nfixp nfixpxy, nfixp1 set.mm (indirectly) uses excluded middle to combine the cases where 𝑥 and 𝑦 are distinct and where they are not.
    ixpexg ixpexgg
    ixpiin ixpiinm
    ixpint ixpintm
    ixpn0 ixpm
    undifixp none The set.mm proof relies on undif
    resixpfo none The set.mm proof relies on membership in 𝐵 being decidable and would need to have nonempty changed to inhabited, but might be adaptable with those conditions added. However, this theorem is currently only used in the proof of Tychonoff's Theorem, which we do not expect to be able to prove.
    boxriin none Would seem to need a condition that 𝐼 has decidable equality.
    boxcutc none Would seem to need a condition that 𝐴 has decidable equality.
    df-sdom , relsdom , brsdom , dfdom2 , sdomdom , sdomnen , brdom2 , bren2 , domdifsn none Many aspects of strict dominance as developed in set.mm rely on excluded middle and a different definition would be needed if we wanted strict dominance to have the expected properties.
    en1b en1bg
    snfi snfig
    difsnen fidifsnen
    undom none The set.mm proof uses undif2 and we just have undif2ss
    xpdom3 xpdom3m
    domunsncan none The set.mm proof relies on difsnen
    omxpenlem , omxpen , omf1o none The set.mm proof relies on omwordi , oaord , om0r , and other theorems we do not have
    pw2f1o , pw2eng , pw2en none Presumably would require some kind of decidability hypothesis. Discussions of this sort tend to get into how many truth values there are and sets like {𝑠𝑠 ⊆ 1o} (relatively undeveloped so far except for a few results like exmid01 and uni0b).
    enfixsn none The set.mm proof relies on difsnen
    sbth and its lemmas, sbthb , sbthcl fisbth The Schroeder-Bernstein Theorem is equivalent to excluded middle by exmidsbth
    fodomr none Equivalent to excluded middle per exmidfodomr
    mapdom1 mapdom1g
    2pwuninel 2pwuninelg
    mapunen none The set.mm proof relies on fresaunres1 and fresaunres2 .
    map2xp none The set.mm proof relies on mapunen
    mapdom2 , mapdom3 none The set.mm proof relies on case elimination and undif . At a minimum, it would appear that nonempty would need to be changed to inhabited.
    pwen none The set.mm proof relies on pw2eng
    limenpsi none The set.mm proof relies on sbth
    limensuci , limensuc none The set.mm proof relies on undif
    infensuc none The set.mm proof relies on limensuc
    php phpm
    snnen2o snnen2og, snnen2oprc
    onomeneq , onfin none Not possible because they would imply onfin2
    onfin2 none Implies excluded middle as shown as exmidonfin
    nnsdomo , sucdom2 , sucdom , 0sdom1dom , sdom1 none iset.mm doesn't yet have strict dominance
    1sdom2 1nen2 Although the presence of 1nen2 might make it look like a natural definition for strict dominance would be 𝐴𝐵 ∧ ¬ 𝐴𝐵, that definition may be more suitable for finite sets than all sets, so at least for now we only define and express certain theorems (such as this one) in terms of equinumerosity which in set.mm are expressed in terms of strict dominance.
    modom , modom2 none The set.mm proofs rely on excluded middle
    1sdom , unxpdom , unxpdom2 , sucxpdom none iset.mm doesn't yet have strict dominance
    pssinf none The set.mm proof relies on sdomnen
    isinf isinfinf
    fineqv none The set.mm proof relies on theorems we don't have, and even for the theorems we do have, we'd need to carefully look at what axioms they rely on.
    pssnn none The set.mm proof uses excluded middle.
    ssnnfi none The proof in ssfiexmid would apply to this as well as to ssfi , since {∅} ∈ ω
    ssfi ssfirab when the subset is defined by a decidable property
    ssfidc when membership in the subset is decidable
    for the general case Implies excluded middle as shown at ssfiexmid
    domfi none Implies excluded middle as shown at domfiexmid
    xpfir none Nonempty would need to be changed to inhabited, but the set.mm proof also uses domfi
    infi none Implies excluded middle as shown at infiexmid. It is conjectured that we could prove the special case (𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ (𝐴𝐵) ∈ Fin) → (𝐴𝐵) ∈ Fin
    rabfi none Presumably the proof of ssfiexmid could be adapted to show this implies excluded middle
    finresfin none The set.mm proof is in terms of ssfi
    f1finf1o none The set.mm proof is not intuitionistic
    nfielex none The set.mm proof relies on neq0
    diffi diffisn, diffifi diffi is not provable, as shown at diffitest
    enp1ilem , enp1i , en2 , en3 , en4 none The set.mm proof relies on excluded middle and undif1
    findcard3 none The set.mm proof is in terms of strict dominance.
    frfi none Not known whether this can be proved (either with the current df-frind or any other possible concept analogous to Fr).
    fimax2g fimax2gtri
    fimaxg none The set.mm proof of fimaxg relies on fimax2g which relies on frfi and fri
    fisupg none The set.mm proof relies on excluded middle and presumably this theorem would need to be modified to be provable.
    unbnn unbendc the impossibility proof at exmidunben should apply here as well
    unbnn2 unbendc the impossibility proof at exmidunben should apply here as well
    unfi unsnfi For the union of a set and a singleton whose element is not a member of that set
    unfidisj For the union of two disjoint sets
    unfiin When the intersection is known to be finite
    for any two finite sets Implies excluded middle as shown at unfiexmid.
    difinf difinfinf
    prfi prfidisj for two unequal sets
    in general The set.mm proof depends on unfi and it would appear that mapping {𝐴, 𝐵} to a natural number would decide whether 𝐴 and 𝐵 are equal and thus imply any set has decidable equality.
    tpfi tpfidisj
    fiint fiintim
    fodomfi none Might be provable, for example via ac6sfi or induction directly. The set.mm proof does use undom in addition to induction.
    fofinf1o none The set.mm proof uses excluded middle in several places.
    dmfi fundmfi
    resfnfinfin resfnfinfinss
    residfi none Presumably provable, but lightly used in set.mm
    cnvfi relcnvfi
    rnfi funrnfi
    fofi f1ofi Presumably precluded by an argument similar to domfiexmid (the set.mm proof relies on domfi).
    iunfi iunfidisj for a disjoint collection
    in general Presumably not possible for the same reasons as in unfiexmid
    unifi none Presumably the issues are similar to iunfi
    pwfi none The set.mm proof uses domfi and other theorems we don't have
    abrexfi none At first glance it would appear that the mapping would need to be one to one or some other condition.
    fisuppfi preimaf1ofi The set.mm proof of fisuppfi uses ssfi
    intrnfi none presumably not provable; the set.mm proof uses fofi
    iinfi none presumably not provable; the set.mm proof uses intrnfi
    inelfi none may need a condition such as 𝐴𝐵; the set.mm proof uses prfi
    fiin none presumably needs a condition analogous to those in unfidisj or unfiin; the set.mm proof uses unfi
    dffi2 none the set.mm proof uses fiin and other theorems we do not have
    inficl none the set.mm proof uses fiin and dffi2 (see also inelfi which might be relevant)
    fipwuni none would need a 𝐴 ∈ V condition but even with that, the set.mm proof uses inficl
    fisn none presumably would be provable (with an 𝐴 ∈ V condition added), but the set.mm proof uses inficl
    fipwss fipwssg adds the condition that 𝐴 is a set
    elfiun none the set.mm proof uses ssfi , fiin , and excluded middle
    dffi3 none might be possible (perhaps using df-frec notation), but the set.mm proof does not work as-is
    dfsup2 none The set.mm proof uses excluded middle in several places and the theorem is lightly used in set.mm.
    supmo supmoti The conditions on the order are different.
    supexd , supex supex2g The set.mm proof of supexd uses rmorabex
    supeu supeuti
    supval2 supval2ti
    eqsup eqsupti
    eqsupd eqsuptid
    supcl supclti
    supub supubti
    suplub suplubti
    suplub2 suplub2ti
    supnub none Presumably provable, although the set.mm proof relies on excluded middle and it is not used until later in set.mm.
    sup0riota , sup0 , infempty none Suitably modified verions may be provable, but they are unused in set.mm.
    supmax supmaxti
    fisup2g , fisupcl none Other variations may be possible, but the set.mm proof will not work as-is or with small modifications.
    supgtoreq none The set.mm proof uses fisup2g and also trichotomy.
    suppr none The formulation using if would seem to require a trichotomous order. For real numbers, supremum on a pair does yield the maximum of two numbers: see maxcl, maxle1, maxle2, maxleast, and maxleb.
    supiso supisoti
    infexd , infex infex2g
    eqinf , eqinfd eqinfti, eqinftid
    infval infvalti
    infcllem cnvinfex infcllem has an unnecessary hypothesis; other than that these are the same
    infcl infclti
    inflb inflbti
    infglb infglbti
    infglbb none Presumably provable with additional conditions (see suplub2)
    infnlb infnlbti
    infmin infminti
    infmo infmoti
    infeu infeuti
    fimin2g , fiming none The set.mm proof relies on frfi and fri
    fiinfg , fiinf2g none The set.mm proof relies on fiming
    fiinfcl none See fisupcl
    infltoreq none The set.mm proof depends on supgtoreq and fiinfcl
    infpr none See suppr
    infsn infsnti
    infiso infisoti
    ax-reg , axreg2 , zfregcl ax-setind ax-reg implies excluded middle as seen at regexmid
    ax-inf , zfinf , axinf2 , axinf ax-iinf, zfinf2 probably most of the variations of the axiom of infinity in set.mm could be shown to be equivalent to each other in iset.mm as well
    inf5 none as this is in terms of proper subset it is unlikely to work well in iset.mm
    elom3 , dfom4 , dfom5 none the set.mm theorems depend on theorems we do not have
    oancom none presumably provable but the set.mm proof does not work as-is
    isfinite fict
    omenps , omensuc none presumably provable but the set.mm proofs do not work as-is
    infdifsn none possibly provable with added 𝑥𝐴𝑦𝐴DECID 𝑥 = 𝑦 and 𝐵𝐴 conditions, for example via a technique analogous to difinfsn
    infdiffi none if we can prove a version of infdifsn it should carry over from singletons to finite sets, much the way difinfinf follows from difinfsn
    unbnn3 unbendc the impossibility proof at exmidunben should apply here as well
    noinfep none the set.mm proof uses fri
    df-rank and all theorems related to the rank function none One possible definition is Definition 9.3.4 of [AczelRathjen], p. 91
    df-aleph and all theorems involving aleph none
    df-cf and all theorems involving cofinality none
    df-acn and all theorems using this definition none
    cardf2 , cardon , isnum2 cardcl, isnumi It would also be easy to prove Fun card if there is a need.
    ennum none The set.mm proof relies on isnum2
    tskwe none Relies on df-sdom
    xpnum none The set.mm proof relies on isnum2
    cardval3 cardval3ex
    cardid2 none The set.mm proof relies on onint
    isnum3 none
    oncardid none The set.mm proof relies on cardid2
    cardidm none Presumably this would need a condition on 𝐴 but even with that, the set.mm proof relies on cardid2
    oncard none The set.mm proof relies on theorems we don't have, and this theorem is unused in set.mm.
    ficardom none Presumably not possible for the same reasons as onfin2
    ficardid none The set.mm proof relies on cardid2
    cardnn none The set.mm proof relies on a variety of theorems we don't have currently.
    cardnueq0 none The set.mm proof relies on cardid2
    cardne none The set.mm proof relies on ordinal trichotomy (and if that can be solved there might be some more minor problems which require revisions to the theorem)
    carden2a none The set.mm proof relies on excluded middle.
    carden2b carden2bex
    card1 , cardsn none Rely on a variety of theorems we don't currently have. Lightly used in set.mm.
    carddomi2 none The set.mm proof relies on excluded middle.
    sdomsdomcardi none Relies on a variety of theorems we don't currently have.
    prdom2 none The set.mm proof would only work in the case where 𝐴 = 𝐵 is decidable. If we can prove fodomfi , that would appear to imply prsomd2 fairly quickly.
    dif1card none The set.mm proof relies on cardennn
    leweon none We lack the well ordering related theorems this relies on, and it isn't clear they are provable.
    r0weon none We lack the well ordering related theorems this relies on, and it isn't clear they are provable.
    infxpen none The set.mm proof relies on well ordering related theorems that we don't have (and may not be able to have), and it isn't clear that infxpen is provable.
    infxpidm2 none Depends on cardinality theorems we don't have.
    infxpenc none Relies on notations and theorems we don't have.
    infxpenc2 none Relies on theorems we don't have.
    dfac8a none The set.mm proof does not work as-is and numerability may not be able to work the same way.
    dfac8b none We are lacking much of what this proof relies on and we may not be able to make numerability and well-ordering work as in set.mm.
    dfac8c none The set.mm proof does not work as-is and well-ordering may not be able to work the same way.
    ac10ct none The set.mm proof does not work as-is and well-ordering may not be able to work the same way.
    ween none The set.mm proof does not work as-is and well-ordering and numerability may not be able to work the same way.
    ac5num , ondomen , numdom , ssnum , onssnum , indcardi none Numerability (or cardinality in general) is not well developed and to a certain extent cannot be.
    undjudom none The set.mm proof relies on undom
    dju1dif none presumably provable
    mapdjuen none the set.mm proof relies on mapunen
    pwdjuen none the set.mm proof relies on mapdjuen
    djudom1 none the set.mm proof relies on undom
    djudom2 none the set.mm proof relies on djudom1
    djuxpdom none presumably provable if having cardinality greater than one is expressed as 2o𝐴 instead
    djufi none we should be able to prove (𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴𝐵) ∈ Fin
    cdainflem , djuinf none the set.mm proof is not easily adapted
    infdju1 none the set.mm proof relies on infdifsn
    pwdju1 none the set.mm proof relies on pwdjuen and pwpw0
    pwdjuidm none the set.mm proof relies on infdju1 and pwdju1
    djulepw none
    onadju none the set.mm proof uses oacomf1olem and oarec
    cardadju none the set.mm proof uses cardon , onadju , and cardid2
    djunum none the set.mm proof uses cardon and cardadju
    unnum none the set.mm proof uses djunum , numdom , and undjudom
    nnadju none depends on various cardinality theorems we don't have
    ficardun none depends on various cardinality theorems we don't have
    ficardun2 none depends on various cardinality theorems we don't have
    pwsdompw none depends on various cardinality theorems we don't have
    unctb unct
    infdjuabs none the set.mm proof uses sbth and other theorems we don't have
    infunabs none the set.mm proof uses undjudom and infdjuabs
    infdju none the set.mm proof uses sbth and other theorems we don't have
    infdif none the set.mm proof uses sbth and other theorems we don't have
    pwdjudom none
    ax-cc cc1
    axcc2 cc2
    axcc3 cc3
    axcc4 cc4
    fodom , fodomnum none Presumably not provable as stated
    fodomb none That the reverse direction is equivalent to excluded middle is exmidfodomr. The forward direction is presumably also not provable.
    entri3 fientri3 Because full entri3 is equivalent to the axiom of choice, it implies excluded middle.
    infinf infnfi Defining "A is infinite" as ω ≼ 𝐴 follows definition 8.1.4 of [AczelRathjen], p. 71. It can presumably not be shown to be equivalent to ¬ 𝐴 ∈ Fin in the absence of excluded middle (see inffiexmid which isn't exactly about ¬ 𝐴 ∈ Fin ↔ ω ≼ 𝐴 but which is close).
    df-wina , df-ina , df-tsk , df-gru , ax-groth and all theorems related to inaccessibles and large cardinals none For an introduction to inaccessibles and large set properties see Chapter 18 of [AczelRathjen], p. 165 (including why "large set properties" is more apt terminology than "large cardinal properties" in the absence of excluded middle).
    df-wun and all weak universe theorems none
    addcompi addcompig
    addasspi addasspig
    mulcompi mulcompig
    mulasspi mulasspig
    distrpi distrpig
    addcanpi addcanpig
    mulcanpi mulcanpig
    addnidpi addnidpig
    ltapi ltapig
    ltmpi ltmpig
    nlt1pi nlt1pig
    df-nq df-nqqs
    df-nq df-nqqs
    df-erq none Not needed given df-nqqs
    df-plq df-plqqs
    df-mq df-mqqs
    df-1nq df-1nqqs
    df-ltnq df-ltnqqs
    elpqn none Not needed given df-nqqs
    ordpipq ordpipqqs
    addnqf dmaddpq, addclnq It should be possible to prove that +Q is a function, but so far there hasn't been a need to do so.
    addcomnq addcomnqg
    mulcomnq mulcomnqg
    mulassnq mulassnqg
    recmulnq recmulnqg
    ltanq ltanqg
    ltmnq ltmnqg
    ltexnq ltexnqq
    archnq archnqq
    df-np df-inp
    df-1p df-i1p
    df-plp df-iplp
    df-ltp df-iltp
    elnp , elnpi elinp
    prn0 prml, prmu
    prpssnq prssnql, prssnqu
    elprnq elprnql, elprnqu
    prcdnq prcdnql, prcunqu
    prub prubl
    prnmax prnmaxl
    npomex none
    prnmadd prnmaddl
    genpv genipv
    genpcd genpcdl
    genpnmax genprndl
    ltrnq ltrnqg, ltrnqi
    genpcl addclpr, mulclpr
    genpass genpassg
    addclprlem1 addnqprllem, addnqprulem
    addclprlem2 addnqprl, addnqpru
    plpv plpvlu
    mpv mpvlu
    nqpr nqprlu
    mulclprlem mulnqprl, mulnqpru
    addcompr addcomprg
    addasspr addassprg
    mulcompr mulcomprg
    mulasspr mulassprg
    distrlem1pr distrlem1prl, distrlem1pru
    distrlem4pr distrlem4prl, distrlem4pru
    distrlem5pr distrlem5prl, distrlem5pru
    distrpr distrprg
    ltprord ltprordil There hasn't yet been a need to investigate versions which are biconditional or which involve proper subsets.
    psslinpr ltsopr
    prlem934 prarloc2
    ltaddpr2 ltaddpr
    ltexprlem1 , ltexprlem2 , ltexprlem3 , ltexprlem4 none See the lemmas for ltexpri generally.
    ltexprlem5 ltexprlempr
    ltexprlem6 ltexprlemfl, ltexprlemfu
    ltexprlem7 ltexprlemrl, ltexprlemru
    ltapr ltaprg
    addcanpr addcanprg
    prlem936 prmuloc2
    reclem2pr recexprlempr
    reclem3pr recexprlem1ssl, recexprlem1ssu
    reclem4pr recexprlemss1l, recexprlemss1u, recexprlemex
    supexpr suplocexpr also see caucvgprpr but completeness cannot be formulated as in set.mm without changes
    mulcmpblnrlem mulcmpblnrlemg
    ltsrpr ltsrprg
    dmaddsr , dmmulsr none Although these presumably could be proved in a way similar to dmaddpq and dmmulpq (in fact dmaddpqlem would seem to be easily generalizable to anything of the form ((𝑆 × 𝑇) / 𝑅)), we haven't yet had a need to do so.
    addcomsr addcomsrg
    addasssr addasssrg
    mulcomsr mulcomsrg
    mulasssr mulasssrg
    distrsr distrsrg
    ltasr ltasrg
    sqgt0sr mulgt0sr, apsqgt0
    recexsr recexsrlem This would follow from sqgt0sr (as in the set.mm proof of recexsr), but "not equal to zero" would need to be changed to "apart from zero".
    mappsrpr mappsrprg
    ltpsrpr ltpsrprg
    map2psrpr map2psrprg
    supsr suplocsr also see caucvgsr
    ax1ne0 , ax-1ne0 ax0lt1, ax-0lt1, 1ap0, 1ne0
    axrrecex , ax-rrecex axprecex, ax-precex
    axpre-lttri , ax-pre-lttri axpre-ltirr, axpre-ltwlin, ax-pre-ltirr, ax-pre-ltwlin
    axpre-sup , ax-pre-sup axpre-suploc, ax-pre-suploc
    axsup axsuploc
    elimne0 none Even in set.mm, the weak deduction theorem is discouraged in favor of theorems in deduction form.
    xrltnle xrlenlt
    ssxr df-xr Lightly used in set.mm
    ltnle , ltnlei , ltnled lenlt, zltnle
    lttri2 , lttri2i , lttri2d qlttri2 Real number trichotomy is not provable.
    lttri4 ztri3or, qtri3or Real number trichotomy is not provable.
    leloe , leloei , leloed none
    leltne , leltned leltap, leltapd
    ltneOLD ltne, ltap
    letric , letrii , letrid zletric, qletric
    ltlen , ltleni , ltlend ltleap, zltlen, qltlen
    ne0gt0 , ne0gt0d ap0gt0, ap0gt0d
    lecasei zletric or qletric (plus mpjaodan) 𝑥 ∈ ℝ∀𝑦 ∈ ℝ(𝑥𝑦𝑦𝑥) is known as the analytic lesser limited principle of omniscience and is not provable from IZF axioms
    ltlecasei none Would need one of the analytic omniscience principles
    lelttric zlelttric, qlelttric
    lttrid , lttri4d none These are real number trichotomy
    leneltd leltapd
    dedekind , dedekindle dedekindeu various details are different including that in dedekindeu the lower and upper cuts have to be open (and thus the real corresponding to the Dedekind cut is not contained in either the lower or upper cut)
    mul02lem1 none The one use in set.mm is not needed in iset.mm.
    negex negcl
    msqgt0 , msqgt0i , msqgt0d apsqgt0 "Not equal to zero" is changed to "apart from zero"
    relin01 none Relies on real number trichotomy.
    ltord1 , leord1 , ltord2 , leord2 none The set.mm proof relies on real number trichotomy.
    wloglei , wlogle none These depend on real number trichotomy and are not used until later in set.mm.
    recex recexap In theorems involving reciprocals or division, not equal to zero changes to apart from zero.
    mulcand, mulcan2d mulcanapd, mulcanap2d In theorems involving reciprocals or division, not equal to zero changes to apart from zero.
    mulcanad , mulcan2ad mulcanapad, mulcanap2ad In theorems involving reciprocals or division, not equal to zero changes to apart from zero.
    mulcan , mulcan2 , mulcani mulcanap, mulcanap2, mulcanapi In theorems involving reciprocals or division, not equal to zero changes to apart from zero.
    mul0or , mul0ori , mul0ord mul0eqap Remark 2.19 of [Geuvers] says that (𝐴 · 𝐵) = 0 → (𝐴 = 0 ∨ 𝐵 = 0) does not hold in general and has a counterexample.
    mulne0b , mulne0bd , mulne0bad , mulne0bbd mulap0b, mulap0bd, mulap0bad, mulap0bbd
    mulne0 , mulne0i , mulne0d mulap0, mulap0i, mulap0d
    receu receuap In theorems involving reciprocals or division, not equal to zero changes to apart from zero.
    mulnzcnopr none
    msq0i , msq0d sqeq0, sqeq0i These slight restatements of sqeq0 are unused in set.mm.
    mulcan1g , mulcan2g various cancellation theorems Presumably this is unavailable for the same reason that mul0or is unavailable.
    1div0 none This could be proved, but the set.mm proof does not work as-is.
    divval divvalap In theorems involving reciprocals or division, not equal to zero changes to apart from zero.
    divmul , divmul2 , divmul3 divmulap, divmulap2, divmulap3 In theorems involving reciprocals or division, not equal to zero changes to apart from zero.
    divcl , reccl divclap, recclap In theorems involving reciprocals or division, not equal to zero changes to apart from zero.
    divcan1 , divcan2 divcanap1, divcanap2 In theorems involving reciprocals or division, not equal to zero changes to apart from zero.
    diveq0 diveqap0 In theorems involving reciprocals or division, not equal to zero changes to apart from zero.
    divne0b , divne0 divap0b, divap0
    recne0 recap0
    recid , recid2 recidap, recidap2
    divrec divrecap
    divrec2 divrecap2
    divass divassap
    div23 , div32 , div13 , div12 div23ap, div32ap, div13ap, div12ap
    divmulass divmulassap
    divmulasscom divmulasscomap
    divdir , divcan3 , divcan4 divdirap, divcanap3, divcanap4
    div11 , divid , div0 div11ap, dividap, div0ap
    diveq1 , divneg diveqap1, divnegap
    muldivdir muldivdirap
    divsubdir divsubdirap
    recrec , rec11 , rec11r recrecap, rec11ap, rec11rap
    divmuldiv , divdivdiv , divcan5 divmuldivap, divdivdivap, divcanap5
    divmul13 , divmul24 , divmuleq divmul13ap, divmul24ap, divmuleqap
    recdiv , divcan6 , divdiv32 , divcan7 recdivap, divcanap6, divdiv32ap, divcanap7
    dmdcan , divdiv1 , divdiv2 , recdiv2 dmdcanap, divdivap1, divdivap2, recdivap2
    ddcan , divadddiv , divsubdiv ddcanap, divadddivap, divsubdivap
    ddcan , divadddiv , divsubdiv ddcanap, divadddivap, divsubdivap
    conjmul , rereccl, redivcl conjmulap, rerecclap, redivclap
    div2neg , divneg2 div2negap, divneg2ap
    recclzi , recne0zi , recidzi recclapzi, recap0apzi, recidapzi
    reccli , recidi , recreci recclapi, recidapi, recrecapi
    dividi , div0i dividapi, div0api
    divclzi , divcan1zi , divcan2zi divclapzi, divcanap1zi, divcanap2zi
    divreczi , divcan3zi , divcan4zi divrecapzi, divcanap3zi, divcanap4zi
    rec11i , rec11ii rec11api, rec11apii
    divcli , divcan2i , divcan1i , divreci , divcan3i , divcan4i divclapi, divcanap2i, divcanap1i, divrecapi, divcanap3i, divcanap4i
    div0i divap0i
    divasszi , divmulzi , divdirzi , divdiv23zi divassapzi, divmulapzi, divdirapzi, divdiv23apzi
    divmuli , divdiv32i divmulapi, divdiv32api
    divassi , divdiri , div23i , div11i divassapi, divdirapi, div23api, div11api
    divmuldivi, divmul13i, divadddivi, divdivdivi divmuldivapi, divmul13api, divadddivapi, divdivdivapi
    rerecclzi , rereccli , redivclzi , redivcli rerecclapzi, rerecclapi, redivclapzi, redivclapi
    reccld , rec0d , recidd , recid2d , recrecd , dividd , div0d recclapd, recap0d, recidapd, recidap2d, recrecapd, dividapd, div0apd
    divcld , divcan1d , divcan2d , divrecd , divrec2d , divcan3d , divcan4d divclapd, divcanap1d, divcanap2d, divrecapd, divrecap2d, divcanap3d, divcanap4d
    diveq0d , diveq1d , diveq1ad , diveq0ad , divne1d , div0bd , divnegd , divneg2d , div2negd diveqap0d, diveqap1d, diveqap1ad, diveqap0ad, divap1d, divap0bd, divnegapd, divneg2apd, div2negapd
    divne0d , recdivd , recdiv2d , divcan6d , ddcand , rec11d divap0d, recdivapd, recdivap2d, divcanap6d, ddcanapd, rec11apd
    divmuld , div32d , div13d , divdiv32d , divcan5d , divcan5rd , divcan7d , dmdcand , dmdcan2d , divdiv1d , divdiv2d divmulapd, div32apd, div13apd, divdiv32apd, divcanap5d, divcanap5rd, divcanap7d, dmdcanapd, dmdcanap2d, divdivap1d, divdivap2d
    divmul2d, divmul3d, divassd, div12d, div23d, divdird, divsubdird, div11d divmulap2d, divmulap3d, divassapd, div12apd, div23apd, divdirapd, divsubdirapd, div11apd
    divmuldivd divmuldivapd
    divmuleqd divmuleqapd
    rereccld , redivcld rerecclapd, redivclapd
    diveq1bd diveqap1bd
    div2sub , div2subd div2subap, div2subapd
    subrec , subreci , subrecd subrecap, subrecapi, subrecapd
    mvllmuld mvllmulapd
    mvllmuli mvllmulapd
    elimgt0 , elimge0 none Even in set.mm, the weak deduction theorem is discouraged in favor of theorems in deduction form.
    mulge0b , mulsuble0b none Presumably unprovable for reasons analogous to mul0or.
    mulle0b mulle0r The converse of mulle0r is presumably unprovable for reasons analogous to mul0or.
    ledivp1i , ltdivp1i none Presumably could be proved, but unused in set.mm.
    fimaxre fimaxq, fimaxre2 When applied to a pair fimaxre could show which of two unequal real numbers is larger, so perhaps not provable for that reason. (see fin0 for inhabited versus nonempty).
    fimaxre3 none The set.mm proof relies on abrexfi .
    fiminre none See fimaxre
    sup2 none Presumably provable (with a locatedness condition added) but most likely not as interesting as sup3 in the absence of leloe
    sup3 , sup3ii none We won't be able to have the least upper bound property for all inhabited bounded sets, as shown at sup3exmid.
    infm3 none See sup3
    suprcl , suprcld , suprclii supclti
    suprub , suprubd , suprubii suprubex
    suprlub , suprlubii suprlubex
    suprnub , suprnubii suprnubex
    suprleub , suprleubii suprleubex
    supaddc , supadd none Presumably provable with suitable conditions for the existence of the supremums
    supmul1 , supmul none Presumably provable with suitable conditions for the existence of the supremums
    riotaneg none The theorem is unused in set.mm and the set.mm proof relies on reuxfrd
    infrecl infclti
    infrenegsup infrenegsupex
    infregelb infregelbex
    infrelb none yet Presumably could be handled in a way analogous to suprubex
    supfirege suprubex The question here is whether results like maxle1 can be generalized (presumably by induction) from pairs to finite sets.
    crne0 crap0
    ofsubeq0 , ofnegsub , ofsubge0 none Depend on ofval and/or offn .
    df-nn dfnn2
    dfnn3 dfnn2 Presumably could be proved, as it is a slight variation of dfnn2
    avgle qavgle
    nnunb none Presumably provable from arch but unused in set.mm.
    frnnn0supp , frnnn0fsupp nn0supp iset.mm does not yet have either the notation, or in some cases the theorems, related to the support of a function or a fintely supported function.
    suprzcl suprzclex, suprzcl2dc
    zriotaneg none Lightly used in set.mm
    suprfinzcl none
    decex deccl
    uzwo uzwodc
    nnwo nnwodc
    nnwof nnwofdc
    nnwos nnwosdc
    uzwo2 none Presumably would imply excluded middle, unless there is something which makes this different from nnregexmid.
    negn0 negm
    uzinfi, nninf, nn0inf none Presumably provable
    infssuzle infssuzledc, nnminle
    infssuzcl infssuzcldc
    supminf supminfex
    zsupss zsupssdc
    suprzcl2 suprzclex, suprzcl2dc
    suprzub suprzubdc
    uzsupss zsupcl
    uzwo3 , zmin none Proved in terms of supremum theorems and presumably not possible without excluded middle.
    zbtwnre none Proved in terms of supremum theorems and presumably not possible without excluded middle.
    rebtwnz qbtwnz
    rpneg rpnegap
    mul2lt0bi mul2lt0np, mul2lt0pn The set.mm proof of the forward direction of mul2lt0bi is not intuitionistic.
    xrlttri , xrlttri2 none A generalization of real trichotomy.
    xrleloe , xrleltne , dfle2 none Consequences of real trichotomy.
    xrltlen none We presumably could prove an analogue to ltleap but we have not yet defined apartness for extended reals (# is for complex numbers).
    dflt2 none
    xrletri xnn0letri
    xrmax1 xrmax1sup
    xrmax2 xrmax2sup
    xrmin1 , xrmin2 xrmin1inf, xrmin2inf
    xrmaxeq xrmaxleim
    xrmineq xrmineqinf
    xrmaxlt xrmaxltsup
    xrltmin xrltmininf
    xrmaxle xrmaxlesup
    xrlemin xrlemininf
    max0sub , ifle none
    max1 maxle1
    max2 maxle2
    2resupmax 2zsupmax for integers
    in general The set.mm proof uses real trichotomy in an apparently essential way. We express maximum in iset.mm using sup({𝐴, 𝐵}, ℝ, < ) rather than if(𝐴𝐵, 𝐵, 𝐴). The former has the expected maximum properties such as maxcl, maxle1, maxle2, maxleast, and maxleb.
    ssfzunsnext none Presumably provable using 2zsupmax and similar theorems.
    min1 min1inf
    min2 min2inf
    maxle maxleastb
    lemin lemininf
    maxlt maxltsup
    ltmin ltmininf
    lemaxle maxle2
    qsqueeze none yet Presumably provable from qbtwnre and squeeze0, but unused in set.mm.
    qextltlem , qextlt , qextle none The set.mm proof is not intuitionistic.
    xralrple , alrple none yet Now that we have qbtwnxr, it looks like the set.mm proof would work with minor changes.
    xnegex xnegcl
    xmulval none The set.mm definition would appear to only function if comparing a real number with zero is decidable (which we will not be able to show in general)
    xnn0xaddcl none presumably provable
    xmullem , xmullem2 , xmulcom , xmul01 , xmul02 , xmulneg1 , xmulneg2 , rexmul , xmulf , xmulcl , xmulpnf1 , xmulpnf2 , xmulmnf1 , xmulmnf2 , xmulpnf1n , xmulid1 , xmulid2 , xmulm1 , xmulasslem2 , xmulgt0 , xmulge0 , xmulasslem , xmulasslem3 , xmulass , xlemul1a , xlemul2a , xlemul1 , xlemul2 , xltmul1 , xltmul2 , xadddilem , xadddi , xadddir , xadddi2 , xadddi2r , x2times , xmulcld none Although a few of these contain hypotheses that arguments are apart from zero (and thus could be proved with the current definition of ·e), in general extended real multiplication will not work as in set.mm using that definition.
    xrsupss none the set.mm proof relies on sup3 which implies excluded middle by sup3exmid
    supxrcl none the set.mm proof relies on xrsupss
    infxrcl none presumably not provable for all the usual sup3exmid reasons
    ixxub , ixxlb none
    supicc , supiccub , supicclub , supicclub2 suplociccreex, suplociccex
    ixxun , ixxin none
    ioon0 ioom Non-empty is changed to inhabited
    iooid iooidg
    ndmioo none See discussion at ndmov but set.mm uses excluded middle, both in proving this and in using it.
    lbioo , ubioo lbioog, ubioog
    iooin iooinsup
    icc0 icc0r
    ioorebas ioorebasg
    ge0xmulcl none Relies on xmulcl ; see discussion in this list for that theorems.
    icoun , snunioo , snunico , snunioc , prunioo none
    ioojoin none
    difreicc none
    iccsplit none This depends, apparently in an essential way, on real number trichotomy.
    xov1plusxeqvd none This presumably could be proved if not equal is changed to apart, but is lightly used in set.mm.
    fzn0 fzm
    fz0 none Although it would be possible to prove a version of this with the additional conditions that 𝑀 ∈ V and 𝑁 ∈ V, the theorem is lightly used in set.mm.
    fzon0 fzom
    fzo0n0 fzo0m
    ssfzoulel none Presumably could be proven, but the set.mm proof is not intuitionistic and it is lightly used in set.mm.
    fzonfzoufzol none Presumably could be proven, but the set.mm proof is not intuitionistic and it is lightly used in set.mm.
    elfznelfzo , elfznelfzob , injresinjlem , injresinj none Some or all of this presumably could be proven, but the set.mm proof is not intuitionistic and it is lightly used in set.mm.
    flcl , reflcl , flcld flqcl, flqcld
    fllelt flqlelt
    flle flqle
    flltp1 , fllep1 flqltp1
    fraclt1 , fracle1 qfraclt1
    fracge0 qfracge0
    flge flqge
    fllt flqlt
    flflp1 none The set.mm proof relies on case elimination.
    flidm flqidm
    flidz flqidz
    flltnz flqltnz
    flwordi flqwordi
    flword2 flqword2
    flval2 , flval3 none Unused in set.mm
    flbi flqbi
    flbi2 flqbi2
    ico01fl0 none Presumably could be proved for rationals, but lightly used in set.mm.
    flge0nn0 flqge0nn0
    flge1nn flqge1nn
    refldivcl flqcl
    fladdz flqaddz
    flzadd flqzadd
    flmulnn0 flqmulnn0
    fldivle flqle
    ltdifltdiv none Unused in set.mm.
    fldiv4lem1div2uz2 , fldiv4lem1div2 none Presumably provable, but lightly used in set.mm.
    ceilval ceilqval The set.mm ceilval, with a real argument and no additional conditions, is probably provable if there is a need.
    dfceil2 , ceilval2 none Unused in set.mm.
    ceicl ceiqcl
    ceilcl ceilqcl
    ceilge ceilqge
    ceige ceiqge
    ceim1l ceiqm1l
    ceilm1lt ceilqm1lt
    ceile ceiqle
    ceille ceilqle
    ceilidz ceilqidz
    flleceil flqleceil
    fleqceilz flqeqceilz
    quoremz , quoremnn0 , quoremnn0ALT none Unused in set.mm.
    intfrac2 intqfrac2
    fldiv flqdiv
    fldiv2 none Presumably would be provable if real is changed to rational.
    fznnfl none Presumably would be provable if real is changed to rational.
    uzsup , ioopnfsup , icopnfsup , rpsup , resup , xrsup none As with most theorems involving supremums, these would likely need significant changes
    modval modqval As with theorems such as flqcl, we prove most of the modulo related theorems for rationals, although other conditions on real arguments other than whether they are rational would be possible in the future.
    modvalr modqvalr
    modcl , modcld modqcl, modqcld
    flpmodeq flqpmodeq
    mod0 modq0
    mulmod0 mulqmod0
    negmod0 negqmod0
    modge0 modqge0
    modlt modqlt
    modelico modqelico
    moddiffl modqdiffl
    moddifz modqdifz
    modfrac modqfrac
    flmod flqmod
    intfrac intqfrac
    modmulnn modqmulnn
    modvalp1 modqvalp1
    modid modqid
    modid0 modqid0
    modid2 modqid2
    0mod q0mod
    1mod q1mod
    modabs modqabs
    modabs2 modqabs2
    modcyc modqcyc
    modcyc2 modqcyc2
    modadd1 modqadd1
    modaddabs modqaddabs
    modaddmod modqaddmod
    muladdmodid mulqaddmodid
    modmuladd modqmuladd
    modmuladdim modqmuladdim
    modmuladdnn0 modqmuladdnn0
    negmod qnegmod
    modadd2mod modqadd2mod
    modm1p1mod0 modqm1p1mod0
    modltm1p1mod modqltm1p1mod
    modmul1 modqmul1
    modmul12d modqmul12d
    modnegd modqnegd
    modadd12d modqadd12d
    modsub12d modqsub12d
    modsubmod modqsubmod
    modsubmodmod modqsubmodmod
    2txmodxeq0 q2txmodxeq0
    2submod q2submod
    modmulmod modqmulmod
    modmulmodr modqmulmodr
    modaddmulmod modqaddmulmod
    moddi modqdi
    modsubdir modqsubdir
    modeqmodmin modqeqmodmin
    modirr none A version of this (presumably modified) may be possible, but it is unused in set.mm
    om2uz0i frec2uz0d
    om2uzsuci frec2uzsucd
    om2uzuzi frec2uzuzd
    om2uzlti frec2uzltd
    om2uzlt2i frec2uzlt2d
    om2uzrani frec2uzrand
    om2uzf1oi frec2uzf1od
    om2uzisoi frec2uzisod
    om2uzoi , ltweuz , ltwenn , ltwefz none Based on theorems like nnregexmid it is not clear what, if anything, along these lines is possible.
    om2uzrdg frec2uzrdg
    uzrdglem frecuzrdglem
    uzrdgfni frecuzrdgtcl
    uzrdg0i frecuzrdg0
    uzrdgsuci frecuzrdgsuc
    uzinf none See ominf
    uzrdgxfr none Presumably could be proved if restated in terms of frec (a la frec2uz0d). However, it is lightly used in set.mm.
    fzennn frecfzennn
    fzen2 frecfzen2
    cardfz none Cardinality does not work the same way without excluded middle and iset.mm has few cardinality related theorems.
    hashgf1o frechashgf1o
    fzfi fzfig
    fzfid fzfigd
    fzofi fzofig
    fsequb none Seems like it might be provable, but unused in set.mm
    fsequb2 none The set.mm proof does not work as-is
    fseqsupcl none The set.mm proof relies on fisupcl and it is not clear whether this supremum theorem or anything similar can be proved.
    fseqsupubi none The set.mm proof relies on fsequb2 and suprub and it is not clear whether this supremum theorem or anything similar can be proved.
    uzindi none This could presumably be proved, perhaps from uzsinds, but is lightly used in set.mm
    axdc4uz none Although some versions of constructive mathematics accept dependent choice, we have not yet developed it in iset.mm
    ssnn0fi , rabssnn0fi none Conjectured to imply excluded middle along the lines of nnregexmid or ssfiexmid
    df-seq df-seqfrec
    seqval seq3val
    seqfn seqf
    seq1 , seq1i seq3-1
    seqp1 , seqp1i seq3p1
    seqm1 seq3m1
    seqcl2 seqf2 seqf2 requires that 𝐹 be defined on (ℤ𝑀) not merely (𝑀...𝑁).
    seqcl seqf, seq3clss seqf requires that 𝐹 be defined on (ℤ𝑀) not merely (𝑀...𝑁). This requirement is relaxed somewhat in seq3clss.
    seqfveq2 seq3fveq2
    seqfeq2 seq3feq2
    seqfveq seq3fveq
    seqfeq seq3feq
    seqshft2 seq3shft2
    seqres none Should be intuitionizable as with the other seq theorems, but unused in set.mm
    sermono ser3mono ser3mono requires that 𝐹 be defined on (ℤ𝑀) not merely (𝑀...𝑁) as in sermono .
    seqsplit seq3split seq3split requires that 𝐹 be defined on (ℤ𝐾) not merely (𝐾...𝑁) as in seqsplit . This is not a problem when used on infinite sequences; finite sums may find it easier to use fsumsplit instead.
    seq1p seq3-1p Requires that 𝐹 be defined on (ℤ𝑀) not merely (𝑀...𝑁). This is not a problem when used on infinite sequences, but perhaps this requirement could be relaxed if there is a need.
    seqcaopr3 seq3caopr3 The functions 𝐹, 𝐺, and 𝐻 need to be defined on (ℤ𝑀) not merely (𝑀...𝑁).
    seqcaopr2 seq3caopr2 The functions 𝐹, 𝐺, and 𝐻 need to be defined on (ℤ𝑀) not merely (𝑀...𝑁).
    seqcaopr seq3caopr The functions 𝐹, 𝐺, and 𝐻 need to be defined on (ℤ𝑀) not merely (𝑀...𝑁).
    seqf1o seq3f1o The functions 𝐺 and 𝐻 need to be defined on (ℤ𝑀) not merely (𝑀...𝑁). Also, a single set 𝑆 takes the place of 𝐶 and 𝑆 because that is sufficient flexibility at least for now.
    seradd ser3add The functions 𝐹, 𝐺, and 𝐻 need to be defined on (ℤ𝑀) not merely (𝑀...𝑁).
    sersub ser3sub The functions 𝐹, 𝐺, and 𝐻 need to be defined on (ℤ𝑀) not merely (𝑀...𝑁).
    seqid3 seq3id3
    seqid seq3id
    seqid2 seq3id2
    seqhomo seq3homo
    seqz seq3z The sequence has to be defined on (ℤ𝑀) not just (𝑀...𝑁)
    seqfeq4 seqfeq3 The sequence has to be defined on (ℤ𝑀) not just (𝑀...𝑁)
    seqdistr seq3distr
    serge0 ser3ge0 The sequence has to be defined on (ℤ𝑀) not just (𝑀...𝑁)
    serle ser3le Changes several hypotheses from (𝑀...𝑁) to (ℤ𝑀)
    ser1const fsumconst Finite summation in iset.mm is easier to express using Σ rather than seq directly.
    seqof , seqof2 none It should be possible to come up with some (presumably modified) versions of these, but we have not done so yet.
    expval exp3val The set.mm theorem does not exclude the case of dividing by zero.
    expneg expnegap0 The set.mm theorem does not exclude the case of dividing by zero.
    expneg2 expineg2
    expn1 expn1ap0
    expcl2lem expcl2lemap
    reexpclz reexpclzap
    expclzlem expclzaplem
    expclz expclzap
    expne0 expap0
    expne0i expap0i
    expnegz expnegzap
    mulexpz mulexpzap
    exprec exprecap
    expaddzlem , expaddz expaddzaplem, expaddzap
    expmulz expmulzap
    expsub expsubap
    expp1z expp1zap
    expm1 expm1ap
    expdiv expdivap
    leexp2 nn0leexp2 leexp2 is presumably provable using ltexp2
    leexp2a , ltexp2d , leexp2d none Presumably provable using ltexp2
    ltexp2r , ltexp2rd none Presumably provable using ltexp2
    sqdiv sqdivap
    sqgt0 sqgt0ap
    sqrecii , sqrecd exprecap
    sqdivi sqdivapi
    sqgt0i sqgt0api
    sqlecan lemul1 Unused in set.mm
    sqeqori , subsq0i , sqeqor qsqeqor Presumably not provable in general for real or complex numbers, see mul0or for more discussion. For the nonnegative real case see sq11.
    none Variations of sqeqori .
    sq01 none Lightly used in set.mm. Presumably not provable as stated, for reasons analogous to mul0or .
    crreczi none Presumably could be proved if not-equal is changed to apart, but unused in set.mm.
    expmulnbnd none Should be possible to prove this or something similar, but the set.mm proof relies on case elimination based on whether 0 ≤ 𝐴 or not.
    digit2 , digit1 none Depends on modulus and floor, and unused in set.mm.
    modexp modqexp
    discr1 , discr none The set.mm proof uses real number trichotomy.
    sqrecd sqrecapd
    expclzd expclzapd
    exp0d expap0d
    expne0d expap0d
    expnegd expnegapd
    exprecd exprecapd
    expp1zd expp1zapd
    expm1d expm1apd
    expsubd expsubapd
    sqdivd sqdivapd
    expdivd expdivapd
    reexpclzd reexpclzapd
    sqgt0d sqgt0apd
    mulsubdivbinom2 none Presumably provable if not equal is changed to apart.
    muldivbinom2 none Presumably provable if not equal is changed to apart.
    nn0le2msqi nn0le2msqd Although nn0le2msqi could be proved, having a version in deduction form will be more useful.
    nn0opthlem1 nn0opthlem1d Although nn0opthlem1 could be proved, having a version in deduction form will be more useful.
    nn0opthlem2 nn0opthlem2d Although nn0opthlem2 could be proved, having a version in deduction form will be more useful.
    nn0opthi nn0opthd Although nn0opthi could be proved, having a version in deduction form will be more useful.
    nn0opth2i nn0opth2d Although nn0opth2i could be proved, having a version in deduction form will be more useful.
    facmapnn faccl Presumably provable now that iset.mm has df-map. But faccl would be sufficient for the uses in set.mm.
    faclbnd4 , faclbnd5 , and lemmas none Presumably provable; unused in set.mm.
    df-hash df-ihash
    hashkf , hashgval , hashginv none Due to the differences between df-hash in set.mm and df-ihash here, there's no particular need for these as stated
    hashinf hashinfom The condition that 𝐴 is infinite is changed from ¬ 𝐴 ∈ Fin to ω ≼ 𝐴.
    hashbnd none The set.mm proof is not intuitionistic.
    hashfxnn0 , hashf , hashxnn0 , hashresfn , dmhashres , hashnn0pnf none Although df-ihash is defined for finite sets and infinite sets, it is not clear we would be able to show this definition (or another definition) is defined for all sets.
    hashnnn0genn0 none Not yet known whether this is provable or whether it is the sort of reverse closure theorem that we (at least so far) have been unable to intuitionize.
    hashnemnf none Presumably provable but the set.mm proof relies on hashnn0pnf
    hashv01gt1 hashfiv01gt1 It is not clear there would be any way to combine the finite and infinite cases.
    hasheni hashen, hashinfom It is not clear there would be any way to combine the finite and infinite cases.
    hasheqf1oi fihasheqf1oi It is not clear there would be any way to combine the finite and infinite cases.
    hashf1rn fihashf1rn It is not clear there would be any way to combine the finite and infinite cases.
    hasheqf1od fihasheqf1od It is not clear there would be any way to combine the finite and infinite cases.
    hashcard none Cardinality is not well developed in iset.mm
    hashxrcl none It is not clear there would be any way to combine the finite and infinite cases.
    hashclb none Not yet known whether this is provable or whether it is the sort of reverse closure theorem that we (at least so far) have been unable to intuitionize.
    nfile filtinf It is not clear there would be any way to combine the case where 𝐴 is finite and the case where it is infinite.
    hashvnfin none This is a form of reverse closure, presumably not provable.
    hashnfinnn0 hashinfom
    isfinite4 isfinite4im
    hasheq0 fihasheq0 It is not clear there would be any way to combine the finite and infinite cases.
    hashneq0 , hashgt0n0 fihashneq0
    hashelne0d fihashelne0d
    hashen1 fihashen1
    hash1elsn none would be easy to prove if 𝐴𝑉 is changed to 𝐴 ∈ Fin
    hashrabrsn none Presumably would need conditions around the existence of 𝐴 and decidability of 𝜑 but unused in set.mm.
    hashrabsn01 none Presumably would need conditions around the existence of 𝐴 and decidability of 𝜑 but unused in set.mm.
    hashrabsn1 none The set.mm proof uses excluded middle and this theorem is unused in set.mm.
    hashfn fihashfn There is an added condition that the domain be finite.
    hashgadd omgadd
    hashgval2 none Presumably provable, when restated as (♯ ↾ ω) = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0), but lightly used in set.mm.
    hashdom fihashdom There is an added condition that 𝐵 is finite.
    hashdomi fihashdom It is presumably not possible to extend fihashdom beyond the finite set case.
    hashun2 none The set.mm proof relies on undif2 (we just have undif2ss) and diffi (we just have diffifi)
    hashun3 none The set.mm proof relies on various theorems we do not have
    hashinfxadd none
    hashunx none It is not clear there would be any way to combine the finite and infinite cases.
    hashge0 hashcl It is not clear there would be any way to combine the finite and infinite cases.
    hashgt0 , hashge1 hashnncl It is not clear there would be any way to combine the finite and infinite cases.
    hashnn0n0nn hashnncl To the extent this is reverse closure, we probably can't prove it. For inhabited versus non-empty, see fin0
    elprchashprn2 hashsng Given either 𝑁 ∈ V or ¬ 𝑁 ∈ V this could be proved (as (♯‘{𝑀, 𝑁}) reduces to hashsng or hash0 respectively), but is not clear we can combine the cases (even 1domsn may not be enough).
    hashprb hashprg
    hashprdifel none This would appear to be a form of reverse closure.
    hashle00 fihasheq0
    hashgt0elex , hashgt0elexb fihashneq0 See fin0 for inhabited versus non-empty. It isn't clear it would be possible to also include the infinite case as hashgt0elex does.
    hashss fihashss
    prsshashgt1 fiprsshashgt1
    hashin none Presumably additional conditions would be needed (see infi entry).
    hashssdif fihashssdif
    hashdif none Modified versions presumably would be provable, but this is unused in set.mm.
    hashsn01 none Presumably not provable
    hashsnle1 none At first glance this would appear to be the same as 1domsn but to apply fihashdom would require that the singleton be finite, which might imply that we cannot improve on hashsng.
    hashsnlei none Presumably not provable
    hash1snb , euhash1 , hash1n0 , hashgt12el , hashgt12el2 none Conjectured to be provable in the finite set case
    hashunlei none Not provable per unfiexmid (see also entry for hashun2)
    hashsslei fihashss Would be provable if we transfered 𝐵 ∈ Fin from the conclusion to the hypothesis but as written falls afoul of ssfiexmid.
    hashmap none Probably provable but the set.mm proof relies on a number of theorems which we don't have.
    hashpw none Unlike pw2en this is only for finite sets, so it presumably is provable. The set.mm proof may be usable.
    hashfun none Presumably provable but the set.mm proof relies on excluded middle and undif.
    hashres , hashreshashfun none Presumably would need to add 𝐵 ∈ Fin or similar conditions.
    hashimarn , hashimarni none Presumably would need an additional condition such as 𝐹 ∈ Fin but unused in set.mm.
    fnfz0hashnn0 none Presumably would need an additional condition such as 𝑁 ∈ ℕ0 but unused in set.mm.
    fnfzo0hashnn0 none Presumably would need an additional condition such as 𝑁 ∈ ℕ0 but unused in set.mm.
    hashbc none The set.mm proof uses pwfi and ssfi .
    hashf1 none The set.mm proof uses ssfi , excluded middle, abn0 , diffi and perhaps other theorems we don't have.
    hashfac none The set.mm proof uses hashf1 .
    leiso none The set.mm proof uses isocnv3 .
    fz1iso zfz1iso The set.mm proof of fz1iso depends on OrdIso. Furthermore, trichotomy rather than weak linearity would seem to be needed.
    ishashinf none May be possible with the antecedent changed from ¬ 𝐴 ∈ Fin to ω ≼ 𝐴 but the set.mm proof does not work as is.
    phphashd , phphashrd none would appear to need hashclb or some other way of showing that the subset is finite
    seqcoll seq3coll The functions 𝐹 and 𝐻 need to be defined on 𝑀 not just a subset thereof.
    seqcoll2 none Presumably can be done with modifications similar to seq3coll.
    df-word and all theorems relating to words over a set none presumably mostly provable
    seqshft seq3shft
    df-sgn and theorems related to the sgn function none To choose a value near zero requires knowing the argument with unlimited precision. It would be possible to define for rational numbers, or real numbers apart from zero.
    mulre mulreap
    rediv redivap
    imdiv imdivap
    cjdiv cjdivap
    sqeqd none The set.mm proof is not intuitionistic, and this theorem is unused in set.mm.
    cjdivi cjdivapi
    cjdivd cjdivapd
    redivd redivapd
    imdivd imdivapd
    df-sqrt df-rsqrt See discussion of complex square roots in the comment of df-rsqrt. Here's one possibility if we do want to define square roots on (some) complex numbers: It should be possible to define the complex square root function on all complex numbers satisfying (ℑ‘𝑥) # 0 ∨ 0 ≤ (ℜ‘𝑥), using a similar construction to the one used in set.mm. You need the real square root as a basis for the construction, but then there is a trick using the complex number x + |x| (see sqreu) that yields the complex square root whenever it is apart from zero (you need to divide by it at one point IIRC), which is exactly on the negative real line. You can either live with this constraint, which gives you the complex square root except on the negative real line (which puts a hole at zero), or you can extend it by continuity to zero as well by joining it with the real square root. The disjunctive domain of the resulting function might not be so useful though.
    sqrtval sqrtrval See discussion of complex square roots in the comment of df-rsqrt
    01sqrex and its lemmas resqrex Both set.mm and iset.mm prove resqrex although via different mechanisms so there is no need for 01sqrex.
    cnpart none See discussion of complex square roots in the comment of df-rsqrt
    sqrmo rsqrmo See discussion of complex square roots in the comment of df-rsqrt
    resqreu rersqreu Although the set.mm theorem is primarily about real square roots, the iset.mm equivalent removes some complex number related parts.
    sqrtneg , sqrtnegd none Although it may be possible to extend the domain of square root somewhat beyond nonnegative reals without excluded middle, in general complex square roots are difficult, as discussed in the comment of df-rsqrt
    sqrtm1 none Although it may be possible to extend the domain of square root somewhat beyond nonnegative reals without excluded middle, in general complex square roots are difficult, as discussed in the comment of df-rsqrt
    absrpcl , absrpcld absrpclap, absrpclapd
    absdiv , absdivzi , absdivd absdivap, absdivapzi, absdivapd
    absor , absori , absord qabsor It also would be possible to prove this for real numbers apart from zero, if we wanted
    absmod0 none See df-mod ; we may want to supply this for rationals or integers
    absexpz absexpzap
    max0add max0addsup
    absz none Although this is presumably provable, the set.mm proof is not intuitionistic and it is lightly used in set.mm
    recval recvalap
    absgt0 , absgt0i absgt0ap, absgt0api
    absmax maxabs
    abs1m none Because this theorem provides (∗‘𝐴) / (abs‘𝐴) as the answer if 𝐴 ≠ 0 and 𝑖 as the answer if 𝐴 = 0, and uses excluded middle to combine those cases, it is presumably not provable as stated. We could prove the theorem with the additional condition that 𝐴 # 0, but it is unused in set.mm.
    abslem2 none Although this could presumably be proved if not equal were changed to apart, it is lightly used in set.mm.
    rddif , absrdbnd none If there is a need, we could prove these for rationals or real numbers apart from any rational. Alternately, we could prove a result with a slightly larger bound for any real number.
    rexuzre none Unless the real number 𝑗 is known to be apart from an integer, it isn't clear there would be any way to prove this (see the steps in the set.mm proof which rely on the floor of a real number). It is unused in set.mm for whatever that is worth.
    caubnd none If we can prove fimaxre3 it would appear that the set.mm proof would work with small changes (in the case of the maximum of two real numbers, using maxle1, maxle2, and maxcl).
    sqreulem , sqreu , sqrtcl , sqrtcld , sqrtthlem , sqrtf , sqrtth , sqsqrtd , msqsqrtd , sqr00d , sqrtrege0 , sqrtrege0d , eqsqrtor , eqsqrtd , eqsqrt2d rersqreu, resqrtcl, resqrtcld, resqrtth As described at df-rsqrt, square roots of complex numbers are in set.mm defined with the help of excluded middle.
    df-limsup and all superior limit theorems none This is not developed in iset.mm currently. If it was it would presumably be noticeably different from set.mm given various differences relating to sequence convergence, supremums, etc.
    df-rlim and theorems related to limits of partial functions on the reals none This is not developed in iset.mm currently. If it was it would presumably be noticeably different from set.mm given various differences relating to convergence.
    df-o1 and theorems related to eventually bounded functions none This is not developed in iset.mm currently. If it was it would presumably be noticeably different from set.mm given various differences relating to sequence convergence, supremums, etc.
    df-lo1 and theorems related to eventually upper bounded functions none This is not developed in iset.mm currently. If it was it would presumably be noticeably different from set.mm given various differences relating to sequence convergence, supremums, etc.
    reccn2 reccn2ap
    isershft iser3shft
    isercoll and its lemmas, isercoll2 none yet The set.mm proof would need modification
    climsup none To show convergence would presumably require a hypothesis related to the rate of convergence.
    climbdd none Presumably could be proved but the current proof of caubnd would need at least some minor adjustments.
    caurcvg2 climrecvg1n
    caucvg climcvg1n
    caucvgb climcaucn, climcvg1n Without excluded middle, there are additional complications related to the rate of convergence.
    iseralt none The set.mm proof relies on caurcvg2 which does not specify a rate of convergence.
    df-sum df-sumdc The iset.mm definition/theorem adds a decidability condition and an if expression (which is to deal with differences in using seq for finite sums). It does function similarity to the set.mm definition of Σ.
    sumex fsumcl, isumcl
    sumeq2w sumeq2 Presumably could be proved, and perhaps also would rely only on extensionality (and logical axioms). But unused in set.mm.
    sumeq2ii sumeq2
    sum2id none The set.mm proof does not work as-is. Lightly used in set.mm.
    sumfc sumfct
    fsumcvg fsum3cvg
    sumrb sumrbdc
    summo summodc
    zsum zsumdc
    fsum fsum3
    sumz isumz
    sumss isumss
    sumss2 isumss2
    fsumcvg2 fsum3cvg2
    fsumsers fsumsersdc
    fsumcvg3 fsum3cvg3
    fsumser fsum3ser
    fsummsnunz none Could be proved if we added a 𝑍 ∈ V condition, but unused in set.mm.
    isumdivc isumdivapc Changes not equal to apart
    sumsplit sumsplitdc Adds decidability conditions
    fsumcom2 fisumcom2 Although it is possible that (𝜑𝑘𝐶) → 𝐷 ∈ Fin can be proved from the other hypotheses, the set.mm proof of that uses ssfi .
    fsum0diag fisum0diag Adds a 𝑁 ∈ ℤ hypothesis
    fsumrev2 fisumrev2 Adds 𝑀 ∈ ℤ and 𝑁 ∈ ℤ hypotheses
    fsum0diag2 fisum0diag2 Adds a 𝑁 ∈ ℤ hypothesis
    fsumdivc fsumdivapc Changes not equal to apart
    fsumless fsumlessfi Whether this can be proved without the 𝐶 ∈ Fin condition is unknown but such a proof would be fairly different from the set.mm proof.
    seqabs fsumabs Finite sums are more naturally expressed with Σ rather than seq especially in iset.mm. Use fsum3ser as needed.
    cvgcmp cvgcmp2n The set.mm proof of cvgcmp relies on caurcvg2 which does not specify a rate of convergence.
    cvgcmpce none The proof, and perhaps the statement of the theorem, would need some changes related to the rate of convergence.
    abscvgcvg none The set.mm proof relies on cvgcmpce
    climfsum none Likely provable, but lightly used in set.mm.
    qshash none The set.mm proof will not work as-is.
    ackbijnn none iset.mm does not have ackbij1
    incexclem , incexc , incexc2 none A metamath 100 theorem but otherwise unused in set.mm.
    isumless isumlessdc Adds a decidability condition on the index set for the sum
    isumsup2 , isumsup none Having an upper bound on the partial sums would not suffice; a stronger convergence condition would be needed.
    isumltss none Should be provable with the addition of a decidability condition such as the one found in isumss2 and fsum3cvg3.
    climcnds none The set.mm proof will not work without modifications.
    divcnvshft none The set.mm proof uses ovex to show that 𝐴 / (𝑘 + 𝐵) is a set, even when 𝑘 + 𝐵 might be zero. This could be solved by adding another usage of df-div or proving (1 / 0) = ∅ but relying on the value of dividing by zero is not something we usually let ourselves do. Another solution would be to add a 0 < (𝑀 + 𝐵) hypothesis.
    supcvg none The set.mm proof uses countable choice and also various supremum theorems proved via excluded middle.
    infcvgaux1i , infcvgaux2i none See supcvg entry
    harmonic none Should be feasible once we get climcnds (or a similar theorem). A Metamath 100 theorem but otherwise unused in set.mm.
    geoserg geosergap Not equal is changed to apart
    geoser geoserap Not equal is changed to apart
    pwm1geoser pwm1geoserap1 Adds a condition that the base is apart from one. The set.mm proof relies on case elimination on whether the base is one or not equal to one.
    geomulcvg none The set.mm proof relies on cvgcmpce and expmulnbnd and would appear to also require 𝐴 to be apart from zero.
    cvgrat cvgratgt0 Adds a 0 < 𝐴 condition which presumably is omitted from the set.mm theorem only for convenience (the theorem isn't interesting unless it holds).
    mertens mertensabs Because we don't (yet at least) have abscvgcvg or anything else relating the convergence of a sequence's absolute values to the convergence of the sequence itself, we add the condition that both the sequence 𝐹 and the sequence of its absolute values converge (that is, seq0( + , 𝐹) ∈ dom ⇝ is an additional hypothesis beyond what set.mm has).
    clim2div clim2divap
    prodfmul prod3fmul The functions 𝐹, 𝐺, and 𝐻 need to be defined on (ℤ𝑀) not merely (𝑀...𝑁).
    prodfn0 prodfap0
    prodfrec prodfrecap
    prodfdiv prodfdivap in addition to changing not equal to apart, various hypotheses need to hold for (ℤ𝑀) not merely (𝑀...𝑁)
    ntrivcvg ntrivcvgap
    ntrivcvgn0 ntrivcvgap0
    ntrivcvgfvn0 none To be useful, presumably not equal needs to be changed to apart. This means the set.mm proof does not work and we need another approach (for example, something a bit like seq3p1 or seq3split but for convergence expressed with rather than for a finite subsequence).
    ntrivcvgtail none the set.mm proof depends on ntrivcvgfvn0 . Would need not equal changed to apart.
    ntrivcvgmullem , ntrivcvgmul none the set.mm proof depends on ntrivcvgtail . Would need not equal changed to apart.
    df-prod df-proddc Changes not equal to apart, adds a decidability condition for indexing by a set of integers, and passes a more fully defined sequence to seq in the finite case. Should function similarly to the set.mm definition of .
    prodex none presumably will need to be replaced by fprodcl and iprodcl analogous to sumex
    prodeq2ii prodeq2 the set.mm proof uses excluded middle
    prod2id none the set.mm proof uses prodeq2ii
    prodrblem prodrbdclem
    fprodcvg fproddccvg
    prodrblem2 prodrbdclem2
    prodrb prodrbdc
    prodmolem3 prodmodclem3
    prodmolem2a prodmodclem2a
    prodmolem2 prodmodclem2
    prodmo prodmodc
    zprod zproddc
    iprod iprodap
    zprodn0 zprodap0
    iprodn0 iprodap0
    fprod fprodseq
    fprodntriv fprodntrivap
    prod1 prod1dc
    prodfc prodfct
    prodss prodssdc
    fprodss fprodssdc
    fprodser none presumably could be proved with some modifications
    fproddiv fproddivap
    fprodn0 fprodap0
    fprod2dlem fprod2dlemstep
    fprodcom2 fprodcom2fi Although it is possible that (𝜑𝑘𝐶) → 𝐷 ∈ Fin can be proved from the other hypotheses, the set.mm proof of that uses ssfi .
    fprod0diag fprod0diagfz Adds a 𝑁 ∈ ℤ hypothesis
    fproddivf fproddivapf
    fprodn0f fprodap0f
    eftval eftvalcn Adds an easily satisfied condition.
    fprodefsum none Presumably feasible once finite products are better developed.
    tanval tanvalap
    tancl , tancld tanclap, tanclapd
    tanval2 tanval2ap
    tanval3 tanval3ap
    retancl , retancld retanclap, retanclapd
    tanneg tannegap
    sinhval , coshval , resinhcl , rpcoshcl , recoshcl , retanhcl , tanhlt1 , tanhbnd none yet should be provable
    tanadd tanaddap
    sinltx sin01bnd, sinbnd Although we can prove the 𝐴 ≤ 1 case (see sin01bnd) or the 1 < 𝐴 case (from sinbnd), set.mm uses real number trichotomy to combine those cases.
    ruc none A proof would need either excluded middle or countable choice, per [BauerHanson]
    dvdsaddre2b none Something along these lines (perhaps with real changed to rational) may be possible
    fsumdvds , 3dvds none May be possible when summation is well enough developed
    sumeven , sumodd , evensumodd , oddsumodd , pwp1fsum , oddpwp1fsum none Presumably possible when summation is well enough developed
    divalglem0 and other divalg lemmas divalglemnn and other lemmas Since the end result divalg is the same, we don't list all the differences in lemmas here.
    gcdcllem1 , gcdcllem2 , gcdcllem3 gcdn0cl, gcddvds, dvdslegcd These are lemmas which are part of the proof of theorems that iset.mm proves a somewhat different way
    seq1st none The sequence passed to seq, at least as handled in theorems such as seqf, must be defined on all integers greater than or equal to 𝑀, not just at 𝑀 itself. It may be possible to patch this up, but seq1st is unused in set.mm.
    algr0 ialgr0 The 𝐹:𝑆𝑆 hypothesis is added (related theorems already have that hypothesis).
    df-lcmf and theorems using it none Although this could be defined, most of the theorems would need decidability conditions analogous to zsupcl
    absproddvds , absprodnn none Needs product to be developed, but once that is done seems like it might be possible.
    fissn0dvds , fissn0dvdsn0 none Possibly could be proved using findcard2 or the like.
    coprmprod , coprmproddvds none Can investigate once product is better developed.
    isprm7 none Presumably provable but likely to need further development of the floor function for irrational numbers (as seen in flapcl and presumably similar theorems which could be proved).
    maxprmfct none Presumably provable with suitable adjustments to the condition for the existence of the supremum
    ncoprmlnprm none Presumably provable but the set.mm proof uses excluded middle
    zsqrtelqelz nn0sqrtelqelz We don't yet have much on the square root of a negative number
    vfermltlALT vfermltl the set.mm proof of vfermltlALT should be intuitionizable
    iserodd none the set.mm proof uses isercoll2
    pclem pclem0, pclemub, pclemdc
    pcadd2 pcadd the set.mm proof uses xrltnle
    sumhash sumhashdc
    unben unbendc not possible as stated, as shown by exmidunben
    4sqlem11 none The set.mm proof uses ssfi to show that 𝐴, ran 𝐹, and (𝐴 ∪ ran 𝐹) are finite.
    4sqlem12 none the set.mm proof would apparently work if 4sqlem11 can be proved (probably with nonempty changed to inhabited).
    4sqlem13 none adapting the set.mm proof would require showing that 𝑇 is decidable (or something similar).
    4sqlem14 none adapting the set.mm proof would require showing that 𝑇 is decidable (or something similar).
    4sqlem15 , 4sqlem16 none the set.mm proof would intuitionize with minimal changes
    4sqlem17 none adapting the set.mm proof would require showing that 𝑇 is decidable (or something similar).
    4sqlem18 none adapting the set.mm proof would require showing that 𝑇 is decidable (or something similar).
    4sqlem19 none the set.mm proof would intuitionize with minimal changes (if previous lemmas could be proved)
    4sq none the set.mm proof would intuitionize with minimal changes (if the lemmas could be proved)
    isstruct2 isstruct2im, isstruct2r The difference is the addition of the 𝐹𝑉 condition for the reverse direction.
    isstruct isstructim, isstructr The difference is the addition of the 𝐹𝑉 condition for the reverse direction.
    slotfn slotslfn
    strfvnd strnfvnd
    strfvn strnfvn
    strfvss strfvssn
    setsval setsvala
    setsidvald strsetsid
    fsets none Apparently would need decidable equality on 𝐴 or some other condition.
    setsdm none The set.mm proof relies on undif1
    setsstruct2 none The set.mm proof relies on setsdm
    setsexstruct2 , setsstruct none The set.mm proofs rely on setsstruct2
    setsres setsresg
    setsabs setsabsd
    strfvd strslfvd
    strfv2d strslfv2d
    strfv2 strslfv2
    strfv strslfv
    strfv3 strslfv3
    strssd strslssd
    strss strslss
    str0 strsl0
    strfvi none The set.mm proof uses excluded middle to combine the proper class and set cases.
    setsid setsslid
    setsnid setsslnid
    sbcie2s none Apparently would require conditions that 𝐴 and 𝐵 are sets.
    sbcie3s none Apparently would require conditions that 𝐴, 𝐵, and 𝐶 are sets.
    elbasfv , elbasov , strov2rcl none The set.mm proofs rely on excluded middle.
    basprssdmsets none The set.mm proof relies on setsdm
    ressval ressid2, ressval2 For the 𝐵𝐴 and ¬ 𝐵𝐴 cases, respectively.
    ressbas none Apparently needs to have conditions added, for example that 𝑊 is a set plus one of 𝐵𝐴 or ¬ 𝐵𝐴.
    ressbas2 , ressbasss none The set.mm proof relies on ressbas .
    resslem , ress0 none The set.mm proof relies on excluded middle.
    ressinbas none Apparently needs to have conditions added, for example that 𝑊 is a set plus one of 𝐵𝐴 or ¬ 𝐵𝐴.
    ressval3d none The set.mm proof relies on setsidvald and sspss .
    ressress none The set.mm proof relies on ressinbas and excluded middle.
    ressabs none The set.mm proof relies on ressress but at first glance this would appear to be feasible given the 𝐵𝐴 condition.
    strle1 strle1g
    strle2 strle2g
    strle3 strle3g
    1strstr 1strstrg
    2strstr 2strstrg
    2strbas 2strbasg
    2strop 2stropg
    2strstr1 2strstr1g
    2strbas1 2strbas1g
    2strop1 2strop1g
    grpstr grpstrg
    grpbase grpbaseg
    grpplusg grpplusgg
    ressplusg none The set.mm proof relies on resslem
    grpbasex , grpplusgx grpbaseg, grpplusgg Marked as discouraged even in set.mm.
    rngstr rngstrg
    rngbase rngbaseg
    rngplusg rngplusgg
    rngmulr rngmulrg
    ressmulr , ressstarv none The set.mm proof relies on resslem
    srngstr srngstrd
    srngbase srngbased
    srngplusg srngplusgd
    srngmulr srngmulrd
    srnginvl srnginvld
    lmodstr lmodstrd
    lmodbase lmodbased
    lmodplusg lmodplusgd
    lmodsca lmodscad
    lmodvsca lmodvscad
    ipsstr ipsstrd
    ipsbase ipsbased
    ipsaddg ipsaddgd
    ipsmulr ipsmulrd
    ipssca ipsscad
    ipsvsca ipsvscad
    ipsip ipsipd
    resssca , ressvsca , ressip none The set.mm proof relies on resslem
    phlstr , phlbase , phlplusg , phlsca , phlvsca , phlip none Intuitionizing these will be straightforward once we get around to it, in a manner similar to lmodstrd. The proofs will use theorems like strle1g, strleund, and opelstrsl.
    topgrpstr topgrpstrd
    topgrpbas topgrpbasd
    topgrpplusg topgrpplusgd
    topgrptset topgrptsetd
    resstset none The set.mm proof relies on resslem
    otpsstr , otpsbas , otpstset , otpsle none Unused in set.mm. If we want to develop this more we may need to figure out whether to define order in terms of < or as the relationship between those may be different without excluded middle.
    0rest none Might need a 𝐴 ∈ V condition added, and this theorem seems to be mostly be used in conjunction with excluded middle.
    topnval topnvalg
    topnid topnidg
    topnpropd topnpropgd
    prdsbasex none Would need some conditions on whether 𝑅 is a function, on set existence, or the like. However, it is unused in set.mm.
    imasvalstr , prdsvalstr , prdsvallem , prdsval , prdssca , prdsbas , prdsplusg , prdsmulr , prdsvsca , prdsip , prdsle , prdsless , prdsds , prdsdsfn , prdstset , prdshom , prdsco , prdsbas2 , prdsbasmpt , prdsbasfn , prdsbasprj , prdsplusgval , prdsplusgfval , prdsmulrval , prdsmulrfval , prdsleval , prdsdsval , prdsvscaval , prdsvscafval , prdsbas3 , prdsbasmpt2 , prdsbascl , prdsdsval2 , prdsdsval3 , pwsval , pwsbas , pwselbasb , pwselbas , pwsplusgval , pwsmulrval , pwsle , pwsleval , pwsvscafval , pwsvscaval , pwssca , pwsdiagel , pwssnf1o none At a minimum, these theorems would need new set existence conditions and other routine intuitionizing. At worst, they would need a bigger revamp for things like how order works.
    df-ordt , df-xrs , and all theorems involving ordTop or RR*s none The set.mm definitions would not seem to fit with constructive definitions of these concepts (for example, the if in df-xrs would apparently needed to be expressed in terms of a suitable maximum and perhaps other changes are needed too)
    df-qtop , df-imas , df-qus and all theorems defined in terms of quotient topology, image structure, and quotient ring. none presumably could be added in some form
    df-xps and all theorems mentioning the binary product on a structure (syntax Xs.) none The set.mm definition depends on df-imas ( "s ) and df-prds ( Xs_ ). By its nature the definition of the binary product considers every structure slot (including most notably order which presumably will need to be handled differently in iset.mm).
    df-mre , df-mrc and all theorems using the Moore or mrCls syntax none The closest we have currently is df-cls but even that doesn't function as it does in set.mm (because complements are different without excluded middle).
    df-acs and all theorems using the ACS syntax none defined in terms of the Moore syntax
    plusffval plusffvalg
    plusfval plusfvalg
    plusfeq plusfeqg
    plusffn plusffng
    issstrmgm none the set.mm proof uses ressbas2
    mgm0b none should be provable if a 𝑂 ∈ V condition is added.
    opifismgm opifismgmdc
    grpidval grpidvalg
    grpidpropd grpidpropdg
    gsumvalx none Would seem to need DECID ran 𝐹𝑂 and DECID 𝐴 ∈ ran ... conditions. Also, probably a closer look at how to express the finite sums here and in df-gsum (most likely would need to define the tail end of the sequence to consist of occurences of the identity, as we do in df-sumdc and df-proddc).
    gsumval none likely the same caveats as gsumvalx would apply
    gsumpropd none the set.mm proof uses gsumvalx
    gsumpropd2lem , gsumpropd2 none the set.mm proof uses gsumvalx
    gsummgmpropd none the set.mm proof uses gsumpropd2
    gsumress none the set.mm proof uses gsumval
    gsumval1 none the set.mm proof uses gsumval
    gsum0 none would seem to need a 𝐺 ∈ V condition
    gsumval2a none the set.mm proof uses gsumval
    gsumval2 none the set.mm proof uses several theorems we do not have
    gsumsplit1r none the set.mm proof uses several theorems we do not have
    gsumprval none the set.mm proof uses several theorems we do not have
    gsumpr12val none the set.mm proof uses gsumprval
    sgrp0b none the set.mm proof uses mgm0b
    sgrpidmnd sgrpidmndm changes nonempty to inhabited
    issubmnd none the set.mm proof uses ressbas2 and ressplusg
    ress0g none the set.mm proof uses ressbas2 and ressplusg
    submnd0 none the set.mm proof uses ressbas2 , ressbasss , and ressplusg
    prdsplusgcl none the set.mm proof uses prdsplusgval , prdsbasmpt , and prdsbasprj
    prdsidlem none the set.mm proof uses prdsplusgval , prdsbasmpt , prdsbasprj , and prdsbasfn
    prdsmndd , prds0g , pwsmnd , pws0g none the set.mm proofs use structure product theorems not present in iset.mm
    imasmnd2 , imasmnd , imasmndf1 none relies on image structure theorems not present in iset.mm
    xpsmnd none the set.mm proof uses prdsmndd
    issubm2 none the set.mm proof uses issubmnd
    issubmndb none the set.mm proof uses issubm2
    resmndismnd none the set.mm proof uses issubmndb
    submmnd , submbas , subm0 , subsubm none the set.mm proofs use structure restriction theorems not present in iset.mm
    resmhm , resmhm2 , resmhm2b none the set.mm proofs use structure restriction theorems not present in iset.mm
    submacs none this is in terms of the ACS syntax
    mndind none this is in terms of the mrCls syntax
    prdspjmhm none the set.mm proof uses structure product theorems not present in iset.mm
    pwspjmhm , pwsdiagmhm , pwsco1mhm , pwsco2mhm none the set.mm proof uses structure product theorems not present in iset.mm
    resgrpplusfrn none the set.mm proof uses ressbas2
    grppropstr none The forward direction seems provable; the reverse direction might need a 𝐾 ∈ V condition.
    grpss none may be provable (perhaps with slight changes), but unused in set.mm
    isgrpix isgrpi Marked as discouraged even in set.mm.
    grpinvfval grpinvfvalg
    grpinvfn grpinvfng
    grpinvfvi none the set.mm proof uses case elimination on 𝐺 ∈ V
    grpsubfval grpsubfvalg
    df-cnfld and all theorems using CCfld none Could presumably be defined in some form, but we'd have to look at the literature definitions of a constructive field and see how we'd need to define this. Plus questions about whether to define order in terms of < or .
    istop2g istopfin
    iinopn none The set.mm proof relies on abrexfi
    riinopn none The set.mm proof relies on iinopn (the other issues in the set.mm proof could apparently be handled by fin0or).
    rintopn none The set.mm proof relies on riinopn
    toponsspwpw toponsspwpwg
    toprntopon none Presumably could be proved but the set.mm proof does not work as it is.
    topsn none The set.mm proof relies on pwsn
    tpsprop2d none The set.mm proof does not work as-is. Unused in set.mm
    basdif0 none The set.mm proof relies on undif1
    0top none The set.mm proof relies on sssn
    en2top none The set.mm proof relies on strict dominance
    2basgen 2basgeng
    tgdif0 none The set.mm proof relies on excluded middle
    indistopon none The set.mm proof relies on sspr
    indistop , indisuni none The set.mm proof relies on indistopon
    fctop none The set.mm proof relies on theorems we don't have including con1d , ssfi , unfi , rexnal , and difindi .
    fctop2 none The set.mm proof relies on fctop
    cctop none The set.mm proof relies on theorems we don't have including con1d , rexnal , and difindi .
    ppttop , pptbas none The set.mm proof relies on theorems we don't have including orrd and ianor
    indistpsx , indistps , indistps2 , indistpsALT , indistps2ALT none The set.mm proofs rely on indiscrete topology theorems we don't have
    isopn2 none The set.mm proof relies on dfss4
    opncld none The set.mm proof relies on isopn2
    iincld none The set.mm proof relies on opncld
    intcld none The set.mm proof relies on iincld
    incld none The set.mm proof relies on intcld
    riincld none The set.mm proof relies on iincld , incld , and case elimination
    clscld none The set.mm proof relies on intcld
    clsf none The set.mm proof relies on clscld
    clsval2 none The set.mm proof relies on dfss4 and opncld
    ntrval2 none The set.mm proof relies on dfss4 and clsval2
    ntrdif , clsdif none
    cmclsopn none The set.mm proof relies on dfss4 and clsval2
    cmntrcld none The set.mm proof relies on opncld
    iscld3 , iscld4 none
    clsidm none The set.mm proof relies on clscld
    0ntr none The set.mm proof relies on ssdif0
    elcls , elcls2 none
    clsndisj none The set.mm proof relies on elcls
    elcls3 none The set.mm proof relies on elcls
    opncldf1 , opncldf2 , opncldf3 none The set.mm proofs rely on dfss4 and opncld
    isclo none One direction of the biconditional may be provable by taking the set.mm proof and replacing undif with undifss
    isclo2 none The set.mm proof relies on isclo
    indiscld none Something along these lines may be possible once we define the indiscrete topology
    neips neipsm
    neindisj none The set.mm proof relies on clsndisj
    opnnei none Apparently the set.mm proof could easily be adapted for the case in which 𝑆 is inhabited
    neindisj2 none The set.mm proof relies on elcls
    neipeltop , neiptopuni , neiptoptop , neiptopnei , neiptopreu none The set.mm proofs rely on several theorems we do not have.
    df-lp and all theorems using the limPt syntax none
    df-perf and all theorems using the Perf syntax none
    restbas restbasg
    restsn2 none The set.mm proof relies on topsn
    restcld none The set.mm proof relies on opncld
    restcldi none The set.mm proof relies on restcld
    restcldr none The set.mm proof relies on restcld
    restfpw none The set.mm proof relies on ssfi
    neitr none The set.mm proof relies on inundif
    restcls none The set.mm proof relies on clscld
    restntr none The set.mm proof relies on excluded middle
    resstopn none The set.mm proof relies on resstset
    resstps none The set.mm proof relies on resstopn
    lmrel lmreltop
    iscnp2 iscnp
    cnptop1 , cnptop2 none
    cnprcl cnprcl2k
    cnpf , cnpcl cnpf2
    cnprcl2 cnprcl2k
    cnpimaex icnpimaex
    cnpco cnptopco
    iscncl none The set.mm proof relies on opncld
    cncls2i none The set.mm proof relies on clscld
    cnclsi none The set.mm proof relies on cncls2i
    cncls2 none The set.mm proof relies on cncls2i and iscncl
    cncls none The set.mm proof relies on cncls2 and cnclsi
    cncnp2 cncnp2m
    cnpresti cnptopresti
    cnprest cnptoprest
    cnprest2 cnptoprest2
    cnindis none The set.mm proof relies on indiscrete topology theorems that we don't have.
    paste none The set.mm proof relies on restcldr
    lmcls , lmcld none The set.mm proof relies on elcls
    lmcnp lmtopcnp
    df-cmp and all compactness (syntax Comp) theorems none How compactness fares without excluded middle is a complicated topic. See for example [HoTT], section 11.5.
    df-haus and all Hausdorff (syntax Haus) theorems none Perhaps there would need to be an apartness relation to replace the use of negated equality.
    df-conn and all connected toplogy (syntax Conn) theorems none would apparently need a lot of changes to work
    df-1stc and all first-countable theorems none Worth considering the definition of countable seen in theorems such as ctm and finct, as well as whatever else might come up.
    df-2ndc and all second-countable theorems none Worth considering the definition of countable seen in theorems such as ctm and finct, as well as whatever else might come up.
    df-lly and all theorems using the Locally syntax none
    df-xko and all theorems using the compact-open topology syntax (^ko) none not clear what is possible here
    ptval none This would need more extensive development of theorems related to the Xt_ syntax (not just df-pt itself).
    ptpjpre1 none Perhaps would be provable in the case where 𝐴 has decidable equality.
    elpt , elptr , elptr2 , ptbasid , ptuni2 , ptbasin , ptbasin2 , ptbas , ptpjpre2 , ptbasfi , pttop , ptopn , ptopn2 none Although some parts of these product topology theorems may be intuitionizable, it isn't clear doing so would produce a set of theorems which function as desired.
    txcld none The set.mm proof relies on difxp
    txcls none The set.mm proof relies on txcld
    txcnpi none Should be provable (via icnpimaex and cnpf2) but may need an additional 𝐿 ∈ Top hypothesis.
    ptcld none The set.mm proof depends on pttop , boxcutc , ptopn2 , and riincld
    dfac14 none The left hand side implies excluded middle by acexmid; we could see whether the proof that the right hand side implies choice is also valid without excluded middle.
    txindis none The set.mm proof relies on excluded middle, indistop , and indisuni .
    df-hmph and all theorems using that syntax none presumably would need some modifications to the parts which use set difference
    hmeofval hmeofvalg
    hmeocls none the set.mm proof uses cncls2i
    hmeoqtop none relies on qTop syntax
    pt1hmeo none the set.mm proof uses ptcn
    ptuncnv , ptunhmeo none the set.mm proofs use ptuni
    xmetrtri2 none Presumably this or something similar could be defined once we define RR*s ( df-xrs ) or something along those lines.
    xmetgt0 , metgt0 xmeteq0, meteq0 Presumably would require defining apartness on 𝑋 or something along those lines.
    xbln0 xblm
    blin blininf
    setsmsbas setsmsbasg
    setsmsds setsmsdsg
    setsmstset setsmstsetg
    setsmstopn , setsxms , setsms , tmsval , tmslem , tmsbas , tmsds , tmstopn , tmsxms , tmsms none Presumably could prove these or similar theorems, analogous to setsmsbasg
    blcld none The set.mm proof relies on xrltnle
    blcls none The set.mm proof relies on blcld
    blsscls none The set.mm proof relies on blcls
    stdbdmetval bdmetval
    stdbdxmet bdxmet
    stdbdmet bdmet
    stdbdbl bdbl
    stdbdmopn bdmopn
    ressxms , ressms none Awaits revision of df-ress as described at Clean up multifunction restriction operator for extensible structures in iset.mm
    prdsxms , prdsms none This would need more extensive development of theorems related to the Xs_ syntax (not just df-prds itself).
    pwsxms , pwsms none This would need more extensive development of theorems related to the ^s syntax (not just df-pws itself).
    tmsxps xmetxp tmsxps relies on structure products and related theorems
    tmsxpsmopn xmettx tmsxpsmopn relies on structure products and related theorems
    dscmet , dscopn none The set.mm definition for the discrete metric, and the proofs, would seem to rely on equality being decidable.
    qtopbaslem qtopbasss
    iooretop iooretopg
    icccld , icopnfcld , iocmnfcld , qdensere none depend on various closed set theorems
    cnfldtopn none if we use (MetOpen‘(abs ∘ − )) as our notation for the topology of the complex numbers, this theorem is not needed
    cnfldtopon cntoptopon
    cnfldtop cntoptop
    unicntop unicntopcntop
    cnopn cnopncntop
    qdensere2 none the set.mm proof depends on qdensere
    blcvx none presumably provable for either the 𝑇 = 0 case or the 𝑇 ∈ (0(,]1) case; set.mm uses excluded middle to combine those two cases
    tgioo2 tgioo2cntop
    rerest rerestcntop
    tgioo3 none Until we have defined RRfld (presumably closely related to the issues described at the df-cnfld entry here), we can use (topGen‘ran (,)) as a notation for the topology of the real numbers (as seen at tgioo2cntop).
    zcld none the set.mm proof uses the floor function in ways that we are unlikely to be able to intuitionize
    iccntr none the set.mm proof uses real number trichotomy in many steps
    opnreen none the set.mm proof is not usable as-is but it would be interesting to see if some portions can be adapted
    rectbntr0 none the set.mm proof relies on various theorems we do not have
    xmetdcn2 none the set.mm theorem is defined in terms of the RR*s syntax
    xmetdcn none the set.mm theorem is defined in terms of the ordTop syntax and uses xmetdcn2 in the proof
    metdcn2 none the set.mm proof relies on xmetdcn
    metdcn none the set.mm proof relies on metdcn2
    msdcn none the set.mm proof relies on metdcn2
    cnmpt1ds none the set.mm proof relies on msdcn
    cnmpt2ds none the set.mm proof relies on msdcn
    abscn abscn2, abscncf presumably provable (expressing the topology of the complex numbers as (MetOpen‘(abs ∘ − )) if iset.mm doesn't have CCfld yet).
    metdsval none the set.mm proof uses infex
    metdsf none the set.mm proof uses infxrcl
    addcnlem addcncntoplem expresses the topology of the complex numbers as (MetOpen‘(abs ∘ − ))
    addcn addcncntop expresses the topology of the complex numbers as (MetOpen‘(abs ∘ − ))
    subcn subcncntop expresses the topology of the complex numbers as (MetOpen‘(abs ∘ − ))
    mulcn mulcncntop expresses the topology of the complex numbers as (MetOpen‘(abs ∘ − ))
    divcn divcnap
    fsumcn fsumcncntop
    fsum2cn none the set.mm proof uses fsumcn
    expcn none the set.mm proof uses mulcn
    divccn none Not equal would need to be changed to apart. Also, the set.mm proof uses mulcn
    sqcn none the set.mm proof uses expcn
    divccncf divccncfap
    cncfcn cncfcncntop
    cncfcn1 cncfcn1cntop
    cncfmpt2f cncfmpt2fcntop
    cncfmpt2ss none would apparently only need a change to the notation for the topology on the complex numbers
    cdivcncf cdivcncfap
    cnmpopc none this kind of piecewise definition would apparently rely on real number trichotomy or something similar
    cnrehmeo cnrehmeocntop
    ivth ivthinc
    ivth2 ivthdec
    ivthle2 ivthdec the set.mm proof uses leloe
    df-limc df-limced df-limced is adapted from ellimc3 in set.mm
    df-dv df-dvap The definition is adjusted for the notation of the topology on the complex numbers, and for apartness versus negated equality.
    df-dvn and all theorems mentioning iterated derivative (Dn) none should be easily intuitionizable
    df-cpn and all theorems mentioning -times continuously differentiable functions (C^n) none should be easily intuitionizable
    reldv reldvg
    limcvallem , limcfval , ellimc none rely on decidability of real number equality
    ellimc3 ellimc3apf, ellimc3ap
    limcdif limcdifap changes not equal to apart and adds 𝐴 ⊆ ℂ hypothesis
    ellimc2 none Presumably provable with not equal changed to apart. If iset.mm doesn't have CCfld yet, use (MetOpen‘(abs ∘ − )) for the topology of the complex numbers (see cnfldtopn in set.mm).
    limcmo limcimo
    limcmpt limcmpted
    limcmpt2 none
    limcres none Although this would appear to be provable, it might benefit from some additional theorems which help us manipulate t and metric spaces. If iset.mm doesn't have CCfld yet, use (MetOpen‘(abs ∘ − )) for the topology of the complex numbers (see cnfldtopn in set.mm). Proof sketch: because interiors are open, we can form a ball around 𝐵 which is contained in ((int‘𝐽)‘(𝐶 ∪ {𝐵})) which gives us the delta we need to apply ellimc3ap for (𝐹 lim 𝐵) (given that we can apply ellimc3ap for ((𝐹𝐶) lim 𝐵) when working within 𝐶).
    cnplimc cnplimccntop
    limccnp limccnpcntop
    limccnp2 limccnp2cntop
    limcco limccoap limccoap is only usable in the case where 𝑥 # 𝑋 implies R(x) # 𝐶 so it is less general than limcco
    limciun none The set.mm proof relies on fofi , rintopn and ellimc2 .
    limcun none The set.mm proof relies on limciun .
    dvlem dvlemap not equal is changed to apart
    dvfval dvfvalap changes not equal to apart and changes the notation for the topology on the complex numbers
    eldv eldvap changes not equal to apart and changes the notation for the topology on the complex numbers
    dvbssntr dvbssntrcntop changes the notation for the topology on the complex numbers
    dvbsss dvbsssg
    dvfg dvfgg
    dvf dvfpm
    dvfcn dvfcnpm
    dvres none The set.mm proof relies on restntr and limcres . It may be worth seeing if it is easier to prove the 𝑆 ∈ {ℝ, ℂ} case.
    dvres2 none The set.mm proof relies on restntr
    dvres3 none The set.mm proof relies on dvres2
    dvres3a none The set.mm proof relies on dvres2
    dvidlem dvidlemap
    dvcnp none would appear to rely on decidable equality of real numbers
    dvcnp2 dvcnp2cntop
    dvaddbr dvaddxxbr dvaddbr allows 𝑋 and 𝑌 to be different and uses excluded middle when handling that possibility.
    dvmulbr dvmulxxbr
    dvadd dvaddxx
    dvmul dvmulxx
    dvaddf dviaddf
    dvmulf dvimulf
    dvcmul none unused in set.mm and the set.mm proof depends on dvres2
    dvcmulf none the set.mm proof depends on dvres , dvres3 , and caofid2
    dvcobr dvcoapbr dvcoapbr adds a 𝑢 # 𝐶 → (𝐺𝑢) # (𝐺𝐶) condition
    dvco none the set.mm proof depends on dvcobr
    dvcof none the set.mm proof depends on dvcobr and dvco
    dvrec dvrecap
    dvmptres3 none the set.mm proof depends on dvres3a
    dvmptid dvmptidcn the version for real numbers would presumably be provable as well
    dvmptc dvmptccn the version for real numbers would presumably be provable as well
    dvmptcl dvmptclx adds a 𝑋𝑆 hypothesis
    dvmptadd dvmptaddx adds a 𝑋𝑆 hypothesis
    dvmptmul dvmptmulx adds a 𝑋𝑆 hypothesis
    dvmptres2 none the set.mm proof uses dvres
    dvmptres none the set.mm proof uses dvmptres2
    dvmptcmul dvmptcmulcn dvmptcmulcn is the case where both 𝑋 and 𝑆 are itself rather than subsets. The set.mm proof of dvmptcmul uses dvmptres2 .
    dvmptdivc none the set.mm proof uses dvmptcmul
    dvmptneg dvmptnegcn dvmptnegcn is for rather than a subset thereof
    dvmptsub dvmptsubcn dvmptsubcn is for rather than a subset thereof
    dvmptcj dvmptcjx adds a 𝑋𝑆 hypothesis
    dvmptre none Presumably needs a 𝑋 ⊆ ℝ condition added. Also, the set.mm proof relies on dvmptcmul (with 𝑆 set to ).
    dvmptim none Presumably needs a 𝑋 ⊆ ℝ condition added. Also, the set.mm proof relies on dvmptcmul (with 𝑆 set to ).
    dvmptntr none the set.mm proof uses dvres
    dvmptco none the set.mm proof uses dvcof
    dvrecg none the set.mm proof uses dvmptco
    dvmptdiv none the set.mm proof uses dvrecg
    dvmptfsum none the set.mm proof uses dvmptc and dvmptres
    dvcnvlem , dvcnv none Not equal would need to change to apart and notation for the topology on the complex numbers would change. More seriously, the set.mm proof uses limcco . Changing to limccoap may be possible given a condition along the lines of 𝑥𝑋𝑦𝑋(𝑥 # 𝑦 ↔ (𝐹𝑥) # (𝐹𝑦).
    dvexp3 none the set.mm proof uses dvmptres and dvmptco
    dvle none the set.mm proof uses iccntr , dvmptntr , dvmptsub , and dvge0
    dvcnvre none the set.mm proof depends on compactness ( icccmp and cncfcnvcn ), restntr , evthicc2 , dvres , iccntr , and dvne0
    efcvx none the set.mm proof uses dvres , dvres3 , iccntr , and dvcvx
    reefgim none
    pilem2 pilem3 our proof of pilem3 is different enough from set.mm that it doesn't need to go via pilem2
    tanabsge none the set.mm proof uses real number trichotomy
    sinq12ge0 none the set.mm proof uses leloe
    cosq14ge0 none the set.mm proof uses sinq12ge0
    pige3ALT pige3 the set.mm proof uses various theorems we do not have
    sineq0 none the set.mm proof uses various theorems not in iset.mm
    coseq1 none the set.mm proof uses sineq0
    efeq1 none the set.mm proof uses sineq0
    cosne0 none the set.mm proof uses sineq0
    cosord cosordlem, cos11 presumably provable but the set.mm proof uses real number trichotomy
    sinord none the set.mm proof depends on cosord
    recosf1o ioocosf1o the set.mm proof of recosf1o relies on ivthle2
    resinf1o none the set.mm proof relies on recosf1o
    tanord1 none the set.mm proof relies on ltord1
    tanord none the set.mm proof relies on tanord1 , real number trichotomy, and ltord1
    tanregt0 none the set.mm proof relies on cosne0 , rpcoshcl , rptanhcl , and tanhbnd
    efgh none depends on SubGrp and CCfld
    efif1o none depends on complex square root
    efifo none depends on efif1o
    eff1o , efabl , efsubm , circgrp , circsubm none
    df-log df-relog
    df-cxp df-rpcxp we only define the power function for a positive real base for reasons described in the df-relog comment
    logrn , ellogrn , dflog2 none see df-relog comment for discussion of complex logarithms
    relogrn none Should be provable given reeff1o but perhaps it is better to avoid the theorems involving ran log from set.mm because they would mean something different with df-relog than with the set.mm definition.
    logrncn , eff1o2 , logf1o none see df-relog comment for discussion of complex logarithms
    logrncl none see df-relog comment for discussion of complex logarithms
    logcl relogcl
    logimcl none see df-relog comment for discussion of complex logarithms
    logcld relogcld
    logimcld , logimclad , abslogimle , logrnaddcl none see df-relog comment for discussion of complex logarithms
    eflog reeflog
    logeq0im1 none see df-relog comment for discussion of complex logarithms
    logccne0 logrpap0
    logne0 logrpap0 would be provable but logrpap0 changes not equal to apart and will generally be more helpful)
    logef relogef
    logeftb relogeftb
    logneg , logm1 , lognegb none See df-relog comment for discussion of complex logarithms (including logarithms on negative reals, since iset.mm only defines the logarithm on +).
    explog reexplog
    relog none see df-relog comment for discussion of complex logarithms
    reloggim none may be possible if more group theorems and notation are available
    logfac none Should be provable. Because of the way seqhomo is used in the set.mm proof, it may be necessary to special-case 𝑁 = 1 and start the main proof with two, or prove an analogue of seq3homo which allows using + on one side of the equation and on the other.
    eflogeq none see df-relog comment for discussion of complex logarithms
    logcj , efiarg , cosargd , cosarg0d , argregt0 , argrege0 , argimgt0 , argimlt0 , logimul , logneg2 , logmul2 , logdiv2 , abslogle , tanarg none see df-relog comment for discussion of complex logarithms
    logdivlt none the set.mm proof uses real number trichotomy
    logdivle none the set.mm proof uses logdivlt
    dvrelog none the set.mm proof uses dvres3 and dvcnvre
    relogcn none the set.mm proof uses dvrelog
    ellogdm , logdmn0 , logdmnrp , logdmss , logcnlem2 , logcnlem3 , logcnlem4 , logcnlem5 , logcn , dvloglem , logdmopn , logf1o2 , dvlog , dvlog2lem , dvlog2 none see df-relog comment for discussion of complex logarithms
    advlog none the set.mm proof uses dvmptid , dvmptres , dvrelog , dvmptc , and dvmptsub
    advlogexp none the set.mm proof uses various derivative theorems not present in iset.mm
    efopn none the set.mm proof makes use of the complex logarithm
    logtayl , logtaylsum , logtayl2 none see df-relog comment for discussion of complex logarithms
    logccv none the set.mm proof uses dvrelog , dvmptneg , dvmptres2 , dvcvx , and soisoi
    cxpval , cxpef , cxpefd rpcxpef as described at df-rpcxp we only support positive real bases
    0cxp , 0cxpd none as described at df-rpcxp we only support positive real bases
    cxpexpz , cxpexp , cxpexpzd cxpexpnn, cxpexprp as described at df-rpcxp we only support positive real bases
    cxp0 , cxp0d rpcxp0, rpcxp0d as described at df-rpcxp we only support positive real bases
    cxp1 , cxp1d rpcxp1, rpcxp1d as described at df-rpcxp we only support positive real bases
    cxpcl , cxpcld rpcncxpcl, rpcncxpcld as described at df-rpcxp we only support positive real bases
    recxpcl , recxpcld rpcxpcl as described at df-rpcxp we only support positive real bases
    cxpne0 , cxpne0d cxpap0 the base must be a positive real and the result changes not equal to apart
    cxpeq0 none since we do not support a base of zero, does not apply
    cxpadd , cxpaddd rpcxpadd
    cxpp1 , cxpp1d rpcxpp1
    cxpneg , cxpnegd rpcxpneg
    cxpsub , cxpsubd rpcxpsub
    cxpge0 , cxpge0d rpcxpcl we only support positive real bases
    mulcxp , mulcxpd rpmulcxp
    divcxp , divcxpd rpdivcxp
    cxpmul2 , cxpmul2d cxpmul plus cxpexprp
    cxproot rpcxproot
    cxpmul2z , cxpmul2zd cxpmul plus cxpexprp
    abscxp2 abscxp
    cxplea , cxplead none the set.mm proof uses leloe
    cxple2 , cxple2d rpcxple2
    cxplt2 , cxplt2d rpcxplt2
    cxple2a , cxple2ad none the set.mm proof uses leloe
    cxpsqrt rpcxpsqrt
    cxpsqrtth rpcxpsqrtth
    dvcxp1 none the set.mm proof uses dvrelog , dvmptco , and dvmptres3
    dvcxp2 none the set.mm proof uses dvmptco
    dvsqrt none the set.mm proof uses dvcxp1
    dvcncxp1 none this is for complex bases, see dvcxp1 entry concerning a positive real base
    dvcnsqrt none see df-rsqrt comment for discussion of complex square roots
    cxpcn none as described at df-rpcxp we only support positive real bases
    cxpcn2 none presumably provable; the obvious proof would be via relogcn
    cxpcn3 none as described at df-rpcxp we only support positive real bases
    resqrtcn none the set.mm proof is in terms of the complex exponential, but this theorem should be provable one way or another
    sqrtcn none see df-rsqrt comment for discussion of complex square roots
    cxpaddle none the set.mm proof relies on leloe and other theorems we do not have
    abscxpbnd rpabscxpbnd
    root1id , root1eq1 , root1cj , cxpeq none as described at df-rpcxp we only support positive real bases
    loglesqrt none presumably provable, but the set.mm proof relies on dvmptc , dvmptres , dvrelog , dvmptco , dvle , and relogcn
    logrec none see df-relog comment for discussion of complex logarithms
    logbval rplogbval
    logbcl rplogbcl
    logbid1 rplogbid1
    logb1 rplogb1
    elogb rpelogb
    logbchbase rplogbchbase
    relogbcl rplogbcl
    relogbreexp rplogbreexp
    relogbzexp rplogbzexp
    relogbmul rprelogbmul
    relogbmulexp rprelogbmulexp
    relogbdiv rprelogbdiv
    relogbexp relogbexpap
    relogbcxp rplogbcxp
    cxplogb rpcxplogb
    relogbcxpb relogbcxpbap
    logbmpt , logbf , logbfval , relogbf , logblog none we could add a version of these if iset.mm gets the curry syntax
    angval and all other theorems expressing angle as the complex logarithm of a complex division none depends on complex logarithms and has all the usual problems with selecting which branch to operate on (which set.mm uses excluded middle for)
    quad2 none Since there is a hypothesis that 𝐷 exists, and there is no explicit selection of a principal square root, this one avoids the most obvious problems (once 𝐴 ≠ 0 is changed to 𝐴 # 0 of course). However, the set.mm proof still relies on sqeqor .
    quad none Has all the issues of quad2 plus the usual problems around selection of a primary square root of a complex number.
    1cubr none possibly provable, but the set.mm proof is in terms of 1cubrlem which uses 𝑐 with a base which is not a positive real.
    dcubic1lem , dcubic2 , dcubic1 , dcubic , mcubic , cubic2 , cubic none depends on 1cubr
    dquartlem1 , dquartlem2 , dquart , quart1cl , quart1lem , quart1 , quartlem1 , quartlem2 , quartlem3 , quartlem4 , quart none depends on quad2 and cubic
    lgsfval lgsfvalg adds 𝐴 ∈ ℤ and 𝑁 ∈ ℕ conditions
    2sqlem11 none the set.mm proof uses lgsqr and m1lgs
    2sq none the set.mm proof uses 2sqlem11
    irrdiff apdiff

    Metamath 100 status

    The Metamath 100 theorems, especially those already proved in set.mm, provide one indication of how complete iset.mm is. For each theorem it should be possible to prove it from our axioms or show that it cannot be proved (for example, showing that it implies excluded middle). In some cases the natural statement of the theorem may need to be chosen (for example, "irrational" as used in sqrt2irrap is defined in terms of apartness).

    The Metamath 100 page lists those theorems which have been proved, but here are some notes on those which have been proved in set.mm but not iset.mm:

    Theorem notes
    2. The Fundamental Theorem of Algebra The [Geuvers] reference describes a proof without excluded middle, and presumably could be used as our guide.
    4. Pythagorean Theorem There are a variety of theorems which might plausibly deserve the label of "Pythagorean Theorem" but assuming we stick with pythi from set.mm, there are a number of prerequisites.
    5. The Prime Number Theorem The set.mm proof uses df-rlim .
    7. Law of Quadratic Reciprocity Although this is a long proof it would seem like many of the needed prerequisites are present. Some parts do need intuitionizing. For example we should be able to show that {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))} is finite but it may be most conveniently done by proving a few helper theorems beyond ssfidc.
    9. The Area of a Circle At first glance defining Lebesgue measure would not proceed quite as in set.mm, as it is in terms of an infimum.
    14. Summation of Σ𝑘 ∈ ℕ(𝑘↑-2) Needs a closer look at the set.mm proof but we do have climsqz for whatever that is worth
    15. The Fundamental Theorem of Integral Calculus Although iset.mm has at least a start on developing derivatives, it has nothing on integrals yet
    18. Liouville's Theorem and the Construction of Transcendental Numbers Need to develop polynomials (and figure out how to appropriately state the theorem, as the set.mm statement seems to rely on real number equality in a way which may not apply).
    19. Four Squares Theorem It is not clear whether the set.mm proof can be intuitionized or whether another approach is needed. See the entries for 4sq and its lemmas for more detailed notes.
    20. All Primes (1 mod 4) Equal the Sum of Two Squares At first glance it would appear this would intuitionize without much trouble.
    22. The Non-Denumerability of the Continuum See the ruc entry above. We should be able to prove this given CCHOICE. As for showing that it cannot be done given just the iset.mm axioms, that is harder, and the proof in [BauerHanson] uses something called parameterized realizability which is a different technique than proving constructive taboos as we have done elsewhere in iset.mm.
    26. Leibniz' Series for Pi The first place to look if intuitionizing the set.mm proof is Abel's theorem and the second is arctangent (in particular, does this proof need arctangent for complex numbers or just for real numbers?). We do have climsqz2 .
    27. Sum of the Angles of a Triangle There's a lot to figure out in terms of defining angle and triangle (see angval above).
    30. The Ballot Problem This is a long proof but at first glance should work in iset.mm.
    31. Ramsey's Theorem A quick glance at wikipedia makes it look like Ramsey's Theorem involves some choice and/or excluded middle.
    34. Divergence of the Harmonic Series The set.mm proof depends on climcnds . Seems like this should be provable one way or another.
    35. Taylor's Theorem There are a number of things to develop before this is ready to formalize but it seems like it might be within reach.
    37. The Solution of a Cubic See entry for theorem cubic above.
    38. Arithmetic Mean/Geometric Mean We have amgm2 but assuming we want the version for finite sets seen in set.mm, we can probably just use Σ (df-sumdc) and (df-proddc) notation rather than navigating constructive fields. In set.mm the numbers being added/multiplied are nonnegative reals and we probably have to restrict to positive reals because the set.mm proof assumes that real numbers are equal to or apart from zero.
    39. Solutions to Pell's Equation There's a lot of development of Pell equations in many lemmas and definitions which would be needed.
    45. The Partition Theorem The set.mm proof uses df-bits and df-ind .
    46. The Solution of the General Quartic Equation See entry for theorem quart above.
    48. Dirichlet's Theorem Whether this is a copy-paste from set.mm or something which needs a lot of intuitionizing is not immediately clear. There are several additional notations or concepts which would need to be developed.
    49. The Cayley-Hamilton Theorem It would appear there is a lot to develop in terms of matrices, rings, etc.
    51. Wilson's Theorem Seems like this would not be hard to intuitionize.
    52. The Number of Subsets of a Set Shouldn't be hard to resolve this in the negative, by showing that it is equivalent to excluded middle (see exmidpw).
    54. The Konigsberg Bridge Problem Depends on graph theory definitions and theorems, and words over a set, but nothing that looks difficult.
    55. Product of Segments of Chords There's a lot to figure out in terms of whether we can use complex numbers to represent the plane, and the complex logarithm in particular.
    57. Heron's Formula There's a lot to figure out in terms of whether we can use complex numbers to represent the plane, and the complex logarithm in particular.
    58. Formula for the Number of Combinations The set.mm proof is not especially long proof. It may require a bit of a closer look given the uses of subsets, but it seems like it might intuitionize without much trouble.
    61. Theorem of Ceva There's a lot to figure out in terms of whether we can use complex numbers to represent the plane, but the show-stoppers if present are not obvious.
    63. Cantor's Theorem Although we have canth, current plan is to add df-sdom (using the set.mm definition, we think) and then treat this one as complete once we can prove canth2 .
    64. L'Hôpital's Rule There are enough theorems involving convergence, limits, and derivatives which are different, that significant work may be needed before this is possible.
    65. Isosceles Triangle Theorem There's a lot to figure out in terms of whether we can use complex numbers to represent the plane, and the complex logarithm in particular.
    67. e is Transcendental There's a lot to develop in terms of polynomials and algebraic numbers. Also see transcendental number at ncatlab concerning how we should define transcendental.
    70. The Perfect Number Theorem Depends on the prime count function pCnt .
    71. Order of a Subgroup There's a lot of group theory to develop to get to this point.
    72. Sylow's Theorem There's a lot of group theory to develop to get to this point. The set.mm proof of sylow1 uses pcadd2
    73. Ascending or Descending Sequences Seems unlikely to be provable without significant changes.
    75. The Mean Value Theorem As with the Intermediate Value Theorem, this is likely to need significant changes of some kind.
    76. Fourier Series This is a very large proof which depends on a lot of theorems involving derivatives and integrals.
    77. Sum of kth powers Will require development of Bernoulli polynomials which at least in set.mm are defined using the well-founded recursive function generator wrecs .
    78. The Cauchy-Schwarz Inequality Will require development of inner products and norms.
    81. Erdős's proof of the divergence of the inverse prime series The set.mm proof uses isumsup
    83. The Friendship Theorem Requires development of graph theory.
    85. Divisibility by 3 Rule The set.mm proof would appear to be intuitionizable without much trouble.
    86. Lebesgue Measure and Integration Requires developing integrals and Lebesgue Measure
    87. Desargues's Theorem This is a long proof with unmet prerequisites. Also, it may be using in ways which won't work in iset.mm.
    88. Derangements Formula Presumably the biggest need here is further developing the floor function for irrational numbers (as seen in flapcl and presumably similar theorems which could be proved).
    89. The Factor and Remainder Theorems Requires further development of polynomials.
    90. Stirling's Formula This is a long proof and would require a look at how convergence is handled.
    93. The Birthday Problem Would appear to be intuitionizable.
    94. The Law of Cosines There's a lot to figure out in terms of defining angle and triangle (see angval above).
    96. Principle of Inclusion/Exclusion In light of theorems like unfiexmid this would presumably need additional conditions, if it is possible even then.
    97. Cramer's Rule Requires more development of matrices and determinants.
    98. Bertrand's Postulate This is a long proof. It uses logdivlt .

    Bibliography   
    1. [AczelRathjen] Aczel, Peter, and Rathjen, Michael, "Constructive Set Theory", 2018, http://www1.maths.leeds.ac.uk/~rathjen/book.pdf
    2. [Apostol] Apostol, Tom M., Calculus, vol. 1, 2nd ed., John Wiley & Sons Inc. (1967) [QA300.A645 1967].
    3. [ApostolNT] Apostol, Tom M., Introduction to analytic number theory, Springer-Verlag, New York, Heidelberg, Berlin (1976) [QA241.A6].
    4. [Bauer] Bauer, Andrej, "Five stages of accepting constructive mathematics," Bulletin (New Series) of the American Mathematical Society, 54:481-498 (2017), DOI: 10.1090/bull/1556 .
    5. [BauerHanson] Bauer, Andrej and Hanson, James E, "The Countable Reals", arXiv:2404.01256, 2024, https://arxiv.org/abs/2404.01256
    6. [BauerSwan] Bauer, Andrej and Swan, Andrew, "Every Metric Space is Separable in Function Realizability", Logical Methods in Computer Science, Volume 15, Issue 2, 2019, pp. 14:1–14:7, https://lmcs.episciences.org/5501/pdf
    7. [BauerTaylor] Andrej Bauer and Paul Taylor, "The Dedekind Reals in Abstract Stone Duality", Mathematical structures in computer science, 19(4):757–838, 2009, http://www.paultaylor.eu/ASD/dedras.pdf
    8. [BellMachover] Bell, J. L., and M. Machover, A Course in Mathematical Logic, North-Holland, Amsterdam (1977) [QA9.B3953].
    9. [Bobzien] Bobzien, Susanne, "Stoic Logic", The Cambridge Companion to Stoic Philosophy, Brad Inwood (ed.), Cambridge University Press (2003-2006), https://philpapers.org/rec/BOBSL.
    10. [BourbakiEns] Bourbaki, Nicolas, Théorie des ensembles, Springer-Verlag, Berlin Heidelberg (2007); available in English (for purchase) at http://www.springer.com/us/book/9783540225256 (retrieved 15-Aug-2016). Page references in iset.mm are for the French edition.
    11. [BourbakiTop1] Bourbaki, Nicolas, Topologie générale, Chapitres 1 à 4, Springer-Verlag, Berlin Heidelberg (2007); available in English (for purchase) at http://www.springer.com/us/book/9783540642411 (retrieved 15-Aug-2016). Page references in set.mm are for the French edition.
    12. [ChoquetDD] Choquet-Bruhat, Yvonne and Cecile DeWitt-Morette, with Margaret Dillard-Bleick, Analysis, Manifolds and Physics, Elsevier Science B.V., Amsterdam (1982) [QC20.7.A5C48 1981].
    13. [Crosilla] Crosilla, Laura, "Set Theory: Constructive and Intuitionistic ZF", The Stanford Encyclopedia of Philosophy (Summer 2015 Edition), Edward N. Zalta (ed.), https://plato.stanford.edu/archives/sum2015/entries/set-theory-constructive/.
    14. [Moschovakis] Moschovakis, Joan, "Intuitionistic Logic", The Stanford Encyclopedia of Philosophy (Spring 2015 Edition), Edward N. Zalta (ed.), https://plato.stanford.edu/archives/spr2015/entries/logic-intuitionistic/.
    15. [Munkres] Munkres, James Raymond, Topology: a first course, Prentice-Hall, Englewood Cliffs, New Jersey (1975) [QA611.M82].
    16. [Eisenberg] Eisenberg, Murray, Axiomatic Theory of Sets and Classes, Holt, Rinehart and Winston, Inc., New York (1971) [QA248.E36].
    17. [Enderton] Enderton, Herbert B., Elements of Set Theory, Academic Press, Inc., San Diego, California (1977) [QA248.E5].
    18. [Gleason] Gleason, Andrew M., Fundamentals of Abstract Analysis, Jones and Bartlett Publishers, Boston (1991) [QA300.G554].
    19. [Geuvers] Herman Geuvers, Randy Pollack, Freek Wiedijk, Jan Zwanenburg, "Skeleton for the Proof development leading to the Fundamental Theorem of Algebra", October 2, 2000, http://www.cs.ru.nl/~herman/PUBS/FTA.mathproof.ps.gz (accessed 19 Feb 2020).
    20. [Hamilton] Hamilton, A. G., Logic for Mathematicians, Cambridge University Press, Cambridge, revised edition (1988) [QA9.H298 1988].
    21. [Heyting] Heyting, A., Intuitionism: An introduction, North-Holland publishing company, Amsterdam, second edition (1966).
    22. [Hitchcock] Hitchcock, David, The peculiarities of Stoic propositional logic, McMaster University; available at http://www.humanities.mcmaster.ca/~hitchckd/peculiarities.pdf (retrieved 3 Jul 2016).
    23. [HoTT] The Univalent Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics, https://homotopytypetheory.org/book, first edition.
    24. [Jech] Jech, Thomas, Set Theory, Academic Press, San Diego (1978) [QA248.J42].
    25. [KalishMontague] Kalish, D. and R. Montague, "On Tarski's formalization of predicate logic with identity," Archiv für Mathematische Logik und Grundlagenforschung, 7:81-101 (1965) [QA.A673].
    26. [Kreyszig] Kreysig, Erwin, Introductory Functional Analysis with Applications, John Wiley & Sons, New York (1989) [QA320.K74].
    27. [Kunen] Kunen, Kenneth, Set Theory: An Introduction to Independence Proofs, Elsevier Science B.V., Amsterdam (1980) [QA248.K75].
    28. [KuratowskiMostowski] Kuratowski, K. and A. Mostowski, Set Theory: with an Introduction to Descriptive Set Theory, 2nd ed., North-Holland, Amsterdam (1976) [QA248.K7683 1976].
    29. [Levy] Levy, Azriel, Basic Set Theory, Dover Publications, Mineola, N.Y. (2002) [QA248.L398 2002].
    30. [Lopez-Astorga] Lopez-Astorga, Miguel, "The First Rule of Stoic Logic and its Relationship with the Indemonstrables", Revista de Filosofía Tópicos (2016); available at http://www.scielo.org.mx/pdf/trf/n50/n50a1.pdf (retrieved 3 Jul 2016).
    31. [Margaris] Margaris, Angelo, First Order Mathematical Logic, Blaisdell Publishing Company, Waltham, Massachusetts (1967) [QA9.M327].
    32. [Megill] Megill, N., "A Finitely Axiomatized Formalization of Predicate Calculus with Equality," Notre Dame Journal of Formal Logic, 36:435-453 (1995) [QA.N914]; available at http://projecteuclid.org/euclid.ndjfl/1040149359 (accessed 11 Nov 2014); the PDF preprint has the same content (with corrections) but pages are numbered 1-22, and the database references use the numbers printed on the page itself, not the PDF page numbers.
    33. [Mendelson] Mendelson, Elliott, Introduction to Mathematical Logic, 2nd ed., D. Van Nostrand (1979) [QA9.M537].
    34. [Monk1] Monk, J. Donald, Introduction to Set Theory, McGraw-Hill, Inc. (1969) [QA248.M745].
    35. [Monk2] Monk, J. Donald, "Substitutionless Predicate Logic with Identity," Archiv für Mathematische Logik und Grundlagenforschung, 7:103-121 (1965) [QA.A673].
    36. [Pierik], Pierik, Ceel, "Infinite Omniscient Sets in Constructive Mathematics", Bachelor thesis Computing Science, Radboud University, June 25, 2020, https://www.cs.ru.nl/bachelors-theses/2020/Ceel_Pierik___4806182___Infinite_Omniscient_Sets_in_Constructive_Mathematics.pdf
    37. [PradicBrown2022] Pradic, Cécilia, and Brown, Chad E. (August 15, 2022), "Cantor-Bernstein implies Excluded Middle", https://arxiv.org/abs/1904.09193
    38. [Rudin] Rudin, Walter, Principles of Mathematical Analysis, McGraw-Hill, New York, second edition (1964) [QA300.R916 1964].
    39. [Quine] Quine, Willard van Orman, Set Theory and Its Logic, Harvard University Press, Cambridge, Massachusetts, revised edition (1969) [QA248.Q7 1969].
    40. [Sanford] Sanford, David H., If P, then Q: Conditionals and the Foundations of Reasoning, 2nd ed., Routledge Taylor & Francis Group (2003); ISBN 0-415-28369-8; available at https://books.google.com/books?id=h_AUynB6PA8C&pg=PA39#v=onepage&q&f=false (retrieved 3 Jul 2016).
    41. [Schechter] Schechter, Eric, Handbook of Analysis and Its Foundations, Academic Press, San Diego (1997) [QA300.S339].
    42. [Stoll] Stoll, Robert R., Set Theory and Logic, Dover Publications, Inc. (1979) [QA248.S7985 1979].
    43. [Suppes] Suppes, Patrick, Axiomatic Set Theory, Dover Publications, Inc. (1972) [QA248.S959].
    44. [TakeutiZaring] Takeuti, Gaisi, and Wilson M. Zaring, Introduction to Axiomatic Set Theory, Springer-Verlag, New York, second edition (1982) [QA248.T136 1982].
    45. [Tarski] Tarski, Alfred, "A Simplified Formalization of Predicate Logic with Identity," Archiv für Mathematische Logik und Grundlagenforschung, 7:61-79 (1965) [QA.A673].
    46. [WhiteheadRussell] Whitehead, Alfred North, and Bertrand Russell, Principia Mathematica to *56, Cambridge University Press, Cambridge, 1962 [QA9.W592 1962].

      This page was last updated on 15-Aug-2015.
    Your comments are welcome: Norman Megill nm at alum dot mit dot edu
    Copyright terms: Public domain
    W3C HTML validation [external]