Intuitionistic Logic Explorer Home 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  Intuitionistic Logic Explorer   User Mathboxes  User Mathboxes  

Last updated on 10-Mar-2026 at 7:15 AM ET.
Recent Additions to the Intuitionistic Logic Explorer
DateLabelDescription
Theorem
 
22-Feb-2026isclwwlkni 16176 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-2026clwwlkex 16167 Existence of the set of closed walks (represented by words). (Contributed by Jim Kingdon, 21-Feb-2026.)
(𝐺 ∈ 𝑉 → (ClWWalks‘𝐺) ∈ V)
 
17-Feb-2026vtxdgfif 16079 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‘𝐺)    &   𝐴 = dom 𝐼    &   (𝜑 → 𝐴 ∈ Fin)    &   (𝜑 → 𝑉 ∈ Fin)    &   (𝜑 → 𝐺 ∈ UPGraph)    ⇒   (𝜑 → (VtxDeg‘𝐺):𝑉⟶ℕ0)
 
16-Feb-2026vtxlpfi 16076 In a finite graph, the number of loops from a given vertex is finite. (Contributed by Jim Kingdon, 16-Feb-2026.)
𝑉 = (Vtx‘𝐺)    &   𝐼 = (iEdg‘𝐺)    &   𝐴 = dom 𝐼    &   (𝜑 → 𝐴 ∈ Fin)    &   (𝜑 → 𝑉 ∈ Fin)    &   (𝜑 → 𝑈 ∈ 𝑉)    &   (𝜑 → 𝐺 ∈ UPGraph)    ⇒   (𝜑 → {𝑥 ∈ 𝐴 ∣ (𝐼‘𝑥) = {𝑈}} ∈ Fin)
 
16-Feb-2026vtxedgfi 16075 In a finite graph, the number of edges from a given vertex is finite. (Contributed by Jim Kingdon, 16-Feb-2026.)
𝑉 = (Vtx‘𝐺)    &   𝐼 = (iEdg‘𝐺)    &   𝐴 = dom 𝐼    &   (𝜑 → 𝐴 ∈ Fin)    &   (𝜑 → 𝑉 ∈ Fin)    &   (𝜑 → 𝑈 ∈ 𝑉)    &   (𝜑 → 𝐺 ∈ UPGraph)    ⇒   (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐼‘𝑥)} ∈ Fin)
 
15-Feb-2026eqsndc 7081 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 𝑥 = 𝑦)    &   (𝜑 → 𝑋 ∈ 𝐵)    &   (𝜑 → 𝐴 ⊆ 𝐵)    &   (𝜑 → 𝐴 ∈ Fin)    ⇒   (𝜑 → DECID 𝐴 = {𝑋})
 
14-Feb-2026pw1ninf 16468 The powerset of 1o is not infinite. Since we cannot prove it is finite (see pw1fin 7088), this provides a concrete example of a set which we cannot show to be finite or infinite, as seen another way at inffiexmid 7084. (Contributed by Jim Kingdon, 14-Feb-2026.)
¬ ω ≼ 𝒫 1o
 
14-Feb-2026pw1ndom3 16467 The powerset of 1o does not dominate 3o. This is another way of saying that 𝒫 1o does not have three elements (like pwntru 4284). (Contributed by Steven Nguyen and Jim Kingdon, 14-Feb-2026.)
¬ 3o ≼ 𝒫 1o
 
14-Feb-2026pw1ndom3lem 16466 Lemma for pw1ndom3 16467. (Contributed by Jim Kingdon, 14-Feb-2026.)
(𝜑 → 𝑋 ∈ 𝒫 1o)    &   (𝜑 → 𝑌 ∈ 𝒫 1o)    &   (𝜑 → 𝑍 ∈ 𝒫 1o)    &   (𝜑 → 𝑋 ≠ 𝑌)    &   (𝜑 → 𝑋 ≠ 𝑍)    &   (𝜑 → 𝑌 ≠ 𝑍)    ⇒   (𝜑 → 𝑋 = ∅)
 
12-Feb-2026pw1dceq 16483 The powerset of 1o having decidable equality is equivalent to excluded middle. (Contributed by Jim Kingdon, 12-Feb-2026.)
(EXMID ↔ ∀𝑥 ∈ 𝒫 1o∀𝑦 ∈ 𝒫 1oDECID 𝑥 = 𝑦)
 
12-Feb-20263dom 16465 A set that dominates ordinal 3 has at least 3 different members. (Contributed by Jim Kingdon, 12-Feb-2026.)
(3o ≼ 𝐴 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧))
 
