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 31-May-2026 at 7:20 AM ET.
Recent Additions to the Intuitionistic Logic Explorer
DateLabelDescription
Theorem
 
24-May-2026gfsumz 16855 Value of a finite group sum over the zero element. (Contributed by Jim Kingdon, 24-May-2026.)
0 = (0g‘𝐺)    ⇒   ((𝐺 ∈ CMnd ∧ 𝐴 ∈ Fin) → (𝐺 Σgf (𝑘 ∈ 𝐴 ↦ 0 )) = 0 )
 
22-May-2026sshashneg 11198 Subsets of a class of a negative size (a degenerate case). Together with ssenneg 11197 this shows that sseqn 11196 could not be extended beyond 𝑁 ∈ ℕ0. (Contributed by Jim Kingdon, 22-May-2026.)
((𝑁 ∈ ℤ ∧ 𝑁 < 0) → {𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∣ (♯‘𝑥) = 𝑁} = ∅)
 
22-May-2026ssenneg 11197 Subsets of a class of a negative size (a degenerate case). Together with sshashneg 11198 this shows that sseqn 11196 could not be extended beyond 𝑁 ∈ ℕ0. (Contributed by Jim Kingdon, 22-May-2026.)
((𝑁 ∈ ℤ ∧ 𝑁 < 0) → {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≈ (1...𝑁)} = {∅})
 
22-May-2026sseqn 11196 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 11139 or something similar. Although each side of the equality would be well defined if we changed 𝑁 ∈ ℕ0 to 𝑁 ∈ ℤ, they would give different results for the (degenerate) case of a negative size, as shown at ssenneg 11197 and sshashneg 11198. (Contributed by Jim Kingdon, 22-May-2026.)
(𝑁 ∈ ℕ0 → {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≈ (1...𝑁)} = {𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∣ (♯‘𝑥) = 𝑁})
 
20-May-2026ballotfilemofi 13131 𝑂 is finite. (Contributed by Jim Kingdon, 20-May-2026.)
𝑀 ∈ ℕ    &   𝑁 ∈ ℕ    &   𝑂 = {𝑐 ∈ (𝒫 (1...(𝑀 + 𝑁)) ∩ Fin) ∣ (♯‘𝑐) = 𝑀}    ⇒   𝑂 ∈ Fin
 
19-May-2026fipwfi 7271 The set of finite subsets of a finite set is finite. (Contributed by Jim Kingdon, 19-May-2026.)
(𝐴 ∈ Fin → (𝒫 𝐴 ∩ Fin) ∈ Fin)
 
18-May-20262omapfi 7270 The number of finite subsets of a finite set. (Contributed by Jim Kingdon, 18-May-2026.)
(𝐴 ∈ Fin → (2o ↑𝑚 𝐴) ≈ (𝒫 𝐴 ∩ Fin))
 
18-May-2026fissfi 7215 A finite subset of a finite set is a decidable subset. (Contributed by Jim Kingdon, 18-May-2026.)
((𝑆 ⊆ 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝑆 ∈ Fin) → ∀𝑥 ∈ 𝐴 DECID 𝑥 ∈ 𝑆)
 
18-May-2026fresaunres1disj 5545 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-2026fresaunres2disj 5544 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-2026fsuppcorn 7253 The composition of a 1-1 function with a finitely supported function is finitely supported. The purpose of the (𝐹 supp 𝑍) ⊆ ran 𝐺 condition is to ensure we don't subset the support of the function in such a way as to fun afoul of exmidssfi 7198. (Other alternative conditions might also be sufficient). (Contributed by AV, 28-May-2019.) (Revised by Jim Kingdon, 15-May-2026.)
(𝜑 → 𝐹 finSupp 𝑍)    &   (𝜑 → 𝐺:𝑋–1-1→𝑌)    &   (𝜑 → 𝑍 ∈ 𝑊)    &   (𝜑 → 𝐹 ∈ 𝑉)    &   (𝜑 → 𝐺 ∈ 𝑈)    &   (𝜑 → (𝐹 supp 𝑍) ⊆ ran 𝐺)    ⇒   (𝜑 → (𝐹 ∘ 𝐺) finSupp 𝑍)
 
