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 21-Apr-2026 at 7:14 AM ET.
Recent Additions to the Intuitionistic Logic Explorer
DateLabelDescription
Theorem
 
14-Apr-2026depind 16349 Theorem related to a dependently typed induction principle in type theory. (Contributed by Matthew House, 14-Apr-2026.)
(𝜑 → 𝑃:ℕ0⟶V)    &   (𝜑 → 𝐴 ∈ (𝑃‘0))    &   (𝜑 → ∀𝑛 ∈ ℕ0 (𝐻‘𝑛):(𝑃‘𝑛)⟶(𝑃‘(𝑛 + 1)))    ⇒   (𝜑 → ∃!𝑓 ∈ X 𝑛 ∈ ℕ0 (𝑃‘𝑛)((𝑓‘0) = 𝐴 ∧ ∀𝑛 ∈ ℕ0 (𝑓‘(𝑛 + 1)) = ((𝐻‘𝑛)‘(𝑓‘𝑛))))
 
14-Apr-2026depindlem3 16348 Lemma for depind 16349. (Contributed by Matthew House, 14-Apr-2026.)
(𝜑 → 𝑃:ℕ0⟶V)    &   (𝜑 → 𝐴 ∈ (𝑃‘0))    &   (𝜑 → ∀𝑛 ∈ ℕ0 (𝐻‘𝑛):(𝑃‘𝑛)⟶(𝑃‘(𝑛 + 1)))    &   𝐹 = seq0((𝑥 ∈ V, ℎ ∈ V ↦ (ℎ‘𝑥)), (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐴, (𝐻‘(𝑚 − 1)))))    ⇒   (𝜑 → ∀𝑓 ∈ X 𝑛 ∈ ℕ0 (𝑃‘𝑛)(((𝑓‘0) = 𝐴 ∧ ∀𝑛 ∈ ℕ0 (𝑓‘(𝑛 + 1)) = ((𝐻‘𝑛)‘(𝑓‘𝑛))) → 𝑓 = 𝐹))
 
14-Apr-2026depindlem2 16347 Lemma for depind 16349. (Contributed by Matthew House, 14-Apr-2026.)
(𝜑 → 𝑃:ℕ0⟶V)    &   (𝜑 → 𝐴 ∈ (𝑃‘0))    &   (𝜑 → ∀𝑛 ∈ ℕ0 (𝐻‘𝑛):(𝑃‘𝑛)⟶(𝑃‘(𝑛 + 1)))    &   𝐹 = seq0((𝑥 ∈ V, ℎ ∈ V ↦ (ℎ‘𝑥)), (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐴, (𝐻‘(𝑚 − 1)))))    ⇒   (𝜑 → 𝐹 ∈ X𝑛 ∈ ℕ0 (𝑃‘𝑛))
 
14-Apr-2026depindlem1 16346 Lemma for depind 16349. (Contributed by Matthew House, 14-Apr-2026.)
(𝜑 → 𝑃:ℕ0⟶V)    &   (𝜑 → 𝐴 ∈ (𝑃‘0))    &   (𝜑 → ∀𝑛 ∈ ℕ0 (𝐻‘𝑛):(𝑃‘𝑛)⟶(𝑃‘(𝑛 + 1)))    &   𝐹 = seq0((𝑥 ∈ V, ℎ ∈ V ↦ (ℎ‘𝑥)), (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐴, (𝐻‘(𝑚 − 1)))))    ⇒   (𝜑 → (𝐹:ℕ0⟶V ∧ (𝐹‘0) = 𝐴 ∧ ∀𝑛 ∈ ℕ0 (𝐹‘(𝑛 + 1)) = ((𝐻‘𝑛)‘(𝐹‘𝑛))))
 
8-Apr-2026gfsumcl 16708 Closure of a finite group sum. (Contributed by Jim Kingdon, 8-Apr-2026.)
𝐵 = (Base‘𝐺)    &    0 = (0g‘𝐺)    &   (𝜑 → 𝐺 ∈ CMnd)    &   (𝜑 → 𝐴 ∈ Fin)    &   (𝜑 → 𝐹:𝐴⟶𝐵)    ⇒   (𝜑 → (𝐺 Σgf 𝐹) ∈ 𝐵)
 
