Most Recent Proofs - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer Most Recent Proofs
Mirrors > Home > ILE Home > Th. List > Recent		MPE Most Recent Other > MM 100

Most recent proofs These are the 100 (Unicode, GIF) or 1000 (Unicode, GIF) most recent proofs in the iset.mm database for the Intuitionistic Logic Explorer. The iset.mm database is maintained on GitHub with master (stable) and develop (development) versions. This page was created from the commit given on the MPE Most Recent Proofs page. The database from that commit is also available here: iset.mm.

See the MPE Most Recent Proofs page for news and some useful links.

Color key:

Intuitionistic Logic Explorer

User Mathboxes

Last updated on 29-Sep-2026 at 7:00 AM ET.

**Recent Additions to the Intuitionistic Logic Explorer**
Date	Label	Description
Theorem

23-Sep-2026	sineq0re 16042	A complex number whose sine is zero is real. (Contributed by NM, 17-Aug-2008.) (Revised by Mario Carneiro, 10-May-2014.) (Revised by Jim Kingdon, 23-Sep-2026.)
$/\$

18-Sep-2026	rirrdisj 17256	The rational and irrational numbers are disjoint. Here irrational means apart from any rational number. (Contributed by Jim Kingdon, 18-Sep-2026.)
#

18-Sep-2026	efnthr 16142	An equation involving an -th power. The expression is a way to write the primitive -th root of unity with the smallest positive argument. We could write it as except that we only support positive real numbers as the base for . The converse is presumably also provable but we do not have a proof yet. (Contributed by Mario Carneiro, 23-Apr-2015.) (Revised by Jim Kingdon, 18-Sep-2026.)
$/\$ $/\$

16-Sep-2026	cntzm 14155	If the centralizer of a subset of a magma has an element, the magma is inhabited. (Contributed by Jim Kingdon, 16-Sep-2026.)
Cntz

16-Sep-2026	ressmex 13472	If a structure restriction is inhabited, the structure is a set and so is the class it is restricted to. (Contributed by Jim Kingdon, 16-Sep-2026.)
↾_s $/\$

15-Sep-2026	cntzex 14144	Set existence of the centralizer. (Contributed by Jim Kingdon, 15-Sep-2026.)
Cntz

9-Sep-2026	flaplt 10733	The floor function value is less than the next integer. (Contributed by NM, 24-Feb-2005.) (Revised by Jim Kingdon, 9-Sep-2026.)
$\/$ $/\$ # $/\$

8-Sep-2026	fiidxsupcl 12012	A set of integers indexed by a finite set has an upper bound. (Contributed by Jim Kingdon, 8-Sep-2026.)


6-Sep-2026	ofrfidc 7318	Decidability of a relation applied to two functions. (Contributed by Jim Kingdon, 6-Sep-2026.)
DECID DECID

27-Aug-2026	prmdcz 12928	Primality is decidable. (Contributed by Jim Kingdon, 27-Aug-2026.)
DECID

27-Aug-2026	zmincl 12023	The minumum of two integers is an integer. (Contributed by Jim Kingdon, 27-Aug-2026.)
$/\$ inf

25-Aug-2026	nn0sqdcq 13007	A nonnegative integer is a perfect square or not. This is similar to nn0sqdc 11162 but expresses the idea of being a perfect square as having a rational number which, when squared, gives the original number. (Contributed by Jim Kingdon, 25-Aug-2026.)
DECID

25-Aug-2026	qabscl 11859	The absolute value of a rational number is a rational number. (Contributed by Jim Kingdon, 25-Aug-2026.)


25-Aug-2026	nn0sqdc 11162	A nonnegative integer is a perfect square or not. (Contributed by Jim Kingdon, 25-Aug-2026.)
DECID

24-Aug-2026	sqrtrirr 13008	The square root of a nonnegative integer is either rational or irrational. (Contributed by Jim Kingdon, 24-Aug-2026.)
$\/$ $/\$ #

21-Aug-2026	prmefexple 16274	Convert a bound on a power of a prime to a bound on the exponent. (Contributed by Mario Carneiro, 11-Mar-2014.) (Revised by Jim Kingdon, 21-Aug-2026.)
$/\$ $/\$

20-Aug-2026	zprmlogbap 16184	The logarithm of a natural number to a prime base is either rational or irrational. The proof decomposes into and such that (using nnmaxpw 12972). If the logarithm is , which is rational. If then we can apply logbgcd1irrap 16172 to show that the logarithm is irrational. (Contributed by Jim Kingdon and Taylor Barrella, 20-Aug-2026.)
$/\$ log_b $\/$ log_b $/\$ log_b #

20-Aug-2026	zprmlogbaplem3 16183	Lemma for zprmlogbap 16184. Decomposing a natural number into a power of a prime base and a factor not divisible by that prime. (Contributed by Jim Kingdon, 20-Aug-2026.)
$/\$ $/\$

20-Aug-2026	zprmlogbaplem2 16182	Lemma for zprmlogbap 16184. The logarithm is either rational or irrational. (Contributed by Jim Kingdon, 20-Aug-2026.)
log_b $\/$ log_b $/\$ log_b #

20-Aug-2026	zprmlogbaplem1 16181	Lemma for zprmlogbap 16184. Rearranging an expression involving logarithms. (Contributed by Jim Kingdon, 20-Aug-2026.)
log_b log_b

20-Aug-2026	flaplelt 10724	A basic property of the floor (greatest integer) function. (Contributed by Jim Kingdon, 20-Aug-2026.)
$\/$ $/\$ # $/\$

20-Aug-2026	flapcl 10722	The floor (greatest integer) function yields an integer when applied to a number which is either rational or irrational. (Contributed by Jim Kingdon, 20-Aug-2026.)
$\/$ $/\$ #

20-Aug-2026	irraddap 10057	The sum of an irrational number and a rational number is irrational. (Contributed by Jim Kingdon, 20-Aug-2026.)
$/\$ # $/\$ $/\$ #

19-Aug-2026	nnmaxpw 12972	The function that decomposes a number into its "odd" and "even" parts, which is to say the largest power of a base and largest divisor of the number not divisible by that base, is a bijection from pairs of a nonnegative integer and a number not divisible by that base to positive integers. (Contributed by Thierry Arnoux, 15-Aug-2017.) (Revised by Jim Kingdon, 19-Aug-2026.)


19-Aug-2026	nnmaxpwlemparts 12971	Lemma for nnmaxpw 12972. Decomposing a number into parts. (Contributed by Jim Kingdon, 16-Nov-2021.) (Revised by Jim Kingdon, 19-Aug-2026.)
$/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

19-Aug-2026	nnmaxpwlemnfac 12970	Lemma for nnmaxpw 12972. Removing the powers of a base from a natural number produces a number not divisible by that base. (Contributed by Jim Kingdon, 16-Nov-2021.) (Revised by Jim Kingdon, 19-Aug-2026.)
$/\$ $/\$

19-Aug-2026	nnmaxpwlemndvds 12969	Lemma for nnmaxpw 12972. A natural number is not divisible by one more than the highest power of a base which divides it. (Contributed by Jim Kingdon, 17-Nov-2021.) (Revised by Jim Kingdon, 19-Aug-2026.)
$/\$ $/\$

19-Aug-2026	nnmaxpwlemdvds 12968	Lemma for nnmaxpw 12972. A natural number is divisible by the highest power of a base which divides it. (Contributed by Jim Kingdon, 17-Nov-2021.) (Revised by Jim Kingdon, 19-Aug-2026.)
$/\$ $/\$

18-Aug-2026	nnmaxpwlemxy 12967	Lemma for nnmaxpw 12972. Another way of stating that decomposing a natural number into a power of a base and a number not divisible by that base is unique. (Contributed by Jim Kingdon, 16-Nov-2021.) (Revised by Jim Kingdon, 18-Aug-2026.)
$/\$ $/\$ $/\$

18-Aug-2026	pwbdvdseu 12966	A natural number has a unique highest power of a base which divides it. (Contributed by Jim Kingdon, 16-Nov-2021.) (Revised by Jim Kingdon, 18-Aug-2026.)
$/\$ $/\$

18-Aug-2026	pwbdvdseulemle 12965	Lemma for pwbdvdseu 12966. Powers of a base which do and do not divide a natural number. (Contributed by Jim Kingdon, 17-Nov-2021.) (Revised by Jim Kingdon, 18-Aug-2026.)


18-Aug-2026	pwbdvds 12964	A natural number has a highest power of a base which divides it. (Contributed by Jim Kingdon, 16-Nov-2021.) (Revised by Jim Kingdon, 18-Aug-2026.)
$/\$ $/\$

17-Aug-2026	pwbdvdslemn 12963	Lemma for pwbdvds 12964. If a natural number has some power of a base which does not divide it, there is a highest power of the base which does divide it. (Contributed by Jim Kingdon, 14-Nov-2021.) (Revised by Jim Kingdon, 17-Aug-2026.)
$/\$

14-Aug-2026	reaplog 16063	Apartness and the real natural logarithm. (Contributed by Jim Kingdon, 14-Aug-2026.)
$/\$ # #

13-Aug-2026	efap1p 15971	If the exponential of a number is apart from one plus that number, the number is apart from zero. To some extent can be thought of as the converse of efgt1p 12482. (Contributed by Jim Kingdon, 13-Aug-2026.)
$/\$ # #

6-Aug-2026	relndmfv 5728	The value of a relation outside its domain is the empty set. (Contributed by Jim Kingdon, 6-Aug-2026.)
$/\$

1-Aug-2026	wexmiddifxy 17217	Being able to subtract an arbitrary finite set from a finite set and get a finite set is equivalent to weak excluded middle. By adding additional conditions we can get a theorem which does not need weak excluded middle, at diffifi 7198. (Contributed by Jim Kingdon, 1-Aug-2026.)
WEXMID $/\$ $\$

1-Aug-2026	wexmiddifxylem 17216	Lemma for wexmiddifxylem 17216. Showing weak excluded middle given a suitable finite set. (Contributed by Jim Kingdon, 1-Aug-2026.)
$\$ DECID

31-Jul-2026	rabid1o 17205	Converting between propositions and corresponding subsets of a singleton. (Contributed by Jim Kingdon, 31-Jul-2026.)


30-Jul-2026	wexmiddc 17213	Weak excluded middle expressed using WEXMID implies decidability of a negated proposition. (Contributed by Jim Kingdon, 30-Jul-2026.)
WEXMID DECID

30-Jul-2026	df-wexmid 17212	Weak excluded middle is the principle that any negated proposition is decidable. (Contributed by Jim Kingdon, 30-Jul-2026.)
WEXMID $\/$

29-Jul-2026	wexmiddiffi 17215	Being able to subtract an arbitrary set from a finite set and get a finite set is equivalent to weak excluded middle. By adding additional conditions we can get a theorem which does not need weak excluded middle, at diffifi 7198. (Contributed by Jim Kingdon, 29-Jul-2026.)
WEXMID $\$

29-Jul-2026	wexmiddiffilem 17214	Lemma for wexmiddiffi 17215. The reverse direction, using different notation. (Contributed by Jim Kingdon, 29-Jul-2026.)
$\$ $\/$

28-Jul-2026	psrbaglefifi 15147	There are finitely many bags dominated by a given bag. (Contributed by Mario Carneiro, 29-Dec-2014.) (Revised by Mario Carneiro, 25-Jan-2015.) (Revised by Jim Kingdon, 28-Jul-2026.)
$/\$

24-Jul-2026	stnot 17210	A proposition is double negation stable if and only if it is equivalent to a negated proposition. Here by "proposition" we mean a subset of a singleton (which is a choice which allows us to quantify over them). Posed as an exercise online by Yannick Forster. (Contributed by Jim Kingdon, 24-Jul-2026.)


24-Jul-2026	slotm 13467	A structure with an inhabited slot is inhabited. (Contributed by Jim Kingdon, 24-Jul-2026.)
Slot $/\$

22-Jul-2026	alseu-no-surprise 17351	Demonstrate that there is never a "surprise" when using the "all some one" quantifier, that is, it is never possible for the consequent to be both always true and always false. This follows from als-no-surprise 17319 by alseuals 17337. See als-no-surprise 17319 for why ordinary "for all" with implication has no such property. (Contributed by David A. Wheeler, 22-Jul-2026.)
$/\$

22-Jul-2026	alseueu 17350	"The is " implies that exactly one thing is both and . This is the half of dfalseu2 17349 that drops the universal conjunct; it does not reverse, so $/\$ cannot be used in place of an "all some one" statement. (Contributed by David A. Wheeler, 22-Jul-2026.)
$/\$

22-Jul-2026	dfalseu2 17349	An "all some one" statement is equivalent to its universal part conjoined with the claim that exactly one satisfies both and . In other words, given , requiring exactly one to satisfy , which is what df-alseu 17334 requires, and requiring exactly one to satisfy $/\$ come to the same thing. Read as "is a king" and as "is hungry": if every king is hungry, then "there is exactly one king" and "there is exactly one hungry king" say the same thing, so either of them, together with "every king is hungry", gives "the king is hungry". The universal conjunct is what makes that work, and it cannot be dropped. $/\$ on its own is strictly weaker than , since it is satisfied when many things are and just one of those is , as in a region with five kings exactly one of whom is hungry; see alseueu 17350 for the one direction that does hold without it. Uniqueness attaches to the antecedent, not to the conjunction. Russell's analysis of a definite description is built the same way: its uniqueness clause constrains the description predicate alone, while the predication is a separate conjunct. See his worked example of "the father of Charles II was executed", [Russell1905] p. 482. (Contributed by David A. Wheeler, 22-Jul-2026.)
$/\$ $/\$

22-Jul-2026	nfralseu 17348	Bound-variable hypothesis builder for "all some one" restricted to a class. This is the "all some one" counterpart of nfrals 17317. (Contributed by David A. Wheeler, 22-Jul-2026.)


22-Jul-2026	nfalseu 17347	Bound-variable hypothesis builder for "all some one". This is the "all some one" counterpart of nfals 17316. Unlike the set.mm version of this theorem, no disjoint variable condition is needed, because nfeu 2105 here does not require one. (Contributed by David A. Wheeler, 22-Jul-2026.)


22-Jul-2026	ralseubii 17346	Congruence for "all some one" restricted to a class. This is the "all some one" counterpart of ralsbii 17314. (Contributed by David A. Wheeler, 22-Jul-2026.)


22-Jul-2026	alseubii 17345	Congruence: equivalents may be substituted inside an "all some one". This is the "all some one" counterpart of alsbii 17313. (Contributed by David A. Wheeler, 22-Jul-2026.)


22-Jul-2026	ralseu2d 17344	Deduction rule: Given "all some one" applied to a class, you can extract the "exactly one" part. Note that the witness must satisfy the antecedent , not merely be a member of . (Contributed by David A. Wheeler, 22-Jul-2026.)


22-Jul-2026	ralseu1d 17343	Deduction rule: Given "all some one" applied to a class, you can extract the "for all" part. (Contributed by David A. Wheeler, 22-Jul-2026.)


22-Jul-2026	alseu2d 17342	Deduction rule: Given "all some one" applied to a top-level inference, you can extract the "exactly one" part. (Contributed by David A. Wheeler, 22-Jul-2026.)


22-Jul-2026	alseu1d 17341	Deduction rule: Given "all some one" applied to a top-level inference, you can extract the "for all" part. (Contributed by David A. Wheeler, 22-Jul-2026.)


22-Jul-2026	ralseud 17340	Introduction rule for "all some one" restricted to a class. This is the converse of ralseu1d 17343 and ralseu2d 17344 taken together. (Contributed by David A. Wheeler, 22-Jul-2026.)


22-Jul-2026	alseud 17339	Introduction rule: "all some one" holds if the "for all" part holds and the antecedent has exactly one witness. This is the converse of alseu1d 17341 and alseu2d 17342 taken together. (Contributed by David A. Wheeler, 22-Jul-2026.)


22-Jul-2026	ralseurals 17338	"All some one" restricted to a class implies "all some" restricted to that class. Restricted counterpart of alseuals 17337. (Contributed by David A. Wheeler, 22-Jul-2026.)


22-Jul-2026	alseuals 17337	"All some one" implies "all some": requiring exactly one witness is stronger than requiring at least one. Any consequence of an allsome statement is therefore a consequence of the corresponding "all some one" statement, which is how alseu-no-surprise 17351 is proved. (Contributed by David A. Wheeler, 22-Jul-2026.)


22-Jul-2026	dfralseu2 17336	The bounded "all some one" form is the general form with the class membership folded into the antecedent. This is the "all some one" counterpart of dfrals2 17302. (Contributed by David A. Wheeler, 22-Jul-2026.)
$/\$

22-Jul-2026	df-ralseu 17335	Define "all some one" applied to a class, which means is true whenever is true for in , and exactly one in satisfies . (Contributed by David A. Wheeler, 22-Jul-2026.)
$/\$

22-Jul-2026	df-alseu 17334	Define "all some one" applied to a top-level implication, which means is true whenever is true and exactly one satisfies . (Contributed by David A. Wheeler, 22-Jul-2026.)
$/\$

22-Jul-2026	wralseu 17333	Extend wff definition to include "all some one" applied to a class, which means is true whenever is true for in , and exactly one in satisfies . (Contributed by David A. Wheeler, 22-Jul-2026.)


22-Jul-2026	walseu 17332	Extend wff definition to include "all some one" applied to a top-level implication, which means is true whenever is true, and exactly one satisfies . (Contributed by David A. Wheeler, 22-Jul-2026.)


22-Jul-2026	mptmex 5945	If a function given by maps-to notation is inhabited, then the class it is defined on is inhabited. (Contributed by Jim Kingdon, 22-Jul-2026.)


20-Jul-2026	2alsraln0idm 17331	Nested general "all some" quantifiers with class membership as their antecedents, for the same class : holds for every and every in , and is inhabited. (Contributed by Peter Mazsa, 28-May-2019.) (Revised by David A. Wheeler, 20-Jul-2026.)
$/\$

20-Jul-2026	2alsraln0m 17330	Nested general "all some" quantifiers with class membership as their antecedents: holds for every in and every in , and both and are inhabited. (Contributed by Peter Mazsa, 28-May-2019.) (Revised by David A. Wheeler, 20-Jul-2026.)
$/\$ $/\$

20-Jul-2026	n0alsm 17329	If is inhabited, then the general "all some" quantifier with class membership as its antecedent reduces to the assertion that holds for every in . (Contributed by Peter Mazsa, 19-Dec-2018.) (Revised by David A. Wheeler, 20-Jul-2026.)


20-Jul-2026	alsraln0m 17326	The general "all some" quantifier with class membership as its antecedent holds if and only if holds for every in and is inhabited. This is the intuitionistic form of what set.mm states using ; see the section comment. (Contributed by Peter Mazsa, 28-Nov-2018.) (Revised by David A. Wheeler, 20-Jul-2026.)
$/\$

20-Jul-2026	alsralrex 17325	The general "all some" quantifier with class membership as its antecedent holds if and only if holds for every in and some in satisfies . (Contributed by Peter Mazsa, 27-Nov-2018.) (Revised by David A. Wheeler, 20-Jul-2026.)
$/\$

20-Jul-2026	ralsanmo 17324	An "all some" statement restricted to a class, conjoined with the claim that at most one in satisfies its antecedent, is equivalent to the universal part conjoined with the claim that exactly one in satisfies the antecedent. This is the restricted counterpart of alsanmo 17323. (Contributed by Peter Mazsa and David A. Wheeler, 20-Jul-2026.)
$/\$ $/\$

20-Jul-2026	alsanmo 17323	An "all some" statement conjoined with the claim that at most one satisfies its antecedent is equivalent to the universal part conjoined with the claim that exactly one satisfies the antecedent. The "all some" quantifier supplies the existence of such an and supplies the at-most-one part, so together they yield . (Contributed by Peter Mazsa and David A. Wheeler, 20-Jul-2026.)
$/\$ $/\$

20-Jul-2026	rexrals 17322	If a member of satisfying the antecedent exists, then a restricted "all some" statement reduces to its universal part. This is the restricted counterpart of rexals 17328. (Contributed by Peter Mazsa and David A. Wheeler, 20-Jul-2026.)


20-Jul-2026	ralrals 17321	If the universal part of a restricted "all some" statement holds, then the statement reduces to the existence of a member of satisfying its antecedent. This is the restricted counterpart of ralals 17327. (Contributed by Peter Mazsa and David A. Wheeler, 20-Jul-2026.)


20-Jul-2026	als-no-surprise 17319	Demonstrate that there is never a "surprise" when using the allsome quantifier, that is, it is never possible for the consequent to be both always true and always false. This uses the definition of df-als 17300: the universal parts give , which contradicts the witness that the allsome quantifier supplies. Ordinary "for all" with implication has no such property, since and can both hold when nothing satisfies . (Contributed by David A. Wheeler, 27-Oct-2018.) (Revised by David A. Wheeler, 20-Jul-2026.)
$/\$

20-Jul-2026	ralsmd 17310	Deduction rule: Given "all some" applied to a class, the class is inhabited. This is stronger than ralsn0d 17309, which only concludes that the class is nonempty; see n0r 3535. (Contributed by David A. Wheeler, 20-Jul-2026.)


19-Jul-2026	disjdifg 3598	A class and its relative complement are disjoint. (Contributed by NM, 24-Mar-1998.) Generalize from disjdif 3599. (Revised by BJ, 19-Jul-2026.)
$\$

19-Jul-2026	sseq0b 3564	The only subclass of the empty class is itself. (Contributed by NM, 7-Mar-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) Strengthen sseq0 3565 to a biconditional. (Revised by BJ, 19-Jul-2026.)


18-Jul-2026	sepab 4278	Separation Scheme (Aussonderung) in terms of a class abstraction. Prefer using the more natural statement rabexg 4279. (Contributed by NM, 8-Jun-1994.) Put in closed form. (Revised by BJ, 18-Jul-2026.)
$/\$

18-Jul-2026	inssdif0im 3592	Intersection, subclass, and difference relationship. The converse holds in classical logic but not in intuitionistic logic. (Contributed by Jim Kingdon, 3-Aug-2018.) (Proof shortened by BJ, 18-Jul-2026.)
$\$

15-Jul-2026	rexals 17328	If some in satisfies , then the general "all some" quantifier with class membership as its antecedent reduces to the assertion that holds for every in . See rexrals 17322 for the restricted counterpart. (Contributed by Peter Mazsa, 19-Dec-2018.) (Revised by David A. Wheeler, 15-Jul-2026.)


15-Jul-2026	ralals 17327	If holds for every in , then the general "all some" quantifier with class membership as its antecedent reduces to the assertion that some in satisfies . See ralrals 17321 for the restricted counterpart. (Contributed by Peter Mazsa, 19-Dec-2018.) (Revised by David A. Wheeler, 15-Jul-2026.)


14-Jul-2026	uniex2 4581	The Axiom of Union using the standard abbreviation for union. Given any set , its union exists. (Contributed by NM, 4-Jun-2006.) (Proof shortened by BJ, 14-Jul-2026.)


14-Jul-2026	sepgi 4252	Inference associated with sepg 4251. (Contributed by NM, 21-Jun-1993.) (Revised by BJ, 14-Jul-2026.)
$/\$

13-Jul-2026	f1setfi 7317	The set of injections between two finite sets is finite. (Contributed by Jim Kingdon, 13-Jul-2026.)
$/\$

13-Jul-2026	fdcf1 7316	It is decidable whether a function from a finite set into another finite set is one-to-one. (Contributed by Jim Kingdon, 13-Jul-2026.)
$/\$ $/\$ DECID

12-Jul-2026	rals-no-surprise 17320	Demonstrate that there is never a "surprise" when using the allsome quantifier restricted to a class, that is, it is never possible for the consequent to be both always true and always false of the members of that satisfy the antecedent. This is the restricted counterpart of als-no-surprise 17319, and follows from it by dfrals2 17302. Note that this holds without any assumption that is inhabited; that is the point of allsome, since the corresponding claim for the ordinary restricted "for all" fails when nothing in satisfies . (Contributed by David A. Wheeler, 12-Jul-2026.)
$/\$

12-Jul-2026	cbvals 17318	Rule used to change bound variables, using implicit substitution. (Contributed by David A. Wheeler, 12-Jul-2026.)


12-Jul-2026	nfrals 17317	Bound-variable hypothesis builder for "all some" restricted to a class. (Contributed by David A. Wheeler, 12-Jul-2026.)


12-Jul-2026	nfals 17316	Bound-variable hypothesis builder for "all some". (Contributed by David A. Wheeler, 12-Jul-2026.)


12-Jul-2026	alsbid 17315	Deduction form of alsbii 17313. (Contributed by David A. Wheeler, 12-Jul-2026.)


12-Jul-2026	ralsbii 17314	Congruence for "all some" restricted to a class. (Contributed by David A. Wheeler, 12-Jul-2026.)


12-Jul-2026	alsbii 17313	Congruence: equivalents may be substituted inside an "all some". (Contributed by David A. Wheeler, 12-Jul-2026.)


12-Jul-2026	ralsex 17312	The consequent of an "all some" restricted to a class is witnessed: some member of satisfying also satisfies . Restricted counterpart of alsex 17311. (Contributed by David A. Wheeler, 12-Jul-2026.)


12-Jul-2026	alsex 17311	The consequent of an "all some" is witnessed: if holds of every satisfying , and some satisfies , then some satisfies . This is the positive counterpart of als-no-surprise 17319, and it is the property that ordinary "for all" with implication lacks: from alone nothing whatever follows about , since nothing need satisfy . It is the allsome quantifier says what a speaker of "all Martians are green" usually means. (Contributed by David A. Wheeler, 12-Jul-2026.)


12-Jul-2026	ralsn0d 17309	Deduction rule: Given "all some" applied to a class, the class is not the empty set. (Contributed by David A. Wheeler, 23-Oct-2018.) (Revised by David A. Wheeler, 12-Jul-2026.)


12-Jul-2026	rals2d 17308	Deduction rule: Given "all some" applied to a class, you can extract the "there exists" part. Note that the witness must satisfy the antecedent , not merely be a member of . (Contributed by David A. Wheeler, 20-Oct-2018.) (Revised by David A. Wheeler, 12-Jul-2026.)


12-Jul-2026	rals1d 17307	Deduction rule: Given "all some" applied to a class, you can extract the "for all" part. (Contributed by David A. Wheeler, 20-Oct-2018.) (Revised by David A. Wheeler, 12-Jul-2026.)


12-Jul-2026	ralsd 17304	Introduction rule for "all some" restricted to a class. This is the converse of rals1d 17307 and rals2d 17308 taken together. (Contributed by David A. Wheeler, 12-Jul-2026.)


12-Jul-2026	alsd 17303	Introduction rule: "all some" holds if the "for all" part holds and the antecedent has a witness. This is the converse of als1d 17305 and als2d 17306 taken together, and is what lets an "all some" statement be proved rather than merely taken apart. (Contributed by David A. Wheeler, 12-Jul-2026.)


12-Jul-2026	dfrals2 17302	The bounded "all some" form is the general form with the class membership folded into the antecedent. (Contributed by David A. Wheeler, 22-Oct-2018.) (Revised by David A. Wheeler, 12-Jul-2026.)
$/\$

12-Jul-2026	df-rals 17301	Define "all some" applied to a class, which means is true whenever is true for in , and there is at least one in where is true. An older definition of the "all some" quantifier when scoped to a class, named df-alsc and now removed, instead applied a bare formula to the members of a class, asserting only $/\$ , that is, that the formula held throughout and that had at least one member. I've now decided that that was a mistake. Its older existence conjunct did not require any member of to satisfy the antecedent, so if the formula was itself an implication, that inner implication could still be vacuously true, which is precisely what the allsome quantifier exists to prevent. For example, the older definition meant that "among Martians, all tall ones are green" could be considered true if there are Martians, but no tall Martians. This version of the definition instead ensures that claims of the form "among Martians, all tall ones are green" can only be true if all tall Martians are green and that there is at least one tall Martian. (Contributed by David A. Wheeler, 20-Oct-2018.) (Revised by David A. Wheeler, 12-Jul-2026.)
$/\$