13-May-2026lincmble 10333 A linear combination of two reals which lies in the interval between them. Like lincmb01cmp 10332 but generalized to require merely 𝐴 ≤ 𝐵 not 𝐴 < 𝐵. (Contributed by Jim Kingdon, 13-May-2026.)
(((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) ∧ 𝑇 ∈ (0[,]1)) → (((1 − 𝑇) · 𝐴) + (𝑇 · 𝐵)) ∈ (𝐴[,]𝐵))
 
5-May-2026fmelpw1o 7556 With a formula 𝜑 one can associate an element of 𝒫 1o, 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 859, which translate to 1o and ∅ respectively by iftrue 3626 and iffalse 3629, giving pwtrufal 16758).

As proved in if0ab 3622, the associated element of 𝒫 1o is the extension, in 𝒫 1o, of the formula 𝜑. (Contributed by BJ, 15-Aug-2024.) (Proof shortened by BJ, 5-May-2026.)

if(𝜑, 1o, ∅) ∈ 𝒫 1o
 
5-May-2026if0elpw 4270 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 4601. (Contributed by BJ, 5-May-2026.)
(𝐴 ∈ 𝑉 → if(𝜑, 𝐴, ∅) ∈ 𝒫 𝐴)
 
5-May-2026if0ss 3623 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.)
if(𝜑, 𝐴, ∅) ⊆ 𝐴
 
27-Apr-2026repiecef 16799 Piecewise definition on the reals yields a function. The function agrees with 𝐹 and 𝐺 on their respective parts of the real line; see repiecele0 16797 and repiecege0 16798. 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. 16798 (Contributed by Jim Kingdon, 27-Apr-2026.)
(𝜑 → 𝐹:(-∞(,]0)⟶ℝ)    &   (𝜑 → 𝐺:(0[,)+∞)⟶ℝ)    &   (𝜑 → (𝐹‘0) = (𝐺‘0))    &   𝐻 = (𝑥 ∈ ℝ ↦ (((𝐹‘inf({𝑥, 0}, ℝ, < )) + (𝐺‘sup({𝑥, 0}, ℝ, < ))) − (𝐹‘0)))    ⇒   (𝜑 → 𝐻:ℝ⟶ℝ)
 
27-Apr-2026repiecege0 16798 Piecewise definition on the reals agrees with the nonnegative part of the definition. See repiecef 16799 for more on this construction. (Contributed by Jim Kingdon, 27-Apr-2026.)
(𝜑 → 𝐹:(-∞(,]0)⟶ℝ)    &   (𝜑 → 𝐺:(0[,)+∞)⟶ℝ)    &   (𝜑 → (𝐹‘0) = (𝐺‘0))    &   𝐻 = (𝑥 ∈ ℝ ↦ (((𝐹‘inf({𝑥, 0}, ℝ, < )) + (𝐺‘sup({𝑥, 0}, ℝ, < ))) − (𝐹‘0)))    ⇒   ((𝜑 ∧ 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (𝐻‘𝐴) = (𝐺‘𝐴))
 
27-Apr-2026repiecele0 16797 Piecewise definition on the reals agrees with the nonpositive part of the definition. See repiecef 16799 for more on this construction. (Contributed by Jim Kingdon, 27-Apr-2026.)
(𝜑 → 𝐹:(-∞(,]0)⟶ℝ)    &   (𝜑 → 𝐺:(0[,)+∞)⟶ℝ)    &   (𝜑 → (𝐹‘0) = (𝐺‘0))    &   𝐻 = (𝑥 ∈ ℝ ↦ (((𝐹‘inf({𝑥, 0}, ℝ, < )) + (𝐺‘sup({𝑥, 0}, ℝ, < ))) − (𝐹‘0)))    ⇒   ((𝜑 ∧ 𝐴 ∈ ℝ ∧ 𝐴 ≤ 0) → (𝐻‘𝐴) = (𝐹‘𝐴))
 
27-Apr-2026repiecelem 16796 Lemma for repiecele0 16797, repiecege0 16798, and repiecef 16799. The function 𝐻 is defined everywhere. (Contributed by Jim Kingdon, 27-Apr-2026.)
(𝜑 → 𝐹:(-∞(,]0)⟶ℝ)    &   (𝜑 → 𝐺:(0[,)+∞)⟶ℝ)    &   (𝜑 → (𝐹‘0) = (𝐺‘0))    &   𝐻 = (𝑥 ∈ ℝ ↦ (((𝐹‘inf({𝑥, 0}, ℝ, < )) + (𝐺‘sup({𝑥, 0}, ℝ, < ))) − (𝐹‘0)))    ⇒   ((𝜑 ∧ 𝐴 ∈ ℝ) → (((𝐹‘inf({𝐴, 0}, ℝ, < )) + (𝐺‘sup({𝐴, 0}, ℝ, < ))) − (𝐹‘0)) ∈ ℝ)
 
24-Apr-2026qdiff 16820 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 16819 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.)
(𝐴 ∈ ℝ → (𝐴 ∈ ℚ ↔ ∃𝑞 ∈ ℚ ∃𝑟 ∈ ℚ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))))
 