4-Apr-2026gsumsplit0 13935 Splitting off the rightmost summand of a group sum (even if it is the only summand). Similar to gsumsplit1r 13483 except that 𝑁 can equal 𝑀 − 1. (Contributed by Jim Kingdon, 4-Apr-2026.)
𝐵 = (Base‘𝐺)    &    + = (+g‘𝐺)    &   (𝜑 → 𝐺 ∈ Mnd)    &   (𝜑 → 𝑀 ∈ ℤ)    &   (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑀 − 1)))    &   (𝜑 → 𝐹:(𝑀...(𝑁 + 1))⟶𝐵)    ⇒   (𝜑 → (𝐺 Σg 𝐹) = ((𝐺 Σg (𝐹 ↾ (𝑀...𝑁))) + (𝐹‘(𝑁 + 1))))
 
4-Apr-2026fzf1o 11938 A finite set can be enumerated by integers starting at one. (Contributed by Jim Kingdon, 4-Apr-2026.)
(𝐴 ∈ Fin → ∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)
 
3-Apr-2026gfsump1 16707 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.)
𝐵 = (Base‘𝐺)    &    + = (+g‘𝐺)    &   (𝜑 → 𝐺 ∈ CMnd)    &   (𝜑 → 𝐹:(𝑌 ∪ {𝑍})⟶𝐵)    &   (𝜑 → 𝑌 ∈ Fin)    &   (𝜑 → 𝑍 ∈ 𝑉)    &   (𝜑 → ¬ 𝑍 ∈ 𝑌)    ⇒   (𝜑 → (𝐺 Σgf 𝐹) = ((𝐺 Σgf (𝐹 ↾ 𝑌)) + (𝐹‘𝑍)))
 
2-Apr-2026gfsumsn 16706 Group sum of a singleton. (Contributed by Jim Kingdon, 2-Apr-2026.)
𝐵 = (Base‘𝐺)    &   (𝑘 = 𝑀 → 𝐴 = 𝐶)    ⇒   ((𝐺 ∈ CMnd ∧ 𝑀 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵) → (𝐺 Σgf (𝑘 ∈ {𝑀} ↦ 𝐴)) = 𝐶)
 
31-Mar-2026sspw1or2 7403 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.)
{𝑥 ∈ {𝑠 ∈ 𝒫 𝑉 ∣ ∃𝑗 𝑗 ∈ 𝑠} ∣ (𝑥 ≈ 1o ∨ 𝑥 ≈ 2o)} = {𝑥 ∈ 𝒫 𝑉 ∣ (𝑥 ≈ 1o ∨ 𝑥 ≈ 2o)}
 
28-Mar-2026imaf1fi 7125 The image of a finite set under a one-to-one mapping is finite. (Contributed by Jim Kingdon, 28-Mar-2026.)
((𝐹:𝐴–1-1→𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑋 ∈ Fin) → (𝐹 “ 𝑋) ∈ Fin)
 
26-Mar-2026gsumgfsumlem 16704 Shifting the indexes of a group sum indexed by consecutive integers. (Contributed by Jim Kingdon, 26-Mar-2026.)
𝐵 = (Base‘𝐺)    &   (𝜑 → 𝐺 ∈ CMnd)    &   (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   (𝜑 → 𝐹:(𝑀...𝑁)⟶𝐵)    &   𝑆 = (𝑗 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑗 − (1 − 𝑀)))    ⇒   (𝜑 → (𝐺 Σg 𝐹) = (𝐺 Σg (𝐹 ∘ 𝑆)))
 
26-Mar-2026gfsum0 16703 An empty finite group sum is the identity. (Contributed by Jim Kingdon, 26-Mar-2026.)
(𝐺 ∈ CMnd → (𝐺 Σgf ∅) = (0g‘𝐺))
 
25-Mar-2026gsumgfsum 16705 On an integer range, Σg and Σgf agree. (Contributed by Jim Kingdon, 25-Mar-2026.)
𝐵 = (Base‘𝐺)    &   (𝜑 → 𝐺 ∈ CMnd)    &   (𝜑 → 𝑀 ∈ ℤ)    &   (𝜑 → 𝑁 ∈ ℤ)    &   (𝜑 → 𝐹:(𝑀...𝑁)⟶𝐵)    ⇒   (𝜑 → (𝐺 Σg 𝐹) = (𝐺 Σgf 𝐹))
 