12-Jul-2026	wrals 17299	Extend wff definition to include "all some" applied to a class, which means is true whenever is true for in , and there is at least one in where is true. (Contributed by David A. Wheeler, 20-Oct-2018.) (Revised by David A. Wheeler, 12-Jul-2026.)


12-Jul-2026	wals 17298	Extend wff definition to include "all some" applied to a top-level implication, which means is true whenever is true, and there is at least one where is true. (Contributed by David A. Wheeler, 20-Oct-2018.) (Revised by David A. Wheeler, 12-Jul-2026.)


12-Jul-2026	vvin 3569	Two classes are both the universal class if and only if their intersection is the universal class. Dual of un00 3567. (Contributed by BJ, 12-Jul-2026.)
$/\$

7-Jul-2026	cmnsubm 14196	A submonoid of a commutative monoid is commutative. (Contributed by Jim Kingdon, 7-Jul-2026.)
SubMnd CMnd ↾_s CMnd

29-Jun-2026	dichmul0or 16931	Real number dichotomy is equivalent to the zero product principle for complex numbers: if a product is zero, one of its factors must be zero. (Contributed by Matthew House, 29-Jun-2026.)
$\/$ $\/$

29-Jun-2026	dichmul0orlem5 16928	Lemma for dichmul0or 16931. (Contributed by Matthew House, 29-Jun-2026.)


29-Jun-2026	dichmul0orlem4 16927	Lemma for dichmul0or 16931. (Contributed by Matthew House, 29-Jun-2026.)


29-Jun-2026	dichmul0orlem3 16926	Lemma for dichmul0or 16931. (Contributed by Matthew House, 29-Jun-2026.)
$\/$ $\/$

29-Jun-2026	dichmul0orlem2 16925	Lemma for dichmul0or 16931. (Contributed by Matthew House, 29-Jun-2026.)


29-Jun-2026	dichmul0orlem1 16924	Lemma for dichmul0or 16931. (Contributed by Matthew House, 29-Jun-2026.)


29-Jun-2026	lealltlt2 16923	Alternative definition for on real numbers. (Contributed by Matthew House, 29-Jun-2026.)
$/\$

29-Jun-2026	lealltlt1 16922	Alternative definition for on real numbers. (Contributed by Matthew House, 29-Jun-2026.)
$/\$

28-Jun-2026	dichmul0orlem7 16930	Lemma for dichmul0or 16931. (Contributed by Matthew House, 28-Jun-2026.)
$\/$ $\/$

28-Jun-2026	dichmul0orlem6 16929	Lemma for dichmul0or 16931. (Contributed by Matthew House, 28-Jun-2026.)


28-Jun-2026	msq0 9000	A number is zero iff its square is zero. (Contributed by Matthew House, 28-Jun-2026.)


28-Jun-2026	msqap0 8999	A number is apart from zero iff its square is apart from zero. (Contributed by Matthew House, 28-Jun-2026.)
# #

28-Jun-2026	letrid 8444	Tightness of real apartness. (Contributed by Matthew House, 28-Jun-2026.)


19-Jun-2026	ringen1zr0 14706	The only unital ring with one element is the zero ring (at least if its operations are internal binary operations). This holds already for nonunital rings, see rngen1zr0 14345, and semirings, see srgen1zr0 14376. (Contributed by FL, 15-Feb-2010.) (Revised by AV, 25-Jan-2020.) (Proof shortened by AV, 19-Jun-2026.)
$/\$ $/\$ $/\$

19-Jun-2026	srg1zr 14375	The only semiring with a base set consisting of one element is the zero ring (at least if its operations are internal binary operations). (Contributed by FL, 13-Feb-2010.) (Revised by AV, 25-Jan-2020.) (Proof shortened by AV, 19-Jun-2026.)
SRing $/\$ $/\$ $/\$ $/\$

18-Jun-2026	rngen1zr0 14345	The only ring with one element is the zero ring (at least if its operations are internal binary operations). (Contributed by FL, 15-Feb-2010.) (Revised by AV, 18-Jun-2026.)
Rng $/\$ $/\$ $/\$

18-Jun-2026	rngen1zr 14344	The only ring with one element is the zero ring (at least if its operations are internal binary operations). (Contributed by FL, 14-Feb-2010.) (Revised by AV, 18-Jun-2026.)
Rng $/\$ $/\$ $/\$ $/\$

18-Jun-2026	rng1zr 14343	The only ring with a base set consisting of one element is the zero ring (at least if its operations are internal binary operations). (Contributed by FL, 13-Feb-2010.) (Revised by AV, 18-Jun-2026.)
Rng $/\$ $/\$ $/\$ $/\$

18-Jun-2026	rng1zrlem 14342	Lemma for rng1zr 14343 and srg1zr 14375. (Contributed by FL, 13-Feb-2010.) (Revised by AV, 18-Jun-2026.)
Mgm $/\$ mulGrp Mgm $/\$ $/\$ $/\$ $/\$

17-Jun-2026	ballotfi 13334	Bertrand's ballot problem : the probability that A is ahead throughout the counting. The proof formalized here is a proof "by reflection", as opposed to other known proofs "by induction" or "by permutation". This is Metamath 100 proof #30. (Contributed by Thierry Arnoux, 7-Dec-2016.) (Revised by Jim Kingdon, 17-Jun-2026.)
♯ ♯ ♯ ♯ ♯ $\$

17-Jun-2026	ballotfilembfi 13291	The set of countings where B got the first vote is finite. (Contributed by Jim Kingdon, 17-Jun-2026.)
♯ ♯ ♯ ♯ ♯ $\$ $\$

17-Jun-2026	ballotfilemafi 13290	The set of countings where A got the first vote, but does not stay strictly ahead throughout, is finite. (Contributed by Jim Kingdon, 17-Jun-2026.)
♯ ♯ ♯ ♯ ♯ $\$ $\$

17-Jun-2026	ballotfilemefi 13289	is finite. (Contributed by Jim Kingdon, 17-Jun-2026.)
♯ ♯ ♯ ♯ ♯ $\$

17-Jun-2026	rabxmdc 3554	Law of excluded middle given decidability, in terms of restricted class abstractions. (Contributed by Jeff Madsen, 20-Jun-2011.) (Revised by Jim Kingdon, 17-Jun-2026.)
DECID

15-Jun-2026	ballotfilemgun 13320	A property of the defined operator. (Contributed by Thierry Arnoux, 26-Apr-2017.) (Revised by Jim Kingdon, 15-Jun-2026.)
♯ ♯ ♯ ♯ ♯ $\$ $\$ inf $\$ $\$ ♯ ♯ $\$

15-Jun-2026	ballotfilemgval 13319	Expand the value of . (Contributed by Thierry Arnoux, 21-Apr-2017.) (Revised by Jim Kingdon, 15-Jun-2026.)
♯ ♯ ♯ ♯ ♯ $\$ $\$ inf $\$ $\$ ♯ ♯ $\$ ♯ ♯ $\$

15-Jun-2026	ballotfilemdifcfz 13279	Lemma for ballotfi . The portion of a counting representing votes for B within a specified integer range is finite. (Contributed by Jim Kingdon, 15-Jun-2026.)
♯ $\$

15-Jun-2026	ballotfilemcinfz 13278	Lemma for ballotfi . The portion of a counting representing votes for A within a specified integer range is finite. (Contributed by Jim Kingdon, 15-Jun-2026.)
♯

12-Jun-2026	ballotfilemsle 13300	The infimum of the set of zeroes of is a lower bound. (Contributed by Jim Kingdon, 12-Jun-2026.)
♯ ♯ ♯ ♯ ♯ $\$ $\$ inf $\$ $/\$ inf

12-Jun-2026	ballotfilemscl 13299	The set of zeroes of has an infimum. (Contributed by Jim Kingdon, 12-Jun-2026.)
♯ ♯ ♯ ♯ ♯ $\$ $\$ inf $\$ inf

12-Jun-2026	infssfzledc 10681	The infimum of a decidable inhabited subset of an integer range is a lower bound for that set. (Contributed by Jim Kingdon, 12-Jun-2026.)
$/\$ DECID inf

12-Jun-2026	infssfzcldc 10680	The infimum of a decidable inhabited subset of an integer range is a member of the set. (Contributed by Jim Kingdon, 12-Jun-2026.)
$/\$ DECID inf

10-Jun-2026	10nprm 13251	10 is not a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.)
;

10-Jun-2026	11nn 9806	11 is a positive integer. (Contributed by Umit Teoman Dogan, 10-Jun-2026.)
;

10-Jun-2026	25nn0 9800	25 is a nonnegative integer. (Contributed by Umit Teoman Dogan, 10-Jun-2026.)
;

10-Jun-2026	16nn0 9799	16 is a nonnegative integer. (Contributed by Umit Teoman Dogan, 10-Jun-2026.)
;

10-Jun-2026	12nn0 9798	12 is a nonnegative integer. (Contributed by Umit Teoman Dogan, 10-Jun-2026.)
;

10-Jun-2026	11nn0 9797	11 is a nonnegative integer. (Contributed by Umit Teoman Dogan, 10-Jun-2026.)
;

10-Jun-2026	2t4e8 9468	2 times 4 equals 8. (Contributed by Umit Teoman Dogan, 10-Jun-2026.)


10-Jun-2026	2t3e6 9465	2 times 3 equals 6. (Contributed by Umit Teoman Dogan, 10-Jun-2026.)


8-Jun-2026	ballotfilemdifcfi 13277	Lemma for ballotfi . The portion of a counting representing votes for B up to a specified integer is finite. (Contributed by Jim Kingdon, 8-Jun-2026.)
♯ $\$

8-Jun-2026	ballotfilemcinfi 13276	Lemma for ballotfi . The portion of a counting representing votes for A up to a specified integer is finite. (Contributed by Jim Kingdon, 8-Jun-2026.)
♯

8-Jun-2026	zfidc 9728	Whether an integer is an element of a finite set of integers is decidable. (Contributed by Jim Kingdon, 8-Jun-2026.)
$/\$ $/\$ DECID

7-Jun-2026	ballotfilemcdc 13275	Lemma for ballotfi . It is decidable whether a given integer is an element of a particular element of . (Contributed by Jim Kingdon, 7-Jun-2026.)
♯ DECID

5-Jun-2026	hashpwfi 11285	The number of finite subsets of a finite set is two raised to the power of the size of the set. For a similar theorem with set size expressed using equinumerosity, see 2omapfi 7321. For the number of subsets (which need not be finite) of a set, see pw1mapen 17197. (Contributed by Jim Kingdon, 5-Jun-2026.)
♯ ♯

4-Jun-2026	ballotfilemonn 13273	The size of the universe is at least one. (Contributed by Jim Kingdon, 4-Jun-2026.)
♯ ♯

3-Jun-2026	papeq2 7611	Equality theorem for apartness predicate. (Contributed by Jim Kingdon, 3-Jun-2026.)
Ap Ap

3-Jun-2026	papeq1 7610	Equality theorem for apartness predicate. (Contributed by Jim Kingdon, 3-Jun-2026.)
Ap Ap

2-Jun-2026	resq01 11110	If a real number equals its square, it must be 0 or 1. (Contributed by Jim Kingdon, 2-Jun-2026.)
$\/$

31-May-2026	aprprop 14685	If two structures have the same ring components (properties), df-apr 14674 generates the same relation for both of them. (Contributed by Jim Kingdon, 31-May-2026.)
#_r #_r

31-May-2026	ringunitsap0 14678	The set of units of a ring. If is a local ring, # is an apartness and this theorem states that the units of a ring are those elements apart from zero (see aprlring 14684). Given the definition of #_r this theorem holds even if # is not an apartness, however. (Contributed by Jim Kingdon, 31-May-2026.)
# #_r # Unit

30-May-2026	ringunitap 14677	Elementhood in the set of units. (Contributed by Jim Kingdon, 30-May-2026.)
Unit # #_r $/\$ #

29-May-2026	drnglring 14691	A division ring is a local ring. (Contributed by Jim Kingdon, 29-May-2026.)
LRing

29-May-2026	isdrngtap 14690	The predicate "is a division ring". (Contributed by Jim Kingdon, 29-May-2026.)
# #_r $/\$ # TAp

29-May-2026	df-drngap 14688	Define class of all division rings. A division ring is a ring in which the relation given by df-apr 14674 is a tight apartness. (Contributed by Jim Kingdon, 29-May-2026.)
#_r TAp

29-May-2026	aprunit 14676	The df-apr 14674 relation with zero expresses whether a ring element is a unit. That is, the difference of an element of a ring and zero is invertible iff the element is a unit. (Contributed by Jim Kingdon, 29-May-2026.)
Unit # #_r #

29-May-2026	tapap 7617	A tight apartness is an apartness. (Contributed by Jim Kingdon, 29-May-2026.)
TAp Ap

28-May-2026	aprlring 14684	A ring is a local ring if and only if the relation given by df-apr 14674 is an apartness relation. (Contributed by Jim Kingdon, 28-May-2026.)
LRing #_r Ap

28-May-2026	papcotr 7614	An apartness is cotransitive. (Contributed by Jim Kingdon, 28-May-2026.)
Ap $\/$

27-May-2026	aprnzr 14683	If the relation given by df-apr 14674 on a ring is an apartness relation, then the ring is a nonzero ring. (Contributed by Jim Kingdon, 27-May-2026.)
$/\$ #_r Ap NzRing

27-May-2026	papsym 7613	An apartness is symmetric. (Contributed by Jim Kingdon, 27-May-2026.)
Ap

27-May-2026	papirr 7612	An apartness is irreflexive. (Contributed by Jim Kingdon, 27-May-2026.)
Ap $/\$

24-May-2026	gsumzfi 14242	Value of a finite group sum over the zero element. (Contributed by Jim Kingdon, 24-May-2026.)
CMnd $/\$ _g

22-May-2026	sshashneg 11297	Subsets of a class of a negative size (a degenerate case). Together with ssenneg 11296 this shows that sseqn 11295 could not be extended beyond . (Contributed by Jim Kingdon, 22-May-2026.)
$/\$ ♯

22-May-2026	ssenneg 11296	Subsets of a class of a negative size (a degenerate case). Together with sshashneg 11297 this shows that sseqn 11295 could not be extended beyond . (Contributed by Jim Kingdon, 22-May-2026.)
$/\$

22-May-2026	sseqn 11295	Two ways to express the subsets of a class of a given size. It might seem that ♯ would suffice, but that would require the converse of hashcl 11236 or something similar. Although each side of the equality would be well defined if we changed to , they would give different results for the (degenerate) case of a negative size, as shown at ssenneg 11296 and sshashneg 11297. (Contributed by Jim Kingdon, 22-May-2026.)
♯

22-May-2026	bilanri 389	Inference adding a conjunct to the right-hand side of a biconditional. (Contributed by Matthew House, 22-May-2026.)
$/\$

22-May-2026	biranri 388	Inference adding a conjunct to the right-hand side of a biconditional. (Contributed by Matthew House, 22-May-2026.)
$/\$

22-May-2026	bilani 387	Inference adding a conjunct to the left-hand side of a biconditional. (Contributed by Matthew House, 22-May-2026.)
$/\$

22-May-2026	birani 386	Inference adding a conjunct to the left-hand side of a biconditional. (Contributed by Matthew House, 22-May-2026.)
$/\$

20-May-2026	ballotfilemofi 13271	is finite. (Contributed by Jim Kingdon, 20-May-2026.)
♯

19-May-2026	fipwfi 7322	The set of finite subsets of a finite set is finite. (Contributed by Jim Kingdon, 19-May-2026.)


18-May-2026	2omapfi 7321	The number of finite subsets of a finite set. For a similar theorem with set size expressed using ♯ (df-ihash 11231), see hashpwfi 11285. (Contributed by Jim Kingdon, 18-May-2026.)


18-May-2026	fissfi 7263	A finite subset of a finite set is a decidable subset. (Contributed by Jim Kingdon, 18-May-2026.)
$/\$ $/\$ DECID

18-May-2026	fresaunres1disj 5571	From the union of two functions with disjoint domains, either component can be recovered by restriction. (Contributed by Mario Carneiro, 16-Feb-2015.) (Revised by Jim Kingdon, 18-May-2026.)
$/\$ $/\$

18-May-2026	fresaunres2disj 5570	From the union of two functions with disjoint domains, either component can be recovered by restriction. (Contributed by Stefan O'Rear, 9-Oct-2014.) (Revised by Jim Kingdon, 18-May-2026.)
$/\$ $/\$

15-May-2026	fsuppcorn 7301	The composition of a 1-1 function with a finitely supported function is finitely supported. The purpose of the supp condition is to ensure we don't subset the support of the function in such a way as to fun afoul of exmidssfi 7246. (Other alternative conditions might also be sufficient). (Contributed by AV, 28-May-2019.) (Revised by Jim Kingdon, 15-May-2026.)
finSupp supp finSupp

13-May-2026	lincmble 10417	A linear combination of two reals which lies in the interval between them. Like lincmb01cmp 10416 but generalized to require merely not . (Contributed by Jim Kingdon, 13-May-2026.)
$/\$ $/\$ $/\$

5-May-2026	fmelpw1o 7607	With a formula one can associate an element of , which can therefore be thought of as the set of "truth values" (but recall that there are no other genuine truth values than and , by nndc 863, which translate to and respectively by iftrue 3645 and iffalse 3648, giving pwtrufal 17198). As proved in if0ab 3641, the associated element of is the extension, in , of the formula . (Contributed by BJ, 15-Aug-2024.) (Proof shortened by BJ, 5-May-2026.)


5-May-2026	if0elpw 4295	A conditional class with the False alternative being sent to the empty class is an element of the powerset of the class corresponding to the True alternative when that class is a set. This statement requires fewer axioms than the general case ifelpwung 4627. (Contributed by BJ, 5-May-2026.)


5-May-2026	if0ss 3642	A conditional class with the False alternative being sent to the empty class is included in the class corresponding to the True alternative. (Contributed by BJ, 5-May-2026.)


27-Apr-2026	repiecef 17248	Piecewise definition on the reals yields a function. The function agrees with and on their respective parts of the real line; see repiecele0 17246 and repiecege0 17247. From an online post by James E Hanson. The construction was published in Martín Hötzel Escardó, "Effective and sequential definition by cases on the reals via infinite signed-digit numerals", Electronic Notes in Theoretical Computer Science 10 (1998), page 2, https://martinescardo.github.io/papers/lexnew.pdf. 17247 (Contributed by Jim Kingdon, 27-Apr-2026.)
inf

27-Apr-2026	repiecege0 17247	Piecewise definition on the reals agrees with the nonnegative part of the definition. See repiecef 17248 for more on this construction. (Contributed by Jim Kingdon, 27-Apr-2026.)
inf $/\$ $/\$

27-Apr-2026	repiecele0 17246	Piecewise definition on the reals agrees with the nonpositive part of the definition. See repiecef 17248 for more on this construction. (Contributed by Jim Kingdon, 27-Apr-2026.)
inf $/\$ $/\$

27-Apr-2026	repiecelem 17245	Lemma for repiecele0 17246, repiecege0 17247, and repiecef 17248. The function is defined everywhere. (Contributed by Jim Kingdon, 27-Apr-2026.)
inf $/\$ inf

24-Apr-2026	qdiff 17270	The rationals are exactly those reals for which there exist two distinct rationals that are the same distance from the original number. Similar to apdiff 17269 but by stating the result positively we can completely sidestep the issue of not equal versus apart in the statement of the result. From an online post by Ingo Blechschmidt. (Contributed by Jim Kingdon, 24-Apr-2026.)
$/\$

23-Apr-2026	exmidpeirce 17209	Excluded middle is equivalent to Peirce's law. Read an element of as being a truth value and being that is true. For a similar theorem, but expressed in terms of formulas rather than subsets of , see dcfrompeirce 1499. (Contributed by Jim Kingdon, 23-Apr-2026.)
EXMID

22-Apr-2026	exmidcon 17208	Excluded middle is equivalent to the form of contraposition which removes negation. Read an element of as being a truth value and being that is true. For a similar theorem, but expressed in terms of formulas rather than subsets of , see dcfromcon 1498. (Contributed by Jim Kingdon, 22-Apr-2026.)
EXMID

22-Apr-2026	exmidnotnotr 17207	Excluded middle is equivalent to double negation elimination. Read an element of as being a truth value and being that is true. For a similar theorem, but expressed in terms of formulas rather than subsets of , see dcfromnotnotr 1497. (Contributed by Jim Kingdon, 22-Apr-2026.)
EXMID

18-Apr-2026	hashtpglem 11314	Lemma for hashtpg 11315. This is one of the three not-equal conclusions required for the reverse direction. (Contributed by Jim Kingdon, 18-Apr-2026.)
♯

17-Apr-2026	hashtpgim 11313	The size of an unordered triple of three different elements. (Contributed by Alexander van der Vekens, 10-Nov-2017.) (Revised by AV, 18-Sep-2021.) (Revised by Jim Kingdon, 17-Apr-2026.)
$/\$ $/\$ $/\$ $/\$ ♯

14-Apr-2026	depind 16921	Theorem related to a dependently typed induction principle in type theory. (Contributed by Matthew House, 14-Apr-2026.)
$/\$

14-Apr-2026	depindlem3 16920	Lemma for depind 16921. (Contributed by Matthew House, 14-Apr-2026.)
$/\$

14-Apr-2026	depindlem2 16919	Lemma for depind 16921. (Contributed by Matthew House, 14-Apr-2026.)


14-Apr-2026	depindlem1 16918	Lemma for depind 16921. (Contributed by Matthew House, 14-Apr-2026.)
$/\$ $/\$

11-Apr-2026	indval0 9300	The indicator function generator does not generate a (meaningful) indicator function for a class which is not a subset of the domain. (Contributed by AV, 11-Apr-2026.)
𝟭

8-Apr-2026	gsumclfi 14243	Closure of a finite group sum. (Contributed by Jim Kingdon, 8-Apr-2026.)
CMnd _g

4-Apr-2026	gzsumsplit0 14232	Splitting off the rightmost summand of a group sum (even if it is the only summand). Similar to gzsumsplit1r 13768 except that can equal . (Contributed by Jim Kingdon, 4-Apr-2026.)
_gz _gz

4-Apr-2026	fzf1o 12161	A finite set can be enumerated by integers starting at one. (Contributed by Jim Kingdon, 4-Apr-2026.)
♯

3-Apr-2026	gsump1 14241	Splitting off one element from a finite group sum. This would typically used in a proof by induction. (Contributed by Jim Kingdon, 3-Apr-2026.)
CMnd _g _g

2-Apr-2026	gsumsncmn 14240	Group sum of a singleton. (Contributed by Jim Kingdon, 2-Apr-2026.)
CMnd $/\$ $/\$ _g

31-Mar-2026	sspw1or2 7545	The set of subsets of a given set with one or two elements can be expressed as elements of the power set or as inhabited elements of the power set. (Contributed by Jim Kingdon, 31-Mar-2026.)
$\/$ $\/$

28-Mar-2026	imaf1fi 7240	The image of a finite set under a one-to-one mapping is finite. (Contributed by Jim Kingdon, 28-Mar-2026.)
$/\$ $/\$

26-Mar-2026	gsum0cmn 14238	An empty finite group sum is the identity. (Contributed by Jim Kingdon, 26-Mar-2026.)
CMnd _g

26-Mar-2026	gzsumshift 14233	Shifting the indexes of a group sum indexed by consecutive integers. (Contributed by Jim Kingdon, 26-Mar-2026.)
CMnd _gz _gz

25-Mar-2026	gzsumgsum 14239	On an integer range, _gz and _g agree. (Contributed by Jim Kingdon, 25-Mar-2026.)
CMnd _gz _g

25-Mar-2026	gzsumgsum1 14237	On an integer range starting at one, _gz and _g agree. (Contributed by Jim Kingdon, 25-Mar-2026.)
CMnd _gz _g

24-Mar-2026	gsumvalfi 14236	Value of the finite group sum over an unordered finite set. (Contributed by Jim Kingdon, 24-Mar-2026.)
CMnd ♯ _g _gz

23-Mar-2026	df-gsumfi 14235	Define the finite group sum (iterated sum) over an unordered finite set. Given _g where , the set of indices is and the values are given by at each index. For this notation, is a finite set and is a commutative monoid, and the sum adds up these elements in some order (the sum does not depend on the order). For a sum indexed by consecutive integers (and thus defining an order for the sum), see df-gzsum 13666. (Contributed by Jim Kingdon, 23-Mar-2026.)
_g CMnd $/\$ ♯ $/\$ _gz

20-Mar-2026	exmidssfi 7246	Excluded middle is equivalent to any subset of a finite set being finite. Theorem 2.1 of [Bauer], p. 485. (Contributed by Jim Kingdon, 20-Mar-2026.)
EXMID $/\$

18-Mar-2026	umgr1een 16537	A graph with one non-loop edge is a multigraph. (Contributed by Jim Kingdon, 18-Mar-2026.)
UMGraph

18-Mar-2026	upgr1een 16536	A graph with one non-loop edge is a pseudograph. Variation of upgr1edc 16533 for a different way of specifying a graph with one edge. (Contributed by Jim Kingdon, 18-Mar-2026.)
UPGraph

14-Mar-2026	trlsex 16799	The class of trails on a graph is a set. (Contributed by Jim Kingdon, 14-Mar-2026.)
Trails

13-Mar-2026	eupthv 16858	The classes involved in a Eulerian path are sets. (Contributed by Jim Kingdon, 13-Mar-2026.)
EulerPaths $/\$ $/\$

13-Mar-2026	1hevtxdg0fi 16719	The vertex degree of vertex in a finite pseudograph with only one edge is 0 if is not incident with the edge . (Contributed by AV, 2-Mar-2021.) (Revised by Jim Kingdon, 13-Mar-2026.)
iEdg Vtx UPGraph VtxDeg

11-Mar-2026	en1hash 11255	A set equinumerous to the ordinal one has size 1 . (Contributed by Jim Kingdon, 11-Mar-2026.)
♯

4-Mar-2026	elmpom 6474	If a maps-to operation is inhabited, the first class it is defined with is inhabited. (Contributed by Jim Kingdon, 4-Mar-2026.)


22-Feb-2026	isclwwlkni 16819	A word over the set of vertices representing a closed walk of a fixed length. (Contributed by Jim Kingdon, 22-Feb-2026.)
ClWWalksN ClWWalks $/\$ ♯

21-Feb-2026	clwwlkex 16810	Existence of the set of closed walks (represented by words). (Contributed by Jim Kingdon, 21-Feb-2026.)
ClWWalks

17-Feb-2026	vtxdgfif 16705	In a finite graph, the vertex degree function is a function from vertices to nonnegative integers. (Contributed by Jim Kingdon, 17-Feb-2026.)
Vtx iEdg UPGraph VtxDeg

16-Feb-2026	vtxlpfi 16702	In a finite graph, the number of loops from a given vertex is finite. (Contributed by Jim Kingdon, 16-Feb-2026.)
Vtx iEdg UPGraph

16-Feb-2026	vtxedgfi 16701	In a finite graph, the number of edges from a given vertex is finite. (Contributed by Jim Kingdon, 16-Feb-2026.)
Vtx iEdg UPGraph

15-Feb-2026	eqsndc 7210	Decidability of equality between a finite subset of a set with decidable equality, and a singleton whose element is an element of the larger set. (Contributed by Jim Kingdon, 15-Feb-2026.)
DECID DECID

14-Feb-2026	pw1ninf 17192	The powerset of is not infinite. Since we cannot prove it is finite (see pw1fin 7217), this provides a concrete example of a set which we cannot show to be finite or infinite, as seen another way at inffiexmid 7213. (Contributed by Jim Kingdon, 14-Feb-2026.)


14-Feb-2026	pw1ndom3 17191	The powerset of does not dominate . This is another way of saying that does not have three elements (like pwntru 4336). (Contributed by Steven Nguyen and Jim Kingdon, 14-Feb-2026.)


14-Feb-2026	pw1ndom3lem 17190	Lemma for pw1ndom3 17191. (Contributed by Jim Kingdon, 14-Feb-2026.)


12-Feb-2026	pw1dceq 17206	The powerset of having decidable equality is equivalent to excluded middle. (Contributed by Jim Kingdon, 12-Feb-2026.)
EXMID DECID

12-Feb-2026	3dom 17189	A set that dominates ordinal 3 has at least 3 different members. (Contributed by Jim Kingdon, 12-Feb-2026.)
$/\$ $/\$

11-Feb-2026	elssdc 7209	Membership in a finite subset of a set with decidable equality is decidable. (Contributed by Jim Kingdon, 11-Feb-2026.)
DECID DECID

10-Feb-2026	vtxdgfifival 16703	The degree of a vertex for graphs with finite vertex and edge sets. (Contributed by Jim Kingdon, 10-Feb-2026.)
Vtx iEdg UPGraph VtxDeg ♯ ♯

10-Feb-2026	fidcen 7203	Equinumerosity of finite sets is decidable. (Contributed by Jim Kingdon, 10-Feb-2026.)
$/\$ DECID

8-Feb-2026	wlkvtxm 16752	A graph with a walk has at least one vertex. (Contributed by Jim Kingdon, 8-Feb-2026.)
Vtx Walks

7-Feb-2026	trlsv 16796	The classes involved in a trail are sets. (Contributed by Jim Kingdon, 7-Feb-2026.)
Trails $/\$ $/\$

7-Feb-2026	wlkex 16737	The class of walks on a graph is a set. (Contributed by Jim Kingdon, 7-Feb-2026.)
Walks

3-Feb-2026	dom1oi 7117	A set with an element dominates one. (Contributed by Jim Kingdon, 3-Feb-2026.)
$/\$

2-Feb-2026	edginwlkd 16767	The value of the edge function for an index of an edge within a walk is an edge. (Contributed by AV, 2-Jan-2021.) (Revised by AV, 9-Dec-2021.) (Revised by Jim Kingdon, 2-Feb-2026.)
iEdg Edg Word ..^♯

2-Feb-2026	wlkelvv 16761	A walk is an ordered pair. (Contributed by Jim Kingdon, 2-Feb-2026.)
Walks

1-Feb-2026	wlkcprim 16762	A walk as class with two components. (Contributed by Alexander van der Vekens, 22-Jul-2018.) (Revised by AV, 2-Jan-2021.) (Revised by Jim Kingdon, 1-Feb-2026.)
Walks Walks

1-Feb-2026	wlkmex 16731	If there are walks on a graph, the graph is a set. (Contributed by Jim Kingdon, 1-Feb-2026.)
Walks

31-Jan-2026	fvmbr 5731	If a function value is inhabited, the argument is related to the function value. (Contributed by Jim Kingdon, 31-Jan-2026.)


30-Jan-2026	elfvfvex 5730	If a function value is inhabited, the function value is a set. (Contributed by Jim Kingdon, 30-Jan-2026.)


30-Jan-2026	reldmm 5000	A relation is inhabited iff its domain is inhabited. (Contributed by Jim Kingdon, 30-Jan-2026.)


25-Jan-2026	indconst1 9306	Indicator of the whole set. (Contributed by Thierry Arnoux, 25-Jan-2026.)
𝟭

25-Jan-2026	indconst0 9305	Indicator of the empty set. (Contributed by Thierry Arnoux, 25-Jan-2026.)
𝟭

25-Jan-2026	ifp2 993	Forward direction of dfifp2dc 994. This direction does not require decidability. (Contributed by Jim Kingdon, 25-Jan-2026.)
if- $/\$

25-Jan-2026	ifpdc 992	The conditional operator for propositions implies decidability. (Contributed by Jim Kingdon, 25-Jan-2026.)
if- DECID

24-Jan-2026	eqabcbw 2376	Version of eqabcb 2377 using implicit substitution, which requires fewer axioms. (Contributed by TM, 24-Jan-2026.)


20-Jan-2026	cats1fvd 11554	A symbol other than the last in a concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) (Revised by Jim Kingdon, 20-Jan-2026.)
++ Word ♯

