Home - Intuitionistic Logic Explorer

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	|- ph   &   |- ph -> ps   ⇒   |- ps
Left 'and' elimination	ax-ia1	|- ( ( ph /\ ps ) -> ph )
Right 'and' elimination	ax-ia2	⊢ ((φ ∧ ψ) → ψ)
'And' introduction	ax-ia3	⊢ (φ → (ψ → (φ ∧ ψ)))
Definition of 'or'	ax-io	⊢ (((φ ∨ χ) → ψ) ↔ ((φ → ψ) ∧ (χ → ψ)))
'Not' introduction	ax-in1	⊢ ((φ → ¬ φ) → ¬ φ)
'Not' elimination	ax-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	⊢ (∀x∀yφ → ∀y∀xφ)
Rule of Generalization	ax-gen	⊢ φ   =>    ⊢ ∀xφ
x is bound in ∀xφ	ax-ial	⊢ (∀xφ → ∀x∀xφ)
x is bound in ∃xφ	ax-ie1	⊢ (∃xφ → ∀x∃xφ)
Define existential quantification	ax-ie2	⊢ (∀x(ψ → ∀xψ) → (∀x(φ → ψ) ↔ (∃xφ → ψ)))
Axiom of Equality	ax-8	⊢ (x = y → (x = z → y = z))
Axiom of Existence	ax-i9	⊢ ∃x x = y
Axiom of Quantifier Substitution	ax-10	⊢ (∀x x = y → ∀y 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 = y → ∀z x = y)))
Axiom of Bundling	ax-bndl	⊢ (∀z z = x ∨ (∀z z = y ∨ ∀x∀z(x = y → ∀z x = y)))
Left Membership Equality	ax-13	⊢ (x = y → (x ∈ z → y ∈ z))
Right Membership Equality	ax-14	⊢ (x = y → (z ∈ x → z ∈ 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 ∈ x ↔ z ∈ y) → x = y)
Axiom of Collection	ax-coll	⊢ (∀x ∈ 𝑎 ∃yφ → ∃𝑏∀x ∈ 𝑎 ∃y ∈ 𝑏 φ)
Axiom of Separation	ax-sep	⊢ ∃y∀x(x ∈ y ↔ (x ∈ z ∧ φ))
Axiom of Power Sets	ax-pow	⊢ ∃y∀z(∀w(w ∈ z → w ∈ x) → z ∈ y)
Axiom of Pairing	ax-pr	⊢ ∃z∀w((w = x ∨ w = y) → w ∈ z)
Axiom of Union	ax-un	⊢ ∃y∀z(∃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.

• If you see case elimination ( pm2.61 or its variants) you'll probably end up with two theorems for the two cases. In particular, if the cases were A e. _V and -. A e. _V you probably just care about the A e. _V case. On the other hand, 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 df-dc and mpjaodan.
• Non-empty almost always needs to be changed to inhabited (those terms are defined at n0rf).
• If the original proof relied on propositional/predicate logic which isn't a theorem of intuitionistic logic, maybe there is a way of expressing the logic more directly. This is perhaps the hardest one to put in cookbook form: you might need to try some things and see if anything works.
• If the original proof relied on df-ex so that it could prove a theorem for A. and then get E. for free (or vice versa), instead go look at the original proof and try to come up the analogues to each step for the other quantifier (for example, cbvrexcsf, sbcrext, rexxpf). Similarly, if you have a theorem for <_ and are trying to prove the corresponding theorem for < you'll probably need to use analogous steps rather than negation (examples: leaddsub, ltsub1, ltsub2).
• If you are dealing with a definition, try to find the best constructive definition from the literature ([HoTT] book, Stanford Encyclopedia of Philosophy, [Bauer], etc). Once you pick a definition, that'll affect the proofs which rely on that definition.
• If there is case elimination on whether variables are distinct, most of the time you just need the variant with distinct variables. Sometimes you can then remove the constraint with a temporary variable (e.g. the various sbco2* variants, nfralya, r19.3rm).
• Sometimes one direction of a biconditional holds, or subset holds instead of equality. You might be able to keep the easy direction and worry about the other one later.
• If there is case elimination sometimes only one of the two cases is possible. For example, in mosubopt the rest of the formula being proved constrains which case matters.
• If you need an additional condition (for example, because the original proof used case elimination) and you are proving a biconditional, consider whether both sides of the biconditional imply the condition. If so, you'll be able to prove the biconditional with that condition as an antecedent, and then use pm5.21nii or one of its variants to remove the antecedent (example: elxp4).
• If your proof relies on dveeq2 try dveeq2or and likewise for the other things downstream of ax-i12 or ax-bndl.
• If you have a disjunction, be reluctant to turn it into an implication using ord and the like. Instead, show that each disjunct implies what you are trying to prove and use jaoi to join those two implications into something which can hook up to the disjunction.
• Disjunctive syllogism holds in intuitionistic logic and we state it a few ways (for example orel1 and ecased) but we don't have a wide variety of convenience theorems. Unless we add those, you'll use ord or something similar followed by mpd or something similar. This may add a few steps but they are straightforward ones.
• If your proof is doing tricky things perhaps in the interest of shortness, try just expanding the definitions and applying logic in a straightforward way. See if this gets you a working (although perhaps longer) proof.
• If your proof relies on a biconditional in set.mm which isn't in iset.mm, see if one direction is in iset.mm and see which direction your proof is using. For example 19.35-1 or exnalim.
• If you are doing things with inhabited classes (beyond just applying existing inhabited class theorems), you may be able to dig up some predicate logic you haven't used in a while (e.g. raaan).
• Consider the possibility of giving up. Some things just won't have intuitionistic proofs. The more it looks like excluded middle or other non-intuitionistic statements, the more likely you are dealing with one of these. But it can be hard to have good intuition about this. In some cases it may be possible to ask "can I use this statement to prove ph \/ -. ph for an arbitrary proposition" (see ordtriexmid for example ), but this is not always an easy technique to apply.
• Switching between 2th and 2false might help (e.g. dfnul2, dfnul3, rab0).
• In many cases statements which are equivalent in classical logic become several non-equivalent statements (e.g. exclusive or, ordinals, non-empty versus inhabited, apartness versus negated equality). This is usually a good place to look for a literature reference, but don't be afraid to change the statement being proved to "what you really meant is X" as appropriate.
• If a statement has multiple equivalences in set.mm (e.g. mof and mo3 , or dffun2 and dffun3 ) and only some of them in iset.mm, sometimes a pretty similar proof will work (that is, which one to use in the original proof may have been a fairly arbitrary choice).
• A number of theorems related to functions (especially ovex and fvex ) in set.mm perform case elimination based on whether we are evaluating the function within its domain or outside it. The most straightforward solution is to use fnovex or funfvex which only work within the domain. Using these may involve rearranging logic, for example by changing rexlimivw to rexlimdva (example: ovelrn or indeed most uses of fnovex and funfvex). If a function value is inhabited, we know we are evaluating it within its domain by relelfvdm.
• It may be necessary to add conditions, such as A e. CC or A e. NN, on classes used in a theorem. For example, the original proof may have been using case elimination on whether a class is a proper class, or using ovex or fvex in a way which you are replacing with closure theorems.
• With excluded middle, (/) e. A and A =/= (/) are equivalent (where A is an ordinal). In such theorems, (/) e. A is generally the more interesting condition constructively.
• Reverse closure in set.mm uses excluded middle (for example ovrcl or ndmfvrcl ). The most general way to handle this is to add more conditions that we are evaluating operations within their domains (for example set.mm's addasspi versus iset.mm's addasspig in which conditions such as A e. N. are added, or set.mm's ltbtwnnq versus iset.mm's ltbtwnnqq, in which E. x is changed to E. x e. Q.). If the result of applying a function is inhabited, then we know we applied it within its domain - that is relelfvdm or elmpocl may be useful. (These thoughts apply to operations - in at least one place, dvdszrcl, set.mm uses the term "reverse closure" for binary relations - but this is a lot more like brel than like the reverse closure theorems described above).
• With excluded middle not equal ( =/=) and apart (#) are equivalent. When working with real and complex numbers, apartness is almost always what you want. See df-ap for more on apartness.
• Given a theorem of the form X = Y <-> Z = W we can derive X =/= Y <-> Z =/= W but in many contexts what we really want is X # Y <-> Z # W. See if the version with apartness already exists and if not consider adding it (building from basic apartness theorems like apadd1 and apmul1 for example). Once you have proved the version using apartness you can use it to prove the version with equality if you don't already have it, using notbid and apti.
• Exclusive or ( ph \/_ ps) is equivalent to ph <-> -. ps given excluded middle but we just have one direction (xorbin). Consider intuitionizing ph <-> -. ps as ph \/_ ps (example: rpnegap).
• The expression ( _I ` A ) evaluates to A if A is a set (by fvi) and the empty set if A is a proper class (by fvprc). However, combining these two facts and thus using _I to protect against proper classes does not seem to be possible without excluded middle (set.mm examples: sumeq2ii and strfvi ). Usually you will end up adding a A e. _V condition in such cases.
• If you get stuck, ask! (for example in a GitHub issue or on the mailing list). We have a number of contributors who have experience in constructive mathematics in general, or iset.mm in particular, and one of the best things about doing/learning mathematics in metamath is the collaborative nature of how we develop it.

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 ( A C_ B /\ A =/= B ) and this definition is almost always used in conjunction with excluded middle. A more natural definition might be ( A C_ B /\ E. x x e. ( B \ A ) ), 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 A e. _V and -. A e. _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
ifor	none
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 A e. _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 E! theorems still hold, but a decent number of the E* 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 ( { A } e. _V with no condition on whether A 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.
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 om
	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 A 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 -. B e. _V case which follows readily from opprc2 and dmsn0. But we presumably cannot combine the B e. _V and -. B e. _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 -. (/) e. { { (/) } } 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
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 A =/= B 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 ( F ` X ) is the empty set.
fvssunirn	fvssunirng, relfvssunirn
ndmfv	ndmfvg	The -. A e. _V case is fvprc.
elfvdm	relelfvdm
elfvex , elfvexd	relelfvdm, mptrcl
dffn5	dffn5im
fvmpti	fvmptg	The set.mm proof relies on case elimination on C e. _V
fvmpt2i	fvmpt2	The set.mm proof relies on case elimination on C e. _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 S 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.
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
ovif12	none	would be provable under the condition that ph 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 B e. dom F
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. U. A = On -> A e/ V is provable, and ( B e. On /\ U. A C_ B ) -> A e. V is provable. (One thing we presumably could prove is ( U. A C_ On /\ E. x x e. ( On \ U. A ) ) -> A e. V 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 ( ~P A i^i 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 = ( ~P A i^i 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 = { x e. { (/) } | ph } we have X C_ 1o implies X e. suc' 1o = 2o and hence X = (/) \/ X = 1o, and LEM follows (by ordtriexmidlem2 for X = (/) and rabsnt as seen in the onsucsssucexmid proof for X = 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 x and y 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 B 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 I has decidable equality.
boxcutc	none	Would seem to need a condition that A 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 { s | s C_ 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 A ~<_ B /\ -. A ~~ B, 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 { (/) } e. om
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 ( A e. Fin /\ B e. Fin /\ ( A u. B ) e. Fin ) -> ( A i^i B ) e. 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 { A , B } to a natural number would decide whether A and B 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 A =/= B; 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 A e. _V condition but even with that, the set.mm proof uses inficl
fisn	none	presumably would be provable (with an A e. _V condition added), but the set.mm proof uses inficl
fipwss	fipwssg	adds the condition that A 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 A. x e. A A. y e. ADECID x = y and B e. A 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 A 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 A = B 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 ~<_ A instead
djufi	none	we should be able to prove ( A e. Fin /\ B e. Fin ) -> ( A ⊔ B ) e. 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 om ~<_ A follows definition 8.1.4 of [AczelRathjen], p. 71. It can presumably not be shown to be equivalent to -. A e. Fin in the absence of excluded middle (see inffiexmid which isn't exactly about -. A e. Fin <-> om ~<_ A 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 ( ( S X. T ) /. R )), 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)	A. x e. RR A. y e. RR ( x <_ y \/ y <_ x ) 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 ( A x. B ) = 0 -> ( A = 0 \/ B = 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 ( { A , B } , RR , < ) rather than if ( A <_ B , B , A ). 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 xe), 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 M e. _V and N e. _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 F be defined on ( ZZ>= ` M ) not merely ( M ... N ).
seqcl	seqf, seq3clss	seqf requires that F be defined on ( ZZ>= ` M ) not merely ( M ... N ). 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 F be defined on ( ZZ>= ` M ) not merely ( M ... N ) as in sermono .
seqsplit	seq3split	seq3split requires that F be defined on ( ZZ>= ` K ) not merely ( K ... N ) 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 F be defined on ( ZZ>= ` M ) not merely ( M ... N ). 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 F, G, and H need to be defined on ( ZZ>= ` M ) not merely ( M ... N ).
seqcaopr2	seq3caopr2	The functions F, G, and H need to be defined on ( ZZ>= ` M ) not merely ( M ... N ).
seqcaopr	seq3caopr	The functions F, G, and H need to be defined on ( ZZ>= ` M ) not merely ( M ... N ).
seqf1o	seq3f1o	The functions G and H need to be defined on ( ZZ>= ` M ) not merely ( M ... N ). Also, a single set S takes the place of C and S because that is sufficient flexibility at least for now.
seradd	ser3add	The functions F, G, and H need to be defined on ( ZZ>= ` M ) not merely ( M ... N ).
sersub	ser3sub	The functions F, G, and H need to be defined on ( ZZ>= ` M ) not merely ( M ... N ).
seqid3	seq3id3
seqid	seq3id
seqid2	seq3id2
seqhomo	seq3homo
seqz	seq3z	The sequence has to be defined on ( ZZ>= ` M ) not just ( M ... N )
seqfeq4	seqfeq3	The sequence has to be defined on ( ZZ>= ` M ) not just ( M ... N )
seqdistr	seq3distr
serge0	ser3ge0	The sequence has to be defined on ( ZZ>= ` M ) not just ( M ... N )
serle	ser3le	Changes several hypotheses from ( M ... N ) to ( ZZ>= ` M )
ser1const	fsumconst	Finite summation in iset.mm is easier to express using sum_ 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 <_ A 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 A is infinite is changed from -. A e. Fin to om ~<_ A.
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 A 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	none	would be easy to prove if A e. V is changed to A e. Fin
hashen1	fihashen1
hash1elsn	none	would be easy to prove if A e. V is changed to A e. Fin
hashrabrsn	none	Presumably would need conditions around the existence of A and decidability of ph but unused in set.mm.
hashrabsn01	none	Presumably would need conditions around the existence of A and decidability of ph 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 (♯ |` om ) = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 ), but lightly used in set.mm.
hashdom	fihashdom	There is an added condition that B 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 N e. _V or -. N e. _V this could be proved (as (♯ ` { M , N } ) 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 B e. 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 B e. Fin or similar conditions.
hashimarn , hashimarni	none	Presumably would need an additional condition such as F e. Fin but unused in set.mm.
fnfz0hashnn0	none	Presumably would need an additional condition such as N e. NN0 but unused in set.mm.
fnfzo0hashnn0	none	Presumably would need an additional condition such as N e. NN0 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 -. A e. Fin to om ~<_ A 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 F and H need to be defined on ZZ>= ` M 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 ( Im ` x ) # 0 \/ 0 <_ ( Re ` x ), 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 ( * ` A ) / ( abs ` A ) as the answer if A =/= 0 and i as the answer if A = 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 A # 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 j 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 sum_.
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 Z e. _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 ( ph /\ k e. C ) -> D e. Fin can be proved from the other hypotheses, the set.mm proof of that uses ssfi .
fsum0diag	fisum0diag	Adds a N e. ZZ hypothesis
fsumrev2	fisumrev2	Adds M e. ZZ and N e. ZZ hypotheses
fsum0diag2	fisum0diag2	Adds a N e. ZZ hypothesis
fsumdivc	fsumdivapc	Changes not equal to apart
fsumless	fsumlessfi	Whether this can be proved without the C e. 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 sum_ 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 A / ( k + B ) is a set, even when k + B 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 < ( M + B ) 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 A to be apart from zero.
cvgrat	cvgratgt0	Adds a 0 < A 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 F and the sequence of its absolute values converge (that is, seq 0 ( + , F ) e. dom ~~> is an additional hypothesis beyond what set.mm has).
clim2div	clim2divap
prodfmul	prod3fmul	The functions F, G, and H need to be defined on ( ZZ>= ` M ) not merely ( M ... N ).
prodfn0	prodfap0
prodfrec	prodfrecap
prodfdiv	prodfdivap	in addition to changing not equal to apart, various hypotheses need to hold for ( ZZ>= ` M ) not merely ( M ... N )
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 prod_.
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 ( ph /\ k e. C ) -> D e. Fin can be proved from the other hypotheses, the set.mm proof of that uses ssfi .
fprod0diag	fprod0diagfz	Adds a N e. ZZ 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 A <_ 1 case (see sin01bnd) or the 1 < A 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 M, not just at M itself. It may be possible to patch this up, but seq1st is unused in set.mm.
algr0	ialgr0	The F : S --> S 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 A, ran F, and ( A u. ran F ) 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 T is decidable (or something similar).
4sqlem14	none	adapting the set.mm proof would require showing that T 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 T is decidable (or something similar).
4sqlem18	none	adapting the set.mm proof would require showing that T 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 F e. V condition for the reverse direction.
isstruct	isstructim, isstructr	The difference is the addition of the F e. V 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 A 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 A and B are sets.
sbcie3s	none	Apparently would require conditions that A, B, and C 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 B C_ A and -. B C_ A cases, respectively.
ressbas	none	Apparently needs to have conditions added, for example that W is a set plus one of B C_ A or -. B C_ A.
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 W is a set plus one of B C_ A or -. B C_ A.
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 B C_ A 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 A e. _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 R 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-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 S 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 A 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 L e. 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 X 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 o. - ) ) 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 T = 0 case or the T e. ( 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 o. - ) ) 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 o. - ) )
addcn	addcncntop	expresses the topology of the complex numbers as ( MetOpen ` ( abs o. - ) )
subcn	subcncntop	expresses the topology of the complex numbers as ( MetOpen ` ( abs o. - ) )
mulcn	mulcncntop	expresses the topology of the complex numbers as ( MetOpen ` ( abs o. - ) )
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 A C_ CC hypothesis
ellimc2	none	Presumably provable with not equal changed to apart. If iset.mm doesn't have CCfld yet, use ( MetOpen ` ( abs o. - ) ) 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 o. - ) ) for the topology of the complex numbers (see cnfldtopn in set.mm). Proof sketch: because interiors are open, we can form a ball around B which is contained in ( ( int ` J ) ` ( C u. { B } ) ) which gives us the delta we need to apply ellimc3ap for ( F lim CC B ) (given that we can apply ellimc3ap for ( ( F |` C ) lim CC B ) when working within C).
cnplimc	cnplimccntop
limccnp	limccnpcntop
limccnp2	limccnp2cntop
limcco	limccoap	limccoap is only usable in the case where x # X implies R(x) # C 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 S e. { RR , CC } 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 X and Y 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 u # C -> ( G ` u ) # ( G ` C ) 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 X C_ S hypothesis
dvmptadd	dvmptaddx	adds a X C_ S hypothesis
dvmptmul	dvmptmulx	adds a X C_ S 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 X and S are CC 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 CC rather than a subset thereof
dvmptsub	dvmptsubcn	dvmptsubcn is for CC rather than a subset thereof
dvmptcj	dvmptcjx	adds a X C_ S hypothesis
dvmptre	none	Presumably needs a X C_ RR condition added. Also, the set.mm proof relies on dvmptcmul (with S set to RR).
dvmptim	none	Presumably needs a X C_ RR condition added. Also, the set.mm proof relies on dvmptcmul (with S set to RR).
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 A. x e. X A. y e. X ( x # y <-> ( F ` x ) # ( F ` y ).
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 RR+).
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 N = 1 and start the main proof with two, or prove an analogue of seq3homo which allows using RR+ on one side of the equation and RR 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 D exists, and there is no explicit selection of a principal square root, this one avoids the most obvious problems (once A =/= 0 is changed to A # 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 ^c 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 A e. ZZ and N e. NN 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	Needs more development of number theory (for one thing, the Legendre symbol, df-lgs , itself).
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 sum_ k e. NN ( k ^ -u 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 sum_ (df-sumdc) and prod_ (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].