25-Mar-2026gsumgfsum1 16702 On an integer range starting at one, Σg and Σgf agree. (Contributed by Jim Kingdon, 25-Mar-2026.)
𝐵 = (Base‘𝐺)    &   (𝜑 → 𝐺 ∈ CMnd)    &   (𝜑 → 𝑁 ∈ ℕ0)    &   (𝜑 → 𝐹:(1...𝑁)⟶𝐵)    ⇒   (𝜑 → (𝐺 Σg 𝐹) = (𝐺 Σgf 𝐹))
 
24-Mar-2026gfsumval 16701 Value of the finite group sum over an unordered finite set. (Contributed by Jim Kingdon, 24-Mar-2026.)
𝐵 = (Base‘𝑊)    &   (𝜑 → 𝑊 ∈ CMnd)    &   (𝜑 → 𝐹:𝐴⟶𝐵)    &   (𝜑 → 𝐴 ∈ Fin)    &   (𝜑 → 𝐺:(1...(♯‘𝐴))–1-1-onto→𝐴)    ⇒   (𝜑 → (𝑊 Σgf 𝐹) = (𝑊 Σg (𝐹 ∘ 𝐺)))
 
23-Mar-2026df-gfsum 16700 Define the finite group sum (iterated sum) over an unordered finite set. As currently defined, df-igsum 13344 is indexed by consecutive integers, but in the case of a commutative monoid, the order of the sum doesn't matter and we can define a sum indexed by any finite set without needing to specify an order. (Contributed by Jim Kingdon, 23-Mar-2026.)
Σgf = (𝑤 ∈ CMnd, 𝑓 ∈ V ↦ (℩𝑥(dom 𝑓 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑤 Σg (𝑓 ∘ 𝑔))))))
 
20-Mar-2026exmidssfi 7131 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 ↔ ∀𝑥∀𝑦((𝑥 ∈ Fin ∧ 𝑦 ⊆ 𝑥) → 𝑦 ∈ Fin))
 
18-Mar-2026umgr1een 15979 A graph with one non-loop edge is a multigraph. (Contributed by Jim Kingdon, 18-Mar-2026.)
(𝜑 → 𝐾 ∈ 𝑋)    &   (𝜑 → 𝑉 ∈ 𝑌)    &   (𝜑 → 𝐸 ∈ 𝒫 𝑉)    &   (𝜑 → 𝐸 ≈ 2o)    ⇒   (𝜑 → ⟨𝑉, {⟨𝐾, 𝐸⟩}⟩ ∈ UMGraph)
 
18-Mar-2026upgr1een 15978 A graph with one non-loop edge is a pseudograph. Variation of upgr1edc 15975 for a different way of specifying a graph with one edge. (Contributed by Jim Kingdon, 18-Mar-2026.)
(𝜑 → 𝐾 ∈ 𝑋)    &   (𝜑 → 𝑉 ∈ 𝑌)    &   (𝜑 → 𝐸 ∈ 𝒫 𝑉)    &   (𝜑 → 𝐸 ≈ 2o)    ⇒   (𝜑 → ⟨𝑉, {⟨𝐾, 𝐸⟩}⟩ ∈ UPGraph)
 
14-Mar-2026trlsex 16241 The class of trails on a graph is a set. (Contributed by Jim Kingdon, 14-Mar-2026.)
(𝐺 ∈ 𝑉 → (Trails‘𝐺) ∈ V)
 
13-Mar-2026eupthv 16300 The classes involved in a Eulerian path are sets. (Contributed by Jim Kingdon, 13-Mar-2026.)
(𝐹(EulerPaths‘𝐺)𝑃 → (𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V))
 
13-Mar-20261hevtxdg0fi 16161 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‘𝐺) = 𝑉)    &   (𝜑 → 𝐴 ∈ 𝑋)    &   (𝜑 → 𝐷 ∈ 𝑉)    &   (𝜑 → 𝑉 ∈ Fin)    &   (𝜑 → 𝐺 ∈ UPGraph)    &   (𝜑 → 𝐸 ∈ 𝑌)    &   (𝜑 → 𝐷 ∉ 𝐸)    ⇒   (𝜑 → ((VtxDeg‘𝐺)‘𝐷) = 0)
 