20-Jan-2026	cats1fvnd 11553	The last symbol of a concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) (Revised by Jim Kingdon, 20-Jan-2026.)
++ Word ♯

19-Jan-2026	cats2catd 11557	Closure of concatenation of concatenations with singleton words. (Contributed by AV, 1-Mar-2021.) (Revised by Jim Kingdon, 19-Jan-2026.)
Word Word ++ ++ ++ ++ ++

19-Jan-2026	cats1catd 11556	Closure of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) (Revised by Jim Kingdon, 19-Jan-2026.)
++ Word Word ++ ++ ++

19-Jan-2026	cats1lend 11555	The length of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) (Revised by Jim Kingdon, 19-Jan-2026.)
++ Word ♯ ♯

18-Jan-2026	rexanaliim 2656	A transformation of restricted quantifiers and logical connectives. (Contributed by NM, 4-Sep-2005.) (Revised by Jim Kingdon, 18-Jan-2026.)
$/\$

15-Jan-2026	df-uspgren 16567	Define the class of all undirected simple pseudographs (which could have loops). An undirected simple pseudograph is a special undirected pseudograph or a special undirected simple hypergraph, consisting of a set (of "vertices") and an injective (one-to-one) function (representing (indexed) "edges") into subsets of of cardinality one or two, representing the two vertices incident to the edge, or the one vertex if the edge is a loop. In contrast to a pseudograph, there is at most one edge between two vertices resp. at most one loop for a vertex. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by Jim Kingdon, 15-Jan-2026.)
USPGraph Vtx iEdg $\/$

11-Jan-2026	en2prde 7540	A set of size two is an unordered pair of two different elements. (Contributed by Alexander van der Vekens, 8-Dec-2017.) (Revised by Jim Kingdon, 11-Jan-2026.)
$/\$

10-Jan-2026	pw1mapen 17197	Equinumerosity of and the set of subsets of . (Contributed by Jim Kingdon, 10-Jan-2026.)


10-Jan-2026	pw1if 7585	Expressing a truth value in terms of an expression. (Contributed by Jim Kingdon, 10-Jan-2026.)


10-Jan-2026	pw1m 7584	A truth value which is inhabited is equal to true. This is a variation of pwntru 4336 and pwtrufal 17198. (Contributed by Jim Kingdon, 10-Jan-2026.)
$/\$

10-Jan-2026	1ndom2 7166	Two is not dominated by one. (Contributed by Jim Kingdon, 10-Jan-2026.)


9-Jan-2026	pw1map 17196	Mapping between and subsets of . (Contributed by Jim Kingdon, 9-Jan-2026.)


9-Jan-2026	iftrueb01 7583	Using an expression to represent a truth value by or . Unlike some theorems using , does not need to be decidable. (Contributed by Jim Kingdon, 9-Jan-2026.)


8-Jan-2026	pfxclz 11467	Closure of the prefix extractor. This extends pfxclg 11466 from to (negative lengths are trivial, resulting in the empty word). (Contributed by Jim Kingdon, 8-Jan-2026.)
Word $/\$ prefix Word

8-Jan-2026	fnpfx 11465	The domain of the prefix extractor. (Contributed by Jim Kingdon, 8-Jan-2026.)
prefix

7-Jan-2026	pr1or2 7541	An unordered pair, with decidable equality for the specified elements, has either one or two elements. (Contributed by Jim Kingdon, 7-Jan-2026.)
$/\$ $/\$ DECID $\/$

6-Jan-2026	upgr1elem1 16532	Lemma for upgr1edc 16533. (Contributed by AV, 16-Oct-2020.) (Revised by Jim Kingdon, 6-Jan-2026.)
DECID $\/$

3-Jan-2026	df-umgren 16506	Define the class of all undirected multigraphs. An (undirected) multigraph consists of a set (of "vertices") and a function (representing indexed "edges") into subsets of of cardinality two, representing the two vertices incident to the edge. In contrast to a pseudograph, a multigraph has no loop. This is according to Chartrand, Gary and Zhang, Ping (2012): "A First Course in Graph Theory.", Dover, ISBN 978-0-486-48368-9, section 1.4, p. 26: "A multigraph M consists of a finite nonempty set V of vertices and a set E of edges, where every two vertices of M are joined by a finite number of edges (possibly zero). If two or more edges join the same pair of (distinct) vertices, then these edges are called parallel edges." (Contributed by AV, 24-Nov-2020.) (Revised by Jim Kingdon, 3-Jan-2026.)
UMGraph Vtx iEdg

3-Jan-2026	df-upgren 16505	Define the class of all undirected pseudographs. An (undirected) pseudograph consists of a set (of "vertices") and a function (representing indexed "edges") into subsets of of cardinality one or two, representing the two vertices incident to the edge, or the one vertex if the edge is a loop. This is according to Chartrand, Gary and Zhang, Ping (2012): "A First Course in Graph Theory.", Dover, ISBN 978-0-486-48368-9, section 1.4, p. 26: "In a pseudograph, not only are parallel edges permitted but an edge is also permitted to join a vertex to itself. Such an edge is called a loop." (in contrast to a multigraph, see df-umgren 16506). (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 24-Nov-2020.) (Revised by Jim Kingdon, 3-Jan-2026.)
UPGraph Vtx iEdg $\/$

3-Jan-2026	dom1o 7116	Two ways of saying that a set is inhabited. (Contributed by Jim Kingdon, 3-Jan-2026.)


3-Jan-2026	en2m 7113	A set with two elements is inhabited. (Contributed by Jim Kingdon, 3-Jan-2026.)


3-Jan-2026	en1m 7092	A set with one element is inhabited. (Contributed by Jim Kingdon, 3-Jan-2026.)


31-Dec-2025	pw0ss 16495	There are no inhabited subsets of the empty set. (Contributed by Jim Kingdon, 31-Dec-2025.)


31-Dec-2025	df-ushgrm 16482	Define the class of all undirected simple hypergraphs. An undirected simple hypergraph is a special (non-simple, multiple, multi-) hypergraph for which the edge function is an injective (one-to-one) function into subsets of the set of vertices , representing the (one or more) vertices incident to the edge. This definition corresponds to the definition of hypergraphs in section I.1 of [Bollobas] p. 7 (except that the empty set seems to be allowed to be an "edge") or section 1.10 of [Diestel] p. 27, where "E is a subset of [...] the power set of V, that is the set of all subsets of V" resp. "the elements of E are nonempty subsets (of any cardinality) of V". (Contributed by AV, 19-Jan-2020.) (Revised by Jim Kingdon, 31-Dec-2025.)
USHGraph Vtx iEdg

29-Dec-2025	df-uhgrm 16481	Define the class of all undirected hypergraphs. An undirected hypergraph consists of a set (of "vertices") and a function (representing indexed "edges") into the set of inhabited subsets of this set. (Contributed by Alexander van der Vekens, 26-Dec-2017.) (Revised by Jim Kingdon, 29-Dec-2025.)
UHGraph Vtx iEdg

29-Dec-2025	iedgex 16431	Applying the indexed edge function yields a set. (Contributed by Jim Kingdon, 29-Dec-2025.)
iEdg

29-Dec-2025	vtxex 16430	Applying the vertex function yields a set. (Contributed by Jim Kingdon, 29-Dec-2025.)
Vtx

29-Dec-2025	snmb 3834	A singleton is inhabited iff its argument is a set. (Contributed by Scott Fenton, 8-May-2018.) (Revised by Jim Kingdon, 29-Dec-2025.)


27-Dec-2025	lswex 11372	Existence of the last symbol. The last symbol of a word is a set. See lsw0g 11369 or lswcl 11371 if you want more specific results for empty or nonempty words, respectively. (Contributed by Jim Kingdon, 27-Dec-2025.)
Word lastS

23-Dec-2025	fzowrddc 11435	Decidability of whether a range of integers is a subset of a word's domain. (Contributed by Jim Kingdon, 23-Dec-2025.)
Word $/\$ $/\$ DECID ..^

19-Dec-2025	ccatclab 11378	The concatenation of words over two sets is a word over the union of those sets. (Contributed by Jim Kingdon, 19-Dec-2025.)
Word $/\$ Word ++ Word

18-Dec-2025	lswwrd 11367	Extract the last symbol of a word. (Contributed by Alexander van der Vekens, 18-Mar-2018.) (Revised by Jim Kingdon, 18-Dec-2025.)
Word lastS ♯

14-Dec-2025	2strstrndx 13525	A constructed two-slot structure not depending on the hard-coded index value of the base set. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 14-Dec-2025.)
$/\$ Struct

12-Dec-2025	funiedgdm2vald 16444	The set of indexed edges of an extensible structure with (at least) two slots. (Contributed by AV, 22-Sep-2020.) (Revised by Jim Kingdon, 12-Dec-2025.)
$\$ iEdg .ef

11-Dec-2025	funvtxdm2vald 16443	The set of vertices of an extensible structure with (at least) two slots. (Contributed by AV, 22-Sep-2020.) (Revised by Jim Kingdon, 11-Dec-2025.)
$\$ Vtx

11-Dec-2025	funiedgdm2domval 16442	The set of indexed edges of an extensible structure with (at least) two slots. (Contributed by AV, 12-Oct-2020.) (Revised by Jim Kingdon, 11-Dec-2025.)
$/\$ $\$ $/\$ iEdg .ef

11-Dec-2025	funvtxdm2domval 16441	The set of vertices of an extensible structure with (at least) two slots. (Contributed by AV, 12-Oct-2020.) (Revised by Jim Kingdon, 11-Dec-2025.)
$/\$ $\$ $/\$ Vtx

4-Dec-2025	hash2en 11311	Two equivalent ways to say a set has two elements. (Contributed by Jim Kingdon, 4-Dec-2025.)
$/\$ ♯

30-Nov-2025	nninfnfiinf 17237	An element of ℕ_∞ which is not finite is infinite. (Contributed by Jim Kingdon, 30-Nov-2025.)
ℕ_∞ $/\$

30-Nov-2025	eluz3nn 9977	An integer greater than or equal to 3 is a positive integer. (Contributed by Alexander van der Vekens, 17-Sep-2018.) (Proof shortened by AV, 30-Nov-2025.)


27-Nov-2025	psrelbasfi 15152	Simpler form of psrelbas 15151 when the index set is finite. (Contributed by Jim Kingdon, 27-Nov-2025.)
mPwSer

26-Nov-2025	mplsubgfileminv 15182	Lemma for mplsubgfi 15183. The additive inverse of a polynomial is a polynomial. (Contributed by Jim Kingdon, 26-Nov-2025.)
mPwSer mPoly

26-Nov-2025	mplsubgfilemcl 15181	Lemma for mplsubgfi 15183. The sum of two polynomials is a polynomial. (Contributed by Jim Kingdon, 26-Nov-2025.)
mPwSer mPoly

25-Nov-2025	nninfinfwlpo 7521	The point at infinity in ℕ_∞ being isolated is equivalent to the Weak Limited Principle of Omniscience (WLPO). By isolated, we mean that the equality of that point with every other element of ℕ_∞ is decidable. From an online post by Martin Escardo. By contrast, elements of ℕ_∞ corresponding to natural numbers are isolated (nninfisol 7474). (Contributed by Jim Kingdon, 25-Nov-2025.)
ℕ_∞ DECID WOmni

23-Nov-2025	psrbagfi 15143	A finite index set gives a simpler expression for finite bags. (Contributed by Jim Kingdon, 23-Nov-2025.)


22-Nov-2025	df-acnm 7526	Define a local and length-limited version of the axiom of choice. The definition of the predicate AC is that for all families of inhabited subsets of indexed on (i.e. functions ), there is a function which selects an element from each set in the family. (Contributed by Mario Carneiro, 31-Aug-2015.) Change nonempty to inhabited. (Revised by Jim Kingdon, 22-Nov-2025.)
AC $/\$

21-Nov-2025	mplsubgfilemm 15180	Lemma for mplsubgfi 15183. There exists a polynomial. (Contributed by Jim Kingdon, 21-Nov-2025.)
mPwSer mPoly

15-Nov-2025	uzuzle35 9975	An integer greater than or equal to 5 is an integer greater than or equal to 3. (Contributed by AV, 15-Nov-2025.)


14-Nov-2025	2omapen 7320	Equinumerosity of and the set of decidable subsets of . (Contributed by Jim Kingdon, 14-Nov-2025.)
DECID

12-Nov-2025	2omap 7319	Mapping between and decidable subsets of . (Contributed by Jim Kingdon, 12-Nov-2025.)
DECID

11-Nov-2025	domomsubct 17202	A set dominated by is subcountable. (Contributed by Jim Kingdon, 11-Nov-2025.)
$/\$

10-Nov-2025	prdsbaslemss 14258	Lemma for prdsbas 14260 and similar theorems. (Contributed by Jim Kingdon, 10-Nov-2025.)
_s Slot

5-Nov-2025	fnmpl 15175	mPoly has universal domain. (Contributed by Jim Kingdon, 5-Nov-2025.)
mPoly

4-Nov-2025	mplelbascoe 15174	Property of being a polynomial. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 25-Jun-2019.) (Revised by Jim Kingdon, 4-Nov-2025.)
mPoly mPwSer $/\$ $/\$

4-Nov-2025	mplbascoe 15173	Base set of the set of multivariate polynomials. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by AV, 25-Jun-2019.) (Revised by Jim Kingdon, 4-Nov-2025.)
mPoly mPwSer $/\$

4-Nov-2025	mplvalcoe 15172	Value of the set of multivariate polynomials. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by AV, 25-Jun-2019.) (Revised by Jim Kingdon, 4-Nov-2025.)
mPoly mPwSer $/\$ ↾_s

1-Nov-2025	ficardon 7535	The cardinal number of a finite set is an ordinal. (Contributed by Jim Kingdon, 1-Nov-2025.)


31-Oct-2025	bitsdc 12733	Whether a bit is set is decidable. (Contributed by Jim Kingdon, 31-Oct-2025.)
$/\$ DECID bits

28-Oct-2025	nn0maxcl 12008	The maximum of two nonnegative integers is a nonnegative integer. (Contributed by Jim Kingdon, 28-Oct-2025.)
$/\$

28-Oct-2025	qdcle 10692	Rational is decidable. (Contributed by Jim Kingdon, 28-Oct-2025.)
$/\$ DECID

17-Oct-2025	plycoeid3 15949	Reconstruct a polynomial as an explicit sum of the coefficient function up to an index no smaller than the degree of the polynomial. (Contributed by Jim Kingdon, 17-Oct-2025.)


13-Oct-2025	tpfidceq 7237	A triple is finite if it consists of elements of a class with decidable equality. (Contributed by Jim Kingdon, 13-Oct-2025.)
DECID

13-Oct-2025	prfidceq 7235	A pair is finite if it consists of elements of a class with decidable equality. (Contributed by Jim Kingdon, 13-Oct-2025.)
DECID

13-Oct-2025	dcun 3637	The union of two decidable classes is decidable. (Contributed by Jim Kingdon, 5-Oct-2022.) (Revised by Jim Kingdon, 13-Oct-2025.)
DECID DECID DECID

9-Oct-2025	dvdsfi 13040	A natural number has finitely many divisors. (Contributed by Jim Kingdon, 9-Oct-2025.)


7-Oct-2025	df-mplcoe 15132	Define the subalgebra of the power series algebra generated by the variables; this is the polynomial algebra (the set of power series with finite degree). The index set (which has an element for each variable) is , the coefficients are in ring , and for each variable there is a "degree" such that the coefficient is zero for a term where the powers are all greater than those degrees. (Degree is in quotes because there is no guarantee that coefficients below that degree are nonzero, as we do not assume decidable equality for ). (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by AV, 25-Jun-2019.) (Revised by Jim Kingdon, 7-Oct-2025.)
mPoly mPwSer ↾_s

6-Oct-2025	dvconstss 15890	Derivative of a constant function defined on an open set. (Contributed by Jim Kingdon, 6-Oct-2025.)
↾_t

6-Oct-2025	dcfrompeirce 1499	The decidability of a proposition follows from a suitable instance of Peirce's law. Therefore, if we were to introduce Peirce's law as a general principle (without the decidability condition in peircedc 926), then we could prove that every proposition is decidable, giving us the classical system of propositional calculus (since Perice's law is itself classically valid). (Contributed by Adrian Ducourtial, 6-Oct-2025.)
$\/$ DECID

6-Oct-2025	dcfromcon 1498	The decidability of a proposition follows from a suitable instance of the principle of contraposition. Therefore, if we were to introduce contraposition as a general principle (without the decidability condition in condc 865), then we could prove that every proposition is decidable, giving us the classical system of propositional calculus (since the principle of contraposition is itself classically valid). (Contributed by Adrian Ducourtial, 6-Oct-2025.)
$\/$ DECID

6-Oct-2025	dcfromnotnotr 1497	The decidability of a proposition follows from a suitable instance of double negation elimination (DNE). Therefore, if we were to introduce DNE as a general principle (without the decidability condition in notnotrdc 855), then we could prove that every proposition is decidable, giving us the classical system of propositional calculus (since DNE itself is classically valid). (Contributed by Adrian Ducourtial, 6-Oct-2025.)
$\/$ DECID

3-Oct-2025	dvidre 15889	Real derivative of the identity function. (Contributed by Jim Kingdon, 3-Oct-2025.)


3-Oct-2025	dvconstre 15888	Real derivative of a constant function. (Contributed by Jim Kingdon, 3-Oct-2025.)


3-Oct-2025	dvidsslem 15885	Lemma for dvconstss 15890. Analogue of dvidlemap 15883 where is defined on an open subset of the real or complex numbers. (Contributed by Jim Kingdon, 3-Oct-2025.)
↾_t $/\$ $/\$ $/\$ #

3-Oct-2025	dvidrelem 15884	Lemma for dvidre 15889 and dvconstre 15888. Analogue of dvidlemap 15883 for real numbers rather than complex numbers. (Contributed by Jim Kingdon, 3-Oct-2025.)
$/\$ $/\$ $/\$ #

28-Sep-2025	metuex 14976	Applying metUnif yields a set. (Contributed by Jim Kingdon, 28-Sep-2025.)
metUnif

28-Sep-2025	cndsex 14974	The standard distance function on the complex numbers is a set. (Contributed by Jim Kingdon, 28-Sep-2025.)


25-Sep-2025	cntopex 14975	The standard topology on the complex numbers is a set. (Contributed by Jim Kingdon, 25-Sep-2025.)


24-Sep-2025	mopnset 14973	Getting a set by applying . (Contributed by Jim Kingdon, 24-Sep-2025.)


24-Sep-2025	blfn 14972	The ball function has universal domain. (Contributed by Jim Kingdon, 24-Sep-2025.)


23-Sep-2025	elfzoext 10621	Membership of an integer in an extended open range of integers, extension added to the right. (Contributed by AV, 30-Apr-2020.) (Proof shortened by AV, 23-Sep-2025.)
..^ $/\$ ..^

22-Sep-2025	plycjlemc 15952	Lemma for plycj 15953. (Contributed by Mario Carneiro, 24-Jul-2014.) (Revised by Jim Kingdon, 22-Sep-2025.)
Poly

22-Sep-2025	asclelbas 15110	Lifted scalars are in the base set of the algebra. (Contributed by Zhi Wang, 11-Sep-2025.) (Proof shortened by Thierry Arnoux, 22-Sep-2025.)
algSc Scalar AssAlg

20-Sep-2025	plycolemc 15950	Lemma for plyco 15951. The result expressed as a sum, with a degree and coefficients for specified as hypotheses. (Contributed by Jim Kingdon, 20-Sep-2025.)
Poly Poly $/\$ $/\$ $/\$ $/\$ Poly

18-Sep-2025	elfzoextl 10620	Membership of an integer in an extended open range of integers, extension added to the left. (Contributed by AV, 31-Aug-2025.) Generalized by replacing the left border of the ranges. (Revised by SN, 18-Sep-2025.)
..^ $/\$ ..^

16-Sep-2025	lgsquadlemofi 16366	Lemma for lgsquad 16370. There are finitely many members of with odd first part. (Contributed by Jim Kingdon, 16-Sep-2025.)
$\$ $\$ $/\$ $/\$

16-Sep-2025	lgsquadlemsfi 16365	Lemma for lgsquad 16370. is finite. (Contributed by Jim Kingdon, 16-Sep-2025.)
$\$ $\$ $/\$ $/\$

16-Sep-2025	opabfi 7247	Finiteness of an ordered pair abstraction which is a decidable subset of finite sets. (Contributed by Jim Kingdon, 16-Sep-2025.)
$/\$ $/\$ DECID

13-Sep-2025	uchoice 6371	Principle of unique choice. This is also called non-choice. The name choice results in its similarity to something like acfun 7564 (with the key difference being the change of to ) but unique choice in fact follows from the axiom of collection and our other axioms. This is somewhat similar to Corollary 3.9.2 of [HoTT], p. (varies) but is better described by the paragraph at the end of Section 3.9 which starts "A similar issue arises in set-theoretic mathematics". (Contributed by Jim Kingdon, 13-Sep-2025.)
$/\$ $/\$

11-Sep-2025	assa2ass2 15094	Left- and right-associative property of an associative algebra. Notice that the scalars are not commuted! (Contributed by Zhi Wang, 11-Sep-2025.)
Scalar AssAlg $/\$ $/\$ $/\$ $/\$

11-Sep-2025	assa2ass 15093	Left- and right-associative property of an associative algebra. Notice that the scalars are commuted! (Contributed by AV, 14-Aug-2019.) (Proof shortened by Zhi Wang, 11-Sep-2025.)
Scalar AssAlg $/\$ $/\$ $/\$ $/\$

11-Sep-2025	expghmap 15026	Exponentiation is a group homomorphism from addition to multiplication. (Contributed by Mario Carneiro, 18-Jun-2015.) (Revised by AV, 10-Jun-2019.) (Revised by Jim Kingdon, 11-Sep-2025.)
mulGrpℂ_fld ↾_s # $/\$ # ℤ_ring

11-Sep-2025	cnfldui 15008	The invertible complex numbers are exactly those apart from zero. This is recapb 9004 but expressed in terms of ℂ_fld. (Contributed by Jim Kingdon, 11-Sep-2025.)
# Unitℂ_fld

9-Sep-2025	gzsummhm2 14230	Apply a group homomorphism to a group sum, mapping version with implicit substitution. (Contributed by Mario Carneiro, 5-May-2015.) (Revised by AV, 6-Jun-2019.) (Revised by Jim Kingdon, 9-Sep-2025.)
CMnd MndHom $/\$ _gz _gz

8-Sep-2025	gzsummhm 14229	Apply a monoid homomorphism to a group sum. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by AV, 6-Jun-2019.) (Revised by Jim Kingdon, 8-Sep-2025.)
CMnd MndHom _gz _gz

8-Sep-2025	5ndvds6 12721	5 does not divide 6. (Contributed by AV, 8-Sep-2025.)


8-Sep-2025	5ndvds3 12720	5 does not divide 3. (Contributed by AV, 8-Sep-2025.)