11-Feb-2026elssdc 7080 Membership in a finite subset of a set with decidable equality is decidable. (Contributed by Jim Kingdon, 11-Feb-2026.)
(𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 DECID 𝑥 = 𝑦)    &   (𝜑 → 𝑋 ∈ 𝐵)    &   (𝜑 → 𝐴 ⊆ 𝐵)    &   (𝜑 → 𝐴 ∈ Fin)    ⇒   (𝜑 → DECID 𝑋 ∈ 𝐴)
 
10-Feb-2026vtxdgfifival 16077 The degree of a vertex for graphs with finite vertex and edge sets. (Contributed by Jim Kingdon, 10-Feb-2026.)
𝑉 = (Vtx‘𝐺)    &   𝐼 = (iEdg‘𝐺)    &   𝐴 = dom 𝐼    &   (𝜑 → 𝐴 ∈ Fin)    &   (𝜑 → 𝑉 ∈ Fin)    &   (𝜑 → 𝑈 ∈ 𝑉)    &   (𝜑 → 𝐺 ∈ UPGraph)    ⇒   (𝜑 → ((VtxDeg‘𝐺)‘𝑈) = ((♯‘{𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐼‘𝑥)}) + (♯‘{𝑥 ∈ 𝐴 ∣ (𝐼‘𝑥) = {𝑈}})))
 
10-Feb-2026fidcen 7074 Equinumerosity of finite sets is decidable. (Contributed by Jim Kingdon, 10-Feb-2026.)
((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → DECID 𝐴 ≈ 𝐵)
 
8-Feb-2026wlkvtxm 16112 A graph with a walk has at least one vertex. (Contributed by Jim Kingdon, 8-Feb-2026.)
𝑉 = (Vtx‘𝐺)    ⇒   (𝐹(Walks‘𝐺)𝑃 → ∃𝑥 𝑥 ∈ 𝑉)
 
7-Feb-2026trlsv 16154 The classes involved in a trail are sets. (Contributed by Jim Kingdon, 7-Feb-2026.)
(𝐹(Trails‘𝐺)𝑃 → (𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V))
 
7-Feb-2026wlkex 16097 The class of walks on a graph is a set. (Contributed by Jim Kingdon, 7-Feb-2026.)
(𝐺 ∈ 𝑉 → (Walks‘𝐺) ∈ V)
 
3-Feb-2026dom1oi 6991 A set with an element dominates one. (Contributed by Jim Kingdon, 3-Feb-2026.)
((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝐴) → 1o ≼ 𝐴)
 
2-Feb-2026edginwlkd 16127 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‘𝐺)    &   (𝜑 → Fun 𝐼)    &   (𝜑 → 𝐹 ∈ Word dom 𝐼)    &   (𝜑 → 𝐾 ∈ (0..^(♯‘𝐹)))    &   (𝜑 → 𝐺 ∈ 𝑉)    ⇒   (𝜑 → (𝐼‘(𝐹‘𝐾)) ∈ 𝐸)
 
2-Feb-2026wlkelvv 16121 A walk is an ordered pair. (Contributed by Jim Kingdon, 2-Feb-2026.)
(𝑊 ∈ (Walks‘𝐺) → 𝑊 ∈ (V × V))
 
1-Feb-2026wlkcprim 16122 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‘𝐺) → (1st ‘𝑊)(Walks‘𝐺)(2nd ‘𝑊))
 
1-Feb-2026wlkmex 16091 If there are walks on a graph, the graph is a set. (Contributed by Jim Kingdon, 1-Feb-2026.)
(𝑊 ∈ (Walks‘𝐺) → 𝐺 ∈ V)
 
31-Jan-2026fvmbr 5667 If a function value is inhabited, the argument is related to the function value. (Contributed by Jim Kingdon, 31-Jan-2026.)
(𝐴 ∈ (𝐹‘𝑋) → 𝑋𝐹(𝐹‘𝑋))
 
30-Jan-2026elfvfvex 5666 If a function value is inhabited, the function value is a set. (Contributed by Jim Kingdon, 30-Jan-2026.)
(𝐴 ∈ (𝐹‘𝐵) → (𝐹‘𝐵) ∈ V)
 
30-Jan-2026reldmm 4945 A relation is inhabited iff its domain is inhabited. (Contributed by Jim Kingdon, 30-Jan-2026.)
(Rel 𝐴 → (∃𝑥 𝑥 ∈ 𝐴 ↔ ∃𝑦 𝑦 ∈ dom 𝐴))
 
25-Jan-2026ifp2 986 Forward direction of dfifp2dc 987. This direction does not require decidability. (Contributed by Jim Kingdon, 25-Jan-2026.)
(if-(𝜑, 𝜓, 𝜒) → ((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜒)))
 
