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 17-Sep-2024 at 6:39 AM ET.

Recent Additions to the Intuitionistic Logic Explorer

Date	Label	Description
Theorem
14-Sep-2024	nnpredlt 4582	The predecessor (see nnpredcl 4581) of a nonzero natural number is less than (see df-iord 4326) that number. (Contributed by Jim Kingdon, 14-Sep-2024.)
|- ( ( A e. om /\ A =/= (/) ) -> U. A e. A )
13-Sep-2024	nninfisollemeq 7069	Lemma for nninfisol 7070. The case where N is a successor and N and X are equal. (Contributed by Jim Kingdon, 13-Sep-2024.)
|- ( ph -> X e. ℕ∞ )   &    |- ( ph -> ( X ` N ) = (/) )   &    |- ( ph -> N e. om )   &    |- ( ph -> N =/= (/) )   &    |- ( ph -> ( X ` U. N ) = 1o )   =>    |- ( ph -> DECID ( i e. om |-> if ( i e. N , 1o , (/) ) ) = X )
13-Sep-2024	nninfisollemne 7068	Lemma for nninfisol 7070. A case where N is a successor and N and X are not equal. (Contributed by Jim Kingdon, 13-Sep-2024.)
|- ( ph -> X e. ℕ∞ )   &    |- ( ph -> ( X ` N ) = (/) )   &    |- ( ph -> N e. om )   &    |- ( ph -> N =/= (/) )   &    |- ( ph -> ( X ` U. N ) = (/) )   =>    |- ( ph -> DECID ( i e. om |-> if ( i e. N , 1o , (/) ) ) = X )
13-Sep-2024	nninfisollem0 7067	Lemma for nninfisol 7070. The case where N is zero. (Contributed by Jim Kingdon, 13-Sep-2024.)
|- ( ph -> X e. ℕ∞ )   &    |- ( ph -> ( X ` N ) = (/) )   &    |- ( ph -> N e. om )   &    |- ( ph -> N = (/) )   =>    |- ( ph -> DECID ( i e. om |-> if ( i e. N , 1o , (/) ) ) = X )
12-Sep-2024	nninfisol 7070	Finite elements of ℕ∞ are isolated. That is, given a natural number and any element of ℕ∞, it is decidable whether the natural number (when converted to an element of ℕ∞) is equal to the given element of ℕ∞. Stated in an online post by Martin Escardo. One way to understand this theorem is that you do not need to look at an unbounded number of elements of the sequence X to decide whether it is equal to N (in fact, you only need to look at two elements and N tells you where to look). (Contributed by BJ and Jim Kingdon, 12-Sep-2024.)
|- ( ( N e. om /\ X e. ℕ∞ ) -> DECID ( i e. om |-> if ( i e. N , 1o , (/) ) ) = X )
7-Sep-2024	eulerthlemfi 12091	Lemma for eulerth 12096. The set S is finite. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 7-Sep-2024.)
|- ( ph -> ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) )   &    |- S = { y e. ( 0..^ N ) | ( y gcd N ) = 1 }   =>    |- ( ph -> S e. Fin )
7-Sep-2024	modqexp 10537	Exponentiation property of the modulo operation, see theorem 5.2(c) in [ApostolNT] p. 107. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 7-Sep-2024.)
|- ( ph -> A e. ZZ )   &    |- ( ph -> B e. ZZ )   &    |- ( ph -> C e. NN0 )   &    |- ( ph -> D e. QQ )   &    |- ( ph -> 0 < D )   &    |- ( ph -> ( A mod D ) = ( B mod D ) )   =>    |- ( ph -> ( ( A ^ C ) mod D ) = ( ( B ^ C ) mod D ) )
5-Sep-2024	eulerthlemh 12094	Lemma for eulerth 12096. A permutation of ( 1 ... ( phi ` N ) ). (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 5-Sep-2024.)
|- ( ph -> ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) )   &    |- S = { y e. ( 0..^ N ) | ( y gcd N ) = 1 }   &    |- ( ph -> F : ( 1 ... ( phi ` N ) ) -1-1-onto-> S )   &    |- H = ( `' F o. ( y e. ( 1 ... ( phi ` N ) ) |-> ( ( A x. ( F ` y ) ) mod N ) ) )   =>    |- ( ph -> H : ( 1 ... ( phi ` N ) ) -1-1-onto-> ( 1 ... ( phi ` N ) ) )
2-Sep-2024	eulerthlemth 12095	Lemma for eulerth 12096. The result. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 2-Sep-2024.)
|- ( ph -> ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) )   &    |- S = { y e. ( 0..^ N ) | ( y gcd N ) = 1 }   &    |- ( ph -> F : ( 1 ... ( phi ` N ) ) -1-1-onto-> S )   =>    |- ( ph -> ( ( A ^ ( phi ` N ) ) mod N ) = ( 1 mod N ) )
2-Sep-2024	eulerthlema 12093	Lemma for eulerth 12096. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 2-Sep-2024.)
|- ( ph -> ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) )   &    |- S = { y e. ( 0..^ N ) | ( y gcd N ) = 1 }   &    |- ( ph -> F : ( 1 ... ( phi ` N ) ) -1-1-onto-> S )   =>    |- ( ph -> ( ( ( A ^ ( phi ` N ) ) x. prod_ x e. ( 1 ... ( phi ` N ) ) ( F ` x ) ) mod N ) = ( prod_ x e. ( 1 ... ( phi ` N ) ) ( ( A x. ( F ` x ) ) mod N ) mod N ) )
2-Sep-2024	eulerthlemrprm 12092	Lemma for eulerth 12096. N and prod_ x e. ( 1 ... ( phi ` N ) ) ( F ` x ) are relatively prime. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 2-Sep-2024.)
|- ( ph -> ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) )   &    |- S = { y e. ( 0..^ N ) | ( y gcd N ) = 1 }   &    |- ( ph -> F : ( 1 ... ( phi ` N ) ) -1-1-onto-> S )   =>    |- ( ph -> ( N gcd prod_ x e. ( 1 ... ( phi ` N ) ) ( F ` x ) ) = 1 )
30-Aug-2024	fprodap0f 11526	A finite product of terms apart from zero is apart from zero. A version of fprodap0 11511 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) (Revised by Jim Kingdon, 30-Aug-2024.)
|- F/ k ph   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- ( ( ph /\ k e. A ) -> B # 0 )   =>    |- ( ph -> prod_ k e. A B # 0 )
28-Aug-2024	fprodrec 11519	The finite product of reciprocals is the reciprocal of the product. (Contributed by Jim Kingdon, 28-Aug-2024.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- ( ( ph /\ k e. A ) -> B # 0 )   =>    |- ( ph -> prod_ k e. A ( 1 / B ) = ( 1 / prod_ k e. A B ) )
26-Aug-2024	exmidontri2or 7172	Ordinal trichotomy is equivalent to excluded middle. (Contributed by Jim Kingdon, 26-Aug-2024.)
|- (EXMID <-> A. x e. On A. y e. On ( x C_ y \/ y C_ x ) )
26-Aug-2024	exmidontri 7168	Ordinal trichotomy is equivalent to excluded middle. (Contributed by Jim Kingdon, 26-Aug-2024.)
|- (EXMID <-> A. x e. On A. y e. On ( x e. y \/ x = y \/ y e. x ) )
26-Aug-2024	ontri2orexmidim 4530	Ordinal trichotomy implies excluded middle. Closed form of ordtri2or2exmid 4529. (Contributed by Jim Kingdon, 26-Aug-2024.)
|- ( A. x e. On A. y e. On ( x C_ y \/ y C_ x ) -> DECID ph )
26-Aug-2024	ontriexmidim 4480	Ordinal trichotomy implies excluded middle. Closed form of ordtriexmid 4479. (Contributed by Jim Kingdon, 26-Aug-2024.)
|- ( A. x e. On A. y e. On ( x e. y \/ x = y \/ y e. x ) -> DECID ph )
25-Aug-2024	onntri2or 7175	Double negated ordinal trichotomy. (Contributed by Jim Kingdon, 25-Aug-2024.)
|- ( -. -. EXMID <-> A. x e. On A. y e. On -. -. ( x C_ y \/ y C_ x ) )
25-Aug-2024	onntri3or 7174	Double negated ordinal trichotomy. (Contributed by Jim Kingdon, 25-Aug-2024.)
|- ( -. -. EXMID <-> A. x e. On A. y e. On -. -. ( x e. y \/ x = y \/ y e. x ) )
25-Aug-2024	csbcow 3042	Composition law for chained substitutions into a class. Version of csbco 3041 with a disjoint variable condition, which requires fewer axioms. (Contributed by NM, 10-Nov-2005.) (Revised by Gino Giotto, 25-Aug-2024.)
|- [_ A / y ]_ [_ y / x ]_ B = [_ A / x ]_ B
25-Aug-2024	cbvreuvw 2686	Version of cbvreuv 2682 with a disjoint variable condition. (Contributed by Gino Giotto, 10-Jan-2024.) Reduce axiom usage. (Revised by Gino Giotto, 25-Aug-2024.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( E! x e. A ph <-> E! y e. A ps )
25-Aug-2024	cbvrexvw 2685	Version of cbvrexv 2681 with a disjoint variable condition. (Contributed by Gino Giotto, 10-Jan-2024.) Reduce axiom usage. (Revised by Gino Giotto, 25-Aug-2024.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( E. x e. A ph <-> E. y e. A ps )
25-Aug-2024	cbvralvw 2684	Version of cbvralv 2680 with a disjoint variable condition. (Contributed by Gino Giotto, 10-Jan-2024.) Reduce axiom usage. (Revised by Gino Giotto, 25-Aug-2024.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( A. x e. A ph <-> A. y e. A ps )
25-Aug-2024	cbvabw 2280	Version of cbvab 2281 with a disjoint variable condition. (Contributed by Gino Giotto, 10-Jan-2024.) Reduce axiom usage. (Revised by Gino Giotto, 25-Aug-2024.)
|- F/ y ph   &    |- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- { x | ph } = { y | ps }
25-Aug-2024	nfsbv 1927	If z is not free in ph, it is not free in [ y / x ] ph when z is distinct from x and y. Version of nfsb 1926 requiring more disjoint variables. (Contributed by Wolf Lammen, 7-Feb-2023.) Remove disjoint variable condition on x , y. (Revised by Steven Nguyen, 13-Aug-2023.) Reduce axiom usage. (Revised by Gino Giotto, 25-Aug-2024.)
|- F/ z ph   =>    |- F/ z [ y / x ] ph
25-Aug-2024	cbvexvw 1900	Change bound variable. See cbvexv 1898 for a version with fewer disjoint variable conditions. (Contributed by NM, 19-Apr-2017.) Avoid ax-7 1428. (Revised by Gino Giotto, 25-Aug-2024.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( E. x ph <-> E. y ps )
25-Aug-2024	cbvalvw 1899	Change bound variable. See cbvalv 1897 for a version with fewer disjoint variable conditions. (Contributed by NM, 9-Apr-2017.) Avoid ax-7 1428. (Revised by Gino Giotto, 25-Aug-2024.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( A. x ph <-> A. y ps )
25-Aug-2024	nfal 1556	If x is not free in ph, it is not free in A. y ph. (Contributed by Mario Carneiro, 11-Aug-2016.) Remove dependency on ax-4 1490. (Revised by Gino Giotto, 25-Aug-2024.)
|- F/ x ph   =>    |- F/ x A. y ph
24-Aug-2024	gcdcomd 11849	The gcd operator is commutative, deduction version. (Contributed by SN, 24-Aug-2024.)
|- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   =>    |- ( ph -> ( M gcd N ) = ( N gcd M ) )
17-Aug-2024	fprodcl2lem 11495	Finite product closure lemma. (Contributed by Scott Fenton, 14-Dec-2017.) (Revised by Jim Kingdon, 17-Aug-2024.)
|- ( ph -> S C_ CC )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S )   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. S )   &    |- ( ph -> A =/= (/) )   =>    |- ( ph -> prod_ k e. A B e. S )
16-Aug-2024	if0ab 13351	Expression of a conditional class as a class abstraction when the False alternative is the empty class: in that case, the conditional class is the extension, in the True alternative, of the condition. Remark: a consequence which could be formalized is the inclusion |- if ( ph , A , (/) ) C_ A and therefore, using elpwg 3551, |- ( A e. V -> if ( ph , A , (/) ) e. ~P A ), from which fmelpw1o 13352 could be derived, yielding an alternative proof. (Contributed by BJ, 16-Aug-2024.)
|- if ( ph , A , (/) ) = { x e. A | ph }
16-Aug-2024	fprodunsn 11494	Multiply in an additional term in a finite product. See also fprodsplitsn 11523 which is the same but with a F/ k ph hypothesis in place of the distinct variable condition between ph and k. (Contributed by Jim Kingdon, 16-Aug-2024.)
|- F/_ k D   &    |- ( ph -> A e. Fin )   &    |- ( ph -> B e. V )   &    |- ( ph -> -. B e. A )   &    |- ( ( ph /\ k e. A ) -> C e. CC )   &    |- ( ph -> D e. CC )   &    |- ( k = B -> C = D )   =>    |- ( ph -> prod_ k e. ( A u. { B } ) C = ( prod_ k e. A C x. D ) )
15-Aug-2024	bj-charfundcALT 13355	Alternate proof of bj-charfundc 13354. It was expected to be much shorter since it uses bj-charfun 13353 for the main part of the proof and the rest is basic computations, but these turn out to be lengthy, maybe because of the limited library of available lemmas. (Contributed by BJ, 15-Aug-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> F = ( x e. X |-> if ( x e. A , 1o , (/) ) ) )   &    |- ( ph -> A. x e. X DECID x e. A )   =>    |- ( ph -> ( F : X --> 2o /\ ( A. x e. ( X i^i A ) ( F ` x ) = 1o /\ A. x e. ( X \ A ) ( F ` x ) = (/) ) ) )
15-Aug-2024	bj-charfun 13353	Properties of the characteristic function on the class X of the class A. (Contributed by BJ, 15-Aug-2024.)
|- ( ph -> F = ( x e. X |-> if ( x e. A , 1o , (/) ) ) )   =>    |- ( ph -> ( ( F : X --> ~P 1o /\ ( F |` ( ( X i^i A ) u. ( X \ A ) ) ) : ( ( X i^i A ) u. ( X \ A ) ) --> 2o ) /\ ( A. x e. ( X i^i A ) ( F ` x ) = 1o /\ A. x e. ( X \ A ) ( F ` x ) = (/) ) ) )
15-Aug-2024	fmelpw1o 13352	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 837, which translate to 1o and (/) respectively by iftrue 3510 and iffalse 3513, giving pwtrufal 13540). As proved in if0ab 13351, the associated element of ~P 1o is the extension, in ~P 1o, of the formula ph. (Contributed by BJ, 15-Aug-2024.)
|- if ( ph , 1o , (/) ) e. ~P 1o
15-Aug-2024	cnstab 8514	Equality of complex numbers is stable. Stability here means -. -. A = B -> A = B as defined at df-stab 817. This theorem for real numbers is Proposition 5.2 of [BauerHanson], p. 27. (Contributed by Jim Kingdon, 1-Aug-2023.) (Proof shortened by BJ, 15-Aug-2024.)
|- ( ( A e. CC /\ B e. CC ) -> STAB A = B )
15-Aug-2024	subap0d 8513	Two numbers apart from each other have difference apart from zero. (Contributed by Jim Kingdon, 12-Aug-2021.) (Proof shortened by BJ, 15-Aug-2024.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> A # B )   =>    |- ( ph -> ( A - B ) # 0 )
15-Aug-2024	ifexd 4443	Existence of a conditional class (deduction form). (Contributed by BJ, 15-Aug-2024.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   =>    |- ( ph -> if ( ph , A , B ) e. _V )
15-Aug-2024	ifelpwun 4442	Existence of a conditional class, quantitative version (inference form). (Contributed by BJ, 15-Aug-2024.)
|- A e. _V   &    |- B e. _V   =>    |- if ( ph , A , B ) e. ~P ( A u. B )
15-Aug-2024	ifelpwund 4441	Existence of a conditional class, quantitative version (deduction form). (Contributed by BJ, 15-Aug-2024.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   =>    |- ( ph -> if ( ph , A , B ) e. ~P ( A u. B ) )
15-Aug-2024	ifelpwung 4440	Existence of a conditional class, quantitative version (closed form). (Contributed by BJ, 15-Aug-2024.)
|- ( ( A e. V /\ B e. W ) -> if ( ph , A , B ) e. ~P ( A u. B ) )
15-Aug-2024	ifidss 3520	A conditional class whose two alternatives are equal is included in that alternative. With excluded middle, we can prove it is equal to it. (Contributed by BJ, 15-Aug-2024.)
|- if ( ph , A , A ) C_ A
15-Aug-2024	ifssun 3519	A conditional class is included in the union of its two alternatives. (Contributed by BJ, 15-Aug-2024.)
|- if ( ph , A , B ) C_ ( A u. B )
12-Aug-2024	exmidontriimlem2 7151	Lemma for exmidontriim 7154. (Contributed by Jim Kingdon, 12-Aug-2024.)
|- ( ph -> B e. On )   &    |- ( ph -> EXMID )   &    |- ( ph -> A. y e. B ( A e. y \/ A = y \/ y e. A ) )   =>    |- ( ph -> ( A e. B \/ A. y e. B y e. A ) )
12-Aug-2024	exmidontriimlem1 7150	Lemma for exmidontriim 7154. A variation of r19.30dc 2604. (Contributed by Jim Kingdon, 12-Aug-2024.)
|- ( ( A. x e. A ( ph \/ ps \/ ch ) /\ EXMID ) -> ( E. x e. A ph \/ E. x e. A ps \/ A. x e. A ch ) )
11-Aug-2024	nndc 837	Double negation of decidability of a formula. Intuitionistic logic refutes the negation of decidability (but does not prove decidability) of any formula. This should not trick the reader into thinking that -. -. EXMID is provable in intuitionistic logic. Indeed, if we could quantify over formula metavariables, then generalizing nnexmid 836 over ph would give " |- A. ph -. -. DECID ph", but EXMID is " A. phDECID ph", so proving -. -. EXMID would amount to proving " -. -. A. phDECID ph", which is not implied by the above theorem. Indeed, the converse of nnal 1629 does not hold. Since our system does not allow quantification over formula metavariables, we can reproduce this argument by representing formulas as subsets of ~P 1o, like we do in our definition of EXMID (df-exmid 4156): then, we can prove A. x e. ~P 1o -. -. DECID x = 1o but we cannot prove -. -. A. x e. ~P 1oDECID x = 1o because the converse of nnral 2447 does not hold. Actually, -. -. EXMID is not provable in intuitionistic logic since intuitionistic logic has models satisfying -. EXMID and noncontradiction holds (pm3.24 683). (Contributed by BJ, 9-Oct-2019.) Add explanation on non-provability of -. -. EXMID. (Revised by BJ, 11-Aug-2024.)
|- -. -. DECID ph
10-Aug-2024	exmidontriim 7154	Excluded middle implies ordinal trichotomy. Lemma 10.4.1 of [HoTT], p. (varies). The proof follows the proof from the HoTT book fairly closely. (Contributed by Jim Kingdon, 10-Aug-2024.)
|- (EXMID -> A. x e. On A. y e. On ( x e. y \/ x = y \/ y e. x ) )
10-Aug-2024	exmidontriimlem4 7153	Lemma for exmidontriim 7154. The induction step for the induction on A. (Contributed by Jim Kingdon, 10-Aug-2024.)
|- ( ph -> A e. On )   &    |- ( ph -> B e. On )   &    |- ( ph -> EXMID )   &    |- ( ph -> A. z e. A A. y e. On ( z e. y \/ z = y \/ y e. z ) )   =>    |- ( ph -> ( A e. B \/ A = B \/ B e. A ) )
10-Aug-2024	exmidontriimlem3 7152	Lemma for exmidontriim 7154. What we get to do based on induction on both A and B. (Contributed by Jim Kingdon, 10-Aug-2024.)
|- ( ph -> A e. On )   &    |- ( ph -> B e. On )   &    |- ( ph -> EXMID )   &    |- ( ph -> A. z e. A A. y e. On ( z e. y \/ z = y \/ y e. z ) )   &    |- ( ph -> A. y e. B ( A e. y \/ A = y \/ y e. A ) )   =>    |- ( ph -> ( A e. B \/ A = B \/ B e. A ) )
10-Aug-2024	nnnninf2 7064	Canonical embedding of suc om into ℕ∞. (Contributed by BJ, 10-Aug-2024.)
|- ( N e. suc om -> ( i e. om |-> if ( i e. N , 1o , (/) ) ) e. ℕ∞ )
10-Aug-2024	infnninf 7061	The point at infinity in ℕ∞ is the constant sequence equal to 1o. Note that with our encoding of functions, that constant function can also be expressed as ( om X. { 1o } ), as fconstmpt 4632 shows. (Contributed by Jim Kingdon, 14-Jul-2022.) Use maps-to notation. (Revised by BJ, 10-Aug-2024.)
|- ( i e. om |-> 1o ) e. ℕ∞
9-Aug-2024	ss1o0el1o 6854	Reformulation of ss1o0el1 4158 using 1o instead of { (/) }. (Contributed by BJ, 9-Aug-2024.)
|- ( A C_ 1o -> ( (/) e. A <-> A = 1o ) )
9-Aug-2024	pw1dc0el 6853	Another equivalent of excluded middle, which is a mere reformulation of the definition. (Contributed by BJ, 9-Aug-2024.)
|- (EXMID <-> A. x e. ~P 1oDECID (/) e. x )
9-Aug-2024	ss1o0el1 4158	A subclass of { (/) } contains the empty set if and only if it equals { (/) }. (Contributed by BJ and Jim Kingdon, 9-Aug-2024.)
|- ( A C_ { (/) } -> ( (/) e. A <-> A = { (/) } ) )
8-Aug-2024	pw1dc1 6855	If, in the set of truth values (the powerset of 1o), equality to 1o is decidable, then excluded middle holds (and conversely). (Contributed by BJ and Jim Kingdon, 8-Aug-2024.)
|- (EXMID <-> A. x e. ~P 1oDECID x = 1o )
7-Aug-2024	pw1fin 6852	Excluded middle is equivalent to the power set of 1o being finite. (Contributed by SN and Jim Kingdon, 7-Aug-2024.)
|- (EXMID <-> ~P 1o e. Fin )
7-Aug-2024	elomssom 4563	A natural number ordinal is, as a set, included in the set of natural number ordinals. (Contributed by NM, 21-Jun-1998.) Extract this result from the previous proof of elnn 4564. (Revised by BJ, 7-Aug-2024.)
|- ( A e. om -> A C_ om )
6-Aug-2024	bj-charfunbi 13357	In an ambient set X, if membership in A is stable, then it is decidable if and only if A has a characteristic function. This characterization can be applied to singletons when the set X has stable equality, which is the case as soon as it has a tight apartness relation. (Contributed by BJ, 6-Aug-2024.)
|- ( ph -> X e. V )   &    |- ( ph -> A. x e. X STAB x e. A )   =>    |- ( ph -> ( A. x e. X DECID x e. A <-> E. f e. ( 2o ^m X ) ( A. x e. ( X i^i A ) ( f ` x ) = 1o /\ A. x e. ( X \ A ) ( f ` x ) = (/) ) ) )
6-Aug-2024	bj-charfunr 13356	If a class A has a "weak" characteristic function on a class X, then negated membership in A is decidable (in other words, membership in A is testable) in X. The hypothesis imposes that X be a set. As usual, it could be formulated as |- ( ph -> ( F : X --> om /\ ... ) ) to deal with general classes, but that extra generality would not make the theorem much more useful. The theorem would still hold if the codomain of f were any class with testable equality to the point where ( X \ A ) is sent. (Contributed by BJ, 6-Aug-2024.)
|- ( ph -> E. f e. ( om ^m X ) ( A. x e. ( X i^i A ) ( f ` x ) =/= (/) /\ A. x e. ( X \ A ) ( f ` x ) = (/) ) )   =>    |- ( ph -> A. x e. X DECID -. x e. A )
6-Aug-2024	bj-charfundc 13354	Properties of the characteristic function on the class X of the class A, provided membership in A is decidable in X. (Contributed by BJ, 6-Aug-2024.)
|- ( ph -> F = ( x e. X |-> if ( x e. A , 1o , (/) ) ) )   &    |- ( ph -> A. x e. X DECID x e. A )   =>    |- ( ph -> ( F : X --> 2o /\ ( A. x e. ( X i^i A ) ( F ` x ) = 1o /\ A. x e. ( X \ A ) ( F ` x ) = (/) ) ) )
6-Aug-2024	prodssdc 11479	Change the index set to a subset in an upper integer product. (Contributed by Scott Fenton, 11-Dec-2017.) (Revised by Jim Kingdon, 6-Aug-2024.)
|- ( ph -> A C_ B )   &    |- ( ( ph /\ k e. A ) -> C e. CC )   &    |- ( ph -> E. n e. ( ZZ>= ` M ) E. y ( y # 0 /\ seq n ( x. , ( k e. ( ZZ>= ` M ) |-> if ( k e. B , C , 1 ) ) ) ~~> y ) )   &    |- ( ph -> A. j e. ( ZZ>= ` M )DECID j e. A )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ k e. ( B \ A ) ) -> C = 1 )   &    |- ( ph -> B C_ ( ZZ>= ` M ) )   &    |- ( ph -> A. j e. ( ZZ>= ` M )DECID j e. B )   =>    |- ( ph -> prod_ k e. A C = prod_ k e. B C )
5-Aug-2024	fnmptd 13350	The maps-to notation defines a function with domain (deduction form). (Contributed by BJ, 5-Aug-2024.)
|- ( ph -> F = ( x e. A |-> B ) )   &    |- ( ( ph /\ x e. A ) -> B e. V )   =>    |- ( ph -> F Fn A )
5-Aug-2024	funmptd 13349	The maps-to notation defines a function (deduction form). Note: one should similarly prove a deduction form of funopab4 5206, then prove funmptd 13349 from it, and then prove funmpt 5207 from that: this would reduce global proof length. (Contributed by BJ, 5-Aug-2024.)
|- ( ph -> F = ( x e. A |-> B ) )   =>    |- ( ph -> Fun F )
5-Aug-2024	2ssom 13348	The ordinal 2 is included in the set of natural number ordinals. (Contributed by BJ, 5-Aug-2024.)
|- 2o C_ om
5-Aug-2024	bj-dcfal 13298	The false truth value is decidable. (Contributed by BJ, 5-Aug-2024.)
|- DECID F.
5-Aug-2024	bj-dctru 13296	The true truth value is decidable. (Contributed by BJ, 5-Aug-2024.)
|- DECID T.
5-Aug-2024	bj-stfal 13288	The false truth value is stable. (Contributed by BJ, 5-Aug-2024.)
|- STAB F.
5-Aug-2024	bj-sttru 13286	The true truth value is stable. (Contributed by BJ, 5-Aug-2024.)
|- STAB T.
5-Aug-2024	prod1dc 11476	Any product of one over a valid set is one. (Contributed by Scott Fenton, 7-Dec-2017.) (Revised by Jim Kingdon, 5-Aug-2024.)
|- ( ( ( M e. ZZ /\ A C_ ( ZZ>= ` M ) /\ A. j e. ( ZZ>= ` M )DECID j e. A ) \/ A e. Fin ) -> prod_ k e. A 1 = 1 )
2-Aug-2024	onntri52 7173	Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
|- ( -. -. EXMID -> -. -. A. x e. On A. y e. On ( x C_ y \/ y C_ x ) )
2-Aug-2024	onntri24 7171	Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
|- ( -. -. A. x e. On A. y e. On ( x C_ y \/ y C_ x ) -> A. x e. On A. y e. On -. -. ( x C_ y \/ y C_ x ) )
2-Aug-2024	onntri45 7170	Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
|- ( A. x e. On A. y e. On -. -. ( x C_ y \/ y C_ x ) -> -. -. EXMID )
2-Aug-2024	onntri51 7169	Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
|- ( -. -. EXMID -> -. -. A. x e. On A. y e. On ( x e. y \/ x = y \/ y e. x ) )
2-Aug-2024	onntri13 7167	Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
|- ( -. -. A. x e. On A. y e. On ( x e. y \/ x = y \/ y e. x ) -> A. x e. On A. y e. On -. -. ( x e. y \/ x = y \/ y e. x ) )
2-Aug-2024	onntri35 7166	Double negated ordinal trichotomy. There are five equivalent statements: (1) -. -. A. x e. On A. y e. On ( x e. y \/ x = y \/ y e. x ), (2) -. -. A. x e. On A. y e. On ( x C_ y \/ y C_ x ), (3) A. x e. On A. y e. On -. -. ( x e. y \/ x = y \/ y e. x ), (4) A. x e. On A. y e. On -. -. ( x C_ y \/ y C_ x ), and (5) -. -. EXMID. That these are all equivalent is expressed by (1) implies (3) (onntri13 7167), (3) implies (5) (onntri35 7166), (5) implies (1) (onntri51 7169), (2) implies (4) (onntri24 7171), (4) implies (5) (onntri45 7170), and (5) implies (2) (onntri52 7173). Another way of stating this is that EXMID is equivalent to trichotomy, either the x e. y \/ x = y \/ y e. x or the x C_ y \/ y C_ x form, as shown in exmidontri 7168 and exmidontri2or 7172, respectively. Thus -. -. EXMID is equivalent to (1) or (2). In addition, -. -. EXMID is equivalent to (3) by onntri3or 7174 and (4) by onntri2or 7175. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
|- ( A. x e. On A. y e. On -. -. ( x e. y \/ x = y \/ y e. x ) -> -. -. EXMID )
1-Aug-2024	nnral 2447	The double negation of a universal quantification implies the universal quantification of the double negation. Restricted quantifier version of nnal 1629. (Contributed by Jim Kingdon, 1-Aug-2024.)
|- ( -. -. A. x e. A ph -> A. x e. A -. -. ph )
31-Jul-2024	3nsssucpw1 7165	Negated excluded middle implies that 3o is not a subset of the successor of the power set of 1o. (Contributed by James E. Hanson and Jim Kingdon, 31-Jul-2024.)
|- ( -. EXMID -> -. 3o C_ suc ~P 1o )
31-Jul-2024	sucpw1nss3 7164	Negated excluded middle implies that the successor of the power set of 1o is not a subset of 3o. (Contributed by James E. Hanson and Jim Kingdon, 31-Jul-2024.)
|- ( -. EXMID -> -. suc ~P 1o C_ 3o )
30-Jul-2024	3nelsucpw1 7163	Three is not an element of the successor of the power set of 1o. (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.)
|- -. 3o e. suc ~P 1o
30-Jul-2024	sucpw1nel3 7162	The successor of the power set of 1o is not an element of 3o. (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.)
|- -. suc ~P 1o e. 3o
30-Jul-2024	sucpw1ne3 7161	Negated excluded middle implies that the successor of the power set of 1o is not three . (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.)
|- ( -. EXMID -> suc ~P 1o =/= 3o )
30-Jul-2024	pw1nel3 7160	Negated excluded middle implies that the power set of 1o is not an element of 3o. (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.)
|- ( -. EXMID -> -. ~P 1o e. 3o )
30-Jul-2024	pw1ne3 7159	The power set of 1o is not three. (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.)
|- ~P 1o =/= 3o
30-Jul-2024	pw1ne1 7158	The power set of 1o is not one. (Contributed by Jim Kingdon, 30-Jul-2024.)
|- ~P 1o =/= 1o
30-Jul-2024	pw1ne0 7157	The power set of 1o is not zero. (Contributed by Jim Kingdon, 30-Jul-2024.)
|- ~P 1o =/= (/)
29-Jul-2024	pw1on 7155	The power set of 1o is an ordinal. (Contributed by Jim Kingdon, 29-Jul-2024.)
|- ~P 1o e. On
28-Jul-2024	exmidpweq 6851	Excluded middle is equivalent to the power set of 1o being 2o. (Contributed by Jim Kingdon, 28-Jul-2024.)
|- (EXMID <-> ~P 1o = 2o )
27-Jul-2024	dcapnconstALT 13603	Decidability of real number apartness implies the existence of a certain non-constant function from real numbers to integers. A proof of dcapnconst 13602 by means of dceqnconst 13601. (Contributed by Jim Kingdon, 27-Jul-2024.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( A. x e. RR DECID x # 0 -> E. f ( f : RR --> ZZ /\ ( f ` 0 ) = 0 /\ A. x e. RR+ ( f ` x ) =/= 0 ) )
27-Jul-2024	reap0 13600	Real number trichotomy is equivalent to decidability of apartness from zero. (Contributed by Jim Kingdon, 27-Jul-2024.)
|- ( A. x e. RR A. y e. RR ( x < y \/ x = y \/ y < x ) <-> A. z e. RR DECID z # 0 )
26-Jul-2024	nconstwlpolemgt0 13605	Lemma for nconstwlpo 13607. If one of the terms of series is positive, so is the sum. (Contributed by Jim Kingdon, 26-Jul-2024.)
|- ( ph -> G : NN --> { 0 , 1 } )   &    |- A = sum_ i e. NN ( ( 1 / ( 2 ^ i ) ) x. ( G ` i ) )   &    |- ( ph -> E. x e. NN ( G ` x ) = 1 )   =>    |- ( ph -> 0 < A )
26-Jul-2024	nconstwlpolem0 13604	Lemma for nconstwlpo 13607. If all the terms of the series are zero, so is their sum. (Contributed by Jim Kingdon, 26-Jul-2024.)
|- ( ph -> G : NN --> { 0 , 1 } )   &    |- A = sum_ i e. NN ( ( 1 / ( 2 ^ i ) ) x. ( G ` i ) )   &    |- ( ph -> A. x e. NN ( G ` x ) = 0 )   =>    |- ( ph -> A = 0 )
24-Jul-2024	tridceq 13598	Real trichotomy implies decidability of real number equality. Or in other words, analytic LPO implies analytic WLPO (see trilpo 13585 and redcwlpo 13597). Thus, this is an analytic analogue to lpowlpo 7105. (Contributed by Jim Kingdon, 24-Jul-2024.)
|- ( A. x e. RR A. y e. RR ( x < y \/ x = y \/ y < x ) -> A. x e. RR A. y e. RR DECID x = y )
24-Jul-2024	iswomni0 13593	Weak omniscience stated in terms of equality with 0. Like iswomninn 13592 but with zero in place of one. (Contributed by Jim Kingdon, 24-Jul-2024.)
|- ( A e. V -> ( A e. WOmni <-> A. f e. ( { 0 , 1 } ^m A )DECID A. x e. A ( f ` x ) = 0 ) )
24-Jul-2024	lpowlpo 7105	LPO implies WLPO. Easy corollary of the more general omniwomnimkv 7104. There is an analogue in terms of analytic omniscience principles at tridceq 13598. (Contributed by Jim Kingdon, 24-Jul-2024.)
|- ( om e. Omni -> om e. WOmni )
23-Jul-2024	nconstwlpolem 13606	Lemma for nconstwlpo 13607. (Contributed by Jim Kingdon, 23-Jul-2024.)
|- ( ph -> F : RR --> ZZ )   &    |- ( ph -> ( F ` 0 ) = 0 )   &    |- ( ( ph /\ x e. RR+ ) -> ( F ` x ) =/= 0 )   &    |- ( ph -> G : NN --> { 0 , 1 } )   &    |- A = sum_ i e. NN ( ( 1 / ( 2 ^ i ) ) x. ( G ` i ) )   =>    |- ( ph -> ( A. y e. NN ( G ` y ) = 0 \/ -. A. y e. NN ( G ` y ) = 0 ) )
23-Jul-2024	dceqnconst 13601	Decidability of real number equality implies the existence of a certain non-constant function from real numbers to integers. Variation of Exercise 11.6(i) of [HoTT], p. (varies). See redcwlpo 13597 for more discussion of decidability of real number equality. (Contributed by BJ and Jim Kingdon, 24-Jun-2024.) (Revised by Jim Kingdon, 23-Jul-2024.)
|- ( A. x e. RR DECID x = 0 -> E. f ( f : RR --> ZZ /\ ( f ` 0 ) = 0 /\ A. x e. RR+ ( f ` x ) =/= 0 ) )
23-Jul-2024	redc0 13599	Two ways to express decidability of real number equality. (Contributed by Jim Kingdon, 23-Jul-2024.)
|- ( A. x e. RR A. y e. RR DECID x = y <-> A. z e. RR DECID z = 0 )
23-Jul-2024	canth 5775	No set A is equinumerous to its power set (Cantor's theorem), i.e., no function can map A onto its power set. Compare Theorem 6B(b) of [Enderton] p. 132. (Use nex 1480 if you want the form -. E. f f : A -onto-> ~P A.) (Contributed by NM, 7-Aug-1994.) (Revised by Noah R Kingdon, 23-Jul-2024.)
|- A e. _V   =>    |- -. F : A -onto-> ~P A
22-Jul-2024	nconstwlpo 13607	Existence of a certain non-constant function from reals to integers implies om e. WOmni (the Weak Limited Principle of Omniscience or WLPO). Based on Exercise 11.6(ii) of [HoTT], p. (varies). (Contributed by BJ and Jim Kingdon, 22-Jul-2024.)
|- ( ph -> F : RR --> ZZ )   &    |- ( ph -> ( F ` 0 ) = 0 )   &    |- ( ( ph /\ x e. RR+ ) -> ( F ` x ) =/= 0 )   =>    |- ( ph -> om e. WOmni )
15-Jul-2024	fprodseq 11473	The value of a product over a nonempty finite set. (Contributed by Scott Fenton, 6-Dec-2017.) (Revised by Jim Kingdon, 15-Jul-2024.)
|- ( k = ( F ` n ) -> B = C )   &    |- ( ph -> M e. NN )   &    |- ( ph -> F : ( 1 ... M ) -1-1-onto-> A )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- ( ( ph /\ n e. ( 1 ... M ) ) -> ( G ` n ) = C )   =>    |- ( ph -> prod_ k e. A B = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) )