23-Apr-2026exmidpeirce 16768 Excluded middle is equivalent to Peirce's law. Read an element of 𝒫 1o as being a truth value and 𝑥 = 1o being that 𝑥 is true. For a similar theorem, but expressed in terms of formulas rather than subsets of 1o, see dcfrompeirce 1495. (Contributed by Jim Kingdon, 23-Apr-2026.)
(EXMID ↔ ∀𝑥 ∈ 𝒫 1o∀𝑦 ∈ 𝒫 1o(((𝑥 = 1o → 𝑦 = 1o) → 𝑥 = 1o) → 𝑥 = 1o))
 
22-Apr-2026exmidcon 16767 Excluded middle is equivalent to the form of contraposition which removes negation. Read an element of 𝒫 1o as being a truth value and 𝑥 = 1o being that 𝑥 is true. For a similar theorem, but expressed in terms of formulas rather than subsets of 1o, see dcfromcon 1494. (Contributed by Jim Kingdon, 22-Apr-2026.)
(EXMID ↔ ∀𝑥 ∈ 𝒫 1o∀𝑦 ∈ 𝒫 1o((¬ 𝑦 = 1o → ¬ 𝑥 = 1o) → (𝑥 = 1o → 𝑦 = 1o)))
 
22-Apr-2026exmidnotnotr 16766 Excluded middle is equivalent to double negation elimination. Read an element of 𝒫 1o as being a truth value and 𝑥 = 1o being that 𝑥 is true. For a similar theorem, but expressed in terms of formulas rather than subsets of 1o, see dcfromnotnotr 1493. (Contributed by Jim Kingdon, 22-Apr-2026.)
(EXMID ↔ ∀𝑥 ∈ 𝒫 1o(¬ ¬ 𝑥 = 1o → 𝑥 = 1o))
 
18-Apr-2026hashtpglem 11211 Lemma for hashtpg 11212. This is one of the three not-equal conclusions required for the reverse direction. (Contributed by Jim Kingdon, 18-Apr-2026.)
(𝜑 → 𝐴 ∈ 𝑈)    &   (𝜑 → 𝐵 ∈ 𝑉)    &   (𝜑 → 𝐶 ∈ 𝑊)    &   (𝜑 → (♯‘{𝐴, 𝐵, 𝐶}) = 3)    ⇒   (𝜑 → 𝐵 ≠ 𝐶)
 
17-Apr-2026hashtpgim 11210 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.)
((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → (♯‘{𝐴, 𝐵, 𝐶}) = 3))
 
14-Apr-2026depind 16491 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 16490 Lemma for depind 16491. (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 16489 Lemma for depind 16491. (Contributed by Matthew House, 14-Apr-2026.)
(𝜑 → 𝑃:ℕ0⟶V)    &   (𝜑 → 𝐴 ∈ (𝑃‘0))    &   (𝜑 → ∀𝑛 ∈ ℕ0 (𝐻‘𝑛):(𝑃‘𝑛)⟶(𝑃‘(𝑛 + 1)))    &   𝐹 = seq0((𝑥 ∈ V, ℎ ∈ V ↦ (ℎ‘𝑥)), (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐴, (𝐻‘(𝑚 − 1)))))    ⇒   (𝜑 → 𝐹 ∈ X𝑛 ∈ ℕ0 (𝑃‘𝑛))
 