7-Sep-2025	5eluz3 9971	5 is an integer greater than or equal to 3. (Contributed by AV, 7-Sep-2025.)


6-Sep-2025	gzsumconst 14227	Sum of a constant series. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by Jim Kingdon, 6-Sep-2025.)
._g $/\$ $/\$ _gz

5-Sep-2025	uzuzle34 9974	An integer greater than or equal to 4 is an integer greater than or equal to 3. (Contributed by AV, 5-Sep-2025.)


30-Aug-2025	gzsumsubmcl 14226	Closure of a group sum in a submonoid. (Contributed by Mario Carneiro, 10-Jan-2015.) (Revised by AV, 3-Jun-2019.) (Revised by Jim Kingdon, 30-Aug-2025.)
SubMnd _gz

30-Aug-2025	seqm1g 10926	Value of the sequence builder function at a successor. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Jim Kingdon, 30-Aug-2025.)


29-Aug-2025	seqf1og 10973	Rearrange a sum via an arbitrary bijection on . (Contributed by Mario Carneiro, 27-Feb-2014.) (Revised by Jim Kingdon, 29-Aug-2025.)
$/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

25-Aug-2025	irrmulap 10059	The product of an irrational with a nonzero rational is irrational. By irrational we mean apart from any rational number. For a similar theorem with not rational in place of irrational, see irrmul 10058. (Contributed by Jim Kingdon, 25-Aug-2025.)
# #

19-Aug-2025	seqp1g 10918	Value of the sequence builder function at a successor. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Jim Kingdon, 19-Aug-2025.)
$/\$ $/\$

19-Aug-2025	seq1g 10915	Value of the sequence builder function at its initial value. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Jim Kingdon, 19-Aug-2025.)
$/\$ $/\$

18-Aug-2025	iswrdiz 11327	A zero-based sequence is a word. In iswrdinn0 11325 we can specify a length as an nonnegative integer. However, it will occasionally be helpful to allow a negative length, as well as zero, to specify an empty sequence. (Contributed by Jim Kingdon, 18-Aug-2025.)
..^ $/\$ Word

16-Aug-2025	gzsumcl 13857	Closure of an ordered group sum. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by AV, 3-Jun-2019.) (Revised by Jim Kingdon, 16-Aug-2025.)
_gz

16-Aug-2025	iswrdinn0 11325	A zero-based sequence is a word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) (Revised by Jim Kingdon, 16-Aug-2025.)
..^ $/\$ Word

14-Aug-2025	gzsumfzval 13764	An expression for _gz when summing over a finite set of sequential integers. (Contributed by Jim Kingdon, 14-Aug-2025.)
_gz

13-Aug-2025	znidom 15076	The ℤ/nℤ structure is an integral domain when is prime. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by Jim Kingdon, 13-Aug-2025.)
ℤ/nℤ IDomn

12-Aug-2025	rrgmex 14653	A structure whose set of left-regular elements is inhabited is a set. (Contributed by Jim Kingdon, 12-Aug-2025.)
RLReg

10-Aug-2025	gausslemma2dlem1cl 16349	Lemma for gausslemma2dlem1 16351. Closure of the body of the definition of . (Contributed by Jim Kingdon, 10-Aug-2025.)
$\$

9-Aug-2025	gausslemma2dlem1f1o 16350	Lemma for gausslemma2dlem1 16351. (Contributed by Jim Kingdon, 9-Aug-2025.)
$\$

7-Aug-2025	qdclt 10691	Rational is decidable. (Contributed by Jim Kingdon, 7-Aug-2025.)
$/\$ DECID

22-Jul-2025	ivthdich 15845	The intermediate value theorem implies real number dichotomy. Because real number dichotomy (also known as analytic LLPO) is a constructive taboo, this means we will be unable to prove the intermediate value theorem as stated here (although versions with additional conditions, such as ivthinc 15835 for strictly monotonic functions, can be proved). The proof is via a function which we call the hover function and which is also described in Section 5.1 of [Bauer], p. 493. Consider any real number . We want to show that $\/$ . Because of hovercncf 15838, hovera 15839, and hoverb 15840, we are able to apply the intermediate value theorem to get a value such that the hover function at equals . By axltwlin 8394, or , and that leads to by hoverlt1 15841 or by hovergt0 15842. (Contributed by Jim Kingdon and Mario Carneiro, 22-Jul-2025.)
$/\$ $/\$ $/\$ $/\$ $\/$

22-Jul-2025	dich0 15844	Real number dichotomy stated in terms of two real numbers or a real number and zero. (Contributed by Jim Kingdon, 22-Jul-2025.)
$\/$ $\/$

22-Jul-2025	ivthdichlem 15843	Lemma for ivthdich 15845. The result, with a few notational conveniences. (Contributed by Jim Kingdon, 22-Jul-2025.)
inf $/\$ $/\$ $/\$ $/\$ $\/$

22-Jul-2025	hovergt0 15842	The hover function evaluated at a point greater than zero. (Contributed by Jim Kingdon, 22-Jul-2025.)
inf $/\$

22-Jul-2025	hoverlt1 15841	The hover function evaluated at a point less than one. (Contributed by Jim Kingdon, 22-Jul-2025.)
inf $/\$

21-Jul-2025	hoverb 15840	A point at which the hover function is greater than a given value. (Contributed by Jim Kingdon, 21-Jul-2025.)
inf

21-Jul-2025	hovera 15839	A point at which the hover function is less than a given value. (Contributed by Jim Kingdon, 21-Jul-2025.)
inf

21-Jul-2025	rexeqtrrdv 2760	Substitution of equal classes into a restricted existential quantifier. (Contributed by Matthew House, 21-Jul-2025.)


21-Jul-2025	raleqtrrdv 2759	Substitution of equal classes into a restricted universal quantifier. (Contributed by Matthew House, 21-Jul-2025.)


21-Jul-2025	rexeqtrdv 2758	Substitution of equal classes into a restricted existential quantifier. (Contributed by Matthew House, 21-Jul-2025.)


21-Jul-2025	raleqtrdv 2757	Substitution of equal classes into a restricted universal quantifier. (Contributed by Matthew House, 21-Jul-2025.)


20-Jul-2025	hovercncf 15838	The hover function is continuous. By hover function, we mean a a function which starts out as a line of slope one, is constant at zero from zero to one, and then resumes as a slope of one. (Contributed by Jim Kingdon, 20-Jul-2025.)
inf

19-Jul-2025	mincncf 15808	The minimum of two continuous real functions is continuous. (Contributed by Jim Kingdon, 19-Jul-2025.)
inf

18-Jul-2025	maxcncf 15807	The maximum of two continuous real functions is continuous. (Contributed by Jim Kingdon, 18-Jul-2025.)


14-Jul-2025	xnn0nnen 10889	The set of extended nonnegative integers is equinumerous to the set of natural numbers. (Contributed by Jim Kingdon, 14-Jul-2025.)
NN0*

12-Jul-2025	nninfninc 7464	All values beyond a zero in an ℕ_∞ sequence are zero. This is another way of stating that elements of ℕ_∞ are nonincreasing. (Contributed by Jim Kingdon, 12-Jul-2025.)
ℕ_∞

10-Jul-2025	nninfctlemfo 12836	Lemma for nninfct 12837. (Contributed by Jim Kingdon, 10-Jul-2025.)
frec Omni NN0*ℕ_∞

8-Jul-2025	nnnninfen 17235	Equinumerosity of the natural numbers and ℕ_∞ is equivalent to the Limited Principle of Omniscience (LPO). Remark in Section 1.1 of [Pradic2025], p. 2. (Contributed by Jim Kingdon, 8-Jul-2025.)
ℕ_∞ Omni

8-Jul-2025	nninfct 12837	The limited principle of omniscience (LPO) implies that ℕ_∞ is countable. (Contributed by Jim Kingdon, 8-Jul-2025.)
Omni ℕ_∞ ⊔

8-Jul-2025	nninfinf 10895	ℕ_∞ is infinte. (Contributed by Jim Kingdon, 8-Jul-2025.)
ℕ_∞

7-Jul-2025	ivthreinc 15837	Restating the intermediate value theorem. Given a hypothesis stating the intermediate value theorem (in a strong form which is not provable given our axioms alone), provide a conclusion similar to the theorem as stated in the Metamath Proof Explorer (which is also similar to how we state the theorem for a strictly monotonic function at ivthinc 15835). Being able to have a hypothesis stating the intermediate value theorem will be helpful when it comes time to show that it implies a constructive taboo. This version of the theorem requires that the function is continuous on the entire real line, not just which may be an unnecessary condition but which is sufficient for the way we want to use it. (Contributed by Jim Kingdon, 7-Jul-2025.)
$/\$ $/\$ $/\$ $/\$ $/\$

28-Jun-2025	fngzsum 13761	Iterated sum has a universal domain. (Contributed by Jim Kingdon, 28-Jun-2025.)
_gz

28-Jun-2025	iotaexel 6043	Set existence of an iota expression in which all values are contained within a set. (Contributed by Jim Kingdon, 28-Jun-2025.)
$/\$

27-Jun-2025	df-gzsum 13666	Define a finite group sum (also called "iterated sum") of a structure. Given _gz where , the set of indices is and the values are given by at each index. A group sum over a multiplicative group may be viewed as a product. The definition is meaningful in different contexts, depending on the size of the index set and each demanding different properties of . 1. If and has an identity element, then the sum equals this identity. 2. If and is any magma, then the sum is the sum of the elements, evaluated left-to-right, i.e., , etc. 3. This definition does not handle other cases. But see df-gsumfi 14235 for the case where is a finite set (which need not specify an order) and is a commutative monoid. (Contributed by FL, 5-Sep-2010.) (Revised by Mario Carneiro, 7-Dec-2014.) (Revised by Jim Kingdon, 27-Jun-2025.)
_gz $/\$ $\/$ $/\$

20-Jun-2025	opprnzrbg 14576	The opposite of a nonzero ring is nonzero, bidirectional form of opprnzr 14577. (Contributed by SN, 20-Jun-2025.)
opp_r NzRing NzRing

16-Jun-2025	fnpsr 15135	The multivariate power series constructor has a universal domain. (Contributed by Jim Kingdon, 16-Jun-2025.)
mPwSer

14-Jun-2025	basm 13466	A structure whose base is inhabited is inhabited. (Contributed by Jim Kingdon, 14-Jun-2025.)


14-Jun-2025	elfvm 5729	If a function value has a member, the function is inhabited. (Contributed by Jim Kingdon, 14-Jun-2025.)


6-Jun-2025	pcxqcl 13114	The general prime count function is an integer or infinite. (Contributed by Jim Kingdon, 6-Jun-2025.)
$/\$ $\/$

5-Jun-2025	xqltnle 10713	"Less than" expressed in terms of "less than or equal to", for extended numbers which are rational or . We have not yet had enough usage of such numbers to warrant fully developing the concept, as in NN0* or , so for now we just have a handful of theorems for what we need. (Contributed by Jim Kingdon, 5-Jun-2025.)
$\/$ $/\$ $\/$

5-Jun-2025	ceqsexv2d 2862	Elimination of an existential quantifier, using implicit substitution. (Contributed by Thierry Arnoux, 10-Sep-2016.) Shorten, reduce dv conditions. (Revised by Wolf Lammen, 5-Jun-2025.) (Proof shortened by SN, 5-Jun-2025.)


31-May-2025	vtocl4ga 2895	Implicit substitution of 4 classes for 4 setvar variables. (Contributed by AV, 22-Jan-2019.) (Proof shortened by Wolf Lammen, 31-May-2025.)
$/\$ $/\$ $/\$ $/\$ $/\$ $/\$

30-May-2025	4sqexercise2 13201	Exercise which may help in understanding the proof of 4sqlemsdc 13202. (Contributed by Jim Kingdon, 30-May-2025.)
DECID

27-May-2025	iotaexab 5356	Existence of the class when all the possible values are contained in a set. (Contributed by Jim Kingdon, 27-May-2025.)


25-May-2025	4sqlemsdc 13202	Lemma for 4sq 13212. The property of being the sum of four squares is decidable. The proof involves showing that (for a particular ) there are only a finite number of possible ways that it could be the sum of four squares, so checking each of those possibilities in turn decides whether the number is the sum of four squares. If this proof is hard to follow, especially because of its length, the simplified versions at 4sqexercise1 13200 and 4sqexercise2 13201 may help clarify, as they are using very much the same techniques on simplified versions of this lemma. (Contributed by Jim Kingdon, 25-May-2025.)
DECID

25-May-2025	4sqexercise1 13200	Exercise which may help in understanding the proof of 4sqlemsdc 13202. (Contributed by Jim Kingdon, 25-May-2025.)
DECID

24-May-2025	4sqleminfi 13199	Lemma for 4sq 13212. is finite. (Contributed by Jim Kingdon, 24-May-2025.)


24-May-2025	4sqlemffi 13198	Lemma for 4sq 13212. is finite. (Contributed by Jim Kingdon, 24-May-2025.)


24-May-2025	4sqlemafi 13197	Lemma for 4sq 13212. is finite. (Contributed by Jim Kingdon, 24-May-2025.)


24-May-2025	infidc 7248	The intersection of two sets is finite if one of them is and the other is decidable. (Contributed by Jim Kingdon, 24-May-2025.)
$/\$ DECID

19-May-2025	zrhex 15040	Set existence for RHom. (Contributed by Jim Kingdon, 19-May-2025.)
RHom

16-May-2025	rhmex 14548	Set existence for ring homomorphism. (Contributed by Jim Kingdon, 16-May-2025.)
$/\$ RingHom

15-May-2025	ghmex 14111	The set of group homomorphisms exists. (Contributed by Jim Kingdon, 15-May-2025.)
$/\$

15-May-2025	mhmex 13822	The set of monoid homomorphisms exists. (Contributed by Jim Kingdon, 15-May-2025.)
$/\$ MndHom

14-May-2025	idomcringd 14671	An integral domain is a commutative ring with unity. (Contributed by Thierry Arnoux, 4-May-2025.) (Proof shortened by SN, 14-May-2025.)
IDomn

6-May-2025	rrgnz 14661	In a nonzero ring, the zero is a left zero divisor (that is, not a left-regular element). (Contributed by Thierry Arnoux, 6-May-2025.)
RLReg NzRing

5-May-2025	rngressid 14337	A non-unital ring restricted to its base set is a non-unital ring. It will usually be the original non-unital ring exactly, of course, but to show that needs additional conditions such as those in strressid 13478. (Contributed by Jim Kingdon, 5-May-2025.)
Rng ↾_s Rng

5-May-2025	ablressid 14223	A commutative group restricted to its base set is a commutative group. It will usually be the original group exactly, of course, but to show that needs additional conditions such as those in strressid 13478. (Contributed by Jim Kingdon, 5-May-2025.)
↾_s

30-Apr-2025	dvply2g 15958	The derivative of a polynomial with coefficients in a subring is a polynomial with coefficients in the same ring. (Contributed by Mario Carneiro, 1-Jan-2017.) (Revised by GG, 30-Apr-2025.)
SubRingℂ_fld $/\$ Poly Poly

29-Apr-2025	rlmscabas 14881	Scalars in the ring module have the same base set. (Contributed by Jim Kingdon, 29-Apr-2025.)
ScalarringLMod

29-Apr-2025	ressbasid 13477	The trivial structure restriction leaves the base set unchanged. (Contributed by Jim Kingdon, 29-Apr-2025.)
↾_s

28-Apr-2025	lssmex 14776	If a linear subspace is inhabited, the class it is built from is a set. (Contributed by Jim Kingdon, 28-Apr-2025.)


27-Apr-2025	cnfldmul 14985	The multiplication operation of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) (Revised by GG, 27-Apr-2025.)
ℂ_fld

27-Apr-2025	cnfldadd 14983	The addition operation of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) (Revised by GG, 27-Apr-2025.)
ℂ_fld

27-Apr-2025	lidlex 14894	Existence of the set of left ideals. (Contributed by Jim Kingdon, 27-Apr-2025.)
LIdeal

27-Apr-2025	lssex 14775	Existence of a linear subspace. (Contributed by Jim Kingdon, 27-Apr-2025.)


25-Apr-2025	rspex 14895	Existence of the ring span. (Contributed by Jim Kingdon, 25-Apr-2025.)
RSpan

25-Apr-2025	lspex 14816	Existence of the span of a set of vectors. (Contributed by Jim Kingdon, 25-Apr-2025.)


25-Apr-2025	eqgex 14077	The left coset equivalence relation exists. (Contributed by Jim Kingdon, 25-Apr-2025.)
$/\$ ~_QG

25-Apr-2025	qusex 13699	Existence of a quotient structure. (Contributed by Jim Kingdon, 25-Apr-2025.)
$/\$ _s

23-Apr-2025	1dom1el 7107	If a set is dominated by one, then any two of its elements are equal. (Contributed by Jim Kingdon, 23-Apr-2025.)
$/\$ $/\$

22-Apr-2025	mulgex 13979	Existence of the group multiple operation. (Contributed by Jim Kingdon, 22-Apr-2025.)
._g

21-Apr-2025	uspgruhgr 16599	An undirected simple pseudograph is an undirected hypergraph. (Contributed by AV, 21-Apr-2025.)
USPGraph UHGraph

20-Apr-2025	uspgriedgedg 16591	In a simple pseudograph, for each indexed edge there is exactly one edge. (Contributed by AV, 20-Apr-2025.)
Edg iEdg USPGraph $/\$

20-Apr-2025	uspgredgiedg 16590	In a simple pseudograph, for each edge there is exactly one indexed edge. (Contributed by AV, 20-Apr-2025.)
Edg iEdg USPGraph $/\$

20-Apr-2025	elovmpod 6287	Utility lemma for two-parameter classes. (Contributed by Stefan O'Rear, 21-Jan-2015.) Variant of elovmpo 6288 in deduction form. (Revised by AV, 20-Apr-2025.)
$/\$

20-Apr-2025	fdmeu 5746	There is exactly one codomain element for each element of the domain of a function. (Contributed by AV, 20-Apr-2025.)
$/\$

18-Apr-2025	fsumdvdsmul 16251	Product of two divisor sums. (This is also the main part of the proof that " is a multiplicative function if is".) (Contributed by Mario Carneiro, 2-Jul-2015.) Avoid ax-mulf 8303. (Revised by GG, 18-Apr-2025.)
$/\$ $/\$ $/\$ $/\$

18-Apr-2025	mpodvdsmulf1o 16250	If and are two coprime integers, multiplication forms a bijection from the set of pairs where and , to the set of divisors of . (Contributed by GG, 18-Apr-2025.)


18-Apr-2025	df2idl2 14930	Alternate (the usual textbook) definition of a two-sided ideal of a ring to be a subgroup of the additive group of the ring which is closed under left- and right-multiplication by elements of the full ring. (Contributed by AV, 13-Feb-2025.) (Proof shortened by AV, 18-Apr-2025.)
2Ideal SubGrp $/\$ $/\$

18-Apr-2025	2idlmex 14922	Existence of the set a two-sided ideal is built from (when the ideal is inhabited). (Contributed by Jim Kingdon, 18-Apr-2025.)
2Ideal

18-Apr-2025	dflidl2 14909	Alternate (the usual textbook) definition of a (left) ideal of a ring to be a subgroup of the additive group of the ring which is closed under left-multiplication by elements of the full ring. (Contributed by AV, 13-Feb-2025.) (Proof shortened by AV, 18-Apr-2025.)
LIdeal SubGrp $/\$

18-Apr-2025	lidlmex 14896	Existence of the set a left ideal is built from (when the ideal is inhabited). (Contributed by Jim Kingdon, 18-Apr-2025.)
LIdeal

18-Apr-2025	lsslsp 14850	Spans in submodules correspond to spans in the containing module. (Contributed by Stefan O'Rear, 12-Dec-2014.) Terms in the equation were swapped as proposed by NM on 15-Mar-2015. (Revised by AV, 18-Apr-2025.)
↾_s $/\$ $/\$

16-Apr-2025	sraex 14867	Existence of a subring algebra. (Contributed by Jim Kingdon, 16-Apr-2025.)
subringAlg

14-Apr-2025	grpmgmd 13884	A group is a magma, deduction form. (Contributed by SN, 14-Apr-2025.)
Mgm

12-Apr-2025	psraddcl 15156	Closure of the power series addition operation. (Contributed by Mario Carneiro, 28-Dec-2014.) Generalize to magmas. (Revised by SN, 12-Apr-2025.)
mPwSer Mgm

10-Apr-2025	cndcap 17281	Real number trichotomy is equivalent to decidability of complex number apartness. (Contributed by Jim Kingdon, 10-Apr-2025.)
$\/$ $\/$ DECID #

4-Apr-2025	ghmf1 14129	Two ways of saying a group homomorphism is 1-1 into its codomain. (Contributed by Paul Chapman, 3-Mar-2008.) (Revised by Mario Carneiro, 13-Jan-2015.) (Proof shortened by AV, 4-Apr-2025.)


3-Apr-2025	quscrng 14954	The quotient of a commutative ring by an ideal is a commutative ring. (Contributed by Mario Carneiro, 15-Jun-2015.) (Proof shortened by AV, 3-Apr-2025.)
_s ~_QG LIdeal $/\$

31-Mar-2025	cnfldds 14989	The metric of the field of complex numbers. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) Revise df-cnfld 14978. (Revised by GG, 31-Mar-2025.)
ℂ_fld

31-Mar-2025	cnfldle 14988	The ordering of the field of complex numbers. Note that this is not actually an ordering on , but we put it in the structure anyway because restricting to does not affect this component, so that ℂ_fld ↾_s is an ordered field even though ℂ_fld itself is not. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) Revise df-cnfld 14978. (Revised by GG, 31-Mar-2025.)
ℂ_fld

31-Mar-2025	cnfldtset 14987	The topology component of the field of complex numbers. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) (Revised by GG, 31-Mar-2025.)
TopSetℂ_fld

31-Mar-2025	mpocnfldmul 14984	The multiplication operation of the field of complex numbers. Version of cnfldmul 14985 using maps-to notation, which does not require ax-mulf 8303. (Contributed by GG, 31-Mar-2025.)
ℂ_fld

31-Mar-2025	mpocnfldadd 14982	The addition operation of the field of complex numbers. Version of cnfldadd 14983 using maps-to notation, which does not require ax-addf 8302. (Contributed by GG, 31-Mar-2025.)
ℂ_fld

31-Mar-2025	df-cnfld 14978	The field of complex numbers. Other number fields and rings can be constructed by applying the ↾_s restriction operator. The contract of this set is defined entirely by cnfldex 14980, cnfldadd 14983, cnfldmul 14985, cnfldcj 14986, cnfldtset 14987, cnfldle 14988, cnfldds 14989, and cnfldbas 14981. We may add additional members to this in the future. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Thierry Arnoux, 15-Dec-2017.) Use maps-to notation for addition and multiplication. (Revised by GG, 31-Mar-2025.) (New usage is discouraged.)
ℂ_fld TopSet metUnif

31-Mar-2025	2idlcpbl 14945	The coset equivalence relation for a two-sided ideal is compatible with ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015.) (Proof shortened by AV, 31-Mar-2025.)
~_QG 2Ideal $/\$ $/\$

22-Mar-2025	idomringd 14672	An integral domain is a ring. (Contributed by Thierry Arnoux, 22-Mar-2025.)
IDomn

22-Mar-2025	idomdomd 14670	An integral domain is a domain. (Contributed by Thierry Arnoux, 22-Mar-2025.)
IDomn Domn

21-Mar-2025	df2idl2rng 14929	Alternate (the usual textbook) definition of a two-sided ideal of a non-unital ring to be a subgroup of the additive group of the ring which is closed under left- and right-multiplication by elements of the full ring. (Contributed by AV, 21-Mar-2025.)
2Ideal Rng $/\$ SubGrp $/\$

21-Mar-2025	isridlrng 14903	A right ideal is a left ideal of the opposite non-unital ring. This theorem shows that this definition corresponds to the usual textbook definition of a right ideal of a ring to be a subgroup of the additive group of the ring which is closed under right-multiplication by elements of the full ring. (Contributed by AV, 21-Mar-2025.)
LIdealopp_r Rng $/\$ SubGrp

21-Mar-2025	dflidl2rng 14902	Alternate (the usual textbook) definition of a (left) ideal of a non-unital ring to be a subgroup of the additive group of the ring which is closed under left-multiplication by elements of the full ring. (Contributed by AV, 21-Mar-2025.)
LIdeal Rng $/\$ SubGrp

21-Mar-2025	elcntr 14157	Elementhood in the center of a magma. (Contributed by SN, 21-Mar-2025.)
Cntr $/\$

20-Mar-2025	ccoslid 13645	Slot property of comp. (Contributed by Jim Kingdon, 20-Mar-2025.)
comp Slot comp $/\$ comp

20-Mar-2025	homslid 13642	Slot property of . (Contributed by Jim Kingdon, 20-Mar-2025.)
Slot $/\$

19-Mar-2025	ptex 13671	Existence of the product topology. (Contributed by Jim Kingdon, 19-Mar-2025.)


18-Mar-2025	prdsex 14256	Existence of the structure product. (Contributed by Jim Kingdon, 18-Mar-2025.)
$/\$ _s

16-Mar-2025	plycn 15954	A polynomial is a continuous function. (Contributed by Mario Carneiro, 23-Jul-2014.) Avoid ax-mulf 8303. (Revised by GG, 16-Mar-2025.)
Poly

16-Mar-2025	expcn 15761	The power function on complex numbers, for fixed exponent , is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) Avoid ax-mulf 8303. (Revised by GG, 16-Mar-2025.)
ℂ_fld

16-Mar-2025	mpomulcn 15758	Complex number multiplication is a continuous function. (Contributed by GG, 16-Mar-2025.)
ℂ_fld

16-Mar-2025	mpomulf 8317	Multiplication is an operation on complex numbers. Version of ax-mulf 8303 using maps-to notation, proved from the axioms of set theory and ax-mulcl 8278. (Contributed by GG, 16-Mar-2025.)


15-Mar-2025	lmodvscld 14726	Closure of scalar product for a left module. (Contributed by SN, 15-Mar-2025.)
Scalar

13-Mar-2025	2idlss 14935	A two-sided ideal is a subset of the base set. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 20-Feb-2025.) (Proof shortened by AV, 13-Mar-2025.)
2Ideal

13-Mar-2025	imasex 13679	Existence of the image structure. (Contributed by Jim Kingdon, 13-Mar-2025.)
$/\$ _s

11-Mar-2025	rng2idlsubgsubrng 14941	A two-sided ideal of a non-unital ring which is a subgroup of the ring is a subring of the ring. (Contributed by AV, 11-Mar-2025.)
Rng 2Ideal SubGrp SubRng

11-Mar-2025	rng2idlsubrng 14938	A two-sided ideal of a non-unital ring which is a non-unital ring is a subring of the ring. (Contributed by AV, 20-Feb-2025.) (Revised by AV, 11-Mar-2025.)
Rng 2Ideal ↾_s Rng SubRng

11-Mar-2025	rnglidlrng 14919	A (left) ideal of a non-unital ring is a non-unital ring. (Contributed by AV, 17-Feb-2020.) Generalization for non-unital rings. The assumption SubGrp is required because a left ideal of a non-unital ring does not have to be a subgroup. (Revised by AV, 11-Mar-2025.)
LIdeal ↾_s Rng $/\$ $/\$ SubGrp Rng

11-Mar-2025	rnglidlmsgrp 14918	The multiplicative group of a (left) ideal of a non-unital ring is a semigroup. (Contributed by AV, 17-Feb-2020.) Generalization for non-unital rings. The assumption is required because a left ideal of a non-unital ring does not have to be a subgroup. (Revised by AV, 11-Mar-2025.)
LIdeal ↾_s Rng $/\$ $/\$ mulGrp Smgrp

