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 21-Jul-2026 at 7:09 AM ET.

Recent Additions to the Intuitionistic Logic Explorer

Date	Label	Description
Theorem
18-Jul-2026	sepab 4273	Separation Scheme (Aussonderung) in terms of a class abstraction. (Contributed by NM, 8-Jun-1994.) Put in closed form. (Revised by BJ, 18-Jul-2026.)
|- ( A e. V -> { x | ( x e. A /\ ph ) } e. _V )
14-Jul-2026	uniex2 4576	The Axiom of Union using the standard abbreviation for union. Given any set x, its union y exists. (Contributed by NM, 4-Jun-2006.) (Proof shortened by BJ, 14-Jul-2026.)
|- E. y y = U. x
14-Jul-2026	sepgi 4247	Inference associated with sepg 4246. (Contributed by NM, 21-Jun-1993.) (Revised by BJ, 14-Jul-2026.)
|- A e. _V   =>    |- E. y A. x ( x e. y <-> ( x e. A /\ ph ) )
13-Jul-2026	f1setfi 7307	The set of injections between two finite sets is finite. (Contributed by Jim Kingdon, 13-Jul-2026.)
|- ( ( A e. Fin /\ B e. Fin ) -> { f | f : A -1-1-> B } e. Fin )
13-Jul-2026	fdcf1 7306	It is decidable whether a function from a finite set into another finite set is one-to-one. (Contributed by Jim Kingdon, 13-Jul-2026.)
|- ( ( A e. Fin /\ B e. Fin /\ F : A --> B ) -> DECID F : A -1-1-> B )
12-Jul-2026	vvin 3568	Two classes are both the universal class if and only if their intersection is the universal class. Dual of un00 3566. (Contributed by BJ, 12-Jul-2026.)
|- ( ( A = _V /\ B = _V ) <-> ( A i^i B ) = _V )
7-Jul-2026	cmnsubm 14089	A submonoid of a commutative monoid is commutative. (Contributed by Jim Kingdon, 7-Jul-2026.)
|- ( ph -> S e. (SubMnd ` G ) )   &    |- ( ph -> G e. CMnd )   &    |- H = ( G ↾s S )   =>    |- ( ph -> H e. CMnd )
29-Jun-2026	dichmul0or 16674	Real number dichotomy is equivalent to the zero product principle for complex numbers: if a product is zero, one of its factors must be zero. (Contributed by Matthew House, 29-Jun-2026.)
|- ( A. x e. RR A. y e. RR ( x <_ y \/ y <_ x ) <-> A. z e. CC A. w e. CC ( ( z x. w ) = 0 -> ( z = 0 \/ w = 0 ) ) )
29-Jun-2026	dichmul0orlem5 16671	Lemma for dichmul0or 16674. (Contributed by Matthew House, 29-Jun-2026.)
|- ( ph -> A e. RR )   &    |- ( ph -> ( ( abs ` A ) + A ) = 0 )   =>    |- ( ph -> A <_ 0 )
29-Jun-2026	dichmul0orlem4 16670	Lemma for dichmul0or 16674. (Contributed by Matthew House, 29-Jun-2026.)
|- ( ph -> A e. RR )   =>    |- ( ph -> ( ( ( abs ` A ) + A ) x. ( ( abs ` A ) - A ) ) = 0 )
29-Jun-2026	dichmul0orlem3 16669	Lemma for dichmul0or 16674. (Contributed by Matthew House, 29-Jun-2026.)
|- ( ph -> A. x e. RR A. y e. RR ( x <_ y \/ y <_ x ) )   &    |- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> ( A x. B ) = 0 )   =>    |- ( ph -> ( A = 0 \/ B = 0 ) )
29-Jun-2026	dichmul0orlem2 16668	Lemma for dichmul0or 16674. (Contributed by Matthew House, 29-Jun-2026.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> ( A x. B ) = 0 )   &    |- ( ph -> ( abs ` A ) <_ ( abs ` B ) )   =>    |- ( ph -> A = 0 )
29-Jun-2026	dichmul0orlem1 16667	Lemma for dichmul0or 16674. (Contributed by Matthew House, 29-Jun-2026.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> ( A x. B ) = 0 )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> A <_ B )   =>    |- ( ph -> A = 0 )
29-Jun-2026	lealltlt2 16666	Alternative definition for <_ on real numbers. (Contributed by Matthew House, 29-Jun-2026.)
|- ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> A. x e. RR ( B < x -> A < x ) ) )
29-Jun-2026	lealltlt1 16665	Alternative definition for <_ on real numbers. (Contributed by Matthew House, 29-Jun-2026.)
|- ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> A. x e. RR ( x < A -> x < B ) ) )
28-Jun-2026	dichmul0orlem7 16673	Lemma for dichmul0or 16674. (Contributed by Matthew House, 28-Jun-2026.)
|- ( ph -> A. x e. CC A. y e. CC ( ( x x. y ) = 0 -> ( x = 0 \/ y = 0 ) ) )   &    |- ( ph -> A e. RR )   =>    |- ( ph -> ( A <_ 0 \/ 0 <_ A ) )
28-Jun-2026	dichmul0orlem6 16672	Lemma for dichmul0or 16674. (Contributed by Matthew House, 28-Jun-2026.)
|- ( ph -> A e. RR )   &    |- ( ph -> ( ( abs ` A ) - A ) = 0 )   =>    |- ( ph -> 0 <_ A )
28-Jun-2026	msq0 8987	A number is zero iff its square is zero. (Contributed by Matthew House, 28-Jun-2026.)
|- ( A e. CC -> ( ( A x. A ) = 0 <-> A = 0 ) )
28-Jun-2026	msqap0 8986	A number is apart from zero iff its square is apart from zero. (Contributed by Matthew House, 28-Jun-2026.)
|- ( A e. CC -> ( ( A x. A ) # 0 <-> A # 0 ) )
28-Jun-2026	letrid 8432	Tightness of real apartness. (Contributed by Matthew House, 28-Jun-2026.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A <_ B )   &    |- ( ph -> B <_ A )   =>    |- ( ph -> A = B )
19-Jun-2026	ringen1zr0 14595	The only unital ring with one element is the zero ring (at least if its operations are internal binary operations). This holds already for nonunital rings, see rngen1zr0 14236, and semirings, see srgen1zr0 14266. (Contributed by FL, 15-Feb-2010.) (Revised by AV, 25-Jan-2020.) (Proof shortened by AV, 19-Jun-2026.)
|- B = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .* = ( .r ` R )   &    |- Z = ( 0g ` R )   =>    |- ( ( R e. Ring /\ .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) -> ( B ~~ 1o <-> ( .+ = { <. <. Z , Z >. , Z >. } /\ .* = { <. <. Z , Z >. , Z >. } ) ) )
19-Jun-2026	srg1zr 14265	The only semiring with a base set consisting of one element is the zero ring (at least if its operations are internal binary operations). (Contributed by FL, 13-Feb-2010.) (Revised by AV, 25-Jan-2020.) (Proof shortened by AV, 19-Jun-2026.)
|- B = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .* = ( .r ` R )   =>    |- ( ( ( R e. SRing /\ .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) /\ Z e. B ) -> ( B = { Z } <-> ( .+ = { <. <. Z , Z >. , Z >. } /\ .* = { <. <. Z , Z >. , Z >. } ) ) )
18-Jun-2026	rngen1zr0 14236	The only ring with one element is the zero ring (at least if its operations are internal binary operations). (Contributed by FL, 15-Feb-2010.) (Revised by AV, 18-Jun-2026.)
|- B = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .* = ( .r ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. Rng /\ .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) -> ( B ~~ 1o <-> ( .+ = { <. <. .0. , .0. >. , .0. >. } /\ .* = { <. <. .0. , .0. >. , .0. >. } ) ) )
18-Jun-2026	rngen1zr 14235	The only ring with one element is the zero ring (at least if its operations are internal binary operations). (Contributed by FL, 14-Feb-2010.) (Revised by AV, 18-Jun-2026.)
|- B = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .* = ( .r ` R )   =>    |- ( ( ( R e. Rng /\ .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) /\ Z e. B ) -> ( B ~~ 1o <-> ( .+ = { <. <. Z , Z >. , Z >. } /\ .* = { <. <. Z , Z >. , Z >. } ) ) )
18-Jun-2026	rng1zr 14234	The only ring with a base set consisting of one element is the zero ring (at least if its operations are internal binary operations). (Contributed by FL, 13-Feb-2010.) (Revised by AV, 18-Jun-2026.)
|- B = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .* = ( .r ` R )   =>    |- ( ( ( R e. Rng /\ .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) /\ Z e. B ) -> ( B = { Z } <-> ( .+ = { <. <. Z , Z >. , Z >. } /\ .* = { <. <. Z , Z >. , Z >. } ) ) )
18-Jun-2026	rng1zrlem 14233	Lemma for rng1zr 14234 and srg1zr 14265. (Contributed by FL, 13-Feb-2010.) (Revised by AV, 18-Jun-2026.)
|- B = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .* = ( .r ` R )   =>    |- ( ( ( R e. Mgm /\ (mulGrp ` R ) e. Mgm ) /\ ( .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) /\ Z e. B ) -> ( B = { Z } <-> ( .+ = { <. <. Z , Z >. , Z >. } /\ .* = { <. <. Z , Z >. , Z >. } ) ) )
17-Jun-2026	ballotfi 13260	Bertrand's ballot problem : the probability that A is ahead throughout the counting. The proof formalized here is a proof "by reflection", as opposed to other known proofs "by induction" or "by permutation". This is Metamath 100 proof #30. (Contributed by Thierry Arnoux, 7-Dec-2016.) (Revised by Jim Kingdon, 17-Jun-2026.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   =>    |- ( P ` E ) = ( ( M - N ) / ( M + N ) )
17-Jun-2026	ballotfilembfi 13217	The set of countings where B got the first vote is finite. (Contributed by Jim Kingdon, 17-Jun-2026.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   =>    |- { c e. ( O \ E ) | -. 1 e. c } e. Fin
17-Jun-2026	ballotfilemafi 13216	The set of countings where A got the first vote, but does not stay strictly ahead throughout, is finite. (Contributed by Jim Kingdon, 17-Jun-2026.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   =>    |- { c e. ( O \ E ) | 1 e. c } e. Fin
17-Jun-2026	ballotfilemefi 13215	E is finite. (Contributed by Jim Kingdon, 17-Jun-2026.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   =>    |- E e. Fin
17-Jun-2026	rabxmdc 3554	Law of excluded middle given decidability, in terms of restricted class abstractions. (Contributed by Jeff Madsen, 20-Jun-2011.) (Revised by Jim Kingdon, 17-Jun-2026.)
|- ( A. x e. A DECID ph -> A = ( { x e. A | ph } u. { x e. A | -. ph } ) )
15-Jun-2026	ballotfilemgun 13246	A property of the defined .^ operator. (Contributed by Thierry Arnoux, 26-Apr-2017.) (Revised by Jim Kingdon, 15-Jun-2026.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   &    |- R = ( c e. ( O \ E ) |-> ( ( S ` c ) " c ) )   &    |- .^ = ( u e. O , v e. Fin |-> ( (♯ ` ( v i^i u ) ) - (♯ ` ( v \ u ) ) ) )   &    |- ( ph -> U e. O )   &    |- ( ph -> L e. ( J ... K ) )   =>    |- ( ph -> ( U .^ ( J ... K ) ) = ( ( U .^ ( J ... ( L - 1 ) ) ) + ( U .^ ( L ... K ) ) ) )
15-Jun-2026	ballotfilemgval 13245	Expand the value of .^. (Contributed by Thierry Arnoux, 21-Apr-2017.) (Revised by Jim Kingdon, 15-Jun-2026.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   &    |- R = ( c e. ( O \ E ) |-> ( ( S ` c ) " c ) )   &    |- .^ = ( u e. O , v e. Fin |-> ( (♯ ` ( v i^i u ) ) - (♯ ` ( v \ u ) ) ) )   &    |- ( ph -> U e. O )   &    |- ( ph -> J e. ZZ )   &    |- ( ph -> K e. ZZ )   &    |- ( ph -> V = ( J ... K ) )   =>    |- ( ph -> ( U .^ V ) = ( (♯ ` ( V i^i U ) ) - (♯ ` ( V \ U ) ) ) )
15-Jun-2026	ballotfilemdifcfz 13205	Lemma for ballotfi . The portion of a counting representing votes for B within a specified integer range is finite. (Contributed by Jim Kingdon, 15-Jun-2026.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- ( ph -> C e. O )   &    |- ( ph -> J e. ZZ )   &    |- ( ph -> K e. ZZ )   =>    |- ( ph -> ( ( J ... K ) \ C ) e. Fin )
15-Jun-2026	ballotfilemcinfz 13204	Lemma for ballotfi . The portion of a counting representing votes for A within a specified integer range is finite. (Contributed by Jim Kingdon, 15-Jun-2026.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- ( ph -> C e. O )   &    |- ( ph -> J e. ZZ )   &    |- ( ph -> K e. ZZ )   =>    |- ( ph -> ( ( J ... K ) i^i C ) e. Fin )
12-Jun-2026	ballotfilemsle 13226	The infimum of the set of zeroes of F is a lower bound. (Contributed by Jim Kingdon, 12-Jun-2026.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = { k e. ( 1 ... ( M + N ) ) | ( ( F ` C ) ` k ) = 0 }   =>    |- ( ( C e. ( O \ E ) /\ X e. S ) -> inf ( S , RR , < ) <_ X )
12-Jun-2026	ballotfilemscl 13225	The set of zeroes of F has an infimum. (Contributed by Jim Kingdon, 12-Jun-2026.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = { k e. ( 1 ... ( M + N ) ) | ( ( F ` C ) ` k ) = 0 }   =>    |- ( C e. ( O \ E ) -> inf ( S , RR , < ) e. S )
12-Jun-2026	infssfzledc 10648	The infimum of a decidable inhabited subset of an integer range is a lower bound for that set. (Contributed by Jim Kingdon, 12-Jun-2026.)
|- S = { n e. ( M ... N ) | ps }   &    |- ( ph -> A e. S )   &    |- ( ( ph /\ n e. ( M ... A ) ) -> DECID ps )   =>    |- ( ph -> inf ( S , RR , < ) <_ A )
12-Jun-2026	infssfzcldc 10647	The infimum of a decidable inhabited subset of an integer range is a member of the set. (Contributed by Jim Kingdon, 12-Jun-2026.)
|- S = { n e. ( M ... N ) | ps }   &    |- ( ph -> A e. S )   &    |- ( ( ph /\ n e. ( M ... A ) ) -> DECID ps )   =>    |- ( ph -> inf ( S , RR , < ) e. S )
8-Jun-2026	ballotfilemdifcfi 13203	Lemma for ballotfi . The portion of a counting representing votes for B up to a specified integer is finite. (Contributed by Jim Kingdon, 8-Jun-2026.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- ( ph -> C e. O )   &    |- ( ph -> J e. ZZ )   =>    |- ( ph -> ( ( 1 ... J ) \ C ) e. Fin )
8-Jun-2026	ballotfilemcinfi 13202	Lemma for ballotfi . The portion of a counting representing votes for A up to a specified integer is finite. (Contributed by Jim Kingdon, 8-Jun-2026.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- ( ph -> C e. O )   &    |- ( ph -> J e. ZZ )   =>    |- ( ph -> ( ( 1 ... J ) i^i C ) e. Fin )
8-Jun-2026	zfidc 9702	Whether an integer is an element of a finite set of integers is decidable. (Contributed by Jim Kingdon, 8-Jun-2026.)
|- ( ( S C_ ZZ /\ A e. ZZ /\ S e. Fin ) -> DECID A e. S )
7-Jun-2026	ballotfilemcdc 13201	Lemma for ballotfi . It is decidable whether a given integer is an element of a particular element of O. (Contributed by Jim Kingdon, 7-Jun-2026.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- ( ph -> C e. O )   &    |- ( ph -> K e. ZZ )   =>    |- ( ph -> DECID K e. C )
5-Jun-2026	hashpwfi 11247	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 7310. For the number of subsets (which need not be finite) of a set, see pw1mapen 16940. (Contributed by Jim Kingdon, 5-Jun-2026.)
|- ( A e. Fin -> (♯ ` ( ~P A i^i Fin ) ) = ( 2 ^ (♯ ` A ) ) )
4-Jun-2026	ballotfilemonn 13199	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
3-Jun-2026	papeq2 7600	Equality theorem for apartness predicate. (Contributed by Jim Kingdon, 3-Jun-2026.)
|- ( A = B -> ( R Ap A <-> R Ap B ) )
3-Jun-2026	papeq1 7599	Equality theorem for apartness predicate. (Contributed by Jim Kingdon, 3-Jun-2026.)
|- ( R = S -> ( R Ap A <-> S Ap A ) )
2-Jun-2026	resq01 11073	If a real number equals its square, it must be 0 or 1. (Contributed by Jim Kingdon, 2-Jun-2026.)
|- ( A e. RR -> ( ( A ^ 2 ) = A <-> ( A = 0 \/ A = 1 ) ) )
31-May-2026	aprprop 14574	If two structures have the same ring components (properties), df-apr 14563 generates the same relation for both of them. (Contributed by Jim Kingdon, 31-May-2026.)
|- ( Base ` K ) = ( Base ` L )   &    |- ( +g ` K ) = ( +g ` L )   &    |- ( .r ` K ) = ( .r ` L )   =>    |- ( K e. Ring -> (#r ` K ) = (#r ` L ) )
31-May-2026	ringunitsap0 14567	The set of units of a ring. If R 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 14573). Given the definition of #r this theorem holds even if # is not an apartness, however. (Contributed by Jim Kingdon, 31-May-2026.)
|- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- # = (#r ` R )   =>    |- ( R e. Ring -> { x e. B | x # .0. } = (Unit ` R ) )
30-May-2026	ringunitap 14566	Elementhood in the set of units. (Contributed by Jim Kingdon, 30-May-2026.)
|- B = ( Base ` R )   &    |- U = (Unit ` R )   &    |- .0. = ( 0g ` R )   &    |- # = (#r ` R )   =>    |- ( R e. Ring -> ( X e. U <-> ( X e. B /\ X # .0. ) ) )
29-May-2026	drnglring 14580	A division ring is a local ring. (Contributed by Jim Kingdon, 29-May-2026.)
|- ( R e. DivRing -> R e. LRing )
29-May-2026	isdrngtap 14579	The predicate "is a division ring". (Contributed by Jim Kingdon, 29-May-2026.)
|- B = ( Base ` R )   &    |- # = (#r ` R )   =>    |- ( R e. DivRing <-> ( R e. Ring /\ # TAp B ) )
29-May-2026	df-drngap 14577	Define class of all division rings. A division ring is a ring in which the relation given by df-apr 14563 is a tight apartness. (Contributed by Jim Kingdon, 29-May-2026.)
|- DivRing = { r e. Ring | (#r ` r ) TAp ( Base ` r ) }
29-May-2026	aprunit 14565	The df-apr 14563 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.)
|- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- U = (Unit ` R )   &    |- # = (#r ` R )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( X # .0. <-> X e. U ) )
29-May-2026	tapap 7606	A tight apartness is an apartness. (Contributed by Jim Kingdon, 29-May-2026.)
|- ( R TAp A -> R Ap A )
28-May-2026	aprlring 14573	A ring is a local ring if and only if the relation given by df-apr 14563 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 7603	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	aprnzr 14572	If the relation given by df-apr 14563 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 7602	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 7601	An apartness is irreflexive. (Contributed by Jim Kingdon, 27-May-2026.)
|- ( ( R Ap A /\ X e. A ) -> -. X R X )
24-May-2026	gsumzfi 14135	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 gsumg ( k e. A |-> .0. ) ) = .0. )
22-May-2026	sshashneg 11259	Subsets of a class of a negative size (a degenerate case). Together with ssenneg 11258 this shows that sseqn 11257 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 11258	Subsets of a class of a negative size (a degenerate case). Together with sshashneg 11259 this shows that sseqn 11257 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 11257	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 11198 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 11258 and sshashneg 11259. (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 } )
22-May-2026	bilanri 389	Inference adding a conjunct to the right-hand side of a biconditional. (Contributed by Matthew House, 22-May-2026.)
|- ( ph <-> ps )   =>    |- ( ( ch /\ ps ) -> ph )
22-May-2026	biranri 388	Inference adding a conjunct to the right-hand side of a biconditional. (Contributed by Matthew House, 22-May-2026.)
|- ( ph <-> ps )   =>    |- ( ( ps /\ ch ) -> ph )
22-May-2026	bilani 387	Inference adding a conjunct to the left-hand side of a biconditional. (Contributed by Matthew House, 22-May-2026.)
|- ( ph <-> ps )   =>    |- ( ( ch /\ ph ) -> ps )
22-May-2026	birani 386	Inference adding a conjunct to the left-hand side of a biconditional. (Contributed by Matthew House, 22-May-2026.)
|- ( ph <-> ps )   =>    |- ( ( ph /\ ch ) -> ps )
20-May-2026	ballotfilemofi 13197	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 7311	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 7310	The number of finite subsets of a finite set. For a similar theorem with set size expressed using ♯ (df-ihash 11193), see hashpwfi 11247. (Contributed by Jim Kingdon, 18-May-2026.)
|- ( A e. Fin -> ( 2o ^m A ) ~~ ( ~P A i^i Fin ) )
18-May-2026	fissfi 7253	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 5566	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 5565	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 7291	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 7236. (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 10385	A linear combination of two reals which lies in the interval between them. Like lincmb01cmp 10384 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 7596	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 863, which translate to 1o and (/) respectively by iftrue 3642 and iffalse 3645, giving pwtrufal 16941). As proved in if0ab 3638, 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 4290	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 4622. (Contributed by BJ, 5-May-2026.)
|- ( A e. V -> if ( ph , A , (/) ) e. ~P A )
5-May-2026	if0ss 3639	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 16982	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 16980 and repiecege0 16981. 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. 16981 (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 16981	Piecewise definition on the reals agrees with the nonnegative part of the definition. See repiecef 16982 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 16980	Piecewise definition on the reals agrees with the nonpositive part of the definition. See repiecef 16982 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 16979	Lemma for repiecele0 16980, repiecege0 16981, and repiecef 16982. 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 17003	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 17002 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 16951	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 1499. (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 16950	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 1498. (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 16949	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 1497. (Contributed by Jim Kingdon, 22-Apr-2026.)
|- (EXMID <-> A. x e. ~P 1o ( -. -. x = 1o -> x = 1o ) )
18-Apr-2026	hashtpglem 11276	Lemma for hashtpg 11277. 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 11275	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 16664	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 16663	Lemma for depind 16664. (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 16662	Lemma for depind 16664. (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 16661	Lemma for depind 16664. (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	gsumclfi 14136	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 gsumg F ) e. B )
4-Apr-2026	gzsumsplit0 14125	Splitting off the rightmost summand of a group sum (even if it is the only summand). Similar to gzsumsplit1r 13692 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 gzsumgz F ) = ( ( G gzsumgz ( F |` ( M ... N ) ) ) .+ ( F ` ( N + 1 ) ) ) )
4-Apr-2026	fzf1o 12120	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	gsump1 14134	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 gsumg F ) = ( ( G gsumg ( F |` Y ) ) .+ ( F ` Z ) ) )
2-Apr-2026	gsumsncmn 14133	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 gsumg ( k e. { M } |-> A ) ) = C )
31-Mar-2026	sspw1or2 7534	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 ) }