Most Recent Proofs - Intuitionistic Logic Explorer

Most recent proofs    These are the 100 (Unicode, GIF) or 1000 (Unicode, GIF) most recent proofs in the iset.mm database for the Intuitionistic Logic Explorer. The iset.mm database is maintained on GitHub with master (stable) and develop (development) versions. This page was created from the commit given on the MPE Most Recent Proofs page. The database from that commit is also available here: iset.mm.

See the MPE Most Recent Proofs page for news and some useful links.

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

Recent Additions to the Intuitionistic Logic Explorer

Date	Label	Description
Theorem
5-Jun-2026	hashpwfi 11193	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 7271. For the number of subsets (which need not be finite) of a set, see pw1mapen 16770. (Contributed by Jim Kingdon, 5-Jun-2026.)
|- ( A e. Fin -> (♯ ` ( ~P A i^i Fin ) ) = ( 2 ^ (♯ ` A ) ) )
4-Jun-2026	ballotfilemonn 13140	The size of the universe is at least one. (Contributed by Jim Kingdon, 4-Jun-2026.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   =>    |- (♯ ` O ) e. NN
28-May-2026	aprlring 14434	A ring is a local ring if and only if the relation given by df-apr 14427 is an apartness relation. (Contributed by Jim Kingdon, 28-May-2026.)
|- ( R e. Ring -> ( R e. LRing <-> (#r ` R ) Ap ( Base ` R ) ) )
28-May-2026	papcotr 7562	An apartness is cotransitive. (Contributed by Jim Kingdon, 28-May-2026.)
|- ( ph -> R Ap A )   &    |- ( ph -> X e. A )   &    |- ( ph -> Y e. A )   &    |- ( ph -> X R Y )   &    |- ( ph -> Z e. A )   =>    |- ( ph -> ( X R Z \/ Y R Z ) )
27-May-2026	trimul0or 16845	Real number trichotomy implies that if a product is zero, one of its factors must be zero. (Contributed by Jim Kingdon, 27-May-2026.)
|- ( A. x e. RR A. y e. RR ( x < y \/ x = y \/ y < x ) -> A. u e. CC A. v e. CC ( ( u x. v ) = 0 -> ( u = 0 \/ v = 0 ) ) )
27-May-2026	aprnzr 14433	If the relation given by df-apr 14427 on a ring is an apartness relation, then the ring is a nonzero ring. (Contributed by Jim Kingdon, 27-May-2026.)
|- ( ( R e. Ring /\ (#r ` R ) Ap ( Base ` R ) ) -> R e. NzRing )
27-May-2026	papsym 7561	An apartness is symmetric. (Contributed by Jim Kingdon, 27-May-2026.)
|- ( ph -> R Ap A )   &    |- ( ph -> X e. A )   &    |- ( ph -> Y e. A )   &    |- ( ph -> X R Y )   =>    |- ( ph -> Y R X )
27-May-2026	papirr 7560	An apartness is irreflexive. (Contributed by Jim Kingdon, 27-May-2026.)
|- ( ( R Ap A /\ X e. A ) -> -. X R X )
24-May-2026	gfsumz 16869	Value of a finite group sum over the zero element. (Contributed by Jim Kingdon, 24-May-2026.)
|- .0. = ( 0g ` G )   =>    |- ( ( G e. CMnd /\ A e. Fin ) -> ( G gfsumgf ( k e. A |-> .0. ) ) = .0. )
22-May-2026	sshashneg 11205	Subsets of a class of a negative size (a degenerate case). Together with ssenneg 11204 this shows that sseqn 11203 could not be extended beyond N e. NN0. (Contributed by Jim Kingdon, 22-May-2026.)
|- ( ( N e. ZZ /\ N < 0 ) -> { x e. ( ~P A i^i Fin ) | (♯ ` x ) = N } = (/) )
22-May-2026	ssenneg 11204	Subsets of a class of a negative size (a degenerate case). Together with sshashneg 11205 this shows that sseqn 11203 could not be extended beyond N e. NN0. (Contributed by Jim Kingdon, 22-May-2026.)
|- ( ( N e. ZZ /\ N < 0 ) -> { x e. ~P A | x ~~ ( 1 ... N ) } = { (/) } )
22-May-2026	sseqn 11203	Two ways to express the subsets of a class of a given size. It might seem that { x e. ~P A | (♯ ` x ) = N } would suffice, but that would require the converse of hashcl 11144 or something similar. Although each side of the equality would be well defined if we changed N e. NN0 to N e. ZZ, they would give different results for the (degenerate) case of a negative size, as shown at ssenneg 11204 and sshashneg 11205. (Contributed by Jim Kingdon, 22-May-2026.)
|- ( N e. NN0 -> { x e. ~P A | x ~~ ( 1 ... N ) } = { x e. ( ~P A i^i Fin ) | (♯ ` x ) = N } )
20-May-2026	ballotfilemofi 13138	O is finite. (Contributed by Jim Kingdon, 20-May-2026.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   =>    |- O e. Fin
19-May-2026	fipwfi 7272	The set of finite subsets of a finite set is finite. (Contributed by Jim Kingdon, 19-May-2026.)
|- ( A e. Fin -> ( ~P A i^i Fin ) e. Fin )
18-May-2026	2omapfi 7271	The number of finite subsets of a finite set. For a similar theorem with set size expressed using ♯ (df-ihash 11139), see hashpwfi 11193. (Contributed by Jim Kingdon, 18-May-2026.)
|- ( A e. Fin -> ( 2o ^m A ) ~~ ( ~P A i^i Fin ) )
18-May-2026	fissfi 7216	A finite subset of a finite set is a decidable subset. (Contributed by Jim Kingdon, 18-May-2026.)
|- ( ( S C_ A /\ A e. Fin /\ S e. Fin ) -> A. x e. A DECID x e. S )
18-May-2026	fresaunres1disj 5546	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.)
|- ( ( F : A --> C /\ G : B --> C /\ ( A i^i B ) = (/) ) -> ( ( F u. G ) |` A ) = F )
18-May-2026	fresaunres2disj 5545	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.)
|- ( ( F : A --> C /\ G : B --> C /\ ( A i^i B ) = (/) ) -> ( ( F u. G ) |` B ) = G )
15-May-2026	fsuppcorn 7254	The composition of a 1-1 function with a finitely supported function is finitely supported. The purpose of the ( F supp Z ) C_ ran G condition is to ensure we don't subset the support of the function in such a way as to fun afoul of exmidssfi 7199. (Other alternative conditions might also be sufficient). (Contributed by AV, 28-May-2019.) (Revised by Jim Kingdon, 15-May-2026.)
|- ( ph -> F finSupp Z )   &    |- ( ph -> G : X -1-1-> Y )   &    |- ( ph -> Z e. W )   &    |- ( ph -> F e. V )   &    |- ( ph -> G e. U )   &    |- ( ph -> ( F supp Z ) C_ ran G )   =>    |- ( ph -> ( F o. G ) finSupp Z )
13-May-2026	lincmble 10337	A linear combination of two reals which lies in the interval between them. Like lincmb01cmp 10336 but generalized to require merely A <_ B not A < B. (Contributed by Jim Kingdon, 13-May-2026.)
|- ( ( ( A e. RR /\ B e. RR /\ A <_ B ) /\ T e. ( 0 [,] 1 ) ) -> ( ( ( 1 - T ) x. A ) + ( T x. B ) ) e. ( A [,] B ) )
5-May-2026	fmelpw1o 7557	With a formula ph one can associate an element of ~P 1o, which can therefore be thought of as the set of "truth values" (but recall that there are no other genuine truth values than T. and F., by nndc 859, which translate to 1o and (/) respectively by iftrue 3627 and iffalse 3630, giving pwtrufal 16771). As proved in if0ab 3623, the associated element of ~P 1o is the extension, in ~P 1o, of the formula ph. (Contributed by BJ, 15-Aug-2024.) (Proof shortened by BJ, 5-May-2026.)
|- if ( ph , 1o , (/) ) e. ~P 1o
5-May-2026	if0elpw 4271	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 4602. (Contributed by BJ, 5-May-2026.)
|- ( A e. V -> if ( ph , A , (/) ) e. ~P A )
5-May-2026	if0ss 3624	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 ( ph , A , (/) ) C_ A
27-Apr-2026	repiecef 16812	Piecewise definition on the reals yields a function. The function agrees with F and G on their respective parts of the real line; see repiecele0 16810 and repiecege0 16811. 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. 16811 (Contributed by Jim Kingdon, 27-Apr-2026.)
|- ( ph -> F : ( -oo (,] 0 ) --> RR )   &    |- ( ph -> G : ( 0 [,) +oo ) --> RR )   &    |- ( ph -> ( F ` 0 ) = ( G ` 0 ) )   &    |- H = ( x e. RR |-> ( ( ( F ` inf ( { x , 0 } , RR , < ) ) + ( G ` sup ( { x , 0 } , RR , < ) ) ) - ( F ` 0 ) ) )   =>    |- ( ph -> H : RR --> RR )
27-Apr-2026	repiecege0 16811	Piecewise definition on the reals agrees with the nonnegative part of the definition. See repiecef 16812 for more on this construction. (Contributed by Jim Kingdon, 27-Apr-2026.)
|- ( ph -> F : ( -oo (,] 0 ) --> RR )   &    |- ( ph -> G : ( 0 [,) +oo ) --> RR )   &    |- ( ph -> ( F ` 0 ) = ( G ` 0 ) )   &    |- H = ( x e. RR |-> ( ( ( F ` inf ( { x , 0 } , RR , < ) ) + ( G ` sup ( { x , 0 } , RR , < ) ) ) - ( F ` 0 ) ) )   =>    |- ( ( ph /\ A e. RR /\ 0 <_ A ) -> ( H ` A ) = ( G ` A ) )
27-Apr-2026	repiecele0 16810	Piecewise definition on the reals agrees with the nonpositive part of the definition. See repiecef 16812 for more on this construction. (Contributed by Jim Kingdon, 27-Apr-2026.)
|- ( ph -> F : ( -oo (,] 0 ) --> RR )   &    |- ( ph -> G : ( 0 [,) +oo ) --> RR )   &    |- ( ph -> ( F ` 0 ) = ( G ` 0 ) )   &    |- H = ( x e. RR |-> ( ( ( F ` inf ( { x , 0 } , RR , < ) ) + ( G ` sup ( { x , 0 } , RR , < ) ) ) - ( F ` 0 ) ) )   =>    |- ( ( ph /\ A e. RR /\ A <_ 0 ) -> ( H ` A ) = ( F ` A ) )
27-Apr-2026	repiecelem 16809	Lemma for repiecele0 16810, repiecege0 16811, and repiecef 16812. The function H is defined everywhere. (Contributed by Jim Kingdon, 27-Apr-2026.)
|- ( ph -> F : ( -oo (,] 0 ) --> RR )   &    |- ( ph -> G : ( 0 [,) +oo ) --> RR )   &    |- ( ph -> ( F ` 0 ) = ( G ` 0 ) )   &    |- H = ( x e. RR |-> ( ( ( F ` inf ( { x , 0 } , RR , < ) ) + ( G ` sup ( { x , 0 } , RR , < ) ) ) - ( F ` 0 ) ) )   =>    |- ( ( ph /\ A e. RR ) -> ( ( ( F ` inf ( { A , 0 } , RR , < ) ) + ( G ` sup ( { A , 0 } , RR , < ) ) ) - ( F ` 0 ) ) e. RR )
24-Apr-2026	qdiff 16833	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 16832 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.)
|- ( A e. RR -> ( A e. QQ <-> E. q e. QQ E. r e. QQ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) )
23-Apr-2026	exmidpeirce 16781	Excluded middle is equivalent to Peirce's law. Read an element of ~P 1o as being a truth value and x = 1o being that x 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 <-> A. x e. ~P 1o A. y e. ~P 1o ( ( ( x = 1o -> y = 1o ) -> x = 1o ) -> x = 1o ) )
22-Apr-2026	exmidcon 16780	Excluded middle is equivalent to the form of contraposition which removes negation. Read an element of ~P 1o as being a truth value and x = 1o being that x 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 <-> A. x e. ~P 1o A. y e. ~P 1o ( ( -. y = 1o -> -. x = 1o ) -> ( x = 1o -> y = 1o ) ) )
22-Apr-2026	exmidnotnotr 16779	Excluded middle is equivalent to double negation elimination. Read an element of ~P 1o as being a truth value and x = 1o being that x 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 <-> A. x e. ~P 1o ( -. -. x = 1o -> x = 1o ) )
18-Apr-2026	hashtpglem 11218	Lemma for hashtpg 11219. This is one of the three not-equal conclusions required for the reverse direction. (Contributed by Jim Kingdon, 18-Apr-2026.)
|- ( ph -> A e. U )   &    |- ( ph -> B e. V )   &    |- ( ph -> C e. W )   &    |- ( ph -> (♯ ` { A , B , C } ) = 3 )   =>    |- ( ph -> B =/= C )
17-Apr-2026	hashtpgim 11217	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.)
|- ( ( A e. U /\ B e. V /\ C e. W ) -> ( ( A =/= B /\ B =/= C /\ C =/= A ) -> (♯ ` { A , B , C } ) = 3 ) )
14-Apr-2026	depind 16504	Theorem related to a dependently typed induction principle in type theory. (Contributed by Matthew House, 14-Apr-2026.)
|- ( ph -> P : NN0 --> _V )   &    |- ( ph -> A e. ( P ` 0 ) )   &    |- ( ph -> A. n e. NN0 ( H ` n ) : ( P ` n ) --> ( P ` ( n + 1 ) ) )   =>    |- ( ph -> E! f e. X_ n e. NN0 ( P ` n ) ( ( f ` 0 ) = A /\ A. n e. NN0 ( f ` ( n + 1 ) ) = ( ( H ` n ) ` ( f ` n ) ) ) )
14-Apr-2026	depindlem3 16503	Lemma for depind 16504. (Contributed by Matthew House, 14-Apr-2026.)
|- ( ph -> P : NN0 --> _V )   &    |- ( ph -> A e. ( P ` 0 ) )   &    |- ( ph -> A. n e. NN0 ( H ` n ) : ( P ` n ) --> ( P ` ( n + 1 ) ) )   &    |- F = seq 0 ( ( x e. _V , h e. _V |-> ( h ` x ) ) , ( m e. NN0 |-> if ( m = 0 , A , ( H ` ( m - 1 ) ) ) ) )   =>    |- ( ph -> A. f e. X_ n e. NN0 ( P ` n ) ( ( ( f ` 0 ) = A /\ A. n e. NN0 ( f ` ( n + 1 ) ) = ( ( H ` n ) ` ( f ` n ) ) ) -> f = F ) )
14-Apr-2026	depindlem2 16502	Lemma for depind 16504. (Contributed by Matthew House, 14-Apr-2026.)
|- ( ph -> P : NN0 --> _V )   &    |- ( ph -> A e. ( P ` 0 ) )   &    |- ( ph -> A. n e. NN0 ( H ` n ) : ( P ` n ) --> ( P ` ( n + 1 ) ) )   &    |- F = seq 0 ( ( x e. _V , h e. _V |-> ( h ` x ) ) , ( m e. NN0 |-> if ( m = 0 , A , ( H ` ( m - 1 ) ) ) ) )   =>    |- ( ph -> F e. X_ n e. NN0 ( P ` n ) )
14-Apr-2026	depindlem1 16501	Lemma for depind 16504. (Contributed by Matthew House, 14-Apr-2026.)
|- ( ph -> P : NN0 --> _V )   &    |- ( ph -> A e. ( P ` 0 ) )   &    |- ( ph -> A. n e. NN0 ( H ` n ) : ( P ` n ) --> ( P ` ( n + 1 ) ) )   &    |- F = seq 0 ( ( x e. _V , h e. _V |-> ( h ` x ) ) , ( m e. NN0 |-> if ( m = 0 , A , ( H ` ( m - 1 ) ) ) ) )   =>    |- ( ph -> ( F : NN0 --> _V /\ ( F ` 0 ) = A /\ A. n e. NN0 ( F ` ( n + 1 ) ) = ( ( H ` n ) ` ( F ` n ) ) ) )
8-Apr-2026	gfsumcl 16870	Closure of a finite group sum. (Contributed by Jim Kingdon, 8-Apr-2026.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> A e. Fin )   &    |- ( ph -> F : A --> B )   =>    |- ( ph -> ( G gfsumgf F ) e. B )
4-Apr-2026	gsumsplit0 14063	Splitting off the rightmost summand of a group sum (even if it is the only summand). Similar to gsumsplit1r 13611 except that N can equal M - 1. (Contributed by Jim Kingdon, 4-Apr-2026.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. Mnd )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ( ZZ>= ` ( M - 1 ) ) )   &    |- ( ph -> F : ( M ... ( N + 1 ) ) --> B )   =>    |- ( ph -> ( G gsumg F ) = ( ( G gsumg ( F |` ( M ... N ) ) ) .+ ( F ` ( N + 1 ) ) ) )
4-Apr-2026	fzf1o 12061	A finite set can be enumerated by integers starting at one. (Contributed by Jim Kingdon, 4-Apr-2026.)
|- ( A e. Fin -> E. f f : ( 1 ... (♯ ` A ) ) -1-1-onto-> A )
3-Apr-2026	gfsump1 16868	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.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> F : ( Y u. { Z } ) --> B )   &    |- ( ph -> Y e. Fin )   &    |- ( ph -> Z e. V )   &    |- ( ph -> -. Z e. Y )   =>    |- ( ph -> ( G gfsumgf F ) = ( ( G gfsumgf ( F |` Y ) ) .+ ( F ` Z ) ) )
2-Apr-2026	gfsumsn 16867	Group sum of a singleton. (Contributed by Jim Kingdon, 2-Apr-2026.)
|- B = ( Base ` G )   &    |- ( k = M -> A = C )   =>    |- ( ( G e. CMnd /\ M e. V /\ C e. B ) -> ( G gfsumgf ( k e. { M } |-> A ) ) = C )
31-Mar-2026	sspw1or2 7495	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.)
|- { x e. { s e. ~P V | E. j j e. s } | ( x ~~ 1o \/ x ~~ 2o ) } = { x e. ~P V | ( x ~~ 1o \/ x ~~ 2o ) }
28-Mar-2026	imaf1fi 7193	The image of a finite set under a one-to-one mapping is finite. (Contributed by Jim Kingdon, 28-Mar-2026.)
|- ( ( F : A -1-1-> B /\ X C_ A /\ X e. Fin ) -> ( F " X ) e. Fin )
26-Mar-2026	gsumgfsumlem 16865	Shifting the indexes of a group sum indexed by consecutive integers. (Contributed by Jim Kingdon, 26-Mar-2026.)
|- B = ( Base ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ph -> F : ( M ... N ) --> B )   &    |- S = ( j e. ( 1 ... ( N + ( 1 - M ) ) ) |-> ( j - ( 1 - M ) ) )   =>    |- ( ph -> ( G gsumg F ) = ( G gsumg ( F o. S ) ) )
26-Mar-2026	gfsum0 16864	An empty finite group sum is the identity. (Contributed by Jim Kingdon, 26-Mar-2026.)
|- ( G e. CMnd -> ( G gfsumgf (/) ) = ( 0g ` G ) )
25-Mar-2026	gsumgfsum 16866	On an integer range, gsumg and gfsumgf agree. (Contributed by Jim Kingdon, 25-Mar-2026.)
|- B = ( Base ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> F : ( M ... N ) --> B )   =>    |- ( ph -> ( G gsumg F ) = ( G gfsumgf F ) )
25-Mar-2026	gsumgfsum1 16863	On an integer range starting at one, gsumg and gfsumgf agree. (Contributed by Jim Kingdon, 25-Mar-2026.)
|- B = ( Base ` G )   &    |- ( ph -> G e. CMnd )   &    |- ( ph -> N e. NN0 )   &    |- ( ph -> F : ( 1 ... N ) --> B )   =>    |- ( ph -> ( G gsumg F ) = ( G gfsumgf F ) )
24-Mar-2026	gfsumval 16862	Value of the finite group sum over an unordered finite set. (Contributed by Jim Kingdon, 24-Mar-2026.)
|- B = ( Base ` W )   &    |- ( ph -> W e. CMnd )   &    |- ( ph -> F : A --> B )   &    |- ( ph -> A e. Fin )   &    |- ( ph -> G : ( 1 ... (♯ ` A ) ) -1-1-onto-> A )   =>    |- ( ph -> ( W gfsumgf F ) = ( W gsumg ( F o. G ) ) )
23-Mar-2026	df-gfsum 16861	Define the finite group sum (iterated sum) over an unordered finite set. As currently defined, df-igsum 13472 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.)
|- gfsumgf = ( w e. CMnd , f e. _V |-> ( iota x ( dom f e. Fin /\ E. g ( g : ( 1 ... (♯ ` dom f ) ) -1-1-onto-> dom f /\ x = ( w gsumg ( f o. g ) ) ) ) ) )
20-Mar-2026	exmidssfi 7199	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 <-> A. x A. y ( ( x e. Fin /\ y C_ x ) -> y e. Fin ) )
18-Mar-2026	umgr1een 16120	A graph with one non-loop edge is a multigraph. (Contributed by Jim Kingdon, 18-Mar-2026.)
|- ( ph -> K e. X )   &    |- ( ph -> V e. Y )   &    |- ( ph -> E e. ~P V )   &    |- ( ph -> E ~~ 2o )   =>    |- ( ph -> <. V , { <. K , E >. } >. e. UMGraph )
18-Mar-2026	upgr1een 16119	A graph with one non-loop edge is a pseudograph. Variation of upgr1edc 16116 for a different way of specifying a graph with one edge. (Contributed by Jim Kingdon, 18-Mar-2026.)
|- ( ph -> K e. X )   &    |- ( ph -> V e. Y )   &    |- ( ph -> E e. ~P V )   &    |- ( ph -> E ~~ 2o )   =>    |- ( ph -> <. V , { <. K , E >. } >. e. UPGraph )
14-Mar-2026	trlsex 16382	The class of trails on a graph is a set. (Contributed by Jim Kingdon, 14-Mar-2026.)
|- ( G e. V -> (Trails ` G ) e. _V )
13-Mar-2026	eupthv 16441	The classes involved in a Eulerian path are sets. (Contributed by Jim Kingdon, 13-Mar-2026.)
|- ( F (EulerPaths ` G ) P -> ( G e. _V /\ F e. _V /\ P e. _V ) )
13-Mar-2026	1hevtxdg0fi 16302	The vertex degree of vertex D in a finite pseudograph G with only one edge E is 0 if D is not incident with the edge E. (Contributed by AV, 2-Mar-2021.) (Revised by Jim Kingdon, 13-Mar-2026.)
|- ( ph -> (iEdg ` G ) = { <. A , E >. } )   &    |- ( ph -> (Vtx ` G ) = V )   &    |- ( ph -> A e. X )   &    |- ( ph -> D e. V )   &    |- ( ph -> V e. Fin )   &    |- ( ph -> G e. UPGraph )   &    |- ( ph -> E e. Y )   &    |- ( ph -> D e/ E )   =>    |- ( ph -> ( (VtxDeg ` G ) ` D ) = 0 )
11-Mar-2026	en1hash 11163	A set equinumerous to the ordinal one has size 1 . (Contributed by Jim Kingdon, 11-Mar-2026.)
|- ( A ~~ 1o -> (♯ ` A ) = 1 )
4-Mar-2026	elmpom 6434	If a maps-to operation is inhabited, the first class it is defined with is inhabited. (Contributed by Jim Kingdon, 4-Mar-2026.)
|- F = ( x e. A , y e. B |-> C )   =>    |- ( D e. F -> E. z z e. A )
22-Feb-2026	isclwwlkni 16402	A word over the set of vertices representing a closed walk of a fixed length. (Contributed by Jim Kingdon, 22-Feb-2026.)
|- ( W e. ( N ClWWalksN G ) -> ( W e. (ClWWalks ` G ) /\ (♯ ` W ) = N ) )
21-Feb-2026	clwwlkex 16393	Existence of the set of closed walks (represented by words). (Contributed by Jim Kingdon, 21-Feb-2026.)
|- ( G e. V -> (ClWWalks ` G ) e. _V )
17-Feb-2026	vtxdgfif 16288	In a finite graph, the vertex degree function is a function from vertices to nonnegative integers. (Contributed by Jim Kingdon, 17-Feb-2026.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- A = dom I   &    |- ( ph -> A e. Fin )   &    |- ( ph -> V e. Fin )   &    |- ( ph -> G e. UPGraph )   =>    |- ( ph -> (VtxDeg ` G ) : V --> NN0 )
16-Feb-2026	vtxlpfi 16285	In a finite graph, the number of loops from a given vertex is finite. (Contributed by Jim Kingdon, 16-Feb-2026.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- A = dom I   &    |- ( ph -> A e. Fin )   &    |- ( ph -> V e. Fin )   &    |- ( ph -> U e. V )   &    |- ( ph -> G e. UPGraph )   =>    |- ( ph -> { x e. A | ( I ` x ) = { U } } e. Fin )
16-Feb-2026	vtxedgfi 16284	In a finite graph, the number of edges from a given vertex is finite. (Contributed by Jim Kingdon, 16-Feb-2026.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- A = dom I   &    |- ( ph -> A e. Fin )   &    |- ( ph -> V e. Fin )   &    |- ( ph -> U e. V )   &    |- ( ph -> G e. UPGraph )   =>    |- ( ph -> { x e. A | U e. ( I ` x ) } e. Fin )
15-Feb-2026	eqsndc 7163	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.)
|- ( ph -> A. x e. B A. y e. B DECID x = y )   &    |- ( ph -> X e. B )   &    |- ( ph -> A C_ B )   &    |- ( ph -> A e. Fin )   =>    |- ( ph -> DECID A = { X } )
14-Feb-2026	pw1ninf 16765	The powerset of 1o is not infinite. Since we cannot prove it is finite (see pw1fin 7170), this provides a concrete example of a set which we cannot show to be finite or infinite, as seen another way at inffiexmid 7166. (Contributed by Jim Kingdon, 14-Feb-2026.)
|- -. om ~<_ ~P 1o
14-Feb-2026	pw1ndom3 16764	The powerset of 1o does not dominate 3o. This is another way of saying that ~P 1o does not have three elements (like pwntru 4312). (Contributed by Steven Nguyen and Jim Kingdon, 14-Feb-2026.)
|- -. 3o ~<_ ~P 1o
14-Feb-2026	pw1ndom3lem 16763	Lemma for pw1ndom3 16764. (Contributed by Jim Kingdon, 14-Feb-2026.)
|- ( ph -> X e. ~P 1o )   &    |- ( ph -> Y e. ~P 1o )   &    |- ( ph -> Z e. ~P 1o )   &    |- ( ph -> X =/= Y )   &    |- ( ph -> X =/= Z )   &    |- ( ph -> Y =/= Z )   =>    |- ( ph -> X = (/) )
12-Feb-2026	pw1dceq 16778	The powerset of 1o having decidable equality is equivalent to excluded middle. (Contributed by Jim Kingdon, 12-Feb-2026.)
|- (EXMID <-> A. x e. ~P 1o A. y e. ~P 1oDECID x = y )
12-Feb-2026	3dom 16762	A set that dominates ordinal 3 has at least 3 different members. (Contributed by Jim Kingdon, 12-Feb-2026.)
|- ( 3o ~<_ A -> E. x e. A E. y e. A E. z e. A ( x =/= y /\ x =/= z /\ y =/= z ) )
11-Feb-2026	elssdc 7162	Membership in a finite subset of a set with decidable equality is decidable. (Contributed by Jim Kingdon, 11-Feb-2026.)
|- ( ph -> A. x e. B A. y e. B DECID x = y )   &    |- ( ph -> X e. B )   &    |- ( ph -> A C_ B )   &    |- ( ph -> A e. Fin )   =>    |- ( ph -> DECID X e. A )
10-Feb-2026	vtxdgfifival 16286	The degree of a vertex for graphs with finite vertex and edge sets. (Contributed by Jim Kingdon, 10-Feb-2026.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- A = dom I   &    |- ( ph -> A e. Fin )   &    |- ( ph -> V e. Fin )   &    |- ( ph -> U e. V )   &    |- ( ph -> G e. UPGraph )   =>    |- ( ph -> ( (VtxDeg ` G ) ` U ) = ( (♯ ` { x e. A | U e. ( I ` x ) } ) + (♯ ` { x e. A | ( I ` x ) = { U } } ) ) )
10-Feb-2026	fidcen 7156	Equinumerosity of finite sets is decidable. (Contributed by Jim Kingdon, 10-Feb-2026.)
|- ( ( A e. Fin /\ B e. Fin ) -> DECID A ~~ B )
8-Feb-2026	wlkvtxm 16335	A graph with a walk has at least one vertex. (Contributed by Jim Kingdon, 8-Feb-2026.)
|- V = (Vtx ` G )   =>    |- ( F (Walks ` G ) P -> E. x x e. V )
7-Feb-2026	trlsv 16379	The classes involved in a trail are sets. (Contributed by Jim Kingdon, 7-Feb-2026.)
|- ( F (Trails ` G ) P -> ( G e. _V /\ F e. _V /\ P e. _V ) )
7-Feb-2026	wlkex 16320	The class of walks on a graph is a set. (Contributed by Jim Kingdon, 7-Feb-2026.)
|- ( G e. V -> (Walks ` G ) e. _V )
3-Feb-2026	dom1oi 7070	A set with an element dominates one. (Contributed by Jim Kingdon, 3-Feb-2026.)
|- ( ( A e. V /\ B e. A ) -> 1o ~<_ A )
2-Feb-2026	edginwlkd 16350	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.)
|- I = (iEdg ` G )   &    |- E = (Edg ` G )   &    |- ( ph -> Fun I )   &    |- ( ph -> F e. Word dom I )   &    |- ( ph -> K e. ( 0..^ (♯ ` F ) ) )   &    |- ( ph -> G e. V )   =>    |- ( ph -> ( I ` ( F ` K ) ) e. E )
2-Feb-2026	wlkelvv 16344	A walk is an ordered pair. (Contributed by Jim Kingdon, 2-Feb-2026.)
|- ( W e. (Walks ` G ) -> W e. ( _V X. _V ) )
1-Feb-2026	wlkcprim 16345	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.)
|- ( W e. (Walks ` G ) -> ( 1st ` W ) (Walks ` G ) ( 2nd ` W ) )
1-Feb-2026	wlkmex 16314	If there are walks on a graph, the graph is a set. (Contributed by Jim Kingdon, 1-Feb-2026.)
|- ( W e. (Walks ` G ) -> G e. _V )
31-Jan-2026	fvmbr 5705	If a function value is inhabited, the argument is related to the function value. (Contributed by Jim Kingdon, 31-Jan-2026.)
|- ( A e. ( F ` X ) -> X F ( F ` X ) )
30-Jan-2026	elfvfvex 5704	If a function value is inhabited, the function value is a set. (Contributed by Jim Kingdon, 30-Jan-2026.)
|- ( A e. ( F ` B ) -> ( F ` B ) e. _V )
30-Jan-2026	reldmm 4975	A relation is inhabited iff its domain is inhabited. (Contributed by Jim Kingdon, 30-Jan-2026.)
|- ( Rel A -> ( E. x x e. A <-> E. y y e. dom A ) )
25-Jan-2026	ifp2 989	Forward direction of dfifp2dc 990. This direction does not require decidability. (Contributed by Jim Kingdon, 25-Jan-2026.)
|- (if- ( ph , ps , ch ) -> ( ( ph -> ps ) /\ ( -. ph -> ch ) ) )
25-Jan-2026	ifpdc 988	The conditional operator for propositions implies decidability. (Contributed by Jim Kingdon, 25-Jan-2026.)
|- (if- ( ph , ps , ch ) -> DECID ph )
20-Jan-2026	cats1fvd 11458	A symbol other than the last in a concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) (Revised by Jim Kingdon, 20-Jan-2026.)
|- T = ( S ++ <" X "> )   &    |- ( ph -> S e. Word _V )   &    |- ( ph -> (♯ ` S ) = M )   &    |- ( ph -> Y e. V )   &    |- ( ph -> X e. W )   &    |- ( ph -> ( S ` N ) = Y )   &    |- ( ph -> N e. NN0 )   &    |- ( ph -> N < M )   =>    |- ( ph -> ( T ` N ) = Y )
20-Jan-2026	cats1fvnd 11457	The last symbol of a concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) (Revised by Jim Kingdon, 20-Jan-2026.)
|- T = ( S ++ <" X "> )   &    |- ( ph -> S e. Word _V )   &    |- ( ph -> X e. V )   &    |- ( ph -> (♯ ` S ) = M )   =>    |- ( ph -> ( T ` M ) = X )
19-Jan-2026	cats2catd 11461	Closure of concatenation of concatenations with singleton words. (Contributed by AV, 1-Mar-2021.) (Revised by Jim Kingdon, 19-Jan-2026.)
|- ( ph -> B e. Word _V )   &    |- ( ph -> D e. Word _V )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. W )   &    |- ( ph -> A = ( B ++ <" X "> ) )   &    |- ( ph -> C = ( <" Y "> ++ D ) )   =>    |- ( ph -> ( A ++ C ) = ( ( B ++ <" X Y "> ) ++ D ) )
19-Jan-2026	cats1catd 11460	Closure of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) (Revised by Jim Kingdon, 19-Jan-2026.)
|- T = ( S ++ <" X "> )   &    |- ( ph -> A e. Word _V )   &    |- ( ph -> S e. Word _V )   &    |- ( ph -> X e. W )   &    |- ( ph -> C = ( B ++ <" X "> ) )   &    |- ( ph -> B = ( A ++ S ) )   =>    |- ( ph -> C = ( A ++ T ) )
19-Jan-2026	cats1lend 11459	The length of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) (Revised by Jim Kingdon, 19-Jan-2026.)
|- T = ( S ++ <" X "> )   &    |- ( ph -> S e. Word _V )   &    |- ( ph -> X e. W )   &    |- (♯ ` S ) = M   &    |- ( M + 1 ) = N   =>    |- ( ph -> (♯ ` T ) = N )
18-Jan-2026	rexanaliim 2648	A transformation of restricted quantifiers and logical connectives. (Contributed by NM, 4-Sep-2005.) (Revised by Jim Kingdon, 18-Jan-2026.)
|- ( E. x e. A ( ph /\ -. ps ) -> -. A. x e. A ( ph -> ps ) )
15-Jan-2026	df-uspgren 16150	Define the class of all undirected simple pseudographs (which could have loops). An undirected simple pseudograph is a special undirected pseudograph or a special undirected simple hypergraph, consisting of a set v (of "vertices") and an injective (one-to-one) function e (representing (indexed) "edges") into subsets of v of cardinality one or two, representing the two vertices incident to the edge, or the one vertex if the edge is a loop. In contrast to a pseudograph, there is at most one edge between two vertices resp. at most one loop for a vertex. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by Jim Kingdon, 15-Jan-2026.)
|- USPGraph = { g | [. (Vtx ` g ) / v ]. [. (iEdg ` g ) / e ]. e : dom e -1-1-> { x e. ~P v | ( x ~~ 1o \/ x ~~ 2o ) } }
11-Jan-2026	en2prde 7490	A set of size two is an unordered pair of two different elements. (Contributed by Alexander van der Vekens, 8-Dec-2017.) (Revised by Jim Kingdon, 11-Jan-2026.)
|- ( V ~~ 2o -> E. a E. b ( a =/= b /\ V = { a , b } ) )
10-Jan-2026	pw1mapen 16770	Equinumerosity of ( ~P 1o ^m A ) and the set of subsets of A. (Contributed by Jim Kingdon, 10-Jan-2026.)
|- ( A e. V -> ( ~P 1o ^m A ) ~~ ~P A )
10-Jan-2026	pw1if 7535	Expressing a truth value in terms of an if expression. (Contributed by Jim Kingdon, 10-Jan-2026.)
|- ( A e. ~P 1o -> if ( A = 1o , 1o , (/) ) = A )
10-Jan-2026	pw1m 7534	A truth value which is inhabited is equal to true. This is a variation of pwntru 4312 and pwtrufal 16771. (Contributed by Jim Kingdon, 10-Jan-2026.)
|- ( ( A e. ~P 1o /\ E. x x e. A ) -> A = 1o )
10-Jan-2026	1ndom2 7119	Two is not dominated by one. (Contributed by Jim Kingdon, 10-Jan-2026.)
|- -. 2o ~<_ 1o
9-Jan-2026	pw1map 16769	Mapping between ( ~P 1o ^m A ) and subsets of A. (Contributed by Jim Kingdon, 9-Jan-2026.)
|- F = ( s e. ( ~P 1o ^m A ) |-> { z e. A | ( s ` z ) = 1o } )   =>    |- ( A e. V -> F : ( ~P 1o ^m A ) -1-1-onto-> ~P A )
9-Jan-2026	iftrueb01 7533	Using an if expression to represent a truth value by (/) or 1o. Unlike some theorems using if, ph does not need to be decidable. (Contributed by Jim Kingdon, 9-Jan-2026.)
|- ( if ( ph , 1o , (/) ) = 1o <-> ph )
8-Jan-2026	pfxclz 11371	Closure of the prefix extractor. This extends pfxclg 11370 from NN0 to ZZ (negative lengths are trivial, resulting in the empty word). (Contributed by Jim Kingdon, 8-Jan-2026.)
|- ( ( S e. Word A /\ L e. ZZ ) -> ( S prefix L ) e. Word A )