Most Recent Proofs - Intuitionistic Logic Explorer

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.

Last updated on 7-Feb-2026 at 7:09 AM ET.

Recent Additions to the Intuitionistic Logic Explorer

Date	Label	Description
Theorem
31-Jan-2026	fvmbr 5661	If a function value is inhabited, the argument is related to the function value. (Contributed by Jim Kingdon, 31-Jan-2026.)
|- ( A e. ( F ` X ) -> X F ( F ` X ) )
30-Jan-2026	elfvex 5660	If a function value is inhabited, the function value is a set. (Contributed by Jim Kingdon, 30-Jan-2026.)
|- ( A e. ( F ` B ) -> ( F ` B ) e. _V )
30-Jan-2026	reldmm 4941	A relation is inhabited iff its domain is inhabited. (Contributed by Jim Kingdon, 30-Jan-2026.)
|- ( Rel A -> ( E. x x e. A <-> E. y y e. dom A ) )
25-Jan-2026	ifp2 986	Forward direction of dfifp2dc 987. This direction does not require decidability. (Contributed by Jim Kingdon, 25-Jan-2026.)
|- (if- ( ph , ps , ch ) -> ( ( ph -> ps ) /\ ( -. ph -> ch ) ) )
25-Jan-2026	ifpdc 985	The conditional operator for propositions implies decidability. (Contributed by Jim Kingdon, 25-Jan-2026.)
|- (if- ( ph , ps , ch ) -> DECID ph )
20-Jan-2026	cats1fvd 11293	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.)
|- T = ( S ++ <" X "> )   &    |- ( ph -> S e. Word _V )   &    |- ( ph -> (♯ ` S ) = M )   &    |- ( ph -> Y e. V )   &    |- ( ph -> X e. W )   &    |- ( ph -> ( S ` N ) = Y )   &    |- ( ph -> N e. NN0 )   &    |- ( ph -> N < M )   =>    |- ( ph -> ( T ` N ) = Y )
20-Jan-2026	cats1fvnd 11292	The last symbol of a concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) (Revised by Jim Kingdon, 20-Jan-2026.)
|- T = ( S ++ <" X "> )   &    |- ( ph -> S e. Word _V )   &    |- ( ph -> X e. V )   &    |- ( ph -> (♯ ` S ) = M )   =>    |- ( ph -> ( T ` M ) = X )
19-Jan-2026	cats2catd 11296	Closure of concatenation of concatenations with singleton words. (Contributed by AV, 1-Mar-2021.) (Revised by Jim Kingdon, 19-Jan-2026.)
|- ( ph -> B e. Word _V )   &    |- ( ph -> D e. Word _V )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. W )   &    |- ( ph -> A = ( B ++ <" X "> ) )   &    |- ( ph -> C = ( <" Y "> ++ D ) )   =>    |- ( ph -> ( A ++ C ) = ( ( B ++ <" X Y "> ) ++ D ) )
19-Jan-2026	cats1catd 11295	Closure of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) (Revised by Jim Kingdon, 19-Jan-2026.)
|- T = ( S ++ <" X "> )   &    |- ( ph -> A e. Word _V )   &    |- ( ph -> S e. Word _V )   &    |- ( ph -> X e. W )   &    |- ( ph -> C = ( B ++ <" X "> ) )   &    |- ( ph -> B = ( A ++ S ) )   =>    |- ( ph -> C = ( A ++ T ) )
19-Jan-2026	cats1lend 11294	The length of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) (Revised by Jim Kingdon, 19-Jan-2026.)
|- T = ( S ++ <" X "> )   &    |- ( ph -> S e. Word _V )   &    |- ( ph -> X e. W )   &    |- (♯ ` S ) = M   &    |- ( M + 1 ) = N   =>    |- ( ph -> (♯ ` T ) = N )
18-Jan-2026	rexanaliim 2636	A transformation of restricted quantifiers and logical connectives. (Contributed by NM, 4-Sep-2005.) (Revised by Jim Kingdon, 18-Jan-2026.)
|- ( E. x e. A ( ph /\ -. ps ) -> -. A. x e. A ( ph -> ps ) )
15-Jan-2026	df-uspgren 15947	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 v (of "vertices") and an injective (one-to-one) function e (representing (indexed) "edges") into subsets of v 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 = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e -1-1-> { x e. ~P v | ( x ~~ 1o \/ x ~~ 2o ) } }
11-Jan-2026	en2prde 7362	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.)
|- ( V ~~ 2o -> E. a E. b ( a =/= b /\ V = { a , b } ) )
10-Jan-2026	pw1mapen 16321	Equinumerosity of ( ~P 1o ^m A ) and the set of subsets of A. (Contributed by Jim Kingdon, 10-Jan-2026.)
|- ( A e. V -> ( ~P 1o ^m A ) ~~ ~P A )
10-Jan-2026	pw1if 7406	Expressing a truth value in terms of an if expression. (Contributed by Jim Kingdon, 10-Jan-2026.)
|- ( A e. ~P 1o -> if ( A = 1o , 1o , (/) ) = A )
10-Jan-2026	pw1m 7405	A truth value which is inhabited is equal to true. This is a variation of pwntru 4282 and pwtrufal 16322. (Contributed by Jim Kingdon, 10-Jan-2026.)
|- ( ( A e. ~P 1o /\ E. x x e. A ) -> A = 1o )
10-Jan-2026	1ndom2 7022	Two is not dominated by one. (Contributed by Jim Kingdon, 10-Jan-2026.)
|- -. 2o ~<_ 1o
9-Jan-2026	pw1map 16320	Mapping between ( ~P 1o ^m A ) and subsets of A. (Contributed by Jim Kingdon, 9-Jan-2026.)
|- F = ( s e. ( ~P 1o ^m A ) |-> { z e. A | ( s ` z ) = 1o } )   =>    |- ( A e. V -> F : ( ~P 1o ^m A ) -1-1-onto-> ~P A )
9-Jan-2026	iftrueb01 7404	Using an if expression to represent a truth value by (/) or 1o. Unlike some theorems using if, ph does not need to be decidable. (Contributed by Jim Kingdon, 9-Jan-2026.)
|- ( if ( ph , 1o , (/) ) = 1o <-> ph )
8-Jan-2026	pfxclz 11206	Closure of the prefix extractor. This extends pfxclg 11205 from NN0 to ZZ (negative lengths are trivial, resulting in the empty word). (Contributed by Jim Kingdon, 8-Jan-2026.)
|- ( ( S e. Word A /\ L e. ZZ ) -> ( S prefix L ) e. Word A )
8-Jan-2026	fnpfx 11204	The domain of the prefix extractor. (Contributed by Jim Kingdon, 8-Jan-2026.)
|- prefix Fn ( _V X. NN0 )
7-Jan-2026	pr1or2 7363	An unordered pair, with decidable equality for the specified elements, has either one or two elements. (Contributed by Jim Kingdon, 7-Jan-2026.)
|- ( ( A e. C /\ B e. D /\ DECID A = B ) -> ( { A , B } ~~ 1o \/ { A , B } ~~ 2o ) )
6-Jan-2026	upgr1elem1 15914	Lemma for upgr1edc 15915. (Contributed by AV, 16-Oct-2020.) (Revised by Jim Kingdon, 6-Jan-2026.)
|- ( ph -> { B , C } e. S )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   &    |- ( ph -> DECID B = C )   =>    |- ( ph -> { { B , C } } C_ { x e. S | ( x ~~ 1o \/ x ~~ 2o ) } )
3-Jan-2026	dom1o 16314	Two ways of saying that a set is inhabited. (Contributed by Jim Kingdon, 3-Jan-2026.)
|- ( A e. V -> ( 1o ~<_ A <-> E. j j e. A ) )
3-Jan-2026	df-umgren 15888	Define the class of all undirected multigraphs. An (undirected) multigraph consists of a set v (of "vertices") and a function e (representing indexed "edges") into subsets of v 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 = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { x e. ~P v | x ~~ 2o } }
3-Jan-2026	df-upgren 15887	Define the class of all undirected pseudographs. An (undirected) pseudograph consists of a set v (of "vertices") and a function e (representing indexed "edges") into subsets of v 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 15888). (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 24-Nov-2020.) (Revised by Jim Kingdon, 3-Jan-2026.)
|- UPGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { x e. ~P v | ( x ~~ 1o \/ x ~~ 2o ) } }
3-Jan-2026	en2m 6972	A set with two elements is inhabited. (Contributed by Jim Kingdon, 3-Jan-2026.)
|- ( A ~~ 2o -> E. x x e. A )
3-Jan-2026	en1m 6955	A set with one element is inhabited. (Contributed by Jim Kingdon, 3-Jan-2026.)
|- ( A ~~ 1o -> E. x x e. A )
31-Dec-2025	pw0ss 15877	There are no inhabited subsets of the empty set. (Contributed by Jim Kingdon, 31-Dec-2025.)
|- { s e. ~P (/) | E. j j e. s } = (/)
31-Dec-2025	df-ushgrm 15864	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 e is an injective (one-to-one) function into subsets of the set of vertices v, 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 = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e -1-1-> { s e. ~P v | E. j j e. s } }
29-Dec-2025	df-uhgrm 15863	Define the class of all undirected hypergraphs. An undirected hypergraph consists of a set v (of "vertices") and a function e (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 = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e --> { s e. ~P v | E. j j e. s } }
29-Dec-2025	iedgex 15814	Applying the indexed edge function yields a set. (Contributed by Jim Kingdon, 29-Dec-2025.)
|- ( G e. V -> (iEdg ` G ) e. _V )
29-Dec-2025	vtxex 15813	Applying the vertex function yields a set. (Contributed by Jim Kingdon, 29-Dec-2025.)
|- ( G e. V -> (Vtx ` G ) e. _V )
29-Dec-2025	snmb 3787	A singleton is inhabited iff its argument is a set. (Contributed by Scott Fenton, 8-May-2018.) (Revised by Jim Kingdon, 29-Dec-2025.)
|- ( A e. _V <-> E. x x e. { A } )
27-Dec-2025	lswex 11118	Existence of the last symbol. The last symbol of a word is a set. See lsw0g 11115 or lswcl 11117 if you want more specific results for empty or nonempty words, respectively. (Contributed by Jim Kingdon, 27-Dec-2025.)
|- ( W e. Word V -> (lastS ` W ) e. _V )
23-Dec-2025	fzowrddc 11174	Decidability of whether a range of integers is a subset of a word's domain. (Contributed by Jim Kingdon, 23-Dec-2025.)
|- ( ( S e. Word A /\ F e. ZZ /\ L e. ZZ ) -> DECID ( F..^ L ) C_ dom S )
19-Dec-2025	ccatclab 11124	The concatenation of words over two sets is a word over the union of those sets. (Contributed by Jim Kingdon, 19-Dec-2025.)
|- ( ( S e. Word A /\ T e. Word B ) -> ( S ++ T ) e. Word ( A u. B ) )
18-Dec-2025	lswwrd 11113	Extract the last symbol of a word. (Contributed by Alexander van der Vekens, 18-Mar-2018.) (Revised by Jim Kingdon, 18-Dec-2025.)
|- ( W e. Word V -> (lastS ` W ) = ( W ` ( (♯ ` W ) - 1 ) ) )
14-Dec-2025	2strstrndx 13146	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.)
|- G = { <. ( Base ` ndx ) , B >. , <. N , .+ >. }   &    |- ( Base ` ndx ) < N   &    |- N e. NN   =>    |- ( ( B e. V /\ .+ e. W ) -> G Struct <. ( Base ` ndx ) , N >. )
12-Dec-2025	funiedgdm2vald 15827	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.)
|- A e. _V   &    |- B e. _V   &    |- ( ph -> G e. X )   &    |- ( ph -> Fun ( G \ { (/) } ) )   &    |- ( ph -> A =/= B )   &    |- ( ph -> { A , B } C_ dom G )   =>    |- ( ph -> (iEdg ` G ) = (.ef ` G ) )
11-Dec-2025	funvtxdm2vald 15826	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.)
|- A e. _V   &    |- B e. _V   &    |- ( ph -> G e. X )   &    |- ( ph -> Fun ( G \ { (/) } ) )   &    |- ( ph -> A =/= B )   &    |- ( ph -> { A , B } C_ dom G )   =>    |- ( ph -> (Vtx ` G ) = ( Base ` G ) )
11-Dec-2025	funiedgdm2domval 15825	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.)
|- ( ( G e. V /\ Fun ( G \ { (/) } ) /\ 2o ~<_ dom G ) -> (iEdg ` G ) = (.ef ` G ) )
11-Dec-2025	funvtxdm2domval 15824	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.)
|- ( ( G e. V /\ Fun ( G \ { (/) } ) /\ 2o ~<_ dom G ) -> (Vtx ` G ) = ( Base ` G ) )
4-Dec-2025	hash2en 11060	Two equivalent ways to say a set has two elements. (Contributed by Jim Kingdon, 4-Dec-2025.)
|- ( V ~~ 2o <-> ( V e. Fin /\ (♯ ` V ) = 2 ) )
30-Nov-2025	nninfnfiinf 16348	An element of ℕ∞ which is not finite is infinite. (Contributed by Jim Kingdon, 30-Nov-2025.)
|- ( ( A e. ℕ∞ /\ -. E. n e. om A = ( i e. om |-> if ( i e. n , 1o , (/) ) ) ) -> A = ( i e. om |-> 1o ) )
27-Nov-2025	psrelbasfi 14634	Simpler form of psrelbas 14633 when the index set is finite. (Contributed by Jim Kingdon, 27-Nov-2025.)
|- S = ( I mPwSer R )   &    |- K = ( Base ` R )   &    |- ( ph -> I e. Fin )   &    |- B = ( Base ` S )   &    |- ( ph -> X e. B )   =>    |- ( ph -> X : ( NN0 ^m I ) --> K )
26-Nov-2025	mplsubgfileminv 14658	Lemma for mplsubgfi 14659. The additive inverse of a polynomial is a polynomial. (Contributed by Jim Kingdon, 26-Nov-2025.)
|- S = ( I mPwSer R )   &    |- P = ( I mPoly R )   &    |- U = ( Base ` P )   &    |- ( ph -> I e. Fin )   &    |- ( ph -> R e. Grp )   &    |- ( ph -> X e. U )   &    |- N = ( invg ` S )   =>    |- ( ph -> ( N ` X ) e. U )
26-Nov-2025	mplsubgfilemcl 14657	Lemma for mplsubgfi 14659. The sum of two polynomials is a polynomial. (Contributed by Jim Kingdon, 26-Nov-2025.)
|- S = ( I mPwSer R )   &    |- P = ( I mPoly R )   &    |- U = ( Base ` P )   &    |- ( ph -> I e. Fin )   &    |- ( ph -> R e. Grp )   &    |- ( ph -> X e. U )   &    |- ( ph -> Y e. U )   &    |- .+ = ( +g ` S )   =>    |- ( ph -> ( X .+ Y ) e. U )
25-Nov-2025	nninfinfwlpo 7343	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 7296). (Contributed by Jim Kingdon, 25-Nov-2025.)
|- ( A. x e. ℕ∞ DECID x = ( i e. om |-> 1o ) <-> om e. WOmni )
23-Nov-2025	psrbagfi 14631	A finite index set gives a simpler expression for finite bags. (Contributed by Jim Kingdon, 23-Nov-2025.)
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   =>    |- ( I e. Fin -> D = ( NN0 ^m I ) )
22-Nov-2025	df-acnm 7348	Define a local and length-limited version of the axiom of choice. The definition of the predicate X e. AC A is that for all families of inhabited subsets of X indexed on A (i.e. functions A --> { z e. ~P X | E. j j e. z }), 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 A = { x | ( A e. _V /\ A. f e. ( { z e. ~P x | E. j j e. z } ^m A ) E. g A. y e. A ( g ` y ) e. ( f ` y ) ) }
21-Nov-2025	mplsubgfilemm 14656	Lemma for mplsubgfi 14659. There exists a polynomial. (Contributed by Jim Kingdon, 21-Nov-2025.)
|- S = ( I mPwSer R )   &    |- P = ( I mPoly R )   &    |- U = ( Base ` P )   &    |- ( ph -> I e. Fin )   &    |- ( ph -> R e. Grp )   =>    |- ( ph -> E. j j e. U )
14-Nov-2025	2omapen 16319	Equinumerosity of ( 2o ^m A ) and the set of decidable subsets of A. (Contributed by Jim Kingdon, 14-Nov-2025.)
|- ( A e. V -> ( 2o ^m A ) ~~ { x e. ~P A | A. y e. A DECID y e. x } )
12-Nov-2025	2omap 16318	Mapping between ( 2o ^m A ) and decidable subsets of A. (Contributed by Jim Kingdon, 12-Nov-2025.)
|- F = ( s e. ( 2o ^m A ) |-> { z e. A | ( s ` z ) = 1o } )   =>    |- ( A e. V -> F : ( 2o ^m A ) -1-1-onto-> { x e. ~P A | A. y e. A DECID y e. x } )
11-Nov-2025	domomsubct 16326	A set dominated by om is subcountable. (Contributed by Jim Kingdon, 11-Nov-2025.)
|- ( A ~<_ om -> E. s ( s C_ om /\ E. f f : s -onto-> A ) )
10-Nov-2025	prdsbaslemss 13302	Lemma for prdsbas 13304 and similar theorems. (Contributed by Jim Kingdon, 10-Nov-2025.)
|- P = ( S X_s R )   &    |- ( ph -> S e. V )   &    |- ( ph -> R e. W )   &    |- A = ( E ` P )   &    |- E = Slot ( E ` ndx )   &    |- ( E ` ndx ) e. NN   &    |- ( ph -> T e. X )   &    |- ( ph -> { <. ( E ` ndx ) , T >. } C_ P )   =>    |- ( ph -> A = T )
5-Nov-2025	fnmpl 14651	mPoly has universal domain. (Contributed by Jim Kingdon, 5-Nov-2025.)
|- mPoly Fn ( _V X. _V )
4-Nov-2025	mplelbascoe 14650	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.)
|- P = ( I mPoly R )   &    |- S = ( I mPwSer R )   &    |- B = ( Base ` S )   &    |- .0. = ( 0g ` R )   &    |- U = ( Base ` P )   =>    |- ( ( I e. V /\ R e. W ) -> ( X e. U <-> ( X e. B /\ E. a e. ( NN0 ^m I ) A. b e. ( NN0 ^m I ) ( A. k e. I ( a ` k ) < ( b ` k ) -> ( X ` b ) = .0. ) ) ) )
4-Nov-2025	mplbascoe 14649	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.)
|- P = ( I mPoly R )   &    |- S = ( I mPwSer R )   &    |- B = ( Base ` S )   &    |- .0. = ( 0g ` R )   &    |- U = ( Base ` P )   =>    |- ( ( I e. V /\ R e. W ) -> U = { f e. B | E. a e. ( NN0 ^m I ) A. b e. ( NN0 ^m I ) ( A. k e. I ( a ` k ) < ( b ` k ) -> ( f ` b ) = .0. ) } )
4-Nov-2025	mplvalcoe 14648	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.)
|- P = ( I mPoly R )   &    |- S = ( I mPwSer R )   &    |- B = ( Base ` S )   &    |- .0. = ( 0g ` R )   &    |- U = { f e. B | E. a e. ( NN0 ^m I ) A. b e. ( NN0 ^m I ) ( A. k e. I ( a ` k ) < ( b ` k ) -> ( f ` b ) = .0. ) }   =>    |- ( ( I e. V /\ R e. W ) -> P = ( S ↾s U ) )
1-Nov-2025	ficardon 7357	The cardinal number of a finite set is an ordinal. (Contributed by Jim Kingdon, 1-Nov-2025.)
|- ( A e. Fin -> ( card ` A ) e. On )
31-Oct-2025	bitsdc 12453	Whether a bit is set is decidable. (Contributed by Jim Kingdon, 31-Oct-2025.)
|- ( ( N e. ZZ /\ M e. NN0 ) -> DECID M e. (bits ` N ) )
28-Oct-2025	nn0maxcl 11731	The maximum of two nonnegative integers is a nonnegative integer. (Contributed by Jim Kingdon, 28-Oct-2025.)
|- ( ( A e. NN0 /\ B e. NN0 ) -> sup ( { A , B } , RR , < ) e. NN0 )
28-Oct-2025	qdcle 10461	Rational <_ is decidable. (Contributed by Jim Kingdon, 28-Oct-2025.)
|- ( ( A e. QQ /\ B e. QQ ) -> DECID A <_ B )
17-Oct-2025	plycoeid3 15425	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.)
|- ( ph -> D e. NN0 )   &    |- ( ph -> A : NN0 --> CC )   &    |- ( ph -> ( A " ( ZZ>= ` ( D + 1 ) ) ) = { 0 } )   &    |- ( ph -> F = ( z e. CC |-> sum_ k e. ( 0 ... D ) ( ( A ` k ) x. ( z ^ k ) ) ) )   &    |- ( ph -> M e. ( ZZ>= ` D ) )   &    |- ( ph -> X e. CC )   =>    |- ( ph -> ( F ` X ) = sum_ j e. ( 0 ... M ) ( ( A ` j ) x. ( X ^ j ) ) )
13-Oct-2025	tpfidceq 7088	A triple is finite if it consists of elements of a class with decidable equality. (Contributed by Jim Kingdon, 13-Oct-2025.)
|- ( ph -> A e. D )   &    |- ( ph -> B e. D )   &    |- ( ph -> C e. D )   &    |- ( ph -> A. x e. D A. y e. D DECID x = y )   =>    |- ( ph -> { A , B , C } e. Fin )
13-Oct-2025	prfidceq 7086	A pair is finite if it consists of elements of a class with decidable equality. (Contributed by Jim Kingdon, 13-Oct-2025.)
|- ( ph -> A e. C )   &    |- ( ph -> B e. C )   &    |- ( ph -> A. x e. C A. y e. C DECID x = y )   =>    |- ( ph -> { A , B } e. Fin )
13-Oct-2025	dcun 3601	The union of two decidable classes is decidable. (Contributed by Jim Kingdon, 5-Oct-2022.) (Revised by Jim Kingdon, 13-Oct-2025.)
|- ( ph -> DECID C e. A )   &    |- ( ph -> DECID C e. B )   =>    |- ( ph -> DECID C e. ( A u. B ) )
9-Oct-2025	dvdsfi 12756	A natural number has finitely many divisors. (Contributed by Jim Kingdon, 9-Oct-2025.)
|- ( N e. NN -> { x e. NN | x || N } e. Fin )
7-Oct-2025	df-mplcoe 14622	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 i, the coefficients are in ring r, 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 r). (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by AV, 25-Jun-2019.) (Revised by Jim Kingdon, 7-Oct-2025.)
|- mPoly = ( i e. _V , r e. _V |-> [_ ( i mPwSer r ) / w ]_ ( w ↾s { f e. ( Base ` w ) | E. a e. ( NN0 ^m i ) A. b e. ( NN0 ^m i ) ( A. k e. i ( a ` k ) < ( b ` k ) -> ( f ` b ) = ( 0g ` r ) ) } ) )
6-Oct-2025	dvconstss 15366	Derivative of a constant function defined on an open set. (Contributed by Jim Kingdon, 6-Oct-2025.)
|- ( ph -> S e. { RR , CC } )   &    |- J = ( K ↾t S )   &    |- K = ( MetOpen ` ( abs o. - ) )   &    |- ( ph -> X e. J )   &    |- ( ph -> A e. CC )   =>    |- ( ph -> ( S _D ( X X. { A } ) ) = ( X X. { 0 } ) )
6-Oct-2025	dcfrompeirce 1492	The decidability of a proposition ch 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 919), 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.)
|- ( ph <-> ( ch \/ -. ch ) )   &    |- ( ps <-> F. )   &    |- ( ( ( ph -> ps ) -> ph ) -> ph )   =>    |- DECID ch
6-Oct-2025	dcfromcon 1491	The decidability of a proposition ch 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 858), 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.)
|- ( ph <-> ( ch \/ -. ch ) )   &    |- ( ps <-> T. )   &    |- ( ( -. ph -> -. ps ) -> ( ps -> ph ) )   =>    |- DECID ch
6-Oct-2025	dcfromnotnotr 1490	The decidability of a proposition ps 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 848), 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.)
|- ( ph <-> ( ps \/ -. ps ) )   &    |- ( -. -. ph -> ph )   =>    |- DECID ps
3-Oct-2025	dvidre 15365	Real derivative of the identity function. (Contributed by Jim Kingdon, 3-Oct-2025.)
|- ( RR _D ( _I |` RR ) ) = ( RR X. { 1 } )
3-Oct-2025	dvconstre 15364	Real derivative of a constant function. (Contributed by Jim Kingdon, 3-Oct-2025.)
|- ( A e. CC -> ( RR _D ( RR X. { A } ) ) = ( RR X. { 0 } ) )
3-Oct-2025	dvidsslem 15361	Lemma for dvconstss 15366. Analogue of dvidlemap 15359 where F is defined on an open subset of the real or complex numbers. (Contributed by Jim Kingdon, 3-Oct-2025.)
|- ( ph -> S e. { RR , CC } )   &    |- J = ( K ↾t S )   &    |- K = ( MetOpen ` ( abs o. - ) )   &    |- ( ph -> F : X --> CC )   &    |- ( ph -> X e. J )   &    |- ( ( ph /\ ( x e. X /\ z e. X /\ z # x ) ) -> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) = B )   &    |- B e. CC   =>    |- ( ph -> ( S _D F ) = ( X X. { B } ) )
3-Oct-2025	dvidrelem 15360	Lemma for dvidre 15365 and dvconstre 15364. Analogue of dvidlemap 15359 for real numbers rather than complex numbers. (Contributed by Jim Kingdon, 3-Oct-2025.)
|- ( ph -> F : RR --> CC )   &    |- ( ( ph /\ ( x e. RR /\ z e. RR /\ z # x ) ) -> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) = B )   &    |- B e. CC   =>    |- ( ph -> ( RR _D F ) = ( RR X. { B } ) )
28-Sep-2025	metuex 14513	Applying metUnif yields a set. (Contributed by Jim Kingdon, 28-Sep-2025.)
|- ( A e. V -> (metUnif ` A ) e. _V )
28-Sep-2025	cndsex 14511	The standard distance function on the complex numbers is a set. (Contributed by Jim Kingdon, 28-Sep-2025.)
|- ( abs o. - ) e. _V
25-Sep-2025	cntopex 14512	The standard topology on the complex numbers is a set. (Contributed by Jim Kingdon, 25-Sep-2025.)
|- ( MetOpen ` ( abs o. - ) ) e. _V
24-Sep-2025	mopnset 14510	Getting a set by applying MetOpen. (Contributed by Jim Kingdon, 24-Sep-2025.)
|- ( D e. V -> ( MetOpen ` D ) e. _V )
24-Sep-2025	blfn 14509	The ball function has universal domain. (Contributed by Jim Kingdon, 24-Sep-2025.)
|- ball Fn _V
23-Sep-2025	elfzoext 10393	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.)
|- ( ( Z e. ( M..^ N ) /\ I e. NN0 ) -> Z e. ( M..^ ( N + I ) ) )
22-Sep-2025	plycjlemc 15428	Lemma for plycj 15429. (Contributed by Mario Carneiro, 24-Jul-2014.) (Revised by Jim Kingdon, 22-Sep-2025.)
|- ( ph -> N e. NN0 )   &    |- G = ( ( * o. F ) o. * )   &    |- ( ph -> A : NN0 --> ( S u. { 0 } ) )   &    |- ( ph -> F = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) )   &    |- ( ph -> F e. (Poly ` S ) )   =>    |- ( ph -> G = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( ( * o. A ) ` k ) x. ( z ^ k ) ) ) )
20-Sep-2025	plycolemc 15426	Lemma for plyco 15427. The result expressed as a sum, with a degree and coefficients for F specified as hypotheses. (Contributed by Jim Kingdon, 20-Sep-2025.)
|- ( ph -> F e. (Poly ` S ) )   &    |- ( ph -> G e. (Poly ` S ) )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x + y ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S )   &    |- ( ph -> N e. NN0 )   &    |- ( ph -> A : NN0 --> ( S u. { 0 } ) )   &    |- ( ph -> ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )   &    |- ( ph -> F = ( x e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( x ^ k ) ) ) )   =>    |- ( ph -> ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( ( G ` z ) ^ k ) ) ) e. (Poly ` S ) )
18-Sep-2025	elfzoextl 10392	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.)
|- ( ( Z e. ( M..^ N ) /\ I e. NN0 ) -> Z e. ( M..^ ( I + N ) ) )
16-Sep-2025	lgsquadlemofi 15749	Lemma for lgsquad 15753. There are finitely many members of S with odd first part. (Contributed by Jim Kingdon, 16-Sep-2025.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- ( ph -> Q e. ( Prime \ { 2 } ) )   &    |- ( ph -> P =/= Q )   &    |- M = ( ( P - 1 ) / 2 )   &    |- N = ( ( Q - 1 ) / 2 )   &    |- S = { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( y x. P ) < ( x x. Q ) ) }   =>    |- ( ph -> { z e. S | -. 2 || ( 1st ` z ) } e. Fin )
16-Sep-2025	lgsquadlemsfi 15748	Lemma for lgsquad 15753. S is finite. (Contributed by Jim Kingdon, 16-Sep-2025.)
|- ( ph -> P e. ( Prime \ { 2 } ) )   &    |- ( ph -> Q e. ( Prime \ { 2 } ) )   &    |- ( ph -> P =/= Q )   &    |- M = ( ( P - 1 ) / 2 )   &    |- N = ( ( Q - 1 ) / 2 )   &    |- S = { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( y x. P ) < ( x x. Q ) ) }   =>    |- ( ph -> S e. Fin )
16-Sep-2025	opabfi 7096	Finiteness of an ordered pair abstraction which is a decidable subset of finite sets. (Contributed by Jim Kingdon, 16-Sep-2025.)
|- S = { <. x , y >. | ( ( x e. A /\ y e. B ) /\ ps ) }   &    |- ( ph -> A e. Fin )   &    |- ( ph -> B e. Fin )   &    |- ( ph -> A. x e. A A. y e. B DECID ps )   =>    |- ( ph -> S e. Fin )
13-Sep-2025	uchoice 6281	Principle of unique choice. This is also called non-choice. The name choice results in its similarity to something like acfun 7385 (with the key difference being the change of E. to E!) 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.)
|- ( ( A e. V /\ A. x e. A E! y ph ) -> E. f ( f Fn A /\ A. x e. A [. ( f ` x ) / y ]. ph ) )
11-Sep-2025	expghmap 14565	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.)
|- M = (mulGrp ` ℂfld )   &    |- U = ( M ↾s { z e. CC | z # 0 } )   =>    |- ( ( A e. CC /\ A # 0 ) -> ( x e. ZZ |-> ( A ^ x ) ) e. (ℤring GrpHom U ) )
11-Sep-2025	cnfldui 14547	The invertible complex numbers are exactly those apart from zero. This is recapb 8814 but expressed in terms of ℂfld. (Contributed by Jim Kingdon, 11-Sep-2025.)
|- { z e. CC | z # 0 } = (Unit ` ℂfld )
9-Sep-2025	gsumfzfsumlemm 14545	Lemma for gsumfzfsum 14546. The case where the sum is inhabited. (Contributed by Jim Kingdon, 9-Sep-2025.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> B e. CC )   =>    |- ( ph -> (ℂfld gsumg ( k e. ( M ... N ) |-> B ) ) = sum_ k e. ( M ... N ) B )
9-Sep-2025	gsumfzfsumlem0 14544	Lemma for gsumfzfsum 14546. The case where the sum is empty. (Contributed by Jim Kingdon, 9-Sep-2025.)
|- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> N < M )   =>    |- ( ph -> (ℂfld gsumg ( k e. ( M ... N ) |-> B ) ) = sum_ k e. ( M ... N ) B )
9-Sep-2025	gsumfzmhm2 13876	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.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> H e. Mnd )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> ( x e. B |-> C ) e. ( G MndHom H ) )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> X e. B )   &    |- ( x = X -> C = D )   &    |- ( x = ( G gsumg ( k e. ( M ... N ) |-> X ) ) -> C = E )   =>    |- ( ph -> ( H gsumg ( k e. ( M ... N ) |-> D ) ) = E )
8-Sep-2025	gsumfzmhm 13875	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.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> H e. Mnd )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> K e. ( G MndHom H ) )   &    |- ( ph -> F : ( M ... N ) --> B )   =>    |- ( ph -> ( H gsumg ( K o. F ) ) = ( K ` ( G gsumg F ) ) )
8-Sep-2025	5ndvds6 12441	5 does not divide 6. (Contributed by AV, 8-Sep-2025.)
|- -. 5 || 6
8-Sep-2025	5ndvds3 12440	5 does not divide 3. (Contributed by AV, 8-Sep-2025.)
|- -. 5 || 3
6-Sep-2025	gsumfzconst 13873	Sum of a constant series. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by Jim Kingdon, 6-Sep-2025.)
|- B = ( Base ` G )   &    |- .x. = (.g ` G )   =>    |- ( ( G e. Mnd /\ N e. ( ZZ>= ` M ) /\ X e. B ) -> ( G gsumg ( k e. ( M ... N ) |-> X ) ) = ( ( ( N - M ) + 1 ) .x. X ) )