25-Jan-2026ifpdc 985 The conditional operator for propositions implies decidability. (Contributed by Jim Kingdon, 25-Jan-2026.)
(if-(𝜑, 𝜓, 𝜒) → DECID 𝜑)
 
20-Jan-2026cats1fvd 11319 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 V)    &   (𝜑 → (♯‘𝑆) = 𝑀)    &   (𝜑 → 𝑌 ∈ 𝑉)    &   (𝜑 → 𝑋 ∈ 𝑊)    &   (𝜑 → (𝑆‘𝑁) = 𝑌)    &   (𝜑 → 𝑁 ∈ ℕ0)    &   (𝜑 → 𝑁 < 𝑀)    ⇒   (𝜑 → (𝑇‘𝑁) = 𝑌)
 
20-Jan-2026cats1fvnd 11318 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 V)    &   (𝜑 → 𝑋 ∈ 𝑉)    &   (𝜑 → (♯‘𝑆) = 𝑀)    ⇒   (𝜑 → (𝑇‘𝑀) = 𝑋)
 
19-Jan-2026cats2catd 11322 Closure of concatenation of concatenations with singleton words. (Contributed by AV, 1-Mar-2021.) (Revised by Jim Kingdon, 19-Jan-2026.)
(𝜑 → 𝐵 ∈ Word V)    &   (𝜑 → 𝐷 ∈ Word V)    &   (𝜑 → 𝑋 ∈ 𝑉)    &   (𝜑 → 𝑌 ∈ 𝑊)    &   (𝜑 → 𝐴 = (𝐵 ++ ⟨“𝑋”⟩))    &   (𝜑 → 𝐶 = (⟨“𝑌”⟩ ++ 𝐷))    ⇒   (𝜑 → (𝐴 ++ 𝐶) = ((𝐵 ++ ⟨“𝑋𝑌”⟩) ++ 𝐷))
 
19-Jan-2026cats1catd 11321 Closure of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) (Revised by Jim Kingdon, 19-Jan-2026.)
𝑇 = (𝑆 ++ ⟨“𝑋”⟩)    &   (𝜑 → 𝐴 ∈ Word V)    &   (𝜑 → 𝑆 ∈ Word V)    &   (𝜑 → 𝑋 ∈ 𝑊)    &   (𝜑 → 𝐶 = (𝐵 ++ ⟨“𝑋”⟩))    &   (𝜑 → 𝐵 = (𝐴 ++ 𝑆))    ⇒   (𝜑 → 𝐶 = (𝐴 ++ 𝑇))
 
19-Jan-2026cats1lend 11320 The length of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) (Revised by Jim Kingdon, 19-Jan-2026.)
𝑇 = (𝑆 ++ ⟨“𝑋”⟩)    &   (𝜑 → 𝑆 ∈ Word V)    &   (𝜑 → 𝑋 ∈ 𝑊)    &   (♯‘𝑆) = 𝑀    &   (𝑀 + 1) = 𝑁    ⇒   (𝜑 → (♯‘𝑇) = 𝑁)
 
18-Jan-2026rexanaliim 2636 A transformation of restricted quantifiers and logical connectives. (Contributed by NM, 4-Sep-2005.) (Revised by Jim Kingdon, 18-Jan-2026.)
(∃𝑥 ∈ 𝐴 (𝜑 ∧ ¬ 𝜓) → ¬ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))
 
15-Jan-2026df-uspgren 15974 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‘𝑔) / 𝑒]𝑒:dom 𝑒–1-1→{𝑥 ∈ 𝒫 𝑣 ∣ (𝑥 ≈ 1o ∨ 𝑥 ≈ 2o)}}
 
11-Jan-2026en2prde 7382 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.)
(𝑉 ≈ 2o → ∃𝑎∃𝑏(𝑎 ≠ 𝑏 ∧ 𝑉 = {𝑎, 𝑏}))
 
10-Jan-2026pw1mapen 16475 Equinumerosity of (𝒫 1o ↑𝑚 𝐴) and the set of subsets of 𝐴. (Contributed by Jim Kingdon, 10-Jan-2026.)
(𝐴 ∈ 𝑉 → (𝒫 1o ↑𝑚 𝐴) ≈ 𝒫 𝐴)
 
10-Jan-2026pw1if 7426 Expressing a truth value in terms of an if expression. (Contributed by Jim Kingdon, 10-Jan-2026.)
(𝐴 ∈ 𝒫 1o → if(𝐴 = 1o, 1o, ∅) = 𝐴)
 
10-Jan-2026pw1m 7425 A truth value which is inhabited is equal to true. This is a variation of pwntru 4284 and pwtrufal 16476. (Contributed by Jim Kingdon, 10-Jan-2026.)
((𝐴 ∈ 𝒫 1o ∧ ∃𝑥 𝑥 ∈ 𝐴) → 𝐴 = 1o)
 