11-Mar-2026en1hash 11063 A set equinumerous to the ordinal one has size 1 . (Contributed by Jim Kingdon, 11-Mar-2026.)
(𝐴 ≈ 1o → (♯‘𝐴) = 1)
 
4-Mar-2026elmpom 6403 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-2026isclwwlkni 16261 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 16252 Existence of the set of closed walks (represented by words). (Contributed by Jim Kingdon, 21-Feb-2026.)
(𝐺 ∈ 𝑉 → (ClWWalks‘𝐺) ∈ V)
 
17-Feb-2026vtxdgfif 16147 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 16144 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 16143 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 7095 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 16611 The powerset of 1o is not infinite. Since we cannot prove it is finite (see pw1fin 7102), this provides a concrete example of a set which we cannot show to be finite or infinite, as seen another way at inffiexmid 7098. (Contributed by Jim Kingdon, 14-Feb-2026.)
¬ ω ≼ 𝒫 1o
 
14-Feb-2026pw1ndom3 16610 The powerset of 1o does not dominate 3o. This is another way of saying that 𝒫 1o does not have three elements (like pwntru 4289). (Contributed by Steven Nguyen and Jim Kingdon, 14-Feb-2026.)
¬ 3o ≼ 𝒫 1o
 
14-Feb-2026pw1ndom3lem 16609 Lemma for pw1ndom3 16610. (Contributed by Jim Kingdon, 14-Feb-2026.)
(𝜑 → 𝑋 ∈ 𝒫 1o)    &   (𝜑 → 𝑌 ∈ 𝒫 1o)    &   (𝜑 → 𝑍 ∈ 𝒫 1o)    &   (𝜑 → 𝑋 ≠ 𝑌)    &   (𝜑 → 𝑋 ≠ 𝑍)    &   (𝜑 → 𝑌 ≠ 𝑍)    ⇒   (𝜑 → 𝑋 = ∅)
 
12-Feb-2026pw1dceq 16626 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 16608 A set that dominates ordinal 3 has at least 3 different members. (Contributed by Jim Kingdon, 12-Feb-2026.)
(3o ≼ 𝐴 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧))
 
