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 20-Jun-2026 at 7:15 AM ET.
Recent Additions to the Intuitionistic Logic Explorer
DateLabelDescription
Theorem
 
8-Jun-2026ballotfilemdifcfi 13152 Lemma for ballotfi . The portion of an integer range which is not part of a particular element of 𝑂 is finite. (Contributed by Jim Kingdon, 8-Jun-2026.)
𝑀 ∈ ℕ    &   𝑁 ∈ ℕ    &   𝑂 = {𝑐 ∈ (𝒫 (1...(𝑀 + 𝑁)) ∩ Fin) ∣ (♯‘𝑐) = 𝑀}    &   (𝜑 → 𝐶 ∈ 𝑂)    &   (𝜑 → 𝐽 ∈ ℤ)    ⇒   (𝜑 → ((1...𝐽) ∖ 𝐶) ∈ Fin)
 
8-Jun-2026ballotfilemcinfi 13151 Lemma for ballotfi . The portion of a particular element of 𝑂 up to a specified integer is finite. (Contributed by Jim Kingdon, 8-Jun-2026.)
𝑀 ∈ ℕ    &   𝑁 ∈ ℕ    &   𝑂 = {𝑐 ∈ (𝒫 (1...(𝑀 + 𝑁)) ∩ Fin) ∣ (♯‘𝑐) = 𝑀}    &   (𝜑 → 𝐶 ∈ 𝑂)    &   (𝜑 → 𝐽 ∈ ℤ)    ⇒   (𝜑 → ((1...𝐽) ∩ 𝐶) ∈ Fin)
 
8-Jun-2026zfidc 9661 Whether an integer is an element of a finite set of integers is decidable. (Contributed by Jim Kingdon, 8-Jun-2026.)
((𝑆 ⊆ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝑆 ∈ Fin) → DECID 𝐴 ∈ 𝑆)
 
7-Jun-2026ballotfilemcdc 13150 Lemma for ballotfi . It is decidable whether a given integer is an element of a particular element of 𝑂. (Contributed by Jim Kingdon, 7-Jun-2026.)
𝑀 ∈ ℕ    &   𝑁 ∈ ℕ    &   𝑂 = {𝑐 ∈ (𝒫 (1...(𝑀 + 𝑁)) ∩ Fin) ∣ (♯‘𝑐) = 𝑀}    &   (𝜑 → 𝐶 ∈ 𝑂)    &   (𝜑 → 𝐾 ∈ ℤ)    ⇒   (𝜑 → DECID 𝐾 ∈ 𝐶)
 
5-Jun-2026hashpwfi 11201 The number of finite subsets of a finite set is two raised to the power of the size of the set. For a similar theorem with set size expressed using equinumerosity, see 2omapfi 7273. For the number of subsets (which need not be finite) of a set, see pw1mapen 16819. (Contributed by Jim Kingdon, 5-Jun-2026.)
(𝐴 ∈ Fin → (♯‘(𝒫 𝐴 ∩ Fin)) = (2↑(♯‘𝐴)))
 
4-Jun-2026ballotfilemonn 13148 The size of the universe is at least one. (Contributed by Jim Kingdon, 4-Jun-2026.)
𝑀 ∈ ℕ    &   𝑁 ∈ ℕ    &   𝑂 = {𝑐 ∈ (𝒫 (1...(𝑀 + 𝑁)) ∩ Fin) ∣ (♯‘𝑐) = 𝑀}    ⇒   (♯‘𝑂) ∈ ℕ
 
3-Jun-2026papeq2 7563 Equality theorem for apartness predicate. (Contributed by Jim Kingdon, 3-Jun-2026.)
(𝐴 = 𝐵 → (𝑅 Ap 𝐴 ↔ 𝑅 Ap 𝐵))
 
3-Jun-2026papeq1 7562 Equality theorem for apartness predicate. (Contributed by Jim Kingdon, 3-Jun-2026.)
(𝑅 = 𝑆 → (𝑅 Ap 𝐴 ↔ 𝑆 Ap 𝐴))
 