10-Jan-20261ndom2 7039 Two is not dominated by one. (Contributed by Jim Kingdon, 10-Jan-2026.)
¬ 2o ≼ 1o
 
9-Jan-2026pw1map 16474 Mapping between (𝒫 1o ↑𝑚 𝐴) and subsets of 𝐴. (Contributed by Jim Kingdon, 9-Jan-2026.)
𝐹 = (𝑠 ∈ (𝒫 1o ↑𝑚 𝐴) ↦ {𝑧 ∈ 𝐴 ∣ (𝑠‘𝑧) = 1o})    ⇒   (𝐴 ∈ 𝑉 → 𝐹:(𝒫 1o ↑𝑚 𝐴)–1-1-onto→𝒫 𝐴)
 
9-Jan-2026iftrueb01 7424 Using an if expression to represent a truth value by ∅ or 1o. Unlike some theorems using if, 𝜑 does not need to be decidable. (Contributed by Jim Kingdon, 9-Jan-2026.)
(if(𝜑, 1o, ∅) = 1o ↔ 𝜑)
 
8-Jan-2026pfxclz 11232 Closure of the prefix extractor. This extends pfxclg 11231 from ℕ0 to ℤ (negative lengths are trivial, resulting in the empty word). (Contributed by Jim Kingdon, 8-Jan-2026.)
((𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ ℤ) → (𝑆 prefix 𝐿) ∈ Word 𝐴)
 
8-Jan-2026fnpfx 11230 The domain of the prefix extractor. (Contributed by Jim Kingdon, 8-Jan-2026.)
prefix Fn (V × ℕ0)
 
7-Jan-2026pr1or2 7383 An unordered pair, with decidable equality for the specified elements, has either one or two elements. (Contributed by Jim Kingdon, 7-Jan-2026.)
((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ DECID 𝐴 = 𝐵) → ({𝐴, 𝐵} ≈ 1o ∨ {𝐴, 𝐵} ≈ 2o))
 
6-Jan-2026upgr1elem1 15941 Lemma for upgr1edc 15942. (Contributed by AV, 16-Oct-2020.) (Revised by Jim Kingdon, 6-Jan-2026.)
(𝜑 → {𝐵, 𝐶} ∈ 𝑆)    &   (𝜑 → 𝐵 ∈ 𝑊)    &   (𝜑 → 𝐶 ∈ 𝑋)    &   (𝜑 → DECID 𝐵 = 𝐶)    ⇒   (𝜑 → {{𝐵, 𝐶}} ⊆ {𝑥 ∈ 𝑆 ∣ (𝑥 ≈ 1o ∨ 𝑥 ≈ 2o)})
 
3-Jan-2026df-umgren 15915 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‘𝑔) / 𝑒]𝑒:dom 𝑒⟶{𝑥 ∈ 𝒫 𝑣 ∣ 𝑥 ≈ 2o}}
 
3-Jan-2026df-upgren 15914 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 15915). (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 24-Nov-2020.) (Revised by Jim Kingdon, 3-Jan-2026.)
UPGraph = {𝑔 ∣ [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶{𝑥 ∈ 𝒫 𝑣 ∣ (𝑥 ≈ 1o ∨ 𝑥 ≈ 2o)}}
 
3-Jan-2026dom1o 6990 Two ways of saying that a set is inhabited. (Contributed by Jim Kingdon, 3-Jan-2026.)
(𝐴 ∈ 𝑉 → (1o ≼ 𝐴 ↔ ∃𝑗 𝑗 ∈ 𝐴))
 
3-Jan-2026en2m 6987 A set with two elements is inhabited. (Contributed by Jim Kingdon, 3-Jan-2026.)
(𝐴 ≈ 2o → ∃𝑥 𝑥 ∈ 𝐴)
 
3-Jan-2026en1m 6970 A set with one element is inhabited. (Contributed by Jim Kingdon, 3-Jan-2026.)
(𝐴 ≈ 1o → ∃𝑥 𝑥 ∈ 𝐴)
 
31-Dec-2025pw0ss 15904 There are no inhabited subsets of the empty set. (Contributed by Jim Kingdon, 31-Dec-2025.)
{𝑠 ∈ 𝒫 ∅ ∣ ∃𝑗 𝑗 ∈ 𝑠} = ∅
 
31-Dec-2025df-ushgrm 15891 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‘𝑔) / 𝑒]𝑒:dom 𝑒–1-1→{𝑠 ∈ 𝒫 𝑣 ∣ ∃𝑗 𝑗 ∈ 𝑠}}
 