14-Apr-2026depindlem1 16488 Lemma for depind 16491. (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 16856 Closure of a finite group sum. (Contributed by Jim Kingdon, 8-Apr-2026.)
𝐵 = (Base‘𝐺)    &    0 = (0g‘𝐺)    &   (𝜑 → 𝐺 ∈ CMnd)    &   (𝜑 → 𝐴 ∈ Fin)    &   (𝜑 → 𝐹:𝐴⟶𝐵)    ⇒   (𝜑 → (𝐺 Σgf 𝐹) ∈ 𝐵)
 
4-Apr-2026gsumsplit0 14052 Splitting off the rightmost summand of a group sum (even if it is the only summand). Similar to gsumsplit1r 13600 except that 𝑁 can equal 𝑀 − 1. (Contributed by Jim Kingdon, 4-Apr-2026.)
𝐵 = (Base‘𝐺)    &    + = (+g‘𝐺)    &   (𝜑 → 𝐺 ∈ Mnd)    &   (𝜑 → 𝑀 ∈ ℤ)    &   (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑀 − 1)))    &   (𝜑 → 𝐹:(𝑀...(𝑁 + 1))⟶𝐵)    ⇒   (𝜑 → (𝐺 Σg 𝐹) = ((𝐺 Σg (𝐹 ↾ (𝑀...𝑁))) + (𝐹‘(𝑁 + 1))))
 
4-Apr-2026fzf1o 12054 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 16854 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 16853 Group sum of a singleton. (Contributed by Jim Kingdon, 2-Apr-2026.)
𝐵 = (Base‘𝐺)    &   (𝑘 = 𝑀 → 𝐴 = 𝐶)    ⇒   ((𝐺 ∈ CMnd ∧ 𝑀 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵) → (𝐺 Σgf (𝑘 ∈ {𝑀} ↦ 𝐴)) = 𝐶)
 
31-Mar-2026sspw1or2 7494 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 7192 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 16851 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 16850 An empty finite group sum is the identity. (Contributed by Jim Kingdon, 26-Mar-2026.)
(𝐺 ∈ CMnd → (𝐺 Σgf ∅) = (0g‘𝐺))
 
25-Mar-2026gsumgfsum 16852 On an integer range, Σg and Σgf agree. (Contributed by Jim Kingdon, 25-Mar-2026.)
𝐵 = (Base‘𝐺)    &   (𝜑 → 𝐺 ∈ CMnd)    &   (𝜑 → 𝑀 ∈ ℤ)    &   (𝜑 → 𝑁 ∈ ℤ)    &   (𝜑 → 𝐹:(𝑀...𝑁)⟶𝐵)    ⇒   (𝜑 → (𝐺 Σg 𝐹) = (𝐺 Σgf 𝐹))
 
25-Mar-2026gsumgfsum1 16849 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 16848 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 16847 Define the finite group sum (iterated sum) over an unordered finite set. As currently defined, df-igsum 13461 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 7198 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 16107 A graph with one non-loop edge is a multigraph. (Contributed by Jim Kingdon, 18-Mar-2026.)
(𝜑 → 𝐾 ∈ 𝑋)    &   (𝜑 → 𝑉 ∈ 𝑌)    &   (𝜑 → 𝐸 ∈ 𝒫 𝑉)    &   (𝜑 → 𝐸 ≈ 2o)    ⇒   (𝜑 → ⟨𝑉, {⟨𝐾, 𝐸⟩}⟩ ∈ UMGraph)
 
18-Mar-2026upgr1een 16106 A graph with one non-loop edge is a pseudograph. Variation of upgr1edc 16103 for a different way of specifying a graph with one edge. (Contributed by Jim Kingdon, 18-Mar-2026.)
(𝜑 → 𝐾 ∈ 𝑋)    &   (𝜑 → 𝑉 ∈ 𝑌)    &   (𝜑 → 𝐸 ∈ 𝒫 𝑉)    &   (𝜑 → 𝐸 ≈ 2o)    ⇒   (𝜑 → ⟨𝑉, {⟨𝐾, 𝐸⟩}⟩ ∈ UPGraph)
 
14-Mar-2026trlsex 16369 The class of trails on a graph is a set. (Contributed by Jim Kingdon, 14-Mar-2026.)
(𝐺 ∈ 𝑉 → (Trails‘𝐺) ∈ V)
 
13-Mar-2026eupthv 16428 The classes involved in a Eulerian path are sets. (Contributed by Jim Kingdon, 13-Mar-2026.)
(𝐹(EulerPaths‘𝐺)𝑃 → (𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V))
 
13-Mar-20261hevtxdg0fi 16289 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 11158 A set equinumerous to the ordinal one has size 1 . (Contributed by Jim Kingdon, 11-Mar-2026.)
(𝐴 ≈ 1o → (♯‘𝐴) = 1)
 