11-Feb-2026elssdc 7094 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 16145 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 7088 Equinumerosity of finite sets is decidable. (Contributed by Jim Kingdon, 10-Feb-2026.)
((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → DECID 𝐴 ≈ 𝐵)
 
8-Feb-2026wlkvtxm 16194 A graph with a walk has at least one vertex. (Contributed by Jim Kingdon, 8-Feb-2026.)
𝑉 = (Vtx‘𝐺)    ⇒   (𝐹(Walks‘𝐺)𝑃 → ∃𝑥 𝑥 ∈ 𝑉)
 
7-Feb-2026trlsv 16238 The classes involved in a trail are sets. (Contributed by Jim Kingdon, 7-Feb-2026.)
(𝐹(Trails‘𝐺)𝑃 → (𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V))
 
7-Feb-2026wlkex 16179 The class of walks on a graph is a set. (Contributed by Jim Kingdon, 7-Feb-2026.)
(𝐺 ∈ 𝑉 → (Walks‘𝐺) ∈ V)
 
3-Feb-2026dom1oi 7003 A set with an element dominates one. (Contributed by Jim Kingdon, 3-Feb-2026.)
((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝐴) → 1o ≼ 𝐴)
 
2-Feb-2026edginwlkd 16209 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 16203 A walk is an ordered pair. (Contributed by Jim Kingdon, 2-Feb-2026.)
(𝑊 ∈ (Walks‘𝐺) → 𝑊 ∈ (V × V))
 
1-Feb-2026wlkcprim 16204 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 16173 If there are walks on a graph, the graph is a set. (Contributed by Jim Kingdon, 1-Feb-2026.)
(𝑊 ∈ (Walks‘𝐺) → 𝐺 ∈ V)
 
31-Jan-2026fvmbr 5674 If a function value is inhabited, the argument is related to the function value. (Contributed by Jim Kingdon, 31-Jan-2026.)
(𝐴 ∈ (𝐹‘𝑋) → 𝑋𝐹(𝐹‘𝑋))
 
30-Jan-2026elfvfvex 5673 If a function value is inhabited, the function value is a set. (Contributed by Jim Kingdon, 30-Jan-2026.)
(𝐴 ∈ (𝐹‘𝐵) → (𝐹‘𝐵) ∈ V)
 
30-Jan-2026reldmm 4950 A relation is inhabited iff its domain is inhabited. (Contributed by Jim Kingdon, 30-Jan-2026.)
(Rel 𝐴 → (∃𝑥 𝑥 ∈ 𝐴 ↔ ∃𝑦 𝑦 ∈ dom 𝐴))
 
25-Jan-2026ifp2 988 Forward direction of dfifp2dc 989. This direction does not require decidability. (Contributed by Jim Kingdon, 25-Jan-2026.)
(if-(𝜑, 𝜓, 𝜒) → ((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜒)))
 
25-Jan-2026ifpdc 987 The conditional operator for propositions implies decidability. (Contributed by Jim Kingdon, 25-Jan-2026.)
(if-(𝜑, 𝜓, 𝜒) → DECID 𝜑)
 
20-Jan-2026cats1fvd 11348 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 11347 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 11351 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 11350 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 11349 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 2638 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 16009 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 7398 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 16618 Equinumerosity of (𝒫 1o ↑𝑚 𝐴) and the set of subsets of 𝐴. (Contributed by Jim Kingdon, 10-Jan-2026.)
(𝐴 ∈ 𝑉 → (𝒫 1o ↑𝑚 𝐴) ≈ 𝒫 𝐴)
 
10-Jan-2026pw1if 7443 Expressing a truth value in terms of an if expression. (Contributed by Jim Kingdon, 10-Jan-2026.)
(𝐴 ∈ 𝒫 1o → if(𝐴 = 1o, 1o, ∅) = 𝐴)
 
10-Jan-2026pw1m 7442 A truth value which is inhabited is equal to true. This is a variation of pwntru 4289 and pwtrufal 16619. (Contributed by Jim Kingdon, 10-Jan-2026.)
((𝐴 ∈ 𝒫 1o ∧ ∃𝑥 𝑥 ∈ 𝐴) → 𝐴 = 1o)
 
10-Jan-20261ndom2 7051 Two is not dominated by one. (Contributed by Jim Kingdon, 10-Jan-2026.)
¬ 2o ≼ 1o
 
9-Jan-2026pw1map 16617 Mapping between (𝒫 1o ↑𝑚 𝐴) and subsets of 𝐴. (Contributed by Jim Kingdon, 9-Jan-2026.)
𝐹 = (𝑠 ∈ (𝒫 1o ↑𝑚 𝐴) ↦ {𝑧 ∈ 𝐴 ∣ (𝑠‘𝑧) = 1o})    ⇒   (𝐴 ∈ 𝑉 → 𝐹:(𝒫 1o ↑𝑚 𝐴)–1-1-onto→𝒫 𝐴)
 
9-Jan-2026iftrueb01 7441 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 11261 Closure of the prefix extractor. This extends pfxclg 11260 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 11259 The domain of the prefix extractor. (Contributed by Jim Kingdon, 8-Jan-2026.)
prefix Fn (V × ℕ0)
 
7-Jan-2026pr1or2 7399 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 15974 Lemma for upgr1edc 15975. (Contributed by AV, 16-Oct-2020.) (Revised by Jim Kingdon, 6-Jan-2026.)
(𝜑 → {𝐵, 𝐶} ∈ 𝑆)    &   (𝜑 → 𝐵 ∈ 𝑊)    &   (𝜑 → 𝐶 ∈ 𝑋)    &   (𝜑 → DECID 𝐵 = 𝐶)    ⇒   (𝜑 → {{𝐵, 𝐶}} ⊆ {𝑥 ∈ 𝑆 ∣ (𝑥 ≈ 1o ∨ 𝑥 ≈ 2o)})
 
3-Jan-2026df-umgren 15948 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 15947 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 15948). (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 7002 Two ways of saying that a set is inhabited. (Contributed by Jim Kingdon, 3-Jan-2026.)
(𝐴 ∈ 𝑉 → (1o ≼ 𝐴 ↔ ∃𝑗 𝑗 ∈ 𝐴))
 
3-Jan-2026en2m 6999 A set with two elements is inhabited. (Contributed by Jim Kingdon, 3-Jan-2026.)
(𝐴 ≈ 2o → ∃𝑥 𝑥 ∈ 𝐴)
 
3-Jan-2026en1m 6979 A set with one element is inhabited. (Contributed by Jim Kingdon, 3-Jan-2026.)
(𝐴 ≈ 1o → ∃𝑥 𝑥 ∈ 𝐴)
 
31-Dec-2025pw0ss 15937 There are no inhabited subsets of the empty set. (Contributed by Jim Kingdon, 31-Dec-2025.)
{𝑠 ∈ 𝒫 ∅ ∣ ∃𝑗 𝑗 ∈ 𝑠} = ∅
 
31-Dec-2025df-ushgrm 15924 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 15923 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 15873 Applying the indexed edge function yields a set. (Contributed by Jim Kingdon, 29-Dec-2025.)
(𝐺 ∈ 𝑉 → (iEdg‘𝐺) ∈ V)
 
29-Dec-2025vtxex 15872 Applying the vertex function yields a set. (Contributed by Jim Kingdon, 29-Dec-2025.)
(𝐺 ∈ 𝑉 → (Vtx‘𝐺) ∈ V)
 
29-Dec-2025snmb 3793 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 11166 Existence of the last symbol. The last symbol of a word is a set. See lsw0g 11163 or lswcl 11165 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 11229 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 11172 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 11161 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 13203 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 15886 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 15885 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 15884 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 15883 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 11108 Two equivalent ways to say a set has two elements. (Contributed by Jim Kingdon, 4-Dec-2025.)
(𝑉 ≈ 2o ↔ (𝑉 ∈ Fin ∧ (♯‘𝑉) = 2))
 
30-Nov-2025nninfnfiinf 16646 An element of ℕ∞ which is not finite is infinite. (Contributed by Jim Kingdon, 30-Nov-2025.)
((𝐴 ∈ ℕ∞ ∧ ¬ ∃𝑛 ∈ ω 𝐴 = (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) → 𝐴 = (𝑖 ∈ ω ↦ 1o))
 
30-Nov-2025eluz3nn 9801 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.)
(𝑁 ∈ (ℤ≥‘3) → 𝑁 ∈ ℕ)
 
27-Nov-2025psrelbasfi 14693 Simpler form of psrelbas 14692 when the index set is finite. (Contributed by Jim Kingdon, 27-Nov-2025.)
𝑆 = (𝐼 mPwSer 𝑅)    &   𝐾 = (Base‘𝑅)    &   (𝜑 → 𝐼 ∈ Fin)    &   𝐵 = (Base‘𝑆)    &   (𝜑 → 𝑋 ∈ 𝐵)    ⇒   (𝜑 → 𝑋:(ℕ0 ↑𝑚 𝐼)⟶𝐾)
 
26-Nov-2025mplsubgfileminv 14717 Lemma for mplsubgfi 14718. 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 14716 Lemma for mplsubgfi 14718. The sum of two polynomials is a polynomial. (Contributed by Jim Kingdon, 26-Nov-2025.)
𝑆 = (𝐼 mPwSer 𝑅)    &   𝑃 = (𝐼 mPoly 𝑅)    &   𝑈 = (Base‘𝑃)    &   (𝜑 → 𝐼 ∈ Fin)    &   (𝜑 → 𝑅 ∈ Grp)    &   (𝜑 → 𝑋 ∈ 𝑈)    &   (𝜑 → 𝑌 ∈ 𝑈)    &    + = (+g‘𝑆)    ⇒   (𝜑 → (𝑋 + 𝑌) ∈ 𝑈)
 
25-Nov-2025nninfinfwlpo 7379 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 7332). (Contributed by Jim Kingdon, 25-Nov-2025.)
(∀𝑥 ∈ ℕ∞ DECID 𝑥 = (𝑖 ∈ ω ↦ 1o) ↔ ω ∈ WOmni)
 
23-Nov-2025psrbagfi 14690 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 7384 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 14715 Lemma for mplsubgfi 14718. There exists a polynomial. (Contributed by Jim Kingdon, 21-Nov-2025.)
𝑆 = (𝐼 mPwSer 𝑅)    &   𝑃 = (𝐼 mPoly 𝑅)    &   𝑈 = (Base‘𝑃)    &   (𝜑 → 𝐼 ∈ Fin)    &   (𝜑 → 𝑅 ∈ Grp)    ⇒   (𝜑 → ∃𝑗 𝑗 ∈ 𝑈)
  Copyright terms: Public domain W3C HTML validation [external]