29-Dec-2025df-uhgrm 15890 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‘𝑔) / 𝑒]𝑒:dom 𝑒⟶{𝑠 ∈ 𝒫 𝑣 ∣ ∃𝑗 𝑗 ∈ 𝑠}}
 
29-Dec-2025iedgex 15841 Applying the indexed edge function yields a set. (Contributed by Jim Kingdon, 29-Dec-2025.)
(𝐺 ∈ 𝑉 → (iEdg‘𝐺) ∈ V)
 
29-Dec-2025vtxex 15840 Applying the vertex function yields a set. (Contributed by Jim Kingdon, 29-Dec-2025.)
(𝐺 ∈ 𝑉 → (Vtx‘𝐺) ∈ V)
 
29-Dec-2025snmb 3788 A singleton is inhabited iff its argument is a set. (Contributed by Scott Fenton, 8-May-2018.) (Revised by Jim Kingdon, 29-Dec-2025.)
(𝐴 ∈ V ↔ ∃𝑥 𝑥 ∈ {𝐴})
 
27-Dec-2025lswex 11141 Existence of the last symbol. The last symbol of a word is a set. See lsw0g 11138 or lswcl 11140 if you want more specific results for empty or nonempty words, respectively. (Contributed by Jim Kingdon, 27-Dec-2025.)
(𝑊 ∈ Word 𝑉 → (lastS‘𝑊) ∈ V)
 
23-Dec-2025fzowrddc 11200 Decidability of whether a range of integers is a subset of a word's domain. (Contributed by Jim Kingdon, 23-Dec-2025.)
((𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → DECID (𝐹..^𝐿) ⊆ dom 𝑆)
 
19-Dec-2025ccatclab 11147 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-2025lswwrd 11136 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‘𝑊) = (𝑊‘((♯‘𝑊) − 1)))
 
14-Dec-20252strstrndx 13172 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.)
𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨𝑁, + ⟩}    &   (Base‘ndx) < 𝑁    &   𝑁 ∈ ℕ    ⇒   ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) → 𝐺 Struct ⟨(Base‘ndx), 𝑁⟩)
 
12-Dec-2025funiedgdm2vald 15854 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.)
𝐴 ∈ V    &   𝐵 ∈ V    &   (𝜑 → 𝐺 ∈ 𝑋)    &   (𝜑 → Fun (𝐺 ∖ {∅}))    &   (𝜑 → 𝐴 ≠ 𝐵)    &   (𝜑 → {𝐴, 𝐵} ⊆ dom 𝐺)    ⇒   (𝜑 → (iEdg‘𝐺) = (.ef‘𝐺))
 
11-Dec-2025funvtxdm2vald 15853 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.)
𝐴 ∈ V    &   𝐵 ∈ V    &   (𝜑 → 𝐺 ∈ 𝑋)    &   (𝜑 → Fun (𝐺 ∖ {∅}))    &   (𝜑 → 𝐴 ≠ 𝐵)    &   (𝜑 → {𝐴, 𝐵} ⊆ dom 𝐺)    ⇒   (𝜑 → (Vtx‘𝐺) = (Base‘𝐺))
 
11-Dec-2025funiedgdm2domval 15852 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.)
((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅}) ∧ 2o ≼ dom 𝐺) → (iEdg‘𝐺) = (.ef‘𝐺))
 
11-Dec-2025funvtxdm2domval 15851 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.)
((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅}) ∧ 2o ≼ dom 𝐺) → (Vtx‘𝐺) = (Base‘𝐺))
 
4-Dec-2025hash2en 11083 Two equivalent ways to say a set has two elements. (Contributed by Jim Kingdon, 4-Dec-2025.)
(𝑉 ≈ 2o ↔ (𝑉 ∈ Fin ∧ (♯‘𝑉) = 2))
 