11-Mar-2025	rnglidlmmgm 14917	The multiplicative group of a (left) ideal of a non-unital ring is a magma. (Contributed by AV, 17-Feb-2020.) Generalization for non-unital rings. The assumption is required because a left ideal of a non-unital ring does not have to be a subgroup. (Revised by AV, 11-Mar-2025.)
LIdeal ↾_s Rng $/\$ $/\$ mulGrp Mgm

11-Mar-2025	imasival 13680	Value of an image structure. The is a lemma for the theorems imasbas 13681, imasplusg 13682, and imasmulr 13683 and should not be needed once they are proved. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Jim Kingdon, 11-Mar-2025.) (New usage is discouraged.)
_s

9-Mar-2025	2idlridld 14928	A two-sided ideal is a right ideal. (Contributed by Thierry Arnoux, 9-Mar-2025.)
2Ideal opp_r LIdeal

9-Mar-2025	2idllidld 14927	A two-sided ideal is a left ideal. (Contributed by Thierry Arnoux, 9-Mar-2025.)
2Ideal LIdeal

9-Mar-2025	quseccl 14089	Closure of the quotient map for a quotient group. (Contributed by Mario Carneiro, 18-Sep-2015.) (Proof shortened by AV, 9-Mar-2025.)
_s ~_QG NrmSGrp $/\$ ~_QG

9-Mar-2025	fovcl 6194	Closure law for an operation. (Contributed by NM, 19-Apr-2007.) (Proof shortened by AV, 9-Mar-2025.)
$/\$

8-Mar-2025	subgex 14032	The class of subgroups of a group is a set. (Contributed by Jim Kingdon, 8-Mar-2025.)
SubGrp

8-Mar-2025	fsuppfund 7294	A finitely supported function is a function. (Contributed by SN, 8-Mar-2025.)
finSupp

7-Mar-2025	ringrzd 14435	The zero of a unital ring is a right-absorbing element. (Contributed by SN, 7-Mar-2025.)


7-Mar-2025	ringlzd 14434	The zero of a unital ring is a left-absorbing element. (Contributed by SN, 7-Mar-2025.)


7-Mar-2025	qusecsub 14219	Two subgroup cosets are equal if and only if the difference of their representatives is a member of the subgroup. (Contributed by AV, 7-Mar-2025.)
~_QG $/\$ SubGrp $/\$ $/\$

2-Mar-2025	isassad 15095	Sufficient condition for being an associative algebra. (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by SN, 2-Mar-2025.)
Scalar $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ AssAlg

2-Mar-2025	assasca 15092	The scalars of an associative algebra form a ring. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by SN, 2-Mar-2025.)
Scalar AssAlg

2-Mar-2025	isassa 15086	The properties of an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014.) (Revised by SN, 2-Mar-2025.)
Scalar AssAlg $/\$ $/\$ $/\$

2-Mar-2025	df-assa 15083	Definition of an associative algebra. An associative algebra is a set equipped with a left-module structure on a ring, coupled with a multiplicative internal operation on the vectors of the module that is associative and distributive for the additive structure of the left-module (so giving the vectors a ring structure) and that is also bilinear under the scalar product. (Contributed by Mario Carneiro, 29-Dec-2014.) (Revised by SN, 2-Mar-2025.)
AssAlg Scalar $/\$

1-Mar-2025	quselbasg 14086	Membership in the base set of a quotient group. (Contributed by AV, 1-Mar-2025.)
~_QG _s $/\$ $/\$

28-Feb-2025	qusmulrng 14953	Value of the multiplication operation in a quotient ring of a non-unital ring. Formerly part of proof for quscrng 14954. Similar to qusmul2 14950. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 28-Feb-2025.)
~_QG _s Rng $/\$ 2Ideal $/\$ SubGrp $/\$ $/\$

28-Feb-2025	ringressid 14452	A ring restricted to its base set is a ring. It will usually be the original ring exactly, of course, but to show that needs additional conditions such as those in strressid 13478. (Contributed by Jim Kingdon, 28-Feb-2025.)
↾_s

28-Feb-2025	grpressid 13919	A group restricted to its base set is a group. It will usually be the original group exactly, of course, but to show that needs additional conditions such as those in strressid 13478. (Contributed by Jim Kingdon, 28-Feb-2025.)
↾_s

27-Feb-2025	imasringf1 14454	The image of a ring under an injection is a ring. (Contributed by AV, 27-Feb-2025.)
_s $/\$

26-Feb-2025	strext 13512	Extending the upper range of a structure. This works because when we say that a structure has components in we are not saying that every slot in that range is present, just that all the slots that are present are within that range. (Contributed by Jim Kingdon, 26-Feb-2025.)
Struct Struct

25-Feb-2025	subrngringnsg 14597	A subring is a normal subgroup. (Contributed by AV, 25-Feb-2025.)
SubRng NrmSGrp

25-Feb-2025	rngansg 14333	Every additive subgroup of a non-unital ring is normal. (Contributed by AV, 25-Feb-2025.)
Rng NrmSGrp SubGrp

25-Feb-2025	ecqusaddd 14094	Addition of equivalence classes in a quotient group. (Contributed by AV, 25-Feb-2025.)
NrmSGrp ~_QG _s $/\$ $/\$

24-Feb-2025	ecqusaddcl 14095	Closure of the addition in a quotient group. (Contributed by AV, 24-Feb-2025.)
NrmSGrp ~_QG _s $/\$ $/\$

24-Feb-2025	quseccl0g 14087	Closure of the quotient map for a quotient group. (Contributed by Mario Carneiro, 18-Sep-2015.) Generalization of quseccl 14089 for arbitrary sets . (Revised by AV, 24-Feb-2025.)
~_QG _s $/\$ $/\$

23-Feb-2025	ltlenmkv 17292	If can be expressed as holding exactly when holds and the values are not equal, then the analytic Markov's Principle applies. (To get the regular Markov's Principle, combine with neapmkv 17290). (Contributed by Jim Kingdon, 23-Feb-2025.)
$/\$ #

23-Feb-2025	neap0mkv 17291	The analytic Markov principle can be expressed either with two arbitrary real numbers, or one arbitrary number and zero. (Contributed by Jim Kingdon, 23-Feb-2025.)
# #

23-Feb-2025	qus2idrng 14946	The quotient of a non-unital ring modulo a two-sided ideal, which is a subgroup of the additive group of the non-unital ring, is a non-unital ring (qusring 14948 analog). (Contributed by AV, 23-Feb-2025.)
_s ~_QG 2Ideal Rng $/\$ $/\$ SubGrp Rng

23-Feb-2025	2idlcpblrng 14944	The coset equivalence relation for a two-sided ideal is compatible with ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015.) Generalization for non-unital rings and two-sided ideals which are subgroups of the additive group of the non-unital ring. (Revised by AV, 23-Feb-2025.)
~_QG 2Ideal Rng $/\$ $/\$ SubGrp $/\$

23-Feb-2025	lringuplu 14587	If the sum of two elements of a local ring is invertible, then at least one of the summands must be invertible. (Contributed by Jim Kingdon, 18-Feb-2025.) (Revised by SN, 23-Feb-2025.)
Unit LRing $\/$

23-Feb-2025	lringnz 14586	A local ring is a nonzero ring. (Contributed by Jim Kingdon, 20-Feb-2025.) (Revised by SN, 23-Feb-2025.)
LRing

23-Feb-2025	lringring 14585	A local ring is a ring. (Contributed by Jim Kingdon, 20-Feb-2025.) (Revised by SN, 23-Feb-2025.)
LRing

23-Feb-2025	lringnzr 14584	A local ring is a nonzero ring. (Contributed by SN, 23-Feb-2025.)
LRing NzRing

23-Feb-2025	islring 14583	The predicate "is a local ring". (Contributed by SN, 23-Feb-2025.)
Unit LRing NzRing $/\$ $\/$

23-Feb-2025	df-lring 14582	A local ring is a nonzero ring where for any two elements summing to one, at least one is invertible. Any field is a local ring; the ring of integers is an example of a ring which is not a local ring. (Contributed by Jim Kingdon, 18-Feb-2025.) (Revised by SN, 23-Feb-2025.)
LRing NzRing Unit $\/$ Unit

23-Feb-2025	01eq0ring 14580	If the zero and the identity element of a ring are the same, the ring is the zero ring. (Contributed by AV, 16-Apr-2019.) (Proof shortened by SN, 23-Feb-2025.)
$/\$

23-Feb-2025	nzrring 14574	A nonzero ring is a ring. (Contributed by Stefan O'Rear, 24-Feb-2015.) (Proof shortened by SN, 23-Feb-2025.)
NzRing

23-Feb-2025	qusrng 14341	The quotient structure of a non-unital ring is a non-unital ring (qusring2 14455 analog). (Contributed by AV, 23-Feb-2025.)
_s $/\$ $/\$ Rng Rng

23-Feb-2025	rngsubdir 14335	Ring multiplication distributes over subtraction. (subdir 8715 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) Generalization of ringsubdir 14446. (Revised by AV, 23-Feb-2025.)
Rng

23-Feb-2025	rngsubdi 14334	Ring multiplication distributes over subtraction. (subdi 8714 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) Generalization of ringsubdi 14445. (Revised by AV, 23-Feb-2025.)
Rng

23-Feb-2025	abbib 2356	Equal class abstractions require equivalent formulas, and conversely. (Contributed by NM, 25-Nov-2013.) (Revised by Mario Carneiro, 11-Aug-2016.) Remove dependency on ax-8 1557 and df-clel 2234 (by avoiding use of cleqh 2338). (Revised by BJ, 23-Jun-2019.) Definitial form. (Revised by Wolf Lammen, 23-Feb-2025.)


22-Feb-2025	imasrngf1 14340	The image of a non-unital ring under an injection is a non-unital ring. (Contributed by AV, 22-Feb-2025.)
_s $/\$ Rng Rng

22-Feb-2025	imasrng 14339	The image structure of a non-unital ring is a non-unital ring (imasring 14453 analog). (Contributed by AV, 22-Feb-2025.)
_s $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ Rng Rng

22-Feb-2025	rngmgpf 14320	Restricted functionality of the multiplicative group on non-unital rings (mgpf 14399 analog). (Contributed by AV, 22-Feb-2025.)
mulGrp RngRngSmgrp

22-Feb-2025	imasabl 14224	The image structure of an abelian group is an abelian group (imasgrp 13967 analog). (Contributed by AV, 22-Feb-2025.)
_s $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

21-Feb-2025	prdssgrpd 14275	The product of a family of semigroups is a semigroup. (Contributed by AV, 21-Feb-2025.)
_s Smgrp Smgrp

21-Feb-2025	prdsplusgsgrpcl 14274	Structure product pointwise sums are closed when the factors are semigroups. (Contributed by AV, 21-Feb-2025.)
_s Smgrp

21-Feb-2025	dftap2 7618	Tight apartness with the apartness properties from df-pap 7609 expanded. (Contributed by Jim Kingdon, 21-Feb-2025.)
TAp $/\$ $/\$ $/\$ $\/$ $/\$

20-Feb-2025	rng2idlsubg0 14943	The zero (additive identity) of a non-unital ring is an element of each two-sided ideal of the ring which is a subgroup of the ring. (Contributed by AV, 20-Feb-2025.)
Rng 2Ideal SubGrp

20-Feb-2025	rng2idlsubgnsg 14942	A two-sided ideal of a non-unital ring which is a subgroup of the ring is a normal subgroup of the ring. (Contributed by AV, 20-Feb-2025.)
Rng 2Ideal SubGrp NrmSGrp

20-Feb-2025	rng2idl0 14940	The zero (additive identity) of a non-unital ring is an element of each two-sided ideal of the ring which is a non-unital ring. (Contributed by AV, 20-Feb-2025.)
Rng 2Ideal ↾_s Rng

20-Feb-2025	rng2idlnsg 14939	A two-sided ideal of a non-unital ring which is a non-unital ring is a normal subgroup of the ring. (Contributed by AV, 20-Feb-2025.)
Rng 2Ideal ↾_s Rng NrmSGrp

20-Feb-2025	2idlelbas 14937	The base set of a two-sided ideal as structure is a left and right ideal. (Contributed by AV, 20-Feb-2025.)
2Ideal ↾_s LIdeal $/\$ LIdealopp_r

20-Feb-2025	2idlbas 14936	The base set of a two-sided ideal as structure. (Contributed by AV, 20-Feb-2025.)
2Ideal ↾_s

20-Feb-2025	2idlelb 14926	Membership in a two-sided ideal. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 20-Feb-2025.)
LIdeal opp_r LIdeal 2Ideal $/\$

20-Feb-2025	aprap 14682	The relation given by df-apr 14674 for a local ring is an apartness relation. (Contributed by Jim Kingdon, 20-Feb-2025.)
LRing #_r Ap

20-Feb-2025	setscomd 13445	Different components can be set in any order. (Contributed by Jim Kingdon, 20-Feb-2025.)
sSet sSet sSet sSet

20-Feb-2025	ifnebibdc 3686	The converse of ifbi 3661 holds if the two values are not equal. (Contributed by Thierry Arnoux, 20-Feb-2025.)
DECID $/\$ DECID $/\$

20-Feb-2025	ifnefals 3685	Deduce falsehood from a conditional operator value. (Contributed by Thierry Arnoux, 20-Feb-2025.)
$/\$

20-Feb-2025	ifnetruedc 3684	Deduce truth from a conditional operator value. (Contributed by Thierry Arnoux, 20-Feb-2025.)
DECID $/\$ $/\$

18-Feb-2025	rnglidlmcl 14901	A (left) ideal containing the zero element is closed under left-multiplication by elements of the full non-unital ring. If the ring is not a unital ring, and the ideal does not contain the zero element of the ring, then the closure cannot be proven. (Contributed by AV, 18-Feb-2025.)
LIdeal Rng $/\$ $/\$ $/\$ $/\$

17-Feb-2025	aprcotr 14681	The apartness relation given by df-apr 14674 for a local ring is cotransitive. (Contributed by Jim Kingdon, 17-Feb-2025.)
# #_r LRing # # $\/$ #

17-Feb-2025	aprsym 14680	The apartness relation given by df-apr 14674 for a ring is symmetric. (Contributed by Jim Kingdon, 17-Feb-2025.)
# #_r # #

17-Feb-2025	aprval 14675	Expand Definition df-apr 14674. (Contributed by Jim Kingdon, 17-Feb-2025.)
# #_r Unit #

17-Feb-2025	subrngpropd 14608	If two structures have the same ring components (properties), they have the same set of subrings. (Contributed by AV, 17-Feb-2025.)
$/\$ $/\$ $/\$ $/\$ SubRng SubRng

17-Feb-2025	rngm2neg 14332	Double negation of a product in a non-unital ring (mul2neg 8727 analog). (Contributed by Mario Carneiro, 4-Dec-2014.) Generalization of ringm2neg 14444. (Revised by AV, 17-Feb-2025.)
Rng

17-Feb-2025	rngmneg2 14331	Negation of a product in a non-unital ring (mulneg2 8725 analog). In contrast to ringmneg2 14443, the proof does not (and cannot) make use of the existence of a ring unity. (Contributed by AV, 17-Feb-2025.)
Rng

17-Feb-2025	rngmneg1 14330	Negation of a product in a non-unital ring (mulneg1 8724 analog). In contrast to ringmneg1 14442, the proof does not (and cannot) make use of the existence of a ring unity. (Contributed by AV, 17-Feb-2025.)
Rng

17-Feb-2025	cntzsgrpcl 14161	Centralizers are closed under the semigroup operation. (Contributed by AV, 17-Feb-2025.)
Cntz Smgrp $/\$

16-Feb-2025	aprirr 14679	The apartness relation given by df-apr 14674 for a nonzero ring is irreflexive. (Contributed by Jim Kingdon, 16-Feb-2025.)
# #_r #

16-Feb-2025	rngrz 14329	The zero of a non-unital ring is a right-absorbing element. (Contributed by FL, 31-Aug-2009.) Generalization of ringrz 14433. (Revised by AV, 16-Feb-2025.)
Rng $/\$

16-Feb-2025	rng0cl 14326	The zero element of a non-unital ring belongs to its base set. (Contributed by AV, 16-Feb-2025.)
Rng

16-Feb-2025	rngacl 14325	Closure of the addition operation of a non-unital ring. (Contributed by AV, 16-Feb-2025.)
Rng $/\$ $/\$

16-Feb-2025	rnggrp 14321	A non-unital ring is a (additive) group. (Contributed by AV, 16-Feb-2025.)
Rng

16-Feb-2025	aptap 8981	Complex apartness (as defined at df-ap 8913) is a tight apartness (as defined at df-tap 7616). (Contributed by Jim Kingdon, 16-Feb-2025.)
# TAp

15-Feb-2025	subsubrng2 14607	The set of subrings of a subring are the smaller subrings. (Contributed by AV, 15-Feb-2025.)
↾_s SubRng SubRng SubRng

15-Feb-2025	subsubrng 14606	A subring of a subring is a subring. (Contributed by AV, 15-Feb-2025.)
↾_s SubRng SubRng SubRng $/\$

15-Feb-2025	subrngin 14605	The intersection of two subrings is a subring. (Contributed by AV, 15-Feb-2025.)
SubRng $/\$ SubRng SubRng

15-Feb-2025	subrngintm 14604	The intersection of a nonempty collection of subrings is a subring. (Contributed by AV, 15-Feb-2025.)
SubRng $/\$ SubRng

15-Feb-2025	opprsubrngg 14603	Being a subring is a symmetric property. (Contributed by AV, 15-Feb-2025.)
opp_r SubRng SubRng

15-Feb-2025	issubrng2 14602	Characterize the subrings of a ring by closure properties. (Contributed by AV, 15-Feb-2025.)
Rng SubRng SubGrp $/\$

15-Feb-2025	opprrngbg 14467	A set is a non-unital ring if and only if its opposite is a non-unital ring. Bidirectional form of opprrng 14466. (Contributed by AV, 15-Feb-2025.)
opp_r Rng Rng

15-Feb-2025	opprrng 14466	An opposite non-unital ring is a non-unital ring. (Contributed by AV, 15-Feb-2025.)
opp_r Rng Rng

15-Feb-2025	rngpropd 14338	If two structures have the same base set, and the values of their group (addition) and ring (multiplication) operations are equal for all pairs of elements of the base set, one is a non-unital ring iff the other one is. (Contributed by AV, 15-Feb-2025.)
$/\$ $/\$ $/\$ $/\$ Rng Rng

15-Feb-2025	sgrppropd 13781	If two structures are sets, have the same base set, and the values of their group (addition) operations are equal for all pairs of elements of the base set, one is a semigroup iff the other one is. (Contributed by AV, 15-Feb-2025.)
$/\$ $/\$ Smgrp Smgrp

15-Feb-2025	sgrpcl 13777	Closure of the operation of a semigroup. (Contributed by AV, 15-Feb-2025.)
Smgrp $/\$ $/\$

15-Feb-2025	tapeq2 7620	Equality theorem for tight apartness predicate. (Contributed by Jim Kingdon, 15-Feb-2025.)
TAp TAp

14-Feb-2025	subrngmcl 14601	A subgroup is closed under multiplication. (Contributed by Mario Carneiro, 2-Dec-2014.) Generalization of subrgmcl 14625. (Revised by AV, 14-Feb-2025.)
SubRng $/\$ $/\$

14-Feb-2025	subrngacl 14600	A subring is closed under addition. (Contributed by AV, 14-Feb-2025.)
SubRng $/\$ $/\$

14-Feb-2025	subrng0 14599	A subring always has the same additive identity. (Contributed by AV, 14-Feb-2025.)
↾_s SubRng

14-Feb-2025	subrngbas 14598	Base set of a subring structure. (Contributed by AV, 14-Feb-2025.)
↾_s SubRng

14-Feb-2025	subrngsubg 14596	A subring is a subgroup. (Contributed by AV, 14-Feb-2025.)
SubRng SubGrp

14-Feb-2025	subrngrcl 14595	Reverse closure for a subring predicate. (Contributed by AV, 14-Feb-2025.)
SubRng Rng

14-Feb-2025	subrngrng 14594	A subring is a non-unital ring. (Contributed by AV, 14-Feb-2025.)
↾_s SubRng Rng

14-Feb-2025	subrngid 14593	Every non-unital ring is a subring of itself. (Contributed by AV, 14-Feb-2025.)
Rng SubRng

14-Feb-2025	subrngss 14592	A subring is a subset. (Contributed by AV, 14-Feb-2025.)
SubRng

14-Feb-2025	issubrng 14591	The subring of non-unital ring predicate. (Contributed by AV, 14-Feb-2025.)
SubRng Rng $/\$ ↾_s Rng $/\$

14-Feb-2025	df-subrng 14590	Define a subring of a non-unital ring as a set of elements that is a non-unital ring in its own right. In this section, a subring of a non-unital ring is simply called "subring", unless it causes any ambiguity with SubRing. (Contributed by AV, 14-Feb-2025.)
SubRng Rng ↾_s Rng

14-Feb-2025	isrngd 14336	Properties that determine a non-unital ring. (Contributed by AV, 14-Feb-2025.)
$/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ Rng

14-Feb-2025	rngdi 14323	Distributive law for the multiplication operation of a non-unital ring (left-distributivity). (Contributed by AV, 14-Feb-2025.)
Rng $/\$ $/\$ $/\$

14-Feb-2025	exmidmotap 7628	The proposition that every class has at most one tight apartness is equivalent to excluded middle. (Contributed by Jim Kingdon, 14-Feb-2025.)
EXMID TAp

14-Feb-2025	exmidapne 7627	Excluded middle implies there is only one tight apartness on any class, namely negated equality. (Contributed by Jim Kingdon, 14-Feb-2025.)
EXMID TAp $/\$ $/\$

14-Feb-2025	df-pap 7609	Apartness predicate. A relation is an apartness if it is irreflexive, symmetric, and cotransitive. (Contributed by Jim Kingdon, 14-Feb-2025.)
Ap $/\$ $/\$ $/\$ $\/$

13-Feb-2025	2idl1 14934	Every ring contains a unit two-sided ideal. (Contributed by AV, 13-Feb-2025.)
2Ideal

13-Feb-2025	2idl0 14933	Every ring contains a zero two-sided ideal. (Contributed by AV, 13-Feb-2025.)
2Ideal

13-Feb-2025	ridl1 14932	Every ring contains a unit right ideal. (Contributed by AV, 13-Feb-2025.)
LIdealopp_r

13-Feb-2025	ridl0 14931	Every ring contains a zero right ideal. (Contributed by AV, 13-Feb-2025.)
LIdealopp_r

13-Feb-2025	isridl 14925	A right ideal is a left ideal of the opposite ring. This theorem shows that this definition corresponds to the usual textbook definition of a right ideal of a ring to be a subgroup of the additive group of the ring which is closed under right-multiplication by elements of the full ring. (Contributed by AV, 13-Feb-2025.)
LIdealopp_r SubGrp $/\$

13-Feb-2025	df-apr 14674	The relation between elements whose difference is invertible, which for a local ring is an apartness relation by aprap 14682. (Contributed by Jim Kingdon, 13-Feb-2025.)
#_r $/\$ $/\$ Unit

13-Feb-2025	rngass 14322	Associative law for the multiplication operation of a non-unital ring. (Contributed by NM, 27-Aug-2011.) (Revised by AV, 13-Feb-2025.)
Rng $/\$ $/\$ $/\$

13-Feb-2025	issgrpd 13780	Deduce a semigroup from its properties. (Contributed by AV, 13-Feb-2025.)
$/\$ $/\$ $/\$ $/\$ $/\$ Smgrp

13-Feb-2025	eqab 2373	One direction of eqabb 2374. (Contributed by Wolf Lammen, 13-Feb-2025.)


12-Feb-2025	eqabb 2374	Equality of a class variable and a class abstraction (also called a class builder). Theorem 5.1 of [Quine] p. 34. This theorem shows the relationship between expressions with class abstractions and expressions with class variables. Note that abbib 2356 and its relatives are among those useful for converting theorems with class variables to equivalent theorems with wff variables, by first substituting a class abstraction for each class variable. Class variables can always be eliminated from a theorem to result in an equivalent theorem with wff variables, and vice-versa. The idea is roughly as follows. To convert a theorem with a wff variable (that has a free variable ) to a theorem with a class variable , we substitute for throughout and simplify, where is a new class variable not already in the wff. An example is the conversion of sepgi 4252 to inex1 4267 (look at the instance of sepgi 4252 that occurs in the proof of inex1 4267). Conversely, to convert a theorem with a class variable to one with , we substitute for throughout and simplify, where and are new setvar and wff variables not already in the wff. For more information on class variables, see Quine pp. 15-21 and/or Takeuti and Zaring pp. 10-13. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 12-Feb-2025.)


8-Feb-2025	rhmpsrfilem2 15157	Lemma for rhmpsr et al. (Contributed by SN, 8-Feb-2025.)
$/\$ _g

8-Feb-2025	2oneel 7623	and are two unequal elements of . (Contributed by Jim Kingdon, 8-Feb-2025.)
$/\$ $/\$

8-Feb-2025	tapeq1 7619	Equality theorem for tight apartness predicate. (Contributed by Jim Kingdon, 8-Feb-2025.)
TAp TAp

7-Feb-2025	psrgrp 15167	The ring of power series is a group. (Contributed by Mario Carneiro, 29-Dec-2014.) (Proof shortened by SN, 7-Feb-2025.)
mPwSer

7-Feb-2025	resrhm2b 14641	Restriction of the codomain of a (ring) homomorphism. resghm2b 14118 analog. (Contributed by SN, 7-Feb-2025.)
↾_s SubRing $/\$ RingHom RingHom

6-Feb-2025	zzlesq 11161	An integer is less than or equal to its square. (Contributed by BJ, 6-Feb-2025.)


6-Feb-2025	2omotap 7626	If there is at most one tight apartness on , excluded middle follows. Based on online discussions by Tom de Jong, Andrew W Swan, and Martin Escardo. (Contributed by Jim Kingdon, 6-Feb-2025.)
TAp EXMID

6-Feb-2025	2omotaplemst 7625	Lemma for 2omotap 7626. (Contributed by Jim Kingdon, 6-Feb-2025.)
TAp $/\$

6-Feb-2025	2omotaplemap 7624	Lemma for 2omotap 7626. (Contributed by Jim Kingdon, 6-Feb-2025.)
$/\$ $/\$ $/\$ TAp

6-Feb-2025	2onetap 7622	Negated equality is a tight apartness on . (Contributed by Jim Kingdon, 6-Feb-2025.)
$/\$ $/\$ TAp

5-Feb-2025	netap 7621	Negated equality on a set with decidable equality is a tight apartness. (Contributed by Jim Kingdon, 5-Feb-2025.)
DECID $/\$ $/\$ TAp

5-Feb-2025	df-tap 7616	Tight apartness predicate. A relation is a tight apartness if it is irreflexive, symmetric, cotransitive, and tight. (Contributed by Jim Kingdon, 5-Feb-2025.)
TAp Ap $/\$

1-Feb-2025	mulgnn0cld 13999	Closure of the group multiple (exponentiation) operation for a nonnegative multiplier in a monoid. Deduction associated with mulgnn0cl 13994. (Contributed by SN, 1-Feb-2025.)
._g