4-Mar-2026elmpom 6433 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 16389 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 16380 Existence of the set of closed walks (represented by words). (Contributed by Jim Kingdon, 21-Feb-2026.)
(𝐺 ∈ 𝑉 → (ClWWalks‘𝐺) ∈ V)
 
17-Feb-2026vtxdgfif 16275 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 16272 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 16271 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 7162 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 16752 The powerset of 1o is not infinite. Since we cannot prove it is finite (see pw1fin 7169), this provides a concrete example of a set which we cannot show to be finite or infinite, as seen another way at inffiexmid 7165. (Contributed by Jim Kingdon, 14-Feb-2026.)
¬ ω ≼ 𝒫 1o
 
14-Feb-2026pw1ndom3 16751 The powerset of 1o does not dominate 3o. This is another way of saying that 𝒫 1o does not have three elements (like pwntru 4311). (Contributed by Steven Nguyen and Jim Kingdon, 14-Feb-2026.)
¬ 3o ≼ 𝒫 1o
 
14-Feb-2026pw1ndom3lem 16750 Lemma for pw1ndom3 16751. (Contributed by Jim Kingdon, 14-Feb-2026.)
(𝜑 → 𝑋 ∈ 𝒫 1o)    &   (𝜑 → 𝑌 ∈ 𝒫 1o)    &   (𝜑 → 𝑍 ∈ 𝒫 1o)    &   (𝜑 → 𝑋 ≠ 𝑌)    &   (𝜑 → 𝑋 ≠ 𝑍)    &   (𝜑 → 𝑌 ≠ 𝑍)    ⇒   (𝜑 → 𝑋 = ∅)
 
12-Feb-2026pw1dceq 16765 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 16749 A set that dominates ordinal 3 has at least 3 different members. (Contributed by Jim Kingdon, 12-Feb-2026.)
(3o ≼ 𝐴 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧))
 