30-Nov-2025nninfnfiinf 16503 An element of ℕ∞ which is not finite is infinite. (Contributed by Jim Kingdon, 30-Nov-2025.)
((𝐴 ∈ ℕ∞ ∧ ¬ ∃𝑛 ∈ ω 𝐴 = (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) → 𝐴 = (𝑖 ∈ ω ↦ 1o))
 
27-Nov-2025psrelbasfi 14661 Simpler form of psrelbas 14660 when the index set is finite. (Contributed by Jim Kingdon, 27-Nov-2025.)
𝑆 = (𝐼 mPwSer 𝑅)    &   𝐾 = (Base‘𝑅)    &   (𝜑 → 𝐼 ∈ Fin)    &   𝐵 = (Base‘𝑆)    &   (𝜑 → 𝑋 ∈ 𝐵)    ⇒   (𝜑 → 𝑋:(ℕ0 ↑𝑚 𝐼)⟶𝐾)
 
26-Nov-2025mplsubgfileminv 14685 Lemma for mplsubgfi 14686. The additive inverse of a polynomial is a polynomial. (Contributed by Jim Kingdon, 26-Nov-2025.)
𝑆 = (𝐼 mPwSer 𝑅)    &   𝑃 = (𝐼 mPoly 𝑅)    &   𝑈 = (Base‘𝑃)    &   (𝜑 → 𝐼 ∈ Fin)    &   (𝜑 → 𝑅 ∈ Grp)    &   (𝜑 → 𝑋 ∈ 𝑈)    &   𝑁 = (invg‘𝑆)    ⇒   (𝜑 → (𝑁‘𝑋) ∈ 𝑈)
 
26-Nov-2025mplsubgfilemcl 14684 Lemma for mplsubgfi 14686. The sum of two polynomials is a polynomial. (Contributed by Jim Kingdon, 26-Nov-2025.)
𝑆 = (𝐼 mPwSer 𝑅)    &   𝑃 = (𝐼 mPoly 𝑅)    &   𝑈 = (Base‘𝑃)    &   (𝜑 → 𝐼 ∈ Fin)    &   (𝜑 → 𝑅 ∈ Grp)    &   (𝜑 → 𝑋 ∈ 𝑈)    &   (𝜑 → 𝑌 ∈ 𝑈)    &    + = (+g‘𝑆)    ⇒   (𝜑 → (𝑋 + 𝑌) ∈ 𝑈)
 
25-Nov-2025nninfinfwlpo 7363 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 7316). (Contributed by Jim Kingdon, 25-Nov-2025.)
(∀𝑥 ∈ ℕ∞ DECID 𝑥 = (𝑖 ∈ ω ↦ 1o) ↔ ω ∈ WOmni)
 
23-Nov-2025psrbagfi 14658 A finite index set gives a simpler expression for finite bags. (Contributed by Jim Kingdon, 23-Nov-2025.)
𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    ⇒   (𝐼 ∈ Fin → 𝐷 = (ℕ0 ↑𝑚 𝐼))
 
22-Nov-2025df-acnm 7368 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 𝐴 = {𝑥 ∣ (𝐴 ∈ V ∧ ∀𝑓 ∈ ({𝑧 ∈ 𝒫 𝑥 ∣ ∃𝑗 𝑗 ∈ 𝑧} ↑𝑚 𝐴)∃𝑔∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝑓‘𝑦))}
 
21-Nov-2025mplsubgfilemm 14683 Lemma for mplsubgfi 14686. There exists a polynomial. (Contributed by Jim Kingdon, 21-Nov-2025.)
𝑆 = (𝐼 mPwSer 𝑅)    &   𝑃 = (𝐼 mPoly 𝑅)    &   𝑈 = (Base‘𝑃)    &   (𝜑 → 𝐼 ∈ Fin)    &   (𝜑 → 𝑅 ∈ Grp)    ⇒   (𝜑 → ∃𝑗 𝑗 ∈ 𝑈)
 
14-Nov-20252omapen 16473 Equinumerosity of (2o ↑𝑚 𝐴) and the set of decidable subsets of 𝐴. (Contributed by Jim Kingdon, 14-Nov-2025.)
(𝐴 ∈ 𝑉 → (2o ↑𝑚 𝐴) ≈ {𝑥 ∈ 𝒫 𝐴 ∣ ∀𝑦 ∈ 𝐴 DECID 𝑦 ∈ 𝑥})
 
12-Nov-20252omap 16472 Mapping between (2o ↑𝑚 𝐴) and decidable subsets of 𝐴. (Contributed by Jim Kingdon, 12-Nov-2025.)
𝐹 = (𝑠 ∈ (2o ↑𝑚 𝐴) ↦ {𝑧 ∈ 𝐴 ∣ (𝑠‘𝑧) = 1o})    ⇒   (𝐴 ∈ 𝑉 → 𝐹:(2o ↑𝑚 𝐴)–1-1-onto→{𝑥 ∈ 𝒫 𝐴 ∣ ∀𝑦 ∈ 𝐴 DECID 𝑦 ∈ 𝑥})
 
11-Nov-2025domomsubct 16480 A set dominated by ω is subcountable. (Contributed by Jim Kingdon, 11-Nov-2025.)
(𝐴 ≼ ω → ∃𝑠(𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠–onto→𝐴))
 