31-Jan-2025	0subg 14055	The zero subgroup of an arbitrary group. (Contributed by Stefan O'Rear, 10-Dec-2014.) (Proof shortened by SN, 31-Jan-2025.)
SubGrp

29-Jan-2025	grprinvd 13914	The right inverse of a group element. Deduction associated with grprinv 13909. (Contributed by SN, 29-Jan-2025.)


29-Jan-2025	grplinvd 13913	The left inverse of a group element. Deduction associated with grplinv 13908. (Contributed by SN, 29-Jan-2025.)


29-Jan-2025	grpinvcld 13907	A group element's inverse is a group element. (Contributed by SN, 29-Jan-2025.)


29-Jan-2025	grpridd 13892	The identity element of a group is a right identity. Deduction associated with grprid 13890. (Contributed by SN, 29-Jan-2025.)


29-Jan-2025	grplidd 13891	The identity element of a group is a left identity. Deduction associated with grplid 13889. (Contributed by SN, 29-Jan-2025.)


29-Jan-2025	grpassd 13870	A group operation is associative. (Contributed by SN, 29-Jan-2025.)


28-Jan-2025	dvdsrex 14489	Existence of the divisibility relation. (Contributed by Jim Kingdon, 28-Jan-2025.)
SRing _r

24-Jan-2025	reldvdsrsrg 14483	The divides relation is a relation. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Jim Kingdon, 24-Jan-2025.)
SRing _r

18-Jan-2025	rerecapb 9176	A real number has a multiplicative inverse if and only if it is apart from zero. Theorem 11.2.4 of [HoTT], p. (varies). (Contributed by Jim Kingdon, 18-Jan-2025.)
#

18-Jan-2025	recapb 9004	A complex number has a multiplicative inverse if and only if it is apart from zero. Theorem 11.2.4 of [HoTT], p. (varies), generalized from real to complex numbers. (Contributed by Jim Kingdon, 18-Jan-2025.)
#

17-Jan-2025	flddrngd 14699	A field is a division ring. (Contributed by SN, 17-Jan-2025.)
Field

17-Jan-2025	ressval3d 13479	Value of structure restriction, deduction version. (Contributed by AV, 14-Mar-2020.) (Revised by Jim Kingdon, 17-Jan-2025.)
↾_s sSet

17-Jan-2025	strressid 13478	Behavior of trivial restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.) (Revised by Jim Kingdon, 17-Jan-2025.)
Struct ↾_s

17-Jan-2025	snelpwg 4350	A singleton of a set is a member of the powerclass of a class if and only if that set is a member of that class. (Contributed by NM, 1-Apr-1998.) Put in closed form and avoid ax-nul 4259. (Revised by BJ, 17-Jan-2025.)


16-Jan-2025	ressex 13471	Existence of structure restriction. (Contributed by Jim Kingdon, 16-Jan-2025.)
$/\$ ↾_s

16-Jan-2025	ressvalsets 13470	Value of structure restriction. (Contributed by Jim Kingdon, 16-Jan-2025.)
$/\$ ↾_s sSet

15-Jan-2025	vsnex 4348	A singleton built on a setvar is a set. (Contributed by BJ, 15-Jan-2025.)


12-Jan-2025	isrim 14560	An isomorphism of rings is a bijective homomorphism. (Contributed by AV, 22-Oct-2019.) Remove sethood antecedent. (Revised by SN, 12-Jan-2025.)
RingIso RingHom $/\$

10-Jan-2025	rimrhm 14562	A ring isomorphism is a homomorphism. (Contributed by AV, 22-Oct-2019.) Remove hypotheses. (Revised by SN, 10-Jan-2025.)
RingIso RingHom

10-Jan-2025	isrim0 14552	A ring isomorphism is a homomorphism whose converse is also a homomorphism. (Contributed by AV, 22-Oct-2019.) Remove sethood antecedent. (Revised by SN, 10-Jan-2025.)
RingIso RingHom $/\$ RingHom

10-Jan-2025	opprex 14462	Existence of the opposite ring. If you know that is a ring, see opprring 14468. (Contributed by Jim Kingdon, 10-Jan-2025.)
opp_r

10-Jan-2025	mgpex 14307	Existence of the multiplication group. If is known to be a semiring, see srgmgp 14356. (Contributed by Jim Kingdon, 10-Jan-2025.)
mulGrp

6-Jan-2025	ord3 6699	Ordinal 3 is an ordinal class. (Contributed by BTernaryTau, 6-Jan-2025.)


5-Jan-2025	imbibi 252	The antecedent of one side of a biconditional can be moved out of the biconditional to become the antecedent of the remaining biconditional. (Contributed by BJ, 1-Jan-2025.) (Proof shortened by Wolf Lammen, 5-Jan-2025.)


1-Jan-2025	snss 3850	The singleton of an element of a class is a subset of the class (inference form of snssg 3849). Theorem 7.4 of [Quine] p. 49. (Contributed by NM, 21-Jun-1993.) (Proof shortened by BJ, 1-Jan-2025.)


1-Jan-2025	snssg 3849	The singleton formed on a set is included in a class if and only if the set is an element of that class. Theorem 7.4 of [Quine] p. 49. (Contributed by NM, 22-Jul-2001.) (Proof shortened by BJ, 1-Jan-2025.)


1-Jan-2025	snssb 3848	Characterization of the inclusion of a singleton in a class. (Contributed by BJ, 1-Jan-2025.)


30-Dec-2024	rex2dom 7110	A set that has at least 2 different members dominates ordinal 2. (Contributed by BTernaryTau, 30-Dec-2024.)
$/\$

23-Dec-2024	en2prd 7106	Two proper unordered pairs are equinumerous. (Contributed by BTernaryTau, 23-Dec-2024.)


11-Dec-2024	elopabr 4425	Membership in an ordered-pair class abstraction defined by a binary relation. (Contributed by AV, 16-Feb-2021.) (Proof shortened by SN, 11-Dec-2024.)


10-Dec-2024	cbvreuw 2781	Change the bound variable of a restricted unique existential quantifier using implicit substitution. Version of cbvreu 2784 with a disjoint variable condition. (Contributed by Mario Carneiro, 15-Oct-2016.) (Revised by GG, 10-Jan-2024.) (Revised by Wolf Lammen, 10-Dec-2024.)


9-Dec-2024	nninfwlpoim 7520	Decidable equality for ℕ_∞ implies the Weak Limited Principle of Omniscience (WLPO). (Contributed by Jim Kingdon, 9-Dec-2024.)
ℕ_∞ ℕ_∞ DECID WOmni

8-Dec-2024	nninfinfwlpolem 7519	Lemma for nninfinfwlpo 7521. (Contributed by Jim Kingdon, 8-Dec-2024.)
ℕ_∞ DECID DECID

8-Dec-2024	nninfwlpoimlemdc 7518	Lemma for nninfwlpoim 7520. (Contributed by Jim Kingdon, 8-Dec-2024.)
ℕ_∞ ℕ_∞ DECID DECID

8-Dec-2024	nninfwlpoimlemginf 7517	Lemma for nninfwlpoim 7520. (Contributed by Jim Kingdon, 8-Dec-2024.)


8-Dec-2024	nninfwlpoimlemg 7516	Lemma for nninfwlpoim 7520. (Contributed by Jim Kingdon, 8-Dec-2024.)
ℕ_∞

7-Dec-2024	nninfwlpor 7515	The Weak Limited Principle of Omniscience (WLPO) implies that equality for ℕ_∞ is decidable. (Contributed by Jim Kingdon, 7-Dec-2024.)
WOmni ℕ_∞ ℕ_∞ DECID

7-Dec-2024	nninfwlporlem 7514	Lemma for nninfwlpor 7515. The result. (Contributed by Jim Kingdon, 7-Dec-2024.)
WOmni DECID

7-Dec-2024	domssr 7064	If is a superset of and dominates , then also dominates . (Contributed by BTernaryTau, 7-Dec-2024.)
$/\$ $/\$

7-Dec-2024	f1dom4g 7039	The domain of a one-to-one set function is dominated by its codomain when the latter is a set. This variation of f1domg 7044 does not require the Axiom of Collection nor the Axiom of Union. (Contributed by BTernaryTau, 7-Dec-2024.)
$/\$ $/\$ $/\$

7-Dec-2024	f1oen4g 7038	The domain and range of a one-to-one, onto set function are equinumerous. This variation of f1oeng 7043 does not require the Axiom of Collection nor the Axiom of Union. (Contributed by BTernaryTau, 7-Dec-2024.)
$/\$ $/\$ $/\$

6-Dec-2024	nninfwlporlemd 7513	Given two countably infinite sequences of zeroes and ones, they are equal if and only if a sequence formed by pointwise comparing them is all ones. (Contributed by Jim Kingdon, 6-Dec-2024.)


3-Dec-2024	nninfwlpo 7522	Decidability of equality for ℕ_∞ is equivalent to the Weak Limited Principle of Omniscience (WLPO). (Contributed by Jim Kingdon, 3-Dec-2024.)
ℕ_∞ ℕ_∞ DECID WOmni

3-Dec-2024	nninfdcinf 7512	The Weak Limited Principle of Omniscience (WLPO) implies that it is decidable whether an element of ℕ_∞ equals the point at infinity. (Contributed by Jim Kingdon, 3-Dec-2024.)
WOmni ℕ_∞ DECID

29-Nov-2024	brdom2g 7031	Dominance relation. This variation of brdomg 7032 does not require the Axiom of Union. (Contributed by NM, 15-Jun-1998.) Extract from a subproof of brdomg 7032. (Revised by BTernaryTau, 29-Nov-2024.)
$/\$

28-Nov-2024	basmexd 13465	A structure whose base is inhabited is a set. (Contributed by Jim Kingdon, 28-Nov-2024.)


23-Nov-2024	fldcrngd 14700	A field is a commutative ring. (Contributed by SN, 23-Nov-2024.)
Field

22-Nov-2024	eliotaeu 5366	An inhabited iota expression has a unique value. (Contributed by Jim Kingdon, 22-Nov-2024.)


22-Nov-2024	eliota 5365	An element of an iota expression. (Contributed by Jim Kingdon, 22-Nov-2024.)
$/\$

18-Nov-2024	basmex 13464	A structure whose base is inhabited is a set. (Contributed by Jim Kingdon, 18-Nov-2024.)


14-Nov-2024	dcand 945	A conjunction of two decidable propositions is decidable. (Contributed by Jim Kingdon, 12-Apr-2018.) (Revised by BJ, 14-Nov-2024.)
DECID DECID DECID $/\$

12-Nov-2024	sravscag 14864	The scalar product operation of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Proof shortened by AV, 12-Nov-2024.)
subringAlg

12-Nov-2024	srascag 14863	The set of scalars of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Proof shortened by AV, 12-Nov-2024.)
subringAlg ↾_s Scalar

12-Nov-2024	slotsdifipndx 13582	The slot for the scalar is not the index of other slots. (Contributed by AV, 12-Nov-2024.)
$/\$ Scalar

11-Nov-2024	bj-con1st 16950	Contraposition when the antecedent is a negated stable proposition. See con1dc 868. (Contributed by BJ, 11-Nov-2024.)
STAB

11-Nov-2024	slotsdifdsndx 13632	The index of the slot for the distance is not the index of other slots. (Contributed by AV, 11-Nov-2024.)
$/\$

11-Nov-2024	plendxnocndx 13621	The slot for the orthocomplementation is not the slot for the order in an extensible structure. (Contributed by AV, 11-Nov-2024.)


11-Nov-2024	basendxnocndx 13620	The slot for the orthocomplementation is not the slot for the base set in an extensible structure. (Contributed by AV, 11-Nov-2024.)


11-Nov-2024	slotsdifplendx 13617	The index of the slot for the distance is not the index of other slots. (Contributed by AV, 11-Nov-2024.)
$/\$ TopSet

11-Nov-2024	tsetndxnstarvndx 13601	The slot for the topology is not the slot for the involution in an extensible structure. (Contributed by AV, 11-Nov-2024.)
TopSet

11-Nov-2024	ofeqd 6304	Equality theorem for function operation, deduction form. (Contributed by SN, 11-Nov-2024.)


11-Nov-2024	const 864	Contraposition when the antecedent is a negated stable proposition. See comment of condc 865. (Contributed by BJ, 18-Nov-2023.) (Proof shortened by BJ, 11-Nov-2024.)
STAB

10-Nov-2024	slotsdifunifndx 13639	The index of the slot for the uniform set is not the index of other slots. (Contributed by AV, 10-Nov-2024.)
$/\$ $/\$ $/\$ $/\$

7-Nov-2024	ressbasd 13474	Base set of a structure restriction. (Contributed by Stefan O'Rear, 26-Nov-2014.) (Proof shortened by AV, 7-Nov-2024.)
↾_s

6-Nov-2024	oppraddg 14465	Addition operation of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) (Proof shortened by AV, 6-Nov-2024.)
opp_r

6-Nov-2024	opprbasg 14464	Base set of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) (Proof shortened by AV, 6-Nov-2024.)
opp_r

6-Nov-2024	opprsllem 14463	Lemma for opprbasg 14464 and oppraddg 14465. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by AV, 6-Nov-2024.)
opp_r Slot $/\$

4-Nov-2024	lgsfvalg 16295	Value of the function which defines the Legendre symbol at the primes. (Contributed by Mario Carneiro, 4-Feb-2015.) (Revised by Jim Kingdon, 4-Nov-2024.)
$/\$ $/\$

3-Nov-2024	znmul 15061	The multiplicative structure of ℤ/nℤ is the same as the quotient ring it is based on. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) (Revised by AV, 3-Nov-2024.)
RSpanℤ_ring ℤ_ring _s ℤ_ring ~_QG ℤ/nℤ

3-Nov-2024	znadd 15060	The additive structure of ℤ/nℤ is the same as the quotient ring it is based on. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) (Revised by AV, 3-Nov-2024.)
RSpanℤ_ring ℤ_ring _s ℤ_ring ~_QG ℤ/nℤ

3-Nov-2024	znbas2 15059	The base set of ℤ/nℤ is the same as the quotient ring it is based on. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) (Revised by AV, 3-Nov-2024.)
RSpanℤ_ring ℤ_ring _s ℤ_ring ~_QG ℤ/nℤ

3-Nov-2024	znbaslemnn 15058	Lemma for znbas 15063. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by Mario Carneiro, 14-Aug-2015.) (Revised by AV, 13-Jun-2019.) (Revised by AV, 9-Sep-2021.) (Revised by AV, 3-Nov-2024.)
RSpanℤ_ring ℤ_ring _s ℤ_ring ~_QG ℤ/nℤ Slot

3-Nov-2024	zlmmulrg 15050	Ring operation of a -module (if present). (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.)
Mod

3-Nov-2024	zlmplusgg 15049	Group operation of a -module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.)
Mod

3-Nov-2024	zlmbasg 15048	Base set of a -module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.)
Mod

3-Nov-2024	zlmlemg 15047	Lemma for zlmbasg 15048 and zlmplusgg 15049. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.)
Mod Slot Scalar

2-Nov-2024	zlmsca 15051	Scalar ring of a -module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 12-Jun-2019.) (Proof shortened by AV, 2-Nov-2024.)
Mod ℤ_ring Scalar

1-Nov-2024	plendxnvscandx 13616	The slot for the "less than or equal to" ordering is not the slot for the scalar product in an extensible structure. (Contributed by AV, 1-Nov-2024.)


1-Nov-2024	plendxnscandx 13615	The slot for the "less than or equal to" ordering is not the slot for the scalar in an extensible structure. (Contributed by AV, 1-Nov-2024.)
Scalar

1-Nov-2024	plendxnmulrndx 13614	The slot for the "less than or equal to" ordering is not the slot for the ring multiplication operation in an extensible structure. (Contributed by AV, 1-Nov-2024.)


1-Nov-2024	qsqeqor 11102	The squares of two rational numbers are equal iff one number equals the other or its negative. (Contributed by Jim Kingdon, 1-Nov-2024.)
$/\$ $\/$

31-Oct-2024	dsndxnmulrndx 13629	The slot for the distance function is not the slot for the ring multiplication operation in an extensible structure. (Contributed by AV, 31-Oct-2024.)


31-Oct-2024	tsetndxnmulrndx 13600	The slot for the topology is not the slot for the ring multiplication operation in an extensible structure. (Contributed by AV, 31-Oct-2024.)
TopSet

31-Oct-2024	tsetndxnbasendx 13598	The slot for the topology is not the slot for the base set in an extensible structure. (Contributed by AV, 21-Oct-2024.) (Proof shortened by AV, 31-Oct-2024.)
TopSet

31-Oct-2024	basendxlttsetndx 13597	The index of the slot for the base set is less then the index of the slot for the topology in an extensible structure. (Contributed by AV, 31-Oct-2024.)
TopSet

31-Oct-2024	tsetndxnn 13596	The index of the slot for the group operation in an extensible structure is a positive integer. (Contributed by AV, 31-Oct-2024.)
TopSet

30-Oct-2024	basendxltedgfndx 16422	The index value of the slot is less than the index value of the .ef slot. (Contributed by AV, 21-Sep-2020.) (Proof shortened by AV, 30-Oct-2024.)
.ef

30-Oct-2024	plendxnbasendx 13612	The slot for the order is not the slot for the base set in an extensible structure. (Contributed by AV, 21-Oct-2024.) (Proof shortened by AV, 30-Oct-2024.)


30-Oct-2024	basendxltplendx 13611	The index value of the slot is less than the index value of the slot. (Contributed by AV, 30-Oct-2024.)


30-Oct-2024	plendxnn 13610	The index value of the order slot is a positive integer. This property should be ensured for every concrete coding because otherwise it could not be used in an extensible structure (slots must be positive integers). (Contributed by AV, 30-Oct-2024.)


29-Oct-2024	sradsg 14869	Distance function of a subring algebra. (Contributed by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 29-Oct-2024.)
subringAlg

29-Oct-2024	sratsetg 14866	Topology component of a subring algebra. (Contributed by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 29-Oct-2024.)
subringAlg TopSet TopSet

29-Oct-2024	sramulrg 14862	Multiplicative operation of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 29-Oct-2024.)
subringAlg

29-Oct-2024	sraaddgg 14861	Additive operation of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 29-Oct-2024.)
subringAlg

29-Oct-2024	srabaseg 14860	Base set of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 29-Oct-2024.)
subringAlg

29-Oct-2024	sralemg 14859	Lemma for srabaseg 14860 and similar theorems. (Contributed by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 29-Oct-2024.)
subringAlg Slot $/\$ Scalar

29-Oct-2024	dsndxntsetndx 13631	The slot for the distance function is not the slot for the topology in an extensible structure. (Contributed by AV, 29-Oct-2024.)
TopSet

29-Oct-2024	slotsdnscsi 13630	The slots Scalar, and are different from the slot . (Contributed by AV, 29-Oct-2024.)
Scalar $/\$ $/\$

29-Oct-2024	slotstnscsi 13602	The slots Scalar, and are different from the slot TopSet. (Contributed by AV, 29-Oct-2024.)
TopSet Scalar $/\$ TopSet $/\$ TopSet

29-Oct-2024	ipndxnmulrndx 13581	The slot for the inner product is not the slot for the ring (multiplication) operation in an extensible structure. (Contributed by AV, 29-Oct-2024.)


29-Oct-2024	ipndxnplusgndx 13580	The slot for the inner product is not the slot for the group operation in an extensible structure. (Contributed by AV, 29-Oct-2024.)


29-Oct-2024	vscandxnmulrndx 13568	The slot for the scalar product is not the slot for the ring (multiplication) operation in an extensible structure. (Contributed by AV, 29-Oct-2024.)


29-Oct-2024	scandxnmulrndx 13563	The slot for the scalar field is not the slot for the ring (multiplication) operation in an extensible structure. (Contributed by AV, 29-Oct-2024.)
Scalar

29-Oct-2024	fiubnn 11289	A finite set of natural numbers has an upper bound which is a a natural number. (Contributed by Jim Kingdon, 29-Oct-2024.)
$/\$

29-Oct-2024	fiubz 11288	A finite set of integers has an upper bound which is an integer. (Contributed by Jim Kingdon, 29-Oct-2024.)
$/\$

29-Oct-2024	fiubm 11287	Lemma for fiubz 11288 and fiubnn 11289. A general form of those theorems. (Contributed by Jim Kingdon, 29-Oct-2024.)


28-Oct-2024	edgfndxid 16421	The value of the edge function extractor is the value of the corresponding slot of the structure. (Contributed by AV, 21-Sep-2020.) (Proof shortened by AV, 28-Oct-2024.)
.ef .ef

28-Oct-2024	unifndxntsetndx 13638	The slot for the uniform set is not the slot for the topology in an extensible structure. (Contributed by AV, 28-Oct-2024.)
TopSet

28-Oct-2024	basendxltunifndx 13636	The index of the slot for the base set is less then the index of the slot for the uniform set in an extensible structure. (Contributed by AV, 28-Oct-2024.)


28-Oct-2024	unifndxnn 13635	The index of the slot for the uniform set in an extensible structure is a positive integer. (Contributed by AV, 28-Oct-2024.)


28-Oct-2024	dsndxnbasendx 13627	The slot for the distance is not the slot for the base set in an extensible structure. (Contributed by AV, 21-Oct-2024.) (Proof shortened by AV, 28-Oct-2024.)


28-Oct-2024	basendxltdsndx 13626	The index of the slot for the base set is less then the index of the slot for the distance in an extensible structure. (Contributed by AV, 28-Oct-2024.)


28-Oct-2024	dsndxnn 13625	The index of the slot for the distance in an extensible structure is a positive integer. (Contributed by AV, 28-Oct-2024.)