11-Feb-2026elssdc 7161 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 16273 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 7155 Equinumerosity of finite sets is decidable. (Contributed by Jim Kingdon, 10-Feb-2026.)
((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → DECID 𝐴 ≈ 𝐵)
 
8-Feb-2026wlkvtxm 16322 A graph with a walk has at least one vertex. (Contributed by Jim Kingdon, 8-Feb-2026.)
𝑉 = (Vtx‘𝐺)    ⇒   (𝐹(Walks‘𝐺)𝑃 → ∃𝑥 𝑥 ∈ 𝑉)
 
7-Feb-2026trlsv 16366 The classes involved in a trail are sets. (Contributed by Jim Kingdon, 7-Feb-2026.)
(𝐹(Trails‘𝐺)𝑃 → (𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V))
 
7-Feb-2026wlkex 16307 The class of walks on a graph is a set. (Contributed by Jim Kingdon, 7-Feb-2026.)
(𝐺 ∈ 𝑉 → (Walks‘𝐺) ∈ V)
 
3-Feb-2026dom1oi 7069 A set with an element dominates one. (Contributed by Jim Kingdon, 3-Feb-2026.)
((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝐴) → 1o ≼ 𝐴)
 
2-Feb-2026edginwlkd 16337 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 16331 A walk is an ordered pair. (Contributed by Jim Kingdon, 2-Feb-2026.)
(𝑊 ∈ (Walks‘𝐺) → 𝑊 ∈ (V × V))
 
1-Feb-2026wlkcprim 16332 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 16301 If there are walks on a graph, the graph is a set. (Contributed by Jim Kingdon, 1-Feb-2026.)
(𝑊 ∈ (Walks‘𝐺) → 𝐺 ∈ V)
 
31-Jan-2026fvmbr 5704 If a function value is inhabited, the argument is related to the function value. (Contributed by Jim Kingdon, 31-Jan-2026.)
(𝐴 ∈ (𝐹‘𝑋) → 𝑋𝐹(𝐹‘𝑋))
 
30-Jan-2026elfvfvex 5703 If a function value is inhabited, the function value is a set. (Contributed by Jim Kingdon, 30-Jan-2026.)
(𝐴 ∈ (𝐹‘𝐵) → (𝐹‘𝐵) ∈ V)
 
30-Jan-2026reldmm 4974 A relation is inhabited iff its domain is inhabited. (Contributed by Jim Kingdon, 30-Jan-2026.)
(Rel 𝐴 → (∃𝑥 𝑥 ∈ 𝐴 ↔ ∃𝑦 𝑦 ∈ dom 𝐴))
 
25-Jan-2026ifp2 989 Forward direction of dfifp2dc 990. This direction does not require decidability. (Contributed by Jim Kingdon, 25-Jan-2026.)
(if-(𝜑, 𝜓, 𝜒) → ((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜒)))
 
25-Jan-2026ifpdc 988 The conditional operator for propositions implies decidability. (Contributed by Jim Kingdon, 25-Jan-2026.)
(if-(𝜑, 𝜓, 𝜒) → DECID 𝜑)
 
20-Jan-2026cats1fvd 11451 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 11450 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 11454 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 11453 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 11452 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 2648 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 16137 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 7489 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 16757 Equinumerosity of (𝒫 1o ↑𝑚 𝐴) and the set of subsets of 𝐴. (Contributed by Jim Kingdon, 10-Jan-2026.)
(𝐴 ∈ 𝑉 → (𝒫 1o ↑𝑚 𝐴) ≈ 𝒫 𝐴)
 
10-Jan-2026pw1if 7534 Expressing a truth value in terms of an if expression. (Contributed by Jim Kingdon, 10-Jan-2026.)
(𝐴 ∈ 𝒫 1o → if(𝐴 = 1o, 1o, ∅) = 𝐴)
 
10-Jan-2026pw1m 7533 A truth value which is inhabited is equal to true. This is a variation of pwntru 4311 and pwtrufal 16758. (Contributed by Jim Kingdon, 10-Jan-2026.)
((𝐴 ∈ 𝒫 1o ∧ ∃𝑥 𝑥 ∈ 𝐴) → 𝐴 = 1o)
 
10-Jan-20261ndom2 7118 Two is not dominated by one. (Contributed by Jim Kingdon, 10-Jan-2026.)
¬ 2o ≼ 1o
 
9-Jan-2026pw1map 16756 Mapping between (𝒫 1o ↑𝑚 𝐴) and subsets of 𝐴. (Contributed by Jim Kingdon, 9-Jan-2026.)
𝐹 = (𝑠 ∈ (𝒫 1o ↑𝑚 𝐴) ↦ {𝑧 ∈ 𝐴 ∣ (𝑠‘𝑧) = 1o})    ⇒   (𝐴 ∈ 𝑉 → 𝐹:(𝒫 1o ↑𝑚 𝐴)–1-1-onto→𝒫 𝐴)
 
9-Jan-2026iftrueb01 7532 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 11364 Closure of the prefix extractor. This extends pfxclg 11363 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 11362 The domain of the prefix extractor. (Contributed by Jim Kingdon, 8-Jan-2026.)
prefix Fn (V × ℕ0)
 
7-Jan-2026pr1or2 7490 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 16102 Lemma for upgr1edc 16103. (Contributed by AV, 16-Oct-2020.) (Revised by Jim Kingdon, 6-Jan-2026.)
(𝜑 → {𝐵, 𝐶} ∈ 𝑆)    &   (𝜑 → 𝐵 ∈ 𝑊)    &   (𝜑 → 𝐶 ∈ 𝑋)    &   (𝜑 → DECID 𝐵 = 𝐶)    ⇒   (𝜑 → {{𝐵, 𝐶}} ⊆ {𝑥 ∈ 𝑆 ∣ (𝑥 ≈ 1o ∨ 𝑥 ≈ 2o)})
 
3-Jan-2026df-umgren 16076 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 16075 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 16076). (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 7068 Two ways of saying that a set is inhabited. (Contributed by Jim Kingdon, 3-Jan-2026.)
(𝐴 ∈ 𝑉 → (1o ≼ 𝐴 ↔ ∃𝑗 𝑗 ∈ 𝐴))
 
3-Jan-2026en2m 7065 A set with two elements is inhabited. (Contributed by Jim Kingdon, 3-Jan-2026.)
(𝐴 ≈ 2o → ∃𝑥 𝑥 ∈ 𝐴)
 
3-Jan-2026en1m 7044 A set with one element is inhabited. (Contributed by Jim Kingdon, 3-Jan-2026.)
(𝐴 ≈ 1o → ∃𝑥 𝑥 ∈ 𝐴)
  Copyright terms: Public domain W3C HTML validation [external]