10-Nov-2025prdsbaslemss 13328 Lemma for prdsbas 13330 and similar theorems. (Contributed by Jim Kingdon, 10-Nov-2025.)
𝑃 = (𝑆Xs𝑅)    &   (𝜑 → 𝑆 ∈ 𝑉)    &   (𝜑 → 𝑅 ∈ 𝑊)    &   𝐴 = (𝐸‘𝑃)    &   𝐸 = Slot (𝐸‘ndx)    &   (𝐸‘ndx) ∈ ℕ    &   (𝜑 → 𝑇 ∈ 𝑋)    &   (𝜑 → {⟨(𝐸‘ndx), 𝑇⟩} ⊆ 𝑃)    ⇒   (𝜑 → 𝐴 = 𝑇)
 
5-Nov-2025fnmpl 14678 mPoly has universal domain. (Contributed by Jim Kingdon, 5-Nov-2025.)
mPoly Fn (V × V)
 
4-Nov-2025mplelbascoe 14677 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 𝑅)    &   𝐵 = (Base‘𝑆)    &    0 = (0g‘𝑅)    &   𝑈 = (Base‘𝑃)    ⇒   ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑋 ∈ 𝑈 ↔ (𝑋 ∈ 𝐵 ∧ ∃𝑎 ∈ (ℕ0 ↑𝑚 𝐼)∀𝑏 ∈ (ℕ0 ↑𝑚 𝐼)(∀𝑘 ∈ 𝐼 (𝑎‘𝑘) < (𝑏‘𝑘) → (𝑋‘𝑏) = 0 ))))
 
4-Nov-2025mplbascoe 14676 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 𝑅)    &   𝐵 = (Base‘𝑆)    &    0 = (0g‘𝑅)    &   𝑈 = (Base‘𝑃)    ⇒   ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → 𝑈 = {𝑓 ∈ 𝐵 ∣ ∃𝑎 ∈ (ℕ0 ↑𝑚 𝐼)∀𝑏 ∈ (ℕ0 ↑𝑚 𝐼)(∀𝑘 ∈ 𝐼 (𝑎‘𝑘) < (𝑏‘𝑘) → (𝑓‘𝑏) = 0 )})
 
4-Nov-2025mplvalcoe 14675 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 𝑅)    &   𝐵 = (Base‘𝑆)    &    0 = (0g‘𝑅)    &   𝑈 = {𝑓 ∈ 𝐵 ∣ ∃𝑎 ∈ (ℕ0 ↑𝑚 𝐼)∀𝑏 ∈ (ℕ0 ↑𝑚 𝐼)(∀𝑘 ∈ 𝐼 (𝑎‘𝑘) < (𝑏‘𝑘) → (𝑓‘𝑏) = 0 )}    ⇒   ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → 𝑃 = (𝑆 ↾s 𝑈))
 
1-Nov-2025ficardon 7377 The cardinal number of a finite set is an ordinal. (Contributed by Jim Kingdon, 1-Nov-2025.)
(𝐴 ∈ Fin → (card‘𝐴) ∈ On)
 
31-Oct-2025bitsdc 12479 Whether a bit is set is decidable. (Contributed by Jim Kingdon, 31-Oct-2025.)
((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → DECID 𝑀 ∈ (bits‘𝑁))
 
28-Oct-2025nn0maxcl 11757 The maximum of two nonnegative integers is a nonnegative integer. (Contributed by Jim Kingdon, 28-Oct-2025.)
((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → sup({𝐴, 𝐵}, ℝ, < ) ∈ ℕ0)
 
28-Oct-2025qdcle 10483 Rational ≤ is decidable. (Contributed by Jim Kingdon, 28-Oct-2025.)
((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → DECID 𝐴 ≤ 𝐵)
 
17-Oct-2025plycoeid3 15452 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.)
(𝜑 → 𝐷 ∈ ℕ0)    &   (𝜑 → 𝐴:ℕ0⟶ℂ)    &   (𝜑 → (𝐴 “ (ℤ≥‘(𝐷 + 1))) = {0})    &   (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝐷)((𝐴‘𝑘) · (𝑧↑𝑘))))    &   (𝜑 → 𝑀 ∈ (ℤ≥‘𝐷))    &   (𝜑 → 𝑋 ∈ ℂ)    ⇒   (𝜑 → (𝐹‘𝑋) = Σ𝑗 ∈ (0...𝑀)((𝐴‘𝑗) · (𝑋↑𝑗)))
 
13-Oct-2025tpfidceq 7108 A triple is finite if it consists of elements of a class with decidable equality. (Contributed by Jim Kingdon, 13-Oct-2025.)
(𝜑 → 𝐴 ∈ 𝐷)    &   (𝜑 → 𝐵 ∈ 𝐷)    &   (𝜑 → 𝐶 ∈ 𝐷)    &   (𝜑 → ∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐷 DECID 𝑥 = 𝑦)    ⇒   (𝜑 → {𝐴, 𝐵, 𝐶} ∈ Fin)
 