27-Oct-2024	bj-nnst 16942	Double negation of stability of a formula. Intuitionistic logic refutes unstability (but does not prove stability) of any formula. This theorem can also be proved in classical refutability calculus (see https://us.metamath.org/mpeuni/bj-peircestab.html) but not in minimal calculus (see https://us.metamath.org/mpeuni/bj-stabpeirce.html). See nnnotnotr 17187 for the version not using the definition of stability. (Contributed by BJ, 9-Oct-2019.) Prove it in -intuitionistic calculus with definitions (uses of ax-ia1 106, ax-ia2 107, ax-ia3 108 are via sylibr 134, necessary for definition unpackaging), and in -intuitionistic calculus, following a discussion with Jim Kingdon. (Revised by BJ, 27-Oct-2024.)
STAB

27-Oct-2024	bj-imnimnn 16937	If a formula is implied by both a formula and its negation, then it is not refutable. There is another proof using the inference associated with bj-nnclavius 16936 as its last step. (Contributed by BJ, 27-Oct-2024.)


25-Oct-2024	nnwosdc 12835	Well-ordering principle: any inhabited decidable set of positive integers has a least element (schema form). (Contributed by NM, 17-Aug-2001.) (Revised by Jim Kingdon, 25-Oct-2024.)
$/\$ DECID $/\$

23-Oct-2024	nnwodc 12832	Well-ordering principle: any inhabited decidable set of positive integers has a least element. Theorem I.37 (well-ordering principle) of [Apostol] p. 34. (Contributed by NM, 17-Aug-2001.) (Revised by Jim Kingdon, 23-Oct-2024.)
$/\$ $/\$ DECID

22-Oct-2024	uzwodc 12833	Well-ordering principle: any inhabited decidable subset of an upper set of integers has a least element. (Contributed by NM, 8-Oct-2005.) (Revised by Jim Kingdon, 22-Oct-2024.)
$/\$ $/\$ DECID

21-Oct-2024	nnnotnotr 17187	Double negation of double negation elimination. Suggested by an online post by Martin Escardo. Although this statement resembles nnexmid 862, it can be proved with reference only to implication and negation (that is, without use of disjunction). (Contributed by Jim Kingdon, 21-Oct-2024.)


21-Oct-2024	unifndxnbasendx 13637	The slot for the uniform set is not the slot for the base set in an extensible structure. (Contributed by AV, 21-Oct-2024.)


21-Oct-2024	ipndxnbasendx 13579	The slot for the inner product is not the slot for the base set in an extensible structure. (Contributed by AV, 21-Oct-2024.)


21-Oct-2024	scandxnbasendx 13561	The slot for the scalar is not the slot for the base set in an extensible structure. (Contributed by AV, 21-Oct-2024.)
Scalar

20-Oct-2024	isprm5lem 12939	Lemma for isprm5 12940. The interesting direction (showing that one only needs to check prime divisors up to the square root of ). (Contributed by Jim Kingdon, 20-Oct-2024.)


19-Oct-2024	resseqnbasd 13480	The components of an extensible structure except the base set remain unchanged on a structure restriction. (Contributed by Mario Carneiro, 26-Nov-2014.) (Revised by Mario Carneiro, 2-Dec-2014.) (Revised by AV, 19-Oct-2024.)
↾_s Slot $/\$

18-Oct-2024	rmodislmod 14772	The right module induces a left module by replacing the scalar multiplication with a reversed multiplication if the scalar ring is commutative. The hypothesis "rmodislmod.r" is a definition of a right module analogous to Definition df-lmod 14709 of a left module, see also islmod 14711. (Contributed by AV, 3-Dec-2021.) (Proof shortened by AV, 18-Oct-2024.)
Scalar $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ sSet

18-Oct-2024	mgpress 14314	Subgroup commutes with the multiplicative group operator. (Contributed by Mario Carneiro, 10-Jan-2015.) (Proof shortened by AV, 18-Oct-2024.)
↾_s mulGrp $/\$ ↾_s mulGrp

18-Oct-2024	dsndxnplusgndx 13628	The slot for the distance function is not the slot for the group operation in an extensible structure. (Contributed by AV, 18-Oct-2024.)


18-Oct-2024	plendxnplusgndx 13613	The slot for the "less than or equal to" ordering is not the slot for the group operation in an extensible structure. (Contributed by AV, 18-Oct-2024.)


18-Oct-2024	tsetndxnplusgndx 13599	The slot for the topology is not the slot for the group operation in an extensible structure. (Contributed by AV, 18-Oct-2024.)
TopSet

18-Oct-2024	vscandxnscandx 13569	The slot for the scalar product is not the slot for the scalar field in an extensible structure. (Contributed by AV, 18-Oct-2024.)
Scalar

18-Oct-2024	vscandxnplusgndx 13567	The slot for the scalar product is not the slot for the group operation in an extensible structure. (Contributed by AV, 18-Oct-2024.)


18-Oct-2024	vscandxnbasendx 13566	The slot for the scalar product is not the slot for the base set in an extensible structure. (Contributed by AV, 18-Oct-2024.)


18-Oct-2024	scandxnplusgndx 13562	The slot for the scalar field is not the slot for the group operation in an extensible structure. (Contributed by AV, 18-Oct-2024.)
Scalar

18-Oct-2024	starvndxnmulrndx 13551	The slot for the involution function is not the slot for the base set in an extensible structure. (Contributed by AV, 18-Oct-2024.)


18-Oct-2024	starvndxnplusgndx 13550	The slot for the involution function is not the slot for the base set in an extensible structure. (Contributed by AV, 18-Oct-2024.)


18-Oct-2024	starvndxnbasendx 13549	The slot for the involution function is not the slot for the base set in an extensible structure. (Contributed by AV, 18-Oct-2024.)


17-Oct-2024	basendxltplusgndx 13520	The index of the slot for the base set is less then the index of the slot for the group operation in an extensible structure. (Contributed by AV, 17-Oct-2024.)


17-Oct-2024	plusgndxnn 13518	The index of the slot for the group operation in an extensible structure is a positive integer. (Contributed by AV, 17-Oct-2024.)


17-Oct-2024	elnndc 10022	Membership of an integer in is decidable. (Contributed by Jim Kingdon, 17-Oct-2024.)
DECID

14-Oct-2024	2zinfmin 12028	Two ways to express the minimum of two integers. Because order of integers is decidable, we have more flexibility than for real numbers. (Contributed by Jim Kingdon, 14-Oct-2024.)
$/\$ inf

14-Oct-2024	mingeb 12027	Equivalence of and being equal to the minimum of two reals. (Contributed by Jim Kingdon, 14-Oct-2024.)
$/\$ inf

13-Oct-2024	edgfndxnn 16420	The index value of the edge function extractor is a positive integer. This property should be ensured for every concrete coding because otherwise it could not be used in an extensible structure (slots must be positive integers). (Contributed by AV, 21-Sep-2020.) (Proof shortened by AV, 13-Oct-2024.)
.ef

13-Oct-2024	edgfndx 16419	Index value of the df-edgf 16417 slot. (Contributed by AV, 13-Oct-2024.) (New usage is discouraged.)
.ef ;

13-Oct-2024	prdsvallem 13674	Lemma for prdsval 14257. (Contributed by Stefan O'Rear, 3-Jan-2015.) Extracted from the former proof of prdsval 14257, dependency on df-hom 13508 removed. (Revised by AV, 13-Oct-2024.)


13-Oct-2024	pcxnn0cl 13112	Extended nonnegative integer closure of the general prime count function. (Contributed by Jim Kingdon, 13-Oct-2024.)
$/\$ NN0*

13-Oct-2024	xnn0letri 10216	Dichotomy for extended nonnegative integers. (Contributed by Jim Kingdon, 13-Oct-2024.)
NN0* $/\$ NN0* $\/$

13-Oct-2024	xnn0dcle 10215	Decidability of for extended nonnegative integers. (Contributed by Jim Kingdon, 13-Oct-2024.)
NN0* $/\$ NN0* DECID

9-Oct-2024	nn0leexp2 11164	Ordering law for exponentiation. (Contributed by Jim Kingdon, 9-Oct-2024.)
$/\$ $/\$ $/\$

8-Oct-2024	pclemdc 13090	Lemma for the prime power pre-function's properties. (Contributed by Jim Kingdon, 8-Oct-2024.)
$/\$ $/\$ DECID

8-Oct-2024	elnn0dc 10021	Membership of an integer in is decidable. (Contributed by Jim Kingdon, 8-Oct-2024.)
DECID

7-Oct-2024	pclemub 13089	Lemma for the prime power pre-function's properties. (Contributed by Mario Carneiro, 23-Feb-2014.) (Revised by Jim Kingdon, 7-Oct-2024.)
$/\$ $/\$

7-Oct-2024	pclem0 13088	Lemma for the prime power pre-function's properties. (Contributed by Mario Carneiro, 23-Feb-2014.) (Revised by Jim Kingdon, 7-Oct-2024.)
$/\$ $/\$

7-Oct-2024	nn0ltexp2 11163	Special case of ltexp2 16143 which we use here because we haven't yet defined df-rpcxp 16054 which is used in the current proof of ltexp2 16143. (Contributed by Jim Kingdon, 7-Oct-2024.)
$/\$ $/\$ $/\$

6-Oct-2024	suprzcl2dc 10685	The supremum of a bounded-above decidable set of integers is a member of the set. (This theorem avoids ax-pre-suploc 8301.) (Contributed by Mario Carneiro, 21-Apr-2015.) (Revised by Jim Kingdon, 6-Oct-2024.)
DECID

5-Oct-2024	zsupssdc 10684	An inhabited decidable bounded subset of integers has a supremum in the set. (The proof does not use ax-pre-suploc 8301.) (Contributed by Mario Carneiro, 21-Apr-2015.) (Revised by Jim Kingdon, 5-Oct-2024.)
DECID $/\$

5-Oct-2024	suprzubdc 10682	The supremum of a bounded-above decidable set of integers is greater than any member of the set. (Contributed by Mario Carneiro, 21-Apr-2015.) (Revised by Jim Kingdon, 5-Oct-2024.)
DECID

3-Oct-2024	ab0w 3550	The class of sets verifying a property is the empty class if and only if that property is a contradiction. (Contributed by GG, 3-Oct-2024.)


1-Oct-2024	infex2g 7375	Existence of infimum. (Contributed by Jim Kingdon, 1-Oct-2024.)
inf

30-Sep-2024	unbendc 13397	An unbounded decidable set of positive integers is infinite. (Contributed by NM, 5-May-2005.) (Revised by Jim Kingdon, 30-Sep-2024.)
$/\$ DECID $/\$

30-Sep-2024	prmdc 12927	Primality is decidable. (Contributed by Jim Kingdon, 30-Sep-2024.)
DECID

30-Sep-2024	dcfi 7315	Decidability of a family of propositions indexed by a finite set. (Contributed by Jim Kingdon, 30-Sep-2024.)
$/\$ DECID DECID

30-Sep-2024	cbvriotavw 6049	Change bound variable in a restricted description binder. Version of cbvriotav 6051 with a disjoint variable condition. (Contributed by NM, 18-Mar-2013.) (Revised by GG, 30-Sep-2024.)


30-Sep-2024	cbviotavw 5343	Change bound variables in a description binder. Version of cbviotav 5344 with a disjoint variable condition. (Contributed by Andrew Salmon, 1-Aug-2011.) (Revised by GG, 30-Sep-2024.)


29-Sep-2024	ssnnct 13390	A decidable subset of is countable. (Contributed by Jim Kingdon, 29-Sep-2024.)
$/\$ DECID ⊔

29-Sep-2024	ssnnctlemct 13389	Lemma for ssnnct 13390. The result. (Contributed by Jim Kingdon, 29-Sep-2024.)
frec $/\$ DECID ⊔

28-Sep-2024	nninfdcex 10683	A decidable set of natural numbers has an infimum. (Contributed by Jim Kingdon, 28-Sep-2024.)
DECID $/\$

27-Sep-2024	infregelbex 10008	Any lower bound of a set of real numbers with an infimum is less than or equal to the infimum. (Contributed by Jim Kingdon, 27-Sep-2024.)
$/\$ inf

26-Sep-2024	nninfdclemp1 13393	Lemma for nninfdc 13396. Each element of the sequence is greater than the previous element. (Contributed by Jim Kingdon, 26-Sep-2024.)
DECID $/\$ inf

26-Sep-2024	nnminle 12831	The infimum of a decidable subset of the natural numbers is less than an element of the set. The infimum is also a minimum as shown at nnmindc 12830. (Contributed by Jim Kingdon, 26-Sep-2024.)
$/\$ DECID $/\$ inf

25-Sep-2024	nninfdclemcl 13391	Lemma for nninfdc 13396. (Contributed by Jim Kingdon, 25-Sep-2024.)
DECID inf

24-Sep-2024	nninfdclemlt 13394	Lemma for nninfdc 13396. The function from nninfdclemf 13392 is strictly monotonic. (Contributed by Jim Kingdon, 24-Sep-2024.)
DECID $/\$ inf

23-Sep-2024	nninfdc 13396	An unbounded decidable set of positive integers is infinite. (Contributed by Jim Kingdon, 23-Sep-2024.)
$/\$ DECID $/\$

23-Sep-2024	nninfdclemf1 13395	Lemma for nninfdc 13396. The function from nninfdclemf 13392 is one-to-one. (Contributed by Jim Kingdon, 23-Sep-2024.)
DECID $/\$ inf

23-Sep-2024	nninfdclemf 13392	Lemma for nninfdc 13396. A function from the natural numbers into . (Contributed by Jim Kingdon, 23-Sep-2024.)
DECID $/\$ inf

23-Sep-2024	nnmindc 12830	An inhabited decidable subset of the natural numbers has a minimum. (Contributed by Jim Kingdon, 23-Sep-2024.)
$/\$ DECID $/\$ inf

23-Sep-2024	breng 7029	Equinumerosity relation. This variation of bren 7030 does not require the Axiom of Union. (Contributed by NM, 15-Jun-1998.) Extract from a subproof of bren 7030. (Revised by BTernaryTau, 23-Sep-2024.)
$/\$

23-Sep-2024	dfnul3 3524	Alternate definition of the empty set. (Contributed by NM, 25-Mar-2004.) (Proof shortened by BJ, 23-Sep-2024.)


23-Sep-2024	dfnul2 3523	Alternate definition of the empty set. Definition 5.14 of [TakeutiZaring] p. 20. (Contributed by NM, 26-Dec-1996.) Reduce axiom dependencies. (Revised by Steven Nguyen, 3-May-2023.) (Proof shortened by BJ, 23-Sep-2024.)


23-Sep-2024	dfnul4 3522	Alternate definition of the empty class/set. (Contributed by BJ, 30-Nov-2019.) Avoid ax-13 2211, df-clel 2234. (Revised by GG, 3-Sep-2024.) Prove directly from definition to allow shortening dfnul2 3523. (Revised by BJ, 23-Sep-2024.)


20-Sep-2024	ineqcomi 3423	Two ways of expressing that two classes have a given intersection. Inference form of ineqcom 3422. Disjointness inference when . (Contributed by Peter Mazsa, 26-Mar-2017.) (Proof shortened by SN, 20-Sep-2024.)


19-Sep-2024	ssomct 13388	A decidable subset of is countable. (Contributed by Jim Kingdon, 19-Sep-2024.)
$/\$ DECID ⊔

19-Sep-2024	2oex 6704	is a set. (Contributed by BJ, 6-Apr-2019.) (Proof shortened by Zhi Wang, 19-Sep-2024.)


19-Sep-2024	ecase2d 1392	Deduction for elimination by cases. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Sep-2024.)
$/\$ $/\$ $\/$ $\/$

18-Sep-2024	fcof 5894	Composition of a function with domain and codomain and a function as a function with domain and codomain. Generalization of fco 5552. (Contributed by AV, 18-Sep-2024.)
$/\$

18-Sep-2024	eqabbw 2375	Version of eqabb 2374 using implicit substitution. (Contributed by GG and AV, 18-Sep-2024.)


17-Sep-2024	fncofn 5893	Composition of a function with domain and a function as a function with domain. Generalization of fnco 5491. (Contributed by AV, 17-Sep-2024.)
$/\$

14-Sep-2024	nnpredlt 4771	The predecessor (see nnpredcl 4770) of a nonzero natural number is less than (see df-iord 4511) that number. (Contributed by Jim Kingdon, 14-Sep-2024.)
$/\$

13-Sep-2024	nninfisollemeq 7473	Lemma for nninfisol 7474. The case where is a successor and and are equal. (Contributed by Jim Kingdon, 13-Sep-2024.)
ℕ_∞ DECID

13-Sep-2024	nninfisollemne 7472	Lemma for nninfisol 7474. A case where is a successor and and are not equal. (Contributed by Jim Kingdon, 13-Sep-2024.)
ℕ_∞ DECID

13-Sep-2024	nninfisollem0 7471	Lemma for nninfisol 7474. The case where is zero. (Contributed by Jim Kingdon, 13-Sep-2024.)
ℕ_∞ DECID

13-Sep-2024	fset0 6949	The set of functions from the empty set is the singleton containing the empty set. (Contributed by AV, 13-Sep-2024.)


13-Sep-2024	fsetsspwxp 6948	The class of all functions from into is a subclass of the power class of the cartesion product of and . (Contributed by AV, 13-Sep-2024.)


12-Sep-2024	nninfisol 7474	Finite elements of ℕ_∞ are isolated. That is, given a natural number and any element of ℕ_∞, it is decidable whether the natural number (when converted to an element of ℕ_∞) is equal to the given element of ℕ_∞. Stated in an online post by Martin Escardo. One way to understand this theorem is that you do not need to look at an unbounded number of elements of the sequence to decide whether it is equal to (in fact, you only need to look at two elements and tells you where to look). By contrast, the point at infinity being isolated is equivalent to the Weak Limited Principle of Omniscience (WLPO) (nninfinfwlpo 7521). (Contributed by BJ and Jim Kingdon, 12-Sep-2024.)
$/\$ ℕ_∞ DECID

8-Sep-2024	relopabv 4904	A class of ordered pairs is a relation. For a version without a disjoint variable condition, see relopab 4906. (Contributed by SN, 8-Sep-2024.)


7-Sep-2024	eulerthlemfi 13029	Lemma for eulerth 13034. The set is finite. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 7-Sep-2024.)
$/\$ $/\$ ..^

7-Sep-2024	modqexp 11119	Exponentiation property of the modulo operation, see theorem 5.2(c) in [ApostolNT] p. 107. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 7-Sep-2024.)


5-Sep-2024	eulerthlemh 13032	Lemma for eulerth 13034. A permutation of . (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 5-Sep-2024.)
$/\$ $/\$ ..^

2-Sep-2024	eulerthlemth 13033	Lemma for eulerth 13034. The result. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 2-Sep-2024.)
$/\$ $/\$ ..^

2-Sep-2024	eulerthlema 13031	Lemma for eulerth 13034. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 2-Sep-2024.)
$/\$ $/\$ ..^

2-Sep-2024	eulerthlemrprm 13030	Lemma for eulerth 13034. and are relatively prime. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 2-Sep-2024.)
$/\$ $/\$ ..^

1-Sep-2024	qusmul2 14950	Value of the ring operation in a quotient ring. (Contributed by Thierry Arnoux, 1-Sep-2024.)
_s ~_QG 2Ideal ~_QG ~_QG ~_QG

30-Aug-2024	fprodap0f 12422	A finite product of terms apart from zero is apart from zero. A version of fprodap0 12407 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) (Revised by Jim Kingdon, 30-Aug-2024.)
$/\$ $/\$ # #

28-Aug-2024	fprodrec 12415	The finite product of reciprocals is the reciprocal of the product. (Contributed by Jim Kingdon, 28-Aug-2024.)
$/\$ $/\$ #

26-Aug-2024	exmidontri2or 7603	Ordinal trichotomy is equivalent to excluded middle. (Contributed by Jim Kingdon, 26-Aug-2024.)
EXMID $\/$

26-Aug-2024	exmidontri 7599	Ordinal trichotomy is equivalent to excluded middle. (Contributed by Jim Kingdon, 26-Aug-2024.)
EXMID $\/$ $\/$

26-Aug-2024	ontri2orexmidim 4719	Ordinal trichotomy implies excluded middle. Closed form of ordtri2or2exmid 4718. (Contributed by Jim Kingdon, 26-Aug-2024.)
$\/$ DECID

26-Aug-2024	ontriexmidim 4669	Ordinal trichotomy implies excluded middle. Closed form of ordtriexmid 4668. (Contributed by Jim Kingdon, 26-Aug-2024.)
$\/$ $\/$ DECID

25-Aug-2024	onntri2or 7606	Double negated ordinal trichotomy. (Contributed by Jim Kingdon, 25-Aug-2024.)
EXMID $\/$

25-Aug-2024	onntri3or 7605	Double negated ordinal trichotomy. (Contributed by Jim Kingdon, 25-Aug-2024.)
EXMID $\/$ $\/$

25-Aug-2024	csbcow 3158	Composition law for chained substitutions into a class. Version of csbco 3157 with a disjoint variable condition, which requires fewer axioms. (Contributed by NM, 10-Nov-2005.) (Revised by GG, 25-Aug-2024.)


25-Aug-2024	cbvreuvw 2792	Version of cbvreuv 2788 with a disjoint variable condition. (Contributed by GG, 10-Jan-2024.) Reduce axiom usage. (Revised by GG, 25-Aug-2024.)


25-Aug-2024	cbvrexvw 2791	Version of cbvrexv 2787 with a disjoint variable condition. (Contributed by GG, 10-Jan-2024.) Reduce axiom usage. (Revised by GG, 25-Aug-2024.)


25-Aug-2024	cbvralvw 2790	Version of cbvralv 2786 with a disjoint variable condition. (Contributed by GG, 10-Jan-2024.) Reduce axiom usage. (Revised by GG, 25-Aug-2024.)


25-Aug-2024	cbvabw 2363	Version of cbvab 2364 with a disjoint variable condition. (Contributed by GG, 10-Jan-2024.) Reduce axiom usage. (Revised by GG, 25-Aug-2024.)


25-Aug-2024	nfsbv 2007	If is not free in , it is not free in when is distinct from and . Version of nfsb 2006 requiring more disjoint variables. (Contributed by Wolf Lammen, 7-Feb-2023.) Remove disjoint variable condition on . (Revised by Steven Nguyen, 13-Aug-2023.) Reduce axiom usage. (Revised by GG, 25-Aug-2024.)


25-Aug-2024	cbvexvw 1976	Change bound variable. See cbvexv 1974 for a version with fewer disjoint variable conditions. (Contributed by NM, 19-Apr-2017.) Avoid ax-7 1501. (Revised by GG, 25-Aug-2024.)


25-Aug-2024	cbvalvw 1975	Change bound variable. See cbvalv 1973 for a version with fewer disjoint variable conditions. (Contributed by NM, 9-Apr-2017.) Avoid ax-7 1501. (Revised by GG, 25-Aug-2024.)


25-Aug-2024	nfal 1629	If is not free in , it is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) Remove dependency on ax-4 1563. (Revised by GG, 25-Aug-2024.)


24-Aug-2024	gcdcomd 12770	The operator is commutative, deduction version. (Contributed by SN, 24-Aug-2024.)


22-Aug-2024	fsetdmprc0 6950	The set of functions with a proper class as domain is empty. (Contributed by AV, 22-Aug-2024.)


22-Aug-2024	abanssr 3502	A class abstraction with a conjunction is a subset of the class abstraction with the right conjunct only. (Contributed by AV, 7-Aug-2024.) (Proof shortened by SN, 22-Aug-2024.)
$/\$

22-Aug-2024	abanssl 3501	A class abstraction with a conjunction is a subset of the class abstraction with the left conjunct only. (Contributed by AV, 7-Aug-2024.) (Proof shortened by SN, 22-Aug-2024.)
$/\$

21-Aug-2024	dvds2addd 12615	Deduction form of dvds2add 12611. (Contributed by SN, 21-Aug-2024.)


20-Aug-2024	rspcedvdw 2936	Version of rspcedvd 2935 where the implicit substitution hypothesis does not have an antecedent, which also avoids a disjoint variable condition on . (Contributed by SN, 20-Aug-2024.)


18-Aug-2024	prdsmulr 14262	Multiplication in a structure product. (Contributed by Mario Carneiro, 11-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.)
_s

18-Aug-2024	prdsplusg 14261	Addition in a structure product. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.)
_s

18-Aug-2024	prdsbas 14260	Base set of a structure product. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.)
_s

18-Aug-2024	prdssca 14259	Scalar ring of a structure product. (Contributed by Stefan O'Rear, 5-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.)
_s Scalar

18-Aug-2024	prdsval 14257	Value of the structure product. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 7-Jan-2017.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.)
_s _g $/\$ comp Scalar TopSet comp

18-Aug-2024	df-prds 14254	Define a structure product. This can be a product of groups, rings, modules, or ordered topological fields; any unused components will have garbage in them but this is usually not relevant for the purpose of inheriting the structures present in the factors. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Thierry Arnoux, 15-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.)
_s Scalar _g TopSet $/\$ comp comp

17-Aug-2024	fprodcl2lem 12391	Finite product closure lemma. (Contributed by Scott Fenton, 14-Dec-2017.) (Revised by Jim Kingdon, 17-Aug-2024.)
$/\$ $/\$ $/\$

16-Aug-2024	fprodunsn 12390	Multiply in an additional term in a finite product. See also fprodsplitsn 12419 which is the same but with a hypothesis in place of the distinct variable condition between and . (Contributed by Jim Kingdon, 16-Aug-2024.)
$/\$

16-Aug-2024	if0ab 3641	Expression of a conditional class as a class abstraction when the False alternative is the empty class: in that case, the conditional class is the extension, in the True alternative, of the condition. (Contributed by BJ, 16-Aug-2024.)


15-Aug-2024	bj-charfundcALT 17006	Alternate proof of bj-charfundc 17005. It was expected to be much shorter since it uses bj-charfun 17004 for the main part of the proof and the rest is basic computations, but these turn out to be lengthy, maybe because of the limited library of available lemmas. (Contributed by BJ, 15-Aug-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
DECID $/\$ $/\$ $\$

15-Aug-2024	bj-charfun 17004	Properties of the characteristic function on the class of the class . (Contributed by BJ, 15-Aug-2024.)
$/\$ $\$ $\$ $/\$ $/\$ $\$

15-Aug-2024	cnstab 8976	Equality of complex numbers is stable. Stability here means as defined at df-stab 843. This theorem for real numbers is Proposition 5.2 of [BauerHanson], p. 27. (Contributed by Jim Kingdon, 1-Aug-2023.) (Proof shortened by BJ, 15-Aug-2024.)
$/\$ STAB

15-Aug-2024	subap0d 8975	Two numbers apart from each other have difference apart from zero. (Contributed by Jim Kingdon, 12-Aug-2021.) (Proof shortened by BJ, 15-Aug-2024.)
# #

15-Aug-2024	ifexd 4630	Existence of a conditional class (deduction form). (Contributed by BJ, 15-Aug-2024.)


15-Aug-2024	ifelpwun 4629	Existence of a conditional class, quantitative version (inference form). (Contributed by BJ, 15-Aug-2024.)


15-Aug-2024	ifelpwund 4628	Existence of a conditional class, quantitative version (deduction form). (Contributed by BJ, 15-Aug-2024.)


15-Aug-2024	ifelpwung 4627	Existence of a conditional class, quantitative version (closed form). (Contributed by BJ, 15-Aug-2024.)
$/\$

15-Aug-2024	ifidss 3656	A conditional class whose two alternatives are equal is included in that alternative. With excluded middle, we can prove it is equal to it. (Contributed by BJ, 15-Aug-2024.)


15-Aug-2024	ifssun 3655	A conditional class is included in the union of its two alternatives. (Contributed by BJ, 15-Aug-2024.)


14-Aug-2024	hashf1lem1 11301	Lemma for hashf1 11303. (Contributed by Mario Carneiro, 17-Apr-2015.) (Proof shortened by AV, 14-Aug-2024.)
♯ ♯ $/\$ $\$

14-Aug-2024	f1setexg 6951	The set of injections between two sets exists. (Contributed by AV, 14-Aug-2024.)
$/\$

12-Aug-2024	exmidontriimlem2 7579	Lemma for exmidontriim 7582. (Contributed by Jim Kingdon, 12-Aug-2024.)
EXMID $\/$ $\/$ $\/$

12-Aug-2024	exmidontriimlem1 7578	Lemma for exmidontriim 7582. A variation of r19.30dc 2698. (Contributed by Jim Kingdon, 12-Aug-2024.)
$\/$ $\/$ $/\$ EXMID $\/$ $\/$

11-Aug-2024	nndc 863	Double negation of decidability of a formula. Intuitionistic logic refutes the negation of decidability (but does not prove decidability) of any formula. This should not trick the reader into thinking that EXMID is provable in intuitionistic logic. Indeed, if we could quantify over formula metavariables, then generalizing nnexmid 862 over would give " DECID ", but EXMID is "DECID ", so proving EXMID would amount to proving " DECID ", which is not implied by the above theorem. Indeed, the converse of nnal 1702 does not hold. Since our system does not allow quantification over formula metavariables, we can reproduce this argument by representing formulas as subsets of , like we do in our definition of EXMID (df-exmid 4332): then, we can prove DECID but we cannot prove DECID because the converse of nnral 2540 does not hold. Actually, EXMID is not provable in intuitionistic logic since intuitionistic logic has models satisfying EXMID and noncontradiction holds (pm3.24 705). (Contributed by BJ, 9-Oct-2019.) Add explanation on non-provability of EXMID. (Revised by BJ, 11-Aug-2024.)
DECID

10-Aug-2024	exmidontriim 7582	Excluded middle implies ordinal trichotomy. Lemma 10.4.1 of [HoTT], p. (varies). The proof follows the proof from the HoTT book fairly closely. (Contributed by Jim Kingdon, 10-Aug-2024.)
EXMID $\/$ $\/$

10-Aug-2024	exmidontriimlem4 7581	Lemma for exmidontriim 7582. The induction step for the induction on . (Contributed by Jim Kingdon, 10-Aug-2024.)
EXMID $\/$ $\/$ $\/$ $\/$

10-Aug-2024	exmidontriimlem3 7580	Lemma for exmidontriim 7582. What we get to do based on induction on both and . (Contributed by Jim Kingdon, 10-Aug-2024.)
EXMID $\/$ $\/$ $\/$ $\/$ $\/$ $\/$

10-Aug-2024	nnnninf2 7468	Canonical embedding of into ℕ_∞. (Contributed by BJ, 10-Aug-2024.)
ℕ_∞

10-Aug-2024	infnninf 7465	The point at infinity in ℕ_∞ is the constant sequence equal to . Note that with our encoding of functions, that constant function can also be expressed as , as fconstmpt 4822 shows. (Contributed by Jim Kingdon, 14-Jul-2022.) Use maps-to notation. (Revised by BJ, 10-Aug-2024.)
ℕ_∞

10-Aug-2024	mapssfsetg 6946	The value of the set exponentiation is a subset of the class of functions from to . (Contributed by AV, 10-Aug-2024.)


9-Aug-2024	ss1o0el1o 7220	Reformulation of ss1o0el1 4334 using instead of . (Contributed by BJ, 9-Aug-2024.)


9-Aug-2024	pw1dc0el 7218	Another equivalent of excluded middle, which is a mere reformulation of the definition. (Contributed by BJ, 9-Aug-2024.)
EXMID DECID

9-Aug-2024	ss1o0el1 4334	A subclass of contains the empty set if and only if it equals . (Contributed by BJ and Jim Kingdon, 9-Aug-2024.)


8-Aug-2024	pw1dc1 7221	If, in the set of truth values (the powerset of 1o), equality to 1o is decidable, then excluded middle holds (and conversely). (Contributed by BJ and Jim Kingdon, 8-Aug-2024.)
EXMID DECID

8-Aug-2024	mapfset 6945	If is a set, the value of the set exponentiation is the class of all functions from to . Generalisation of mapvalg 6932 to arbitrary domains. Note that the class can only contain set-functions, as opposed to arbitrary class-functions. When is a proper class, there can be no set-functions on it, so the above class is empty (see also fsetdmprc0 6950), hence a set. In this case, both sides of the equality in this theorem are the empty set. (Contributed by AV, 8-Aug-2024.)


8-Aug-2024	fdmexb 5939	The domain of a function is a set iff the function is a set. (Contributed by AV, 8-Aug-2024.)


8-Aug-2024	fndmexb 5938	The domain of a function is a set iff the function is a set. (Contributed by AV, 8-Aug-2024.)


7-Aug-2024	psrbagaddclfi 15145	The sum of two finite bags is a finite bag. (Contributed by Mario Carneiro, 9-Jan-2015.) Shorten proof and remove a sethood antecedent. (Revised by SN, 7-Aug-2024.)
$/\$ $/\$

7-Aug-2024	psrbagfsupp 15139	Finite bags have finite support. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Revised by AV, 18-Jul-2019.) Remove a sethood antecedent. (Revised by SN, 7-Aug-2024.)
finSupp

7-Aug-2024	pw1fin 7217	Excluded middle is equivalent to the power set of being finite. (Contributed by SN and Jim Kingdon, 7-Aug-2024.)
EXMID

7-Aug-2024	mapfoss 6947	The value of the set exponentiation is a superset of the set of all functions from onto . (Contributed by AV, 7-Aug-2024.)


7-Aug-2024	elomssom 4752	A natural number ordinal is, as a set, included in the set of natural number ordinals. (Contributed by NM, 21-Jun-1998.) Extract this result from the previous proof of elnn 4753. (Revised by BJ, 7-Aug-2024.)


6-Aug-2024	bj-charfunbi 17008	In an ambient set , if membership in is stable, then it is decidable if and only if has a characteristic function. This characterization can be applied to singletons when the set has stable equality, which is the case as soon as it has a tight apartness relation. (Contributed by BJ, 6-Aug-2024.)
STAB DECID $/\$ $\$