2-Jun-2026resq01 11027 If a real number equals its square, it must be 0 or 1. (Contributed by Jim Kingdon, 2-Jun-2026.)
(𝐴 ∈ ℝ → ((𝐴↑2) = 𝐴 ↔ (𝐴 = 0 ∨ 𝐴 = 1)))
 
31-May-2026aprprop 14461 If two structures have the same ring components (properties), df-apr 14450 generates the same relation for both of them. (Contributed by Jim Kingdon, 31-May-2026.)
(Base‘𝐾) = (Base‘𝐿)    &   (+g‘𝐾) = (+g‘𝐿)    &   (.r‘𝐾) = (.r‘𝐿)    ⇒   (𝐾 ∈ Ring → (#r‘𝐾) = (#r‘𝐿))
 
31-May-2026ringunitsap0 14454 The set of units of a ring. If 𝑅 is a local ring, # is an apartness and this theorem states that the units of a ring are those elements apart from zero (see aprlring 14460). Given the definition of #r this theorem holds even if # is not an apartness, however. (Contributed by Jim Kingdon, 31-May-2026.)
𝐵 = (Base‘𝑅)    &    0 = (0g‘𝑅)    &    # = (#r‘𝑅)    ⇒   (𝑅 ∈ Ring → {𝑥 ∈ 𝐵 ∣ 𝑥 # 0 } = (Unit‘𝑅))
 
30-May-2026ringunitap 14453 Elementhood in the set of units. (Contributed by Jim Kingdon, 30-May-2026.)
𝐵 = (Base‘𝑅)    &   𝑈 = (Unit‘𝑅)    &    0 = (0g‘𝑅)    &    # = (#r‘𝑅)    ⇒   (𝑅 ∈ Ring → (𝑋 ∈ 𝑈 ↔ (𝑋 ∈ 𝐵 ∧ 𝑋 # 0 )))
 
29-May-2026drnglring 14467 A division ring is a local ring. (Contributed by Jim Kingdon, 29-May-2026.)
(𝑅 ∈ DivRing → 𝑅 ∈ LRing)
 
29-May-2026isdrngtap 14466 The predicate "is a division ring". (Contributed by Jim Kingdon, 29-May-2026.)
𝐵 = (Base‘𝑅)    &    # = (#r‘𝑅)    ⇒   (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧ # TAp 𝐵))
 
29-May-2026df-drngap 14464 Define class of all division rings. A division ring is a ring in which the relation given by df-apr 14450 is a tight apartness. (Contributed by Jim Kingdon, 29-May-2026.)
DivRing = {𝑟 ∈ Ring ∣ (#r‘𝑟) TAp (Base‘𝑟)}
 
29-May-2026aprunit 14452 The df-apr 14450 relation with zero expresses whether a ring element is a unit. That is, the difference of an element of a ring and zero is invertible iff the element is a unit. (Contributed by Jim Kingdon, 29-May-2026.)
𝐵 = (Base‘𝑅)    &    0 = (0g‘𝑅)    &   𝑈 = (Unit‘𝑅)    &    # = (#r‘𝑅)    &   (𝜑 → 𝑅 ∈ Ring)    &   (𝜑 → 𝑋 ∈ 𝐵)    ⇒   (𝜑 → (𝑋 # 0 ↔ 𝑋 ∈ 𝑈))
 
29-May-2026tapap 7569 A tight apartness is an apartness. (Contributed by Jim Kingdon, 29-May-2026.)
(𝑅 TAp 𝐴 → 𝑅 Ap 𝐴)
 
28-May-2026aprlring 14460 A ring is a local ring if and only if the relation given by df-apr 14450 is an apartness relation. (Contributed by Jim Kingdon, 28-May-2026.)
(𝑅 ∈ Ring → (𝑅 ∈ LRing ↔ (#r‘𝑅) Ap (Base‘𝑅)))
 
28-May-2026papcotr 7566 An apartness is cotransitive. (Contributed by Jim Kingdon, 28-May-2026.)
(𝜑 → 𝑅 Ap 𝐴)    &   (𝜑 → 𝑋 ∈ 𝐴)    &   (𝜑 → 𝑌 ∈ 𝐴)    &   (𝜑 → 𝑋𝑅𝑌)    &   (𝜑 → 𝑍 ∈ 𝐴)    ⇒   (𝜑 → (𝑋𝑅𝑍 ∨ 𝑌𝑅𝑍))
 
27-May-2026trimul0or 16894 Real number trichotomy implies that if a product is zero, one of its factors must be zero. (Contributed by Jim Kingdon, 27-May-2026.)
(∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥) → ∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ ((𝑢 · 𝑣) = 0 → (𝑢 = 0 ∨ 𝑣 = 0)))
 
27-May-2026aprnzr 14459 If the relation given by df-apr 14450 on a ring is an apartness relation, then the ring is a nonzero ring. (Contributed by Jim Kingdon, 27-May-2026.)
((𝑅 ∈ Ring ∧ (#r‘𝑅) Ap (Base‘𝑅)) → 𝑅 ∈ NzRing)
 
27-May-2026papsym 7565 An apartness is symmetric. (Contributed by Jim Kingdon, 27-May-2026.)
(𝜑 → 𝑅 Ap 𝐴)    &   (𝜑 → 𝑋 ∈ 𝐴)    &   (𝜑 → 𝑌 ∈ 𝐴)    &   (𝜑 → 𝑋𝑅𝑌)    ⇒   (𝜑 → 𝑌𝑅𝑋)
 
27-May-2026papirr 7564 An apartness is irreflexive. (Contributed by Jim Kingdon, 27-May-2026.)
((𝑅 Ap 𝐴 ∧ 𝑋 ∈ 𝐴) → ¬ 𝑋𝑅𝑋)
 
24-May-2026gfsumz 16918 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 11213 Subsets of a class of a negative size (a degenerate case). Together with ssenneg 11212 this shows that sseqn 11211 could not be extended beyond 𝑁 ∈ ℕ0. (Contributed by Jim Kingdon, 22-May-2026.)
((𝑁 ∈ ℤ ∧ 𝑁 < 0) → {𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∣ (♯‘𝑥) = 𝑁} = ∅)
 
22-May-2026ssenneg 11212 Subsets of a class of a negative size (a degenerate case). Together with sshashneg 11213 this shows that sseqn 11211 could not be extended beyond 𝑁 ∈ ℕ0. (Contributed by Jim Kingdon, 22-May-2026.)
((𝑁 ∈ ℤ ∧ 𝑁 < 0) → {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≈ (1...𝑁)} = {∅})
 
22-May-2026sseqn 11211 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 11152 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 11212 and sshashneg 11213. (Contributed by Jim Kingdon, 22-May-2026.)
(𝑁 ∈ ℕ0 → {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≈ (1...𝑁)} = {𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∣ (♯‘𝑥) = 𝑁})
 
20-May-2026ballotfilemofi 13146 𝑂 is finite. (Contributed by Jim Kingdon, 20-May-2026.)
𝑀 ∈ ℕ    &   𝑁 ∈ ℕ    &   𝑂 = {𝑐 ∈ (𝒫 (1...(𝑀 + 𝑁)) ∩ Fin) ∣ (♯‘𝑐) = 𝑀}    ⇒   𝑂 ∈ Fin
 
19-May-2026fipwfi 7274 The set of finite subsets of a finite set is finite. (Contributed by Jim Kingdon, 19-May-2026.)
(𝐴 ∈ Fin → (𝒫 𝐴 ∩ Fin) ∈ Fin)
 
18-May-20262omapfi 7273 The number of finite subsets of a finite set. For a similar theorem with set size expressed using ♯ (df-ihash 11147), see hashpwfi 11201. (Contributed by Jim Kingdon, 18-May-2026.)
(𝐴 ∈ Fin → (2o ↑𝑚 𝐴) ≈ (𝒫 𝐴 ∩ Fin))
 
18-May-2026fissfi 7218 A finite subset of a finite set is a decidable subset. (Contributed by Jim Kingdon, 18-May-2026.)
((𝑆 ⊆ 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝑆 ∈ Fin) → ∀𝑥 ∈ 𝐴 DECID 𝑥 ∈ 𝑆)
 
18-May-2026fresaunres1disj 5548 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 5547 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 7256 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 7201. (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 10343 A linear combination of two reals which lies in the interval between them. Like lincmb01cmp 10342 but generalized to require merely 𝐴 ≤ 𝐵 not 𝐴 < 𝐵. (Contributed by Jim Kingdon, 13-May-2026.)
(((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) ∧ 𝑇 ∈ (0[,]1)) → (((1 − 𝑇) · 𝐴) + (𝑇 · 𝐵)) ∈ (𝐴[,]𝐵))
 
5-May-2026fmelpw1o 7559 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 3629 and iffalse 3632, giving pwtrufal 16820).

As proved in if0ab 3625, 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 4273 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 4604. (Contributed by BJ, 5-May-2026.)
(𝐴 ∈ 𝑉 → if(𝜑, 𝐴, ∅) ∈ 𝒫 𝐴)
 
5-May-2026if0ss 3626 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 16861 Piecewise definition on the reals yields a function. The function agrees with 𝐹 and 𝐺 on their respective parts of the real line; see repiecele0 16859 and repiecege0 16860. 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. 16860 (Contributed by Jim Kingdon, 27-Apr-2026.)
(𝜑 → 𝐹:(-∞(,]0)⟶ℝ)    &   (𝜑 → 𝐺:(0[,)+∞)⟶ℝ)    &   (𝜑 → (𝐹‘0) = (𝐺‘0))    &   𝐻 = (𝑥 ∈ ℝ ↦ (((𝐹‘inf({𝑥, 0}, ℝ, < )) + (𝐺‘sup({𝑥, 0}, ℝ, < ))) − (𝐹‘0)))    ⇒   (𝜑 → 𝐻:ℝ⟶ℝ)
 
27-Apr-2026repiecege0 16860 Piecewise definition on the reals agrees with the nonnegative part of the definition. See repiecef 16861 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 16859 Piecewise definition on the reals agrees with the nonpositive part of the definition. See repiecef 16861 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 16858 Lemma for repiecele0 16859, repiecege0 16860, and repiecef 16861. 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 16882 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 16881 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 16830 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 16829 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 16828 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 11226 Lemma for hashtpg 11227. 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 11225 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 16553 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 16552 Lemma for depind 16553. (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 16551 Lemma for depind 16553. (Contributed by Matthew House, 14-Apr-2026.)
(𝜑 → 𝑃:ℕ0⟶V)    &   (𝜑 → 𝐴 ∈ (𝑃‘0))    &   (𝜑 → ∀𝑛 ∈ ℕ0 (𝐻‘𝑛):(𝑃‘𝑛)⟶(𝑃‘(𝑛 + 1)))    &   𝐹 = seq0((𝑥 ∈ V, ℎ ∈ V ↦ (ℎ‘𝑥)), (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐴, (𝐻‘(𝑚 − 1)))))    ⇒   (𝜑 → 𝐹 ∈ X𝑛 ∈ ℕ0 (𝑃‘𝑛))
 
14-Apr-2026depindlem1 16550 Lemma for depind 16553. (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 16919 Closure of a finite group sum. (Contributed by Jim Kingdon, 8-Apr-2026.)
𝐵 = (Base‘𝐺)    &    0 = (0g‘𝐺)    &   (𝜑 → 𝐺 ∈ CMnd)    &   (𝜑 → 𝐴 ∈ Fin)    &   (𝜑 → 𝐹:𝐴⟶𝐵)    ⇒   (𝜑 → (𝐺 Σgf 𝐹) ∈ 𝐵)
 
4-Apr-2026gsumsplit0 14084 Splitting off the rightmost summand of a group sum (even if it is the only summand). Similar to gsumsplit1r 13632 except that 𝑁 can equal 𝑀 − 1. (Contributed by Jim Kingdon, 4-Apr-2026.)
𝐵 = (Base‘𝐺)    &    + = (+g‘𝐺)    &   (𝜑 → 𝐺 ∈ Mnd)    &   (𝜑 → 𝑀 ∈ ℤ)    &   (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑀 − 1)))    &   (𝜑 → 𝐹:(𝑀...(𝑁 + 1))⟶𝐵)    ⇒   (𝜑 → (𝐺 Σg 𝐹) = ((𝐺 Σg (𝐹 ↾ (𝑀...𝑁))) + (𝐹‘(𝑁 + 1))))
 
4-Apr-2026fzf1o 12069 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 16917 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 16916 Group sum of a singleton. (Contributed by Jim Kingdon, 2-Apr-2026.)
𝐵 = (Base‘𝐺)    &   (𝑘 = 𝑀 → 𝐴 = 𝐶)    ⇒   ((𝐺 ∈ CMnd ∧ 𝑀 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵) → (𝐺 Σgf (𝑘 ∈ {𝑀} ↦ 𝐴)) = 𝐶)
 
31-Mar-2026sspw1or2 7497 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 7195 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 16914 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 16913 An empty finite group sum is the identity. (Contributed by Jim Kingdon, 26-Mar-2026.)
(𝐺 ∈ CMnd → (𝐺 Σgf ∅) = (0g‘𝐺))
 
25-Mar-2026gsumgfsum 16915 On an integer range, Σg and Σgf agree. (Contributed by Jim Kingdon, 25-Mar-2026.)
𝐵 = (Base‘𝐺)    &   (𝜑 → 𝐺 ∈ CMnd)    &   (𝜑 → 𝑀 ∈ ℤ)    &   (𝜑 → 𝑁 ∈ ℤ)    &   (𝜑 → 𝐹:(𝑀...𝑁)⟶𝐵)    ⇒   (𝜑 → (𝐺 Σg 𝐹) = (𝐺 Σgf 𝐹))
 
25-Mar-2026gsumgfsum1 16912 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 16911 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 16910 Define the finite group sum (iterated sum) over an unordered finite set. As currently defined, df-igsum 13493 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 7201 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 16169 A graph with one non-loop edge is a multigraph. (Contributed by Jim Kingdon, 18-Mar-2026.)
(𝜑 → 𝐾 ∈ 𝑋)    &   (𝜑 → 𝑉 ∈ 𝑌)    &   (𝜑 → 𝐸 ∈ 𝒫 𝑉)    &   (𝜑 → 𝐸 ≈ 2o)    ⇒   (𝜑 → ⟨𝑉, {⟨𝐾, 𝐸⟩}⟩ ∈ UMGraph)
 
18-Mar-2026upgr1een 16168 A graph with one non-loop edge is a pseudograph. Variation of upgr1edc 16165 for a different way of specifying a graph with one edge. (Contributed by Jim Kingdon, 18-Mar-2026.)
(𝜑 → 𝐾 ∈ 𝑋)    &   (𝜑 → 𝑉 ∈ 𝑌)    &   (𝜑 → 𝐸 ∈ 𝒫 𝑉)    &   (𝜑 → 𝐸 ≈ 2o)    ⇒   (𝜑 → ⟨𝑉, {⟨𝐾, 𝐸⟩}⟩ ∈ UPGraph)
 
14-Mar-2026trlsex 16431 The class of trails on a graph is a set. (Contributed by Jim Kingdon, 14-Mar-2026.)
(𝐺 ∈ 𝑉 → (Trails‘𝐺) ∈ V)
 
13-Mar-2026eupthv 16490 The classes involved in a Eulerian path are sets. (Contributed by Jim Kingdon, 13-Mar-2026.)
(𝐹(EulerPaths‘𝐺)𝑃 → (𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V))
 
13-Mar-20261hevtxdg0fi 16351 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 11171 A set equinumerous to the ordinal one has size 1 . (Contributed by Jim Kingdon, 11-Mar-2026.)
(𝐴 ≈ 1o → (♯‘𝐴) = 1)
 
4-Mar-2026elmpom 6436 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 16451 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 16442 Existence of the set of closed walks (represented by words). (Contributed by Jim Kingdon, 21-Feb-2026.)
(𝐺 ∈ 𝑉 → (ClWWalks‘𝐺) ∈ V)
 
17-Feb-2026vtxdgfif 16337 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 16334 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 16333 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 7165 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 16814 The powerset of 1o is not infinite. Since we cannot prove it is finite (see pw1fin 7172), this provides a concrete example of a set which we cannot show to be finite or infinite, as seen another way at inffiexmid 7168. (Contributed by Jim Kingdon, 14-Feb-2026.)
¬ ω ≼ 𝒫 1o
 
14-Feb-2026pw1ndom3 16813 The powerset of 1o does not dominate 3o. This is another way of saying that 𝒫 1o does not have three elements (like pwntru 4314). (Contributed by Steven Nguyen and Jim Kingdon, 14-Feb-2026.)
¬ 3o ≼ 𝒫 1o
 
14-Feb-2026pw1ndom3lem 16812 Lemma for pw1ndom3 16813. (Contributed by Jim Kingdon, 14-Feb-2026.)
(𝜑 → 𝑋 ∈ 𝒫 1o)    &   (𝜑 → 𝑌 ∈ 𝒫 1o)    &   (𝜑 → 𝑍 ∈ 𝒫 1o)    &   (𝜑 → 𝑋 ≠ 𝑌)    &   (𝜑 → 𝑋 ≠ 𝑍)    &   (𝜑 → 𝑌 ≠ 𝑍)    ⇒   (𝜑 → 𝑋 = ∅)
 
12-Feb-2026pw1dceq 16827 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 16811 A set that dominates ordinal 3 has at least 3 different members. (Contributed by Jim Kingdon, 12-Feb-2026.)
(3o ≼ 𝐴 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧))
 
11-Feb-2026elssdc 7164 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 16335 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 7158 Equinumerosity of finite sets is decidable. (Contributed by Jim Kingdon, 10-Feb-2026.)
((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → DECID 𝐴 ≈ 𝐵)
 
8-Feb-2026wlkvtxm 16384 A graph with a walk has at least one vertex. (Contributed by Jim Kingdon, 8-Feb-2026.)
𝑉 = (Vtx‘𝐺)    ⇒   (𝐹(Walks‘𝐺)𝑃 → ∃𝑥 𝑥 ∈ 𝑉)
 
7-Feb-2026trlsv 16428 The classes involved in a trail are sets. (Contributed by Jim Kingdon, 7-Feb-2026.)
(𝐹(Trails‘𝐺)𝑃 → (𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V))
 
7-Feb-2026wlkex 16369 The class of walks on a graph is a set. (Contributed by Jim Kingdon, 7-Feb-2026.)
(𝐺 ∈ 𝑉 → (Walks‘𝐺) ∈ V)
 
3-Feb-2026dom1oi 7072 A set with an element dominates one. (Contributed by Jim Kingdon, 3-Feb-2026.)
((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝐴) → 1o ≼ 𝐴)
 
2-Feb-2026edginwlkd 16399 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 16393 A walk is an ordered pair. (Contributed by Jim Kingdon, 2-Feb-2026.)
(𝑊 ∈ (Walks‘𝐺) → 𝑊 ∈ (V × V))
 
1-Feb-2026wlkcprim 16394 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 16363 If there are walks on a graph, the graph is a set. (Contributed by Jim Kingdon, 1-Feb-2026.)
(𝑊 ∈ (Walks‘𝐺) → 𝐺 ∈ V)
 
31-Jan-2026fvmbr 5707 If a function value is inhabited, the argument is related to the function value. (Contributed by Jim Kingdon, 31-Jan-2026.)
(𝐴 ∈ (𝐹‘𝑋) → 𝑋𝐹(𝐹‘𝑋))
 
30-Jan-2026elfvfvex 5706 If a function value is inhabited, the function value is a set. (Contributed by Jim Kingdon, 30-Jan-2026.)
(𝐴 ∈ (𝐹‘𝐵) → (𝐹‘𝐵) ∈ V)
 
30-Jan-2026reldmm 4977 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 𝜑)
  Copyright terms: Public domain W3C HTML validation [external]