13-Oct-2025prfidceq 7106 A pair is finite if it consists of elements of a class with decidable equality. (Contributed by Jim Kingdon, 13-Oct-2025.)
(𝜑 → 𝐴 ∈ 𝐶)    &   (𝜑 → 𝐵 ∈ 𝐶)    &   (𝜑 → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 DECID 𝑥 = 𝑦)    ⇒   (𝜑 → {𝐴, 𝐵} ∈ Fin)
 
13-Oct-2025dcun 3601 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-2025dvdsfi 12782 A natural number has finitely many divisors. (Contributed by Jim Kingdon, 9-Oct-2025.)
(𝑁 ∈ ℕ → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∈ Fin)
 
7-Oct-2025df-mplcoe 14649 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 = (𝑖 ∈ V, 𝑟 ∈ V ↦ ⦋(𝑖 mPwSer 𝑟) / 𝑤⦌(𝑤 ↾s {𝑓 ∈ (Base‘𝑤) ∣ ∃𝑎 ∈ (ℕ0 ↑𝑚 𝑖)∀𝑏 ∈ (ℕ0 ↑𝑚 𝑖)(∀𝑘 ∈ 𝑖 (𝑎‘𝑘) < (𝑏‘𝑘) → (𝑓‘𝑏) = (0g‘𝑟))}))
 
6-Oct-2025dvconstss 15393 Derivative of a constant function defined on an open set. (Contributed by Jim Kingdon, 6-Oct-2025.)
(𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   𝐽 = (𝐾 ↾t 𝑆)    &   𝐾 = (MetOpen‘(abs ∘ − ))    &   (𝜑 → 𝑋 ∈ 𝐽)    &   (𝜑 → 𝐴 ∈ ℂ)    ⇒   (𝜑 → (𝑆 D (𝑋 × {𝐴})) = (𝑋 × {0}))
 
6-Oct-2025dcfrompeirce 1492 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 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.)
(𝜑 ↔ (𝜒 ∨ ¬ 𝜒))    &   (𝜓 ↔ ⊥)    &   (((𝜑 → 𝜓) → 𝜑) → 𝜑)    ⇒   DECID 𝜒
 
6-Oct-2025dcfromcon 1491 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 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.)
(𝜑 ↔ (𝜒 ∨ ¬ 𝜒))    &   (𝜓 ↔ ⊤)    &   ((¬ 𝜑 → ¬ 𝜓) → (𝜓 → 𝜑))    ⇒   DECID 𝜒
 
6-Oct-2025dcfromnotnotr 1490 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 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.)
(𝜑 ↔ (𝜓 ∨ ¬ 𝜓))    &   (¬ ¬ 𝜑 → 𝜑)    ⇒   DECID 𝜓
 
3-Oct-2025dvidre 15392 Real derivative of the identity function. (Contributed by Jim Kingdon, 3-Oct-2025.)
(ℝ D ( I ↾ ℝ)) = (ℝ × {1})
 
3-Oct-2025dvconstre 15391 Real derivative of a constant function. (Contributed by Jim Kingdon, 3-Oct-2025.)
(𝐴 ∈ ℂ → (ℝ D (ℝ × {𝐴})) = (ℝ × {0}))
 
3-Oct-2025dvidsslem 15388 Lemma for dvconstss 15393. Analogue of dvidlemap 15386 where 𝐹 is defined on an open subset of the real or complex numbers. (Contributed by Jim Kingdon, 3-Oct-2025.)
(𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   𝐽 = (𝐾 ↾t 𝑆)    &   𝐾 = (MetOpen‘(abs ∘ − ))    &   (𝜑 → 𝐹:𝑋⟶ℂ)    &   (𝜑 → 𝑋 ∈ 𝐽)    &   ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ 𝑧 # 𝑥)) → (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥)) = 𝐵)    &   𝐵 ∈ ℂ    ⇒   (𝜑 → (𝑆 D 𝐹) = (𝑋 × {𝐵}))
 
3-Oct-2025dvidrelem 15387 Lemma for dvidre 15392 and dvconstre 15391. Analogue of dvidlemap 15386 for real numbers rather than complex numbers. (Contributed by Jim Kingdon, 3-Oct-2025.)
(𝜑 → 𝐹:ℝ⟶ℂ)    &   ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑧 # 𝑥)) → (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥)) = 𝐵)    &   𝐵 ∈ ℂ    ⇒   (𝜑 → (ℝ D 𝐹) = (ℝ × {𝐵}))
  Copyright terms: Public domain W3C HTML validation [external]