6-Aug-2024	bj-charfunr 17007	If a class has a "weak" characteristic function on a class , then negated membership in is decidable (in other words, membership in is testable) in . The hypothesis imposes that be a set. As usual, it could be formulated as $/\$ to deal with general classes, but that extra generality would not make the theorem much more useful. The theorem would still hold if the codomain of were any class with testable equality to the point where $\$ is sent. (Contributed by BJ, 6-Aug-2024.)
$/\$ $\$ DECID

6-Aug-2024	bj-charfundc 17005	Properties of the characteristic function on the class of the class , provided membership in is decidable in . (Contributed by BJ, 6-Aug-2024.)
DECID $/\$ $/\$ $\$

6-Aug-2024	psrbagconf1o 15149	Bag complementation is a bijection on the set of bags dominated by a given bag . (Contributed by Mario Carneiro, 29-Dec-2014.) Remove a sethood antecedent. (Revised by SN, 6-Aug-2024.)


6-Aug-2024	psrbagconcl 15148	The complement of a bag is a bag. (Contributed by Mario Carneiro, 29-Dec-2014.) Remove a sethood antecedent. (Revised by SN, 6-Aug-2024.)
$/\$

6-Aug-2024	prodssdc 12375	Change the index set to a subset in an upper integer product. (Contributed by Scott Fenton, 11-Dec-2017.) (Revised by Jim Kingdon, 6-Aug-2024.)
$/\$ # $/\$ DECID $/\$ $\$ DECID

5-Aug-2024	fnmptd 17003	The maps-to notation defines a function with domain (deduction form). (Contributed by BJ, 5-Aug-2024.)
$/\$

5-Aug-2024	funmptd 17002	The maps-to notation defines a function (deduction form). Note: one should similarly prove a deduction form of funopab4 5414, then prove funmptd 17002 from it, and then prove funmpt 5415 from that: this would reduce global proof length. (Contributed by BJ, 5-Aug-2024.)


5-Aug-2024	bj-dcfal 16954	The false truth value is decidable. (Contributed by BJ, 5-Aug-2024.)
DECID

5-Aug-2024	bj-dctru 16952	The true truth value is decidable. (Contributed by BJ, 5-Aug-2024.)
DECID

5-Aug-2024	bj-stfal 16941	The false truth value is stable. (Contributed by BJ, 5-Aug-2024.)
STAB

5-Aug-2024	bj-sttru 16939	The true truth value is stable. (Contributed by BJ, 5-Aug-2024.)
STAB

5-Aug-2024	psrbagcon 15146	The analogue of the statement " implies " for finite bags. (Contributed by Mario Carneiro, 29-Dec-2014.) Remove a sethood antecedent. (Revised by SN, 5-Aug-2024.)
$/\$ $/\$ $/\$

5-Aug-2024	psrbaglecl 15144	The set of finite bags is downward-closed. (Contributed by Mario Carneiro, 29-Dec-2014.) Remove a sethood antecedent. (Revised by SN, 5-Aug-2024.)
$/\$ $/\$

5-Aug-2024	psrbaglesupp 15142	The support of a dominated bag is smaller than the dominating bag. (Contributed by Mario Carneiro, 29-Dec-2014.) Remove a sethood antecedent. (Revised by SN, 5-Aug-2024.)
$/\$ $/\$

5-Aug-2024	prod1dc 12372	Any product of one over a valid set is one. (Contributed by Scott Fenton, 7-Dec-2017.) (Revised by Jim Kingdon, 5-Aug-2024.)
$/\$ $/\$ DECID $\/$

5-Aug-2024	fcdmnn0fsuppg 9623	Version of fcdmnn0fsupp 9621 avoiding ax-coll 4246 by assuming is a set rather than its domain . (Contributed by SN, 5-Aug-2024.)
$/\$ finSupp

5-Aug-2024	fcdmnn0suppg 9622	Version of fcdmnn0supp 9620 avoiding ax-coll 4246 by assuming is a set rather than its domain . (Contributed by SN, 5-Aug-2024.)
$/\$ supp

5-Aug-2024	2ssom 6797	The ordinal 2 is included in the set of natural number ordinals. (Contributed by BJ, 5-Aug-2024.)


5-Aug-2024	suppssdc 6500	Show that the support of a function is contained in a set. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 28-May-2019.) (Proof shortened by SN, 5-Aug-2024.)
$/\$ $\$ DECID supp

5-Aug-2024	elsuppfng 6482	An element of the support of a function with a given domain. This version of elsuppfn 6483 assumes is a set rather than its domain , avoiding ax-coll 4246. (Contributed by SN, 5-Aug-2024.)
$/\$ $/\$ supp $/\$

5-Aug-2024	suppvalfng 6480	The value of the operation constructing the support of a function with a given domain. This version of suppvalfn 6481 assumes is a set rather than its domain , avoiding ax-coll 4246. (Contributed by SN, 5-Aug-2024.)
$/\$ $/\$ supp

4-Aug-2024	en3d 7055	Equinumerosity inference from an implicit one-to-one onto function. (Contributed by NM, 27-Jul-2004.) (Revised by Mario Carneiro, 12-May-2014.) (Revised by AV, 4-Aug-2024.)
$/\$

4-Aug-2024	en2d 7054	Equinumerosity inference from an implicit one-to-one onto function. (Contributed by NM, 27-Jul-2004.) (Revised by Mario Carneiro, 12-May-2014.) (Revised by AV, 4-Aug-2024.)
$/\$ $/\$

2-Aug-2024	onntri52 7604	Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
EXMID $\/$

2-Aug-2024	onntri24 7602	Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
$\/$ $\/$

2-Aug-2024	onntri45 7601	Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
$\/$ EXMID

2-Aug-2024	onntri51 7600	Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
EXMID $\/$ $\/$

2-Aug-2024	onntri13 7598	Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
$\/$ $\/$ $\/$ $\/$

2-Aug-2024	onntri35 7597	Double negated ordinal trichotomy. There are five equivalent statements: (1) $\/$ $\/$ , (2) $\/$ , (3) $\/$ $\/$ , (4) $\/$ , and (5) EXMID. That these are all equivalent is expressed by (1) implies (3) (onntri13 7598), (3) implies (5) (onntri35 7597), (5) implies (1) (onntri51 7600), (2) implies (4) (onntri24 7602), (4) implies (5) (onntri45 7601), and (5) implies (2) (onntri52 7604). Another way of stating this is that EXMID is equivalent to trichotomy, either the $\/$ $\/$ or the $\/$ form, as shown in exmidontri 7599 and exmidontri2or 7603, respectively. Thus EXMID is equivalent to (1) or (2). In addition, EXMID is equivalent to (3) by onntri3or 7605 and (4) by onntri2or 7606. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
$\/$ $\/$ EXMID

1-Aug-2024	nnral 2540	The double negation of a universal quantification implies the universal quantification of the double negation. Restricted quantifier version of nnal 1702. (Contributed by Jim Kingdon, 1-Aug-2024.)


31-Jul-2024	3nsssucpw1 7596	Negated excluded middle implies that is not a subset of the successor of the power set of . (Contributed by James E. Hanson and Jim Kingdon, 31-Jul-2024.)
EXMID

31-Jul-2024	sucpw1nss3 7595	Negated excluded middle implies that the successor of the power set of is not a subset of . (Contributed by James E. Hanson and Jim Kingdon, 31-Jul-2024.)
EXMID

30-Jul-2024	psrbagf 15138	A finite bag is a function. (Contributed by Mario Carneiro, 29-Dec-2014.) Remove a sethood antecedent. (Revised by SN, 30-Jul-2024.)


30-Jul-2024	3nelsucpw1 7594	Three is not an element of the successor of the power set of . (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.)


30-Jul-2024	sucpw1nel3 7593	The successor of the power set of is not an element of . (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.)


30-Jul-2024	sucpw1ne3 7592	Negated excluded middle implies that the successor of the power set of is not three . (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.)
EXMID

30-Jul-2024	pw1nel3 7591	Negated excluded middle implies that the power set of is not an element of . (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.)
EXMID

30-Jul-2024	pw1ne3 7590	The power set of is not three. (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.)


30-Jul-2024	pw1ne1 7589	The power set of is not one. (Contributed by Jim Kingdon, 30-Jul-2024.)


30-Jul-2024	pw1ne0 7588	The power set of is not zero. (Contributed by Jim Kingdon, 30-Jul-2024.)


30-Jul-2024	fsuppeqg 6488	Version of fsuppeq 6487 avoiding ax-coll 4246 by assuming is a set rather than its domain . (Contributed by SN, 30-Jul-2024.)
$/\$ supp $\$

29-Jul-2024	ringcld 14406	Closure of the multiplication operation of a ring. (Contributed by SN, 29-Jul-2024.)


29-Jul-2024	grpcld 13872	Closure of the operation of a group. (Contributed by SN, 29-Jul-2024.)


29-Jul-2024	pw1on 7586	The power set of is an ordinal. (Contributed by Jim Kingdon, 29-Jul-2024.)


29-Jul-2024	isfsuppd 7290	Deduction form of isfsupp 7289. (Contributed by SN, 29-Jul-2024.)
supp finSupp

28-Jul-2024	exmidpweq 7216	Excluded middle is equivalent to the power set of being . (Contributed by Jim Kingdon, 28-Jul-2024.)
EXMID

27-Jul-2024	dcapnconstALT 17284	Decidability of real number apartness implies the existence of a certain non-constant function from real numbers to integers. A proof of dcapnconst 17283 by means of dceqnconst 17282. (Contributed by Jim Kingdon, 27-Jul-2024.) (New usage is discouraged.) (Proof modification is discouraged.)
DECID # $/\$ $/\$

27-Jul-2024	reap0 17280	Real number trichotomy is equivalent to decidability of apartness from zero. (Contributed by Jim Kingdon, 27-Jul-2024.)
$\/$ $\/$ DECID #

26-Jul-2024	nconstwlpolemgt0 17286	Lemma for nconstwlpo 17288. If one of the terms of series is positive, so is the sum. (Contributed by Jim Kingdon, 26-Jul-2024.)


26-Jul-2024	nconstwlpolem0 17285	Lemma for nconstwlpo 17288. If all the terms of the series are zero, so is their sum. (Contributed by Jim Kingdon, 26-Jul-2024.)


26-Jul-2024	fvmptd4 5800	Deduction version of fvmpt 5782 (where the substitution hypothesis does not have the antecedent ). (Contributed by SN, 26-Jul-2024.)


24-Jul-2024	tridceq 17278	Real trichotomy implies decidability of real number equality. Or in other words, analytic LPO implies analytic WLPO (see trilpo 17264 and redcwlpo 17277). Thus, this is an analytic analogue to lpowlpo 7509. (Contributed by Jim Kingdon, 24-Jul-2024.)
$\/$ $\/$ DECID

24-Jul-2024	iswomni0 17273	Weak omniscience stated in terms of equality with . Like iswomninn 17272 but with zero in place of one. (Contributed by Jim Kingdon, 24-Jul-2024.)
WOmni DECID

24-Jul-2024	asclmulg 15128	Apply group multiplication to the algebra scalars. (Contributed by Thierry Arnoux, 24-Jul-2024.)
algSc Scalar ._g ._g AssAlg $/\$ $/\$

24-Jul-2024	lpowlpo 7509	LPO implies WLPO. Easy corollary of the more general omniwomnimkv 7508. There is an analogue in terms of analytic omniscience principles at tridceq 17278. (Contributed by Jim Kingdon, 24-Jul-2024.)
Omni WOmni

23-Jul-2024	nconstwlpolem 17287	Lemma for nconstwlpo 17288. (Contributed by Jim Kingdon, 23-Jul-2024.)
$/\$ $\/$

23-Jul-2024	dceqnconst 17282	Decidability of real number equality implies the existence of a certain non-constant function from real numbers to integers. Variation of Exercise 11.6(i) of [HoTT], p. (varies). See redcwlpo 17277 for more discussion of decidability of real number equality. (Contributed by BJ and Jim Kingdon, 24-Jun-2024.) (Revised by Jim Kingdon, 23-Jul-2024.)
DECID $/\$ $/\$

23-Jul-2024	redc0 17279	Two ways to express decidability of real number equality. (Contributed by Jim Kingdon, 23-Jul-2024.)
DECID DECID

23-Jul-2024	canth 6036	No set is equinumerous to its power set (Cantor's theorem), i.e., no function can map onto its power set. Compare Theorem 6B(b) of [Enderton] p. 132. (Use nex 1553 if you want the form .) (Contributed by NM, 7-Aug-1994.) (Revised by Noah R Kingdon, 23-Jul-2024.)


22-Jul-2024	nconstwlpo 17288	Existence of a certain non-constant function from reals to integers implies WOmni (the Weak Limited Principle of Omniscience or WLPO). Based on Exercise 11.6(ii) of [HoTT], p. (varies). (Contributed by BJ and Jim Kingdon, 22-Jul-2024.)
$/\$ WOmni

16-Jul-2024	unexd 4892	The union of two sets is a set. (Contributed by SN, 16-Jul-2024.)


16-Jul-2024	difexd 4277	Existence of a difference. (Contributed by SN, 16-Jul-2024.)
$\$

15-Jul-2024	fprodseq 12369	The value of a product over a nonempty finite set. (Contributed by Scott Fenton, 6-Dec-2017.) (Revised by Jim Kingdon, 15-Jul-2024.)
$/\$ $/\$

14-Jul-2024	rexbid2 2555	Formula-building rule for restricted existential quantifier (deduction form). (Contributed by BJ, 14-Jul-2024.)
$/\$ $/\$

14-Jul-2024	ralbid2 2554	Formula-building rule for restricted universal quantifier (deduction form). (Contributed by BJ, 14-Jul-2024.)


12-Jul-2024	2irrexpqap 16180	There exist real numbers and which are irrational (in the sense of being apart from any rational number) such that is rational. Statement in the Metamath book, section 1.1.5, footnote 27 on page 17, and the "constructive proof" for theorem 1.2 of [Bauer], p. 483. This is a constructive proof because it is based on two explicitly named irrational numbers and log_b , see sqrt2irrap 12979, 2logb9irrap 16179 and sqrt2cxp2logb9e3 16177. Therefore, this proof is acceptable/usable in intuitionistic logic. (Contributed by Jim Kingdon, 12-Jul-2024.)
# $/\$ # $/\$

12-Jul-2024	2logb9irrap 16179	Example for logbgcd1irrap 16172. The logarithm of nine to base two is irrational (in the sense of being apart from any rational number). (Contributed by Jim Kingdon, 12-Jul-2024.)
log_b #

12-Jul-2024	erlecpbl 13706	Translate the relation compatibility relation to a quotient set. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by AV, 12-Jul-2024.)
$/\$ $/\$ $/\$ $/\$ $/\$ $/\$

12-Jul-2024	ercpbl 13705	Translate the function compatibility relation to a quotient set. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by AV, 12-Jul-2024.)
$/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

12-Jul-2024	ercpbllemg 13704	Lemma for ercpbl 13705. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by AV, 12-Jul-2024.)


12-Jul-2024	divsfvalg 13703	Value of the function in qusval 13697. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by AV, 12-Jul-2024.)


12-Jul-2024	divsfval 13702	Value of the function in qusval 13697. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by AV, 12-Jul-2024.)


11-Jul-2024	logbgcd1irraplemexp 16170	Lemma for logbgcd1irrap 16172. Apartness of and . (Contributed by Jim Kingdon, 11-Jul-2024.)
#

11-Jul-2024	reapef 15970	Apartness and the exponential function for reals. (Contributed by Jim Kingdon, 11-Jul-2024.)
$/\$ # #

10-Jul-2024	apcxp2 16140	Apartness and real exponentiation. (Contributed by Jim Kingdon, 10-Jul-2024.)
$/\$ # $/\$ $/\$ # #

9-Jul-2024	logbgcd1irraplemap 16171	Lemma for logbgcd1irrap 16172. The result, with the rational number expressed as numerator and denominator. (Contributed by Jim Kingdon, 9-Jul-2024.)
log_b #

9-Jul-2024	apexp1 11172	Exponentiation and apartness. (Contributed by Jim Kingdon, 9-Jul-2024.)
$/\$ $/\$ # #

5-Jul-2024	logrpap0 16073	The logarithm is apart from 0 if its argument is apart from 1. (Contributed by Jim Kingdon, 5-Jul-2024.)
$/\$ # #

3-Jul-2024	rplogbval 16147	Define the value of the log_b function, the logarithm generalized to an arbitrary base, when used as infix. Most Metamath statements select variables in order of their use, but to make the order clearer we use "B" for base and "X" for the argument of the logarithm function here. (Contributed by David A. Wheeler, 21-Jan-2017.) (Revised by Jim Kingdon, 3-Jul-2024.)
$/\$ # $/\$ log_b

3-Jul-2024	logrpap0d 16074	Deduction form of logrpap0 16073. (Contributed by Jim Kingdon, 3-Jul-2024.)
# #

3-Jul-2024	logrpap0b 16072	The logarithm is apart from 0 if and only if its argument is apart from 1. (Contributed by Jim Kingdon, 3-Jul-2024.)
# #

28-Jun-2024	2o01f 17195	Mapping zero and one between and style integers. (Contributed by Jim Kingdon, 28-Jun-2024.)
frec

28-Jun-2024	012of 17194	Mapping zero and one between and style integers. (Contributed by Jim Kingdon, 28-Jun-2024.)
frec

27-Jun-2024	iooreen 17255	An open interval is equinumerous to the real numbers. (Contributed by Jim Kingdon, 27-Jun-2024.)


27-Jun-2024	iooref1o 17254	A one-to-one mapping from the real numbers onto the open unit interval. (Contributed by Jim Kingdon, 27-Jun-2024.)


25-Jun-2024	neapmkvlem 17289	Lemma for neapmkv 17290. The result, with a few hypotheses broken out for convenience. (Contributed by Jim Kingdon, 25-Jun-2024.)
$/\$ #

25-Jun-2024	ismkvnn 17275	The predicate of being Markov stated in terms of set exponentiation. (Contributed by Jim Kingdon, 25-Jun-2024.)
Markov

25-Jun-2024	ismkvnnlem 17274	Lemma for ismkvnn 17275. The result, with a hypothesis to give a name to an expression for convenience. (Contributed by Jim Kingdon, 25-Jun-2024.)
frec Markov

25-Jun-2024	enmkvlem 7502	Lemma for enmkv 7503. One direction of the biconditional. (Contributed by Jim Kingdon, 25-Jun-2024.)
Markov Markov

24-Jun-2024	neapmkv 17290	If negated equality for real numbers implies apartness, Markov's Principle follows. Exercise 11.10 of [HoTT], p. (varies). (Contributed by Jim Kingdon, 24-Jun-2024.)
# Markov

24-Jun-2024	dcapnconst 17283	Decidability of real number apartness implies the existence of a certain non-constant function from real numbers to integers. Variation of Exercise 11.6(i) of [HoTT], p. (varies). See trilpo 17264 for more discussion of decidability of real number apartness. This is a weaker form of dceqnconst 17282 and in fact this theorem can be proved using dceqnconst 17282 as shown at dcapnconstALT 17284. (Contributed by BJ and Jim Kingdon, 24-Jun-2024.)
DECID # $/\$ $/\$

24-Jun-2024	enmkv 7503	Being Markov is invariant with respect to equinumerosity. For example, this means that we can express the Markov's Principle as either Markov or Markov. The former is a better match to conventional notation in the sense that df2o3 6702 says that whereas the corresponding relationship does not exist between and . (Contributed by Jim Kingdon, 24-Jun-2024.)
Markov Markov

21-Jun-2024	redcwlpolemeq1 17276	Lemma for redcwlpo 17277. A biconditionalized version of trilpolemeq1 17261. (Contributed by Jim Kingdon, 21-Jun-2024.)


20-Jun-2024	redcwlpo 17277	Decidability of real number equality implies the Weak Limited Principle of Omniscience (WLPO). We expect that we'd need some form of countable choice to prove the converse. Here's the outline of the proof. Given an infinite sequence F of zeroes and ones, we need to show the sequence is all ones or it is not. Construct a real number A whose representation in base two consists of a zero, a decimal point, and then the numbers of the sequence. This real number will equal one if and only if the sequence is all ones (redcwlpolemeq1 17276). Therefore decidability of real number equality would imply decidability of whether the sequence is all ones. Because of this theorem, decidability of real number equality is sometimes called "analytic WLPO". WLPO is known to not be provable in IZF (and most constructive foundations), so this theorem establishes that we will be unable to prove an analogue to qdceq 10690 for real numbers. (Contributed by Jim Kingdon, 20-Jun-2024.)
DECID WOmni

20-Jun-2024	iswomninn 17272	Weak omniscience stated in terms of natural numbers. Similar to iswomnimap 7507 but it will sometimes be more convenient to use and rather than and . (Contributed by Jim Kingdon, 20-Jun-2024.)
WOmni DECID

20-Jun-2024	iswomninnlem 17271	Lemma for iswomnimap 7507. The result, with a hypothesis for convenience. (Contributed by Jim Kingdon, 20-Jun-2024.)
frec WOmni DECID

20-Jun-2024	enwomni 7511	Weak omniscience is invariant with respect to equinumerosity. For example, this means that we can express the Weak Limited Principle of Omniscience as either WOmni or WOmni. The former is a better match to conventional notation in the sense that df2o3 6702 says that whereas the corresponding relationship does not exist between and . (Contributed by Jim Kingdon, 20-Jun-2024.)
WOmni WOmni

20-Jun-2024	enwomnilem 7510	Lemma for enwomni 7511. One direction of the biconditional. (Contributed by Jim Kingdon, 20-Jun-2024.)
WOmni WOmni

19-Jun-2024	rpabscxpbnd 16141	Bound on the absolute value of a complex power. (Contributed by Mario Carneiro, 15-Sep-2014.) (Revised by Jim Kingdon, 19-Jun-2024.)


16-Jun-2024	rpcxpsqrt 16123	The exponential function with exponent exactly matches the square root function, and thus serves as a suitable generalization to other -th roots and irrational roots. (Contributed by Mario Carneiro, 2-Aug-2014.) (Revised by Jim Kingdon, 16-Jun-2024.)


16-Jun-2024	biadanid 622	Deduction associated with biadani 620. Add a conjunction to an equivalence. (Contributed by Thierry Arnoux, 16-Jun-2024.)
$/\$ $/\$ $/\$

13-Jun-2024	rpcxpadd 16104	Sum of exponents law for complex exponentiation. (Contributed by Mario Carneiro, 2-Aug-2014.) (Revised by Jim Kingdon, 13-Jun-2024.)
$/\$ $/\$

12-Jun-2024	cxpap0 16103	Complex exponentiation is apart from zero. (Contributed by Mario Carneiro, 2-Aug-2014.) (Revised by Jim Kingdon, 12-Jun-2024.)
$/\$ #

12-Jun-2024	rpcncxpcl 16101	Closure of the complex power function. (Contributed by Jim Kingdon, 12-Jun-2024.)
$/\$

12-Jun-2024	rpcxp0 16097	Value of the complex power function when the second argument is zero. (Contributed by Mario Carneiro, 2-Aug-2014.) (Revised by Jim Kingdon, 12-Jun-2024.)


12-Jun-2024	cxpexpnn 16095	Relate the complex power function to the integer power function. (Contributed by Mario Carneiro, 2-Aug-2014.) (Revised by Jim Kingdon, 12-Jun-2024.)
$/\$

12-Jun-2024	cxpexprp 16094	Relate the complex power function to the integer power function. (Contributed by Mario Carneiro, 2-Aug-2014.) (Revised by Jim Kingdon, 12-Jun-2024.)
$/\$

12-Jun-2024	rpcxpef 16093	Value of the complex power function. (Contributed by Mario Carneiro, 2-Aug-2014.) (Revised by Jim Kingdon, 12-Jun-2024.)
$/\$

12-Jun-2024	df-rpcxp 16054	Define the power function on complex numbers. Because df-relog 16053 is only defined on positive reals, this definition only allows for a base which is a positive real. (Contributed by Jim Kingdon, 12-Jun-2024.)


10-Jun-2024	trirec0xor 17266	Version of trirec0 17265 with exclusive-or. The definition of a discrete field is sometimes stated in terms of exclusive-or but as proved here, this is equivalent to inclusive-or because the two disjuncts cannot be simultaneously true. (Contributed by Jim Kingdon, 10-Jun-2024.)
$\/$ $\/$ $\/_$

10-Jun-2024	trirec0 17265	Every real number having a reciprocal or equaling zero is equivalent to real number trichotomy. This is the key part of the definition of what is known as a discrete field, so "the real numbers are a discrete field" can be taken as an equivalent way to state real trichotomy (see further discussion at trilpo 17264). (Contributed by Jim Kingdon, 10-Jun-2024.)
$\/$ $\/$ $\/$

9-Jun-2024	omniwomnimkv 7508	A set is omniscient if and only if it is weakly omniscient and Markov. The case says that LPO WLPO $/\$ MP which is a remark following Definition 2.5 of [Pierik], p. 9. (Contributed by Jim Kingdon, 9-Jun-2024.)
Omni WOmni $/\$ Markov

9-Jun-2024	iswomnimap 7507	The predicate of being weakly omniscient stated in terms of set exponentiation. (Contributed by Jim Kingdon, 9-Jun-2024.)
WOmni DECID

9-Jun-2024	iswomni 7506	The predicate of being weakly omniscient. (Contributed by Jim Kingdon, 9-Jun-2024.)
WOmni DECID

9-Jun-2024	df-womni 7505	A weakly omniscient set is one where we can decide whether a predicate (here represented by a function ) holds (is equal to ) for all elements or not. Generalization of definition 2.4 of [Pierik], p. 9. In particular, WOmni is known as the Weak Limited Principle of Omniscience (WLPO). The term WLPO is common in the literature; there appears to be no widespread term for what we are calling a weakly omniscient set. (Contributed by Jim Kingdon, 9-Jun-2024.)
WOmni DECID

1-Jun-2024	ringcmnd 14424	A ring is a commutative monoid. (Contributed by SN, 1-Jun-2024.)
CMnd

1-Jun-2024	ringabld 14423	A ring is an Abelian group. (Contributed by SN, 1-Jun-2024.)


1-Jun-2024	cmnmndd 14195	A commutative monoid is a monoid. (Contributed by SN, 1-Jun-2024.)
CMnd

1-Jun-2024	ablcmnd 14179	An Abelian group is a commutative monoid. (Contributed by SN, 1-Jun-2024.)
CMnd

1-Jun-2024	grpmndd 13871	A group is a monoid. (Contributed by SN, 1-Jun-2024.)


1-Jun-2024	fndmi 5481	The domain of a function. (Contributed by Wolf Lammen, 1-Jun-2024.)


29-May-2024	pw1nct 17204	A condition which ensures that the powerset of a singleton is not countable. The antecedent here can be referred to as the uniformity principle. Based on Mastodon posts by Andrej Bauer and Rahul Chhabra. (Contributed by Jim Kingdon, 29-May-2024.)
⊔

28-May-2024	sssneq 17203	Any two elements of a subset of a singleton are equal. (Contributed by Jim Kingdon, 28-May-2024.)


28-May-2024	fvun2d 5772	The value of a union when the argument is in the second domain, a deduction version. (Contributed by metakunt, 28-May-2024.)


28-May-2024	fvun1d 5771	The value of a union when the argument is in the first domain, a deduction version. (Contributed by metakunt, 28-May-2024.)


26-May-2024	elpwi2 4294	Membership in a power class. (Contributed by Glauco Siliprandi, 3-Mar-2021.) (Proof shortened by Wolf Lammen, 26-May-2024.)


25-May-2024	mplnegfi 15187	The negative function on multivariate polynomials. (Contributed by SN, 25-May-2024.)
mPoly

W3C HTML validation [external]