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

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

Color key:   Intuitionistic Logic Explorer  Intuitionistic Logic Explorer   User Mathboxes  User Mathboxes  

Last updated on 21-Nov-2024 at 6:45 AM ET.
Recent Additions to the Intuitionistic Logic Explorer
DateLabelDescription
Theorem
 
18-Nov-2024basmex 12452 A structure whose base is inhabited is a set. (Contributed by Jim Kingdon, 18-Nov-2024.)
𝐵 = (Base‘𝐺)    ⇒   (𝐴 ∈ 𝐵 → 𝐺 ∈ V)
 
11-Nov-2024bj-con1st 13632 Contraposition when the antecedent is a negated stable proposition. See con1dc 846. (Contributed by BJ, 11-Nov-2024.)
(STAB 𝜑 → ((¬ 𝜑 → 𝜓) → (¬ 𝜓 → 𝜑)))
 
11-Nov-2024const 842 Contraposition when the antecedent is a negated stable proposition. See comment of condc 843. (Contributed by BJ, 18-Nov-2023.) (Proof shortened by BJ, 11-Nov-2024.)
(STAB 𝜑 → ((¬ 𝜑 → ¬ 𝜓) → (𝜓 → 𝜑)))
 
4-Nov-2024lgsfvalg 13546 Value of the function 𝐹 which defines the Legendre symbol at the primes. (Contributed by Mario Carneiro, 4-Feb-2015.) (Revised by Jim Kingdon, 4-Nov-2024.)
𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑁)), 1))    ⇒   ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝐹‘𝑀) = if(𝑀 ∈ ℙ, (if(𝑀 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑀 − 1) / 2)) + 1) mod 𝑀) − 1))↑(𝑀 pCnt 𝑁)), 1))
 
1-Nov-2024qsqeqor 10565 The squares of two rational numbers are equal iff one number equals the other or its negative. (Contributed by Jim Kingdon, 1-Nov-2024.)
((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → ((𝐴↑2) = (𝐵↑2) ↔ (𝐴 = 𝐵 ∨ 𝐴 = -𝐵)))
 
29-Oct-2024fiubnn 10743 A finite set of natural numbers has an upper bound which is a a natural number. (Contributed by Jim Kingdon, 29-Oct-2024.)
((𝐴 ⊆ ℕ ∧ 𝐴 ∈ Fin) → ∃𝑥 ∈ ℕ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)
 
29-Oct-2024fiubz 10742 A finite set of integers has an upper bound which is an integer. (Contributed by Jim Kingdon, 29-Oct-2024.)
((𝐴 ⊆ ℤ ∧ 𝐴 ∈ Fin) → ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)
 
29-Oct-2024fiubm 10741 Lemma for fiubz 10742 and fiubnn 10743. A general form of those theorems. (Contributed by Jim Kingdon, 29-Oct-2024.)
(𝜑 → 𝐴 ⊆ 𝐵)    &   (𝜑 → 𝐵 ⊆ ℚ)    &   (𝜑 → 𝐶 ∈ 𝐵)    &   (𝜑 → 𝐴 ∈ Fin)    ⇒   (𝜑 → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)
 
27-Oct-2024bj-nnst 13624 Double negation of stability of a formula. Intuitionistic logic refutes unstability (but does not prove stability) of any formula. This theorem can also be proved in classical refutability calculus (see https://us.metamath.org/mpeuni/bj-peircestab.html) but not in minimal calculus (see https://us.metamath.org/mpeuni/bj-stabpeirce.html). See nnnotnotr 13872 for the version not using the definition of stability. (Contributed by BJ, 9-Oct-2019.) Prove it in ( → , ¬ ) -intuitionistic calculus with definitions (uses of ax-ia1 105, ax-ia2 106, ax-ia3 107 are via sylibr 133, necessary for definition unpackaging), and in ( → , ↔ , ¬ )-intuitionistic calculus, following a discussion with Jim Kingdon. (Revised by BJ, 27-Oct-2024.)
¬ ¬ STAB 𝜑
 
27-Oct-2024bj-imnimnn 13619 If a formula is implied by both a formula and its negation, then it is not refutable. There is another proof using the inference associated with bj-nnclavius 13618 as its last step. (Contributed by BJ, 27-Oct-2024.)
(𝜑 → 𝜓)    &   (¬ 𝜑 → 𝜓)    ⇒    ¬ ¬ 𝜓
 
25-Oct-2024nnwosdc 11972 Well-ordering principle: any inhabited decidable set of positive integers has a least element (schema form). (Contributed by NM, 17-Aug-2001.) (Revised by Jim Kingdon, 25-Oct-2024.)
(𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ((∃𝑥 ∈ ℕ 𝜑 ∧ ∀𝑥 ∈ ℕ DECID 𝜑) → ∃𝑥 ∈ ℕ (𝜑 ∧ ∀𝑦 ∈ ℕ (𝜓 → 𝑥 ≤ 𝑦)))
 
23-Oct-2024nnwodc 11969 Well-ordering principle: any inhabited decidable set of positive integers has a least element. Theorem I.37 (well-ordering principle) of [Apostol] p. 34. (Contributed by NM, 17-Aug-2001.) (Revised by Jim Kingdon, 23-Oct-2024.)
((𝐴 ⊆ ℕ ∧ ∃𝑤 𝑤 ∈ 𝐴 ∧ ∀𝑗 ∈ ℕ DECID 𝑗 ∈ 𝐴) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦)
 
22-Oct-2024uzwodc 11970 Well-ordering principle: any inhabited decidable subset of an upper set of integers has a least element. (Contributed by NM, 8-Oct-2005.) (Revised by Jim Kingdon, 22-Oct-2024.)
((𝑆 ⊆ (ℤ≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ≥‘𝑀)DECID 𝑥 ∈ 𝑆) → ∃𝑗 ∈ 𝑆 ∀𝑘 ∈ 𝑆 𝑗 ≤ 𝑘)
 
21-Oct-2024nnnotnotr 13872 Double negation of double negation elimination. Suggested by an online post by Martin Escardo. Although this statement resembles nnexmid 840, it can be proved with reference only to implication and negation (that is, without use of disjunction). (Contributed by Jim Kingdon, 21-Oct-2024.)
¬ ¬ (¬ ¬ 𝜑 → 𝜑)
 
20-Oct-2024isprm5lem 12073 Lemma for isprm5 12074. The interesting direction (showing that one only needs to check prime divisors up to the square root of 𝑃). (Contributed by Jim Kingdon, 20-Oct-2024.)
(𝜑 → 𝑃 ∈ (ℤ≥‘2))    &   (𝜑 → ∀𝑧 ∈ ℙ ((𝑧↑2) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃))    &   (𝜑 → 𝑋 ∈ (2...(𝑃 − 1)))    ⇒   (𝜑 → ¬ 𝑋 ∥ 𝑃)
 
17-Oct-2024elnndc 9550 Membership of an integer in ℕ is decidable. (Contributed by Jim Kingdon, 17-Oct-2024.)
(𝑁 ∈ ℤ → DECID 𝑁 ∈ ℕ)
 
14-Oct-20242zinfmin 11184 Two ways to express the minimum of two integers. Because order of integers is decidable, we have more flexibility than for real numbers. (Contributed by Jim Kingdon, 14-Oct-2024.)
((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → inf({𝐴, 𝐵}, ℝ, < ) = if(𝐴 ≤ 𝐵, 𝐴, 𝐵))
 
14-Oct-2024mingeb 11183 Equivalence of ≤ and being equal to the minimum of two reals. (Contributed by Jim Kingdon, 14-Oct-2024.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ inf({𝐴, 𝐵}, ℝ, < ) = 𝐴))
 
13-Oct-2024pcxnn0cl 12242 Extended nonnegative integer closure of the general prime count function. (Contributed by Jim Kingdon, 13-Oct-2024.)
((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → (𝑃 pCnt 𝑁) ∈ ℕ0*)
 
13-Oct-2024xnn0letri 9739 Dichotomy for extended nonnegative integers. (Contributed by Jim Kingdon, 13-Oct-2024.)
((𝐴 ∈ ℕ0* ∧ 𝐵 ∈ ℕ0*) → (𝐴 ≤ 𝐵 ∨ 𝐵 ≤ 𝐴))
 
13-Oct-2024xnn0dcle 9738 Decidability of ≤ for extended nonnegative integers. (Contributed by Jim Kingdon, 13-Oct-2024.)
((𝐴 ∈ ℕ0* ∧ 𝐵 ∈ ℕ0*) → DECID 𝐴 ≤ 𝐵)
 
9-Oct-2024nn0leexp2 10624 Ordering law for exponentiation. (Contributed by Jim Kingdon, 9-Oct-2024.)
(((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 1 < 𝐴) → (𝑀 ≤ 𝑁 ↔ (𝐴↑𝑀) ≤ (𝐴↑𝑁)))
 
8-Oct-2024pclemdc 12220 Lemma for the prime power pre-function's properties. (Contributed by Jim Kingdon, 8-Oct-2024.)
𝐴 = {𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑁}    ⇒   ((𝑃 ∈ (ℤ≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ∀𝑥 ∈ ℤ DECID 𝑥 ∈ 𝐴)
 
8-Oct-2024elnn0dc 9549 Membership of an integer in ℕ0 is decidable. (Contributed by Jim Kingdon, 8-Oct-2024.)
(𝑁 ∈ ℤ → DECID 𝑁 ∈ ℕ0)
 
7-Oct-2024pclemub 12219 Lemma for the prime power pre-function's properties. (Contributed by Mario Carneiro, 23-Feb-2014.) (Revised by Jim Kingdon, 7-Oct-2024.)
𝐴 = {𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑁}    ⇒   ((𝑃 ∈ (ℤ≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)
 
7-Oct-2024pclem0 12218 Lemma for the prime power pre-function's properties. (Contributed by Mario Carneiro, 23-Feb-2014.) (Revised by Jim Kingdon, 7-Oct-2024.)
𝐴 = {𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑁}    ⇒   ((𝑃 ∈ (ℤ≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → 0 ∈ 𝐴)
 
7-Oct-2024nn0ltexp2 10623 Special case of ltexp2 13500 which we use here because we haven't yet defined df-rpcxp 13420 which is used in the current proof of ltexp2 13500. (Contributed by Jim Kingdon, 7-Oct-2024.)
(((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 1 < 𝐴) → (𝑀 < 𝑁 ↔ (𝐴↑𝑀) < (𝐴↑𝑁)))
 
6-Oct-2024suprzcl2dc 11888 The supremum of a bounded-above decidable set of integers is a member of the set. (This theorem avoids ax-pre-suploc 7874.) (Contributed by Mario Carneiro, 21-Apr-2015.) (Revised by Jim Kingdon, 6-Oct-2024.)
(𝜑 → 𝐴 ⊆ ℤ)    &   (𝜑 → ∀𝑥 ∈ ℤ DECID 𝑥 ∈ 𝐴)    &   (𝜑 → ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)    &   (𝜑 → ∃𝑥 𝑥 ∈ 𝐴)    ⇒   (𝜑 → sup(𝐴, ℝ, < ) ∈ 𝐴)
 
5-Oct-2024zsupssdc 11887 An inhabited decidable bounded subset of integers has a supremum in the set. (The proof does not use ax-pre-suploc 7874.) (Contributed by Mario Carneiro, 21-Apr-2015.) (Revised by Jim Kingdon, 5-Oct-2024.)
(𝜑 → 𝐴 ⊆ ℤ)    &   (𝜑 → ∃𝑥 𝑥 ∈ 𝐴)    &   (𝜑 → ∀𝑥 ∈ ℤ DECID 𝑥 ∈ 𝐴)    &   (𝜑 → ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)    ⇒   (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ 𝐵 (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)))
 
5-Oct-2024suprzubdc 11885 The supremum of a bounded-above decidable set of integers is greater than any member of the set. (Contributed by Mario Carneiro, 21-Apr-2015.) (Revised by Jim Kingdon, 5-Oct-2024.)
(𝜑 → 𝐴 ⊆ ℤ)    &   (𝜑 → ∀𝑥 ∈ ℤ DECID 𝑥 ∈ 𝐴)    &   (𝜑 → ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)    &   (𝜑 → 𝐵 ∈ 𝐴)    ⇒   (𝜑 → 𝐵 ≤ sup(𝐴, ℝ, < ))
 
1-Oct-2024infex2g 6999 Existence of infimum. (Contributed by Jim Kingdon, 1-Oct-2024.)
(𝐴 ∈ 𝐶 → inf(𝐵, 𝐴, 𝑅) ∈ V)
 
30-Sep-2024unbendc 12387 An unbounded decidable set of positive integers is infinite. (Contributed by NM, 5-May-2005.) (Revised by Jim Kingdon, 30-Sep-2024.)
((𝐴 ⊆ ℕ ∧ ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴 ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝐴 𝑚 < 𝑛) → 𝐴 ≈ ℕ)
 
30-Sep-2024prmdc 12062 Primality is decidable. (Contributed by Jim Kingdon, 30-Sep-2024.)
(𝑁 ∈ ℕ → DECID 𝑁 ∈ ℙ)
 
30-Sep-2024dcfi 6946 Decidability of a family of propositions indexed by a finite set. (Contributed by Jim Kingdon, 30-Sep-2024.)
((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 DECID 𝜑) → DECID ∀𝑥 ∈ 𝐴 𝜑)
 
29-Sep-2024ssnnct 12380 A decidable subset of ℕ is countable. (Contributed by Jim Kingdon, 29-Sep-2024.)
((𝐴 ⊆ ℕ ∧ ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴) → ∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o))
 
29-Sep-2024ssnnctlemct 12379 Lemma for ssnnct 12380. The result. (Contributed by Jim Kingdon, 29-Sep-2024.)
𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 1)    ⇒   ((𝐴 ⊆ ℕ ∧ ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴) → ∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o))
 
28-Sep-2024nninfdcex 11886 A decidable set of natural numbers has an infimum. (Contributed by Jim Kingdon, 28-Sep-2024.)
(𝜑 → 𝐴 ⊆ ℕ)    &   (𝜑 → ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴)    &   (𝜑 → ∃𝑦 𝑦 ∈ 𝐴)    ⇒   (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))
 
27-Sep-2024infregelbex 9536 Any lower bound of a set of real numbers with an infimum is less than or equal to the infimum. (Contributed by Jim Kingdon, 27-Sep-2024.)
(𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))    &   (𝜑 → 𝐴 ⊆ ℝ)    &   (𝜑 → 𝐵 ∈ ℝ)    ⇒   (𝜑 → (𝐵 ≤ inf(𝐴, ℝ, < ) ↔ ∀𝑧 ∈ 𝐴 𝐵 ≤ 𝑧))
 
26-Sep-2024nninfdclemp1 12383 Lemma for nninfdc 12386. Each element of the sequence 𝐹 is greater than the previous element. (Contributed by Jim Kingdon, 26-Sep-2024.)
(𝜑 → 𝐴 ⊆ ℕ)    &   (𝜑 → ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴)    &   (𝜑 → ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝐴 𝑚 < 𝑛)    &   (𝜑 → (𝐽 ∈ 𝐴 ∧ 1 < 𝐽))    &   𝐹 = seq1((𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ≥‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽))    &   (𝜑 → 𝑈 ∈ ℕ)    ⇒   (𝜑 → (𝐹‘𝑈) < (𝐹‘(𝑈 + 1)))
 
26-Sep-2024nnminle 11968 The infimum of a decidable subset of the natural numbers is less than an element of the set. The infimum is also a minimum as shown at nnmindc 11967. (Contributed by Jim Kingdon, 26-Sep-2024.)
((𝐴 ⊆ ℕ ∧ ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐴) → inf(𝐴, ℝ, < ) ≤ 𝐵)
 
25-Sep-2024nninfdclemcl 12381 Lemma for nninfdc 12386. (Contributed by Jim Kingdon, 25-Sep-2024.)
(𝜑 → 𝐴 ⊆ ℕ)    &   (𝜑 → ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴)    &   (𝜑 → ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝐴 𝑚 < 𝑛)    &   (𝜑 → 𝑃 ∈ 𝐴)    &   (𝜑 → 𝑄 ∈ 𝐴)    ⇒   (𝜑 → (𝑃(𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ≥‘(𝑦 + 1))), ℝ, < ))𝑄) ∈ 𝐴)
 
24-Sep-2024nninfdclemlt 12384 Lemma for nninfdc 12386. The function from nninfdclemf 12382 is strictly monotonic. (Contributed by Jim Kingdon, 24-Sep-2024.)
(𝜑 → 𝐴 ⊆ ℕ)    &   (𝜑 → ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴)    &   (𝜑 → ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝐴 𝑚 < 𝑛)    &   (𝜑 → (𝐽 ∈ 𝐴 ∧ 1 < 𝐽))    &   𝐹 = seq1((𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ≥‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽))    &   (𝜑 → 𝑈 ∈ ℕ)    &   (𝜑 → 𝑉 ∈ ℕ)    &   (𝜑 → 𝑈 < 𝑉)    ⇒   (𝜑 → (𝐹‘𝑈) < (𝐹‘𝑉))
 
23-Sep-2024nninfdc 12386 An unbounded decidable set of positive integers is infinite. (Contributed by Jim Kingdon, 23-Sep-2024.)
((𝐴 ⊆ ℕ ∧ ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴 ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝐴 𝑚 < 𝑛) → ω ≼ 𝐴)
 
23-Sep-2024nninfdclemf1 12385 Lemma for nninfdc 12386. The function from nninfdclemf 12382 is one-to-one. (Contributed by Jim Kingdon, 23-Sep-2024.)
(𝜑 → 𝐴 ⊆ ℕ)    &   (𝜑 → ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴)    &   (𝜑 → ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝐴 𝑚 < 𝑛)    &   (𝜑 → (𝐽 ∈ 𝐴 ∧ 1 < 𝐽))    &   𝐹 = seq1((𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ≥‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽))    ⇒   (𝜑 → 𝐹:ℕ–1-1→𝐴)
 
23-Sep-2024nninfdclemf 12382 Lemma for nninfdc 12386. A function from the natural numbers into 𝐴. (Contributed by Jim Kingdon, 23-Sep-2024.)
(𝜑 → 𝐴 ⊆ ℕ)    &   (𝜑 → ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴)    &   (𝜑 → ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝐴 𝑚 < 𝑛)    &   (𝜑 → (𝐽 ∈ 𝐴 ∧ 1 < 𝐽))    &   𝐹 = seq1((𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ≥‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽))    ⇒   (𝜑 → 𝐹:ℕ⟶𝐴)
 
23-Sep-2024nnmindc 11967 An inhabited decidable subset of the natural numbers has a minimum. (Contributed by Jim Kingdon, 23-Sep-2024.)
((𝐴 ⊆ ℕ ∧ ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ 𝐴) → inf(𝐴, ℝ, < ) ∈ 𝐴)
 
19-Sep-2024ssomct 12378 A decidable subset of ω is countable. (Contributed by Jim Kingdon, 19-Sep-2024.)
((𝐴 ⊆ ω ∧ ∀𝑥 ∈ ω DECID 𝑥 ∈ 𝐴) → ∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o))
 
14-Sep-2024nnpredlt 4601 The predecessor (see nnpredcl 4600) of a nonzero natural number is less than (see df-iord 4344) that number. (Contributed by Jim Kingdon, 14-Sep-2024.)
((𝐴 ∈ ω ∧ 𝐴 ≠ ∅) → ∪ 𝐴 ∈ 𝐴)
 
13-Sep-2024nninfisollemeq 7096 Lemma for nninfisol 7097. The case where 𝑁 is a successor and 𝑁 and 𝑋 are equal. (Contributed by Jim Kingdon, 13-Sep-2024.)
(𝜑 → 𝑋 ∈ ℕ∞)    &   (𝜑 → (𝑋‘𝑁) = ∅)    &   (𝜑 → 𝑁 ∈ ω)    &   (𝜑 → 𝑁 ≠ ∅)    &   (𝜑 → (𝑋‘∪ 𝑁) = 1o)    ⇒   (𝜑 → DECID (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋)
 
13-Sep-2024nninfisollemne 7095 Lemma for nninfisol 7097. A case where 𝑁 is a successor and 𝑁 and 𝑋 are not equal. (Contributed by Jim Kingdon, 13-Sep-2024.)
(𝜑 → 𝑋 ∈ ℕ∞)    &   (𝜑 → (𝑋‘𝑁) = ∅)    &   (𝜑 → 𝑁 ∈ ω)    &   (𝜑 → 𝑁 ≠ ∅)    &   (𝜑 → (𝑋‘∪ 𝑁) = ∅)    ⇒   (𝜑 → DECID (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋)
 
13-Sep-2024nninfisollem0 7094 Lemma for nninfisol 7097. The case where 𝑁 is zero. (Contributed by Jim Kingdon, 13-Sep-2024.)
(𝜑 → 𝑋 ∈ ℕ∞)    &   (𝜑 → (𝑋‘𝑁) = ∅)    &   (𝜑 → 𝑁 ∈ ω)    &   (𝜑 → 𝑁 = ∅)    ⇒   (𝜑 → DECID (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋)
 
12-Sep-2024nninfisol 7097 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 𝑋 to decide whether it is equal to 𝑁 (in fact, you only need to look at two elements and 𝑁 tells you where to look). (Contributed by BJ and Jim Kingdon, 12-Sep-2024.)
((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) → DECID (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋)
 
7-Sep-2024eulerthlemfi 12160 Lemma for eulerth 12165. The set 𝑆 is finite. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 7-Sep-2024.)
(𝜑 → (𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1))    &   𝑆 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1}    ⇒   (𝜑 → 𝑆 ∈ Fin)
 
7-Sep-2024modqexp 10581 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.)
(𝜑 → 𝐴 ∈ ℤ)    &   (𝜑 → 𝐵 ∈ ℤ)    &   (𝜑 → 𝐶 ∈ ℕ0)    &   (𝜑 → 𝐷 ∈ ℚ)    &   (𝜑 → 0 < 𝐷)    &   (𝜑 → (𝐴 mod 𝐷) = (𝐵 mod 𝐷))    ⇒   (𝜑 → ((𝐴↑𝐶) mod 𝐷) = ((𝐵↑𝐶) mod 𝐷))
 
5-Sep-2024eulerthlemh 12163 Lemma for eulerth 12165. A permutation of (1...(ϕ‘𝑁)). (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 5-Sep-2024.)
(𝜑 → (𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1))    &   𝑆 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1}    &   (𝜑 → 𝐹:(1...(ϕ‘𝑁))–1-1-onto→𝑆)    &   𝐻 = (◡𝐹 ∘ (𝑦 ∈ (1...(ϕ‘𝑁)) ↦ ((𝐴 · (𝐹‘𝑦)) mod 𝑁)))    ⇒   (𝜑 → 𝐻:(1...(ϕ‘𝑁))–1-1-onto→(1...(ϕ‘𝑁)))
 
2-Sep-2024eulerthlemth 12164 Lemma for eulerth 12165. The result. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 2-Sep-2024.)
(𝜑 → (𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1))    &   𝑆 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1}    &   (𝜑 → 𝐹:(1...(ϕ‘𝑁))–1-1-onto→𝑆)    ⇒   (𝜑 → ((𝐴↑(ϕ‘𝑁)) mod 𝑁) = (1 mod 𝑁))
 
2-Sep-2024eulerthlema 12162 Lemma for eulerth 12165. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 2-Sep-2024.)
(𝜑 → (𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1))    &   𝑆 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1}    &   (𝜑 → 𝐹:(1...(ϕ‘𝑁))–1-1-onto→𝑆)    ⇒   (𝜑 → (((𝐴↑(ϕ‘𝑁)) · ∏𝑥 ∈ (1...(ϕ‘𝑁))(𝐹‘𝑥)) mod 𝑁) = (∏𝑥 ∈ (1...(ϕ‘𝑁))((𝐴 · (𝐹‘𝑥)) mod 𝑁) mod 𝑁))
 
2-Sep-2024eulerthlemrprm 12161 Lemma for eulerth 12165. 𝑁 and ∏𝑥 ∈ (1...(ϕ‘𝑁))(𝐹‘𝑥) are relatively prime. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 2-Sep-2024.)
(𝜑 → (𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1))    &   𝑆 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1}    &   (𝜑 → 𝐹:(1...(ϕ‘𝑁))–1-1-onto→𝑆)    ⇒   (𝜑 → (𝑁 gcd ∏𝑥 ∈ (1...(ϕ‘𝑁))(𝐹‘𝑥)) = 1)
 
30-Aug-2024fprodap0f 11577 A finite product of terms apart from zero is apart from zero. A version of fprodap0 11562 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) (Revised by Jim Kingdon, 30-Aug-2024.)
Ⅎ𝑘𝜑    &   (𝜑 → 𝐴 ∈ Fin)    &   ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 # 0)    ⇒   (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 # 0)
 
28-Aug-2024fprodrec 11570 The finite product of reciprocals is the reciprocal of the product. (Contributed by Jim Kingdon, 28-Aug-2024.)
(𝜑 → 𝐴 ∈ Fin)    &   ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 # 0)    ⇒   (𝜑 → ∏𝑘 ∈ 𝐴 (1 / 𝐵) = (1 / ∏𝑘 ∈ 𝐴 𝐵))
 
26-Aug-2024exmidontri2or 7199 Ordinal trichotomy is equivalent to excluded middle. (Contributed by Jim Kingdon, 26-Aug-2024.)
(EXMID ↔ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥))
 
26-Aug-2024exmidontri 7195 Ordinal trichotomy is equivalent to excluded middle. (Contributed by Jim Kingdon, 26-Aug-2024.)
(EXMID ↔ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥))
 
26-Aug-2024ontri2orexmidim 4549 Ordinal trichotomy implies excluded middle. Closed form of ordtri2or2exmid 4548. (Contributed by Jim Kingdon, 26-Aug-2024.)
(∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥) → DECID 𝜑)
 
26-Aug-2024ontriexmidim 4499 Ordinal trichotomy implies excluded middle. Closed form of ordtriexmid 4498. (Contributed by Jim Kingdon, 26-Aug-2024.)
(∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) → DECID 𝜑)
 
25-Aug-2024onntri2or 7202 Double negated ordinal trichotomy. (Contributed by Jim Kingdon, 25-Aug-2024.)
(¬ ¬ EXMID ↔ ∀𝑥 ∈ On ∀𝑦 ∈ On ¬ ¬ (𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥))
 
25-Aug-2024onntri3or 7201 Double negated ordinal trichotomy. (Contributed by Jim Kingdon, 25-Aug-2024.)
(¬ ¬ EXMID ↔ ∀𝑥 ∈ On ∀𝑦 ∈ On ¬ ¬ (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥))
 
25-Aug-2024csbcow 3056 Composition law for chained substitutions into a class. Version of csbco 3055 with a disjoint variable condition, which requires fewer axioms. (Contributed by NM, 10-Nov-2005.) (Revised by Gino Giotto, 25-Aug-2024.)
⦋𝐴 / 𝑦⦌⦋𝑦 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵
 
25-Aug-2024cbvreuvw 2698 Version of cbvreuv 2694 with a disjoint variable condition. (Contributed by Gino Giotto, 10-Jan-2024.) Reduce axiom usage. (Revised by Gino Giotto, 25-Aug-2024.)
(𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐴 𝜓)
 
25-Aug-2024cbvrexvw 2697 Version of cbvrexv 2693 with a disjoint variable condition. (Contributed by Gino Giotto, 10-Jan-2024.) Reduce axiom usage. (Revised by Gino Giotto, 25-Aug-2024.)
(𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)
 
25-Aug-2024cbvralvw 2696 Version of cbvralv 2692 with a disjoint variable condition. (Contributed by Gino Giotto, 10-Jan-2024.) Reduce axiom usage. (Revised by Gino Giotto, 25-Aug-2024.)
(𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)
 
25-Aug-2024cbvabw 2289 Version of cbvab 2290 with a disjoint variable condition. (Contributed by Gino Giotto, 10-Jan-2024.) Reduce axiom usage. (Revised by Gino Giotto, 25-Aug-2024.)
Ⅎ𝑦𝜑    &   Ⅎ𝑥𝜓    &   (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓}
 
25-Aug-2024nfsbv 1935 If 𝑧 is not free in 𝜑, it is not free in [𝑦 / 𝑥]𝜑 when 𝑧 is distinct from 𝑥 and 𝑦. Version of nfsb 1934 requiring more disjoint variables. (Contributed by Wolf Lammen, 7-Feb-2023.) Remove disjoint variable condition on 𝑥, 𝑦. (Revised by Steven Nguyen, 13-Aug-2023.) Reduce axiom usage. (Revised by Gino Giotto, 25-Aug-2024.)
Ⅎ𝑧𝜑    ⇒   Ⅎ𝑧[𝑦 / 𝑥]𝜑
 
25-Aug-2024cbvexvw 1908 Change bound variable. See cbvexv 1906 for a version with fewer disjoint variable conditions. (Contributed by NM, 19-Apr-2017.) Avoid ax-7 1436. (Revised by Gino Giotto, 25-Aug-2024.)
(𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   (∃𝑥𝜑 ↔ ∃𝑦𝜓)
 
25-Aug-2024cbvalvw 1907 Change bound variable. See cbvalv 1905 for a version with fewer disjoint variable conditions. (Contributed by NM, 9-Apr-2017.) Avoid ax-7 1436. (Revised by Gino Giotto, 25-Aug-2024.)
(𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   (∀𝑥𝜑 ↔ ∀𝑦𝜓)
 
25-Aug-2024nfal 1564 If 𝑥 is not free in 𝜑, it is not free in ∀𝑦𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) Remove dependency on ax-4 1498. (Revised by Gino Giotto, 25-Aug-2024.)
Ⅎ𝑥𝜑    ⇒   Ⅎ𝑥∀𝑦𝜑
 
24-Aug-2024gcdcomd 11907 The gcd operator is commutative, deduction version. (Contributed by SN, 24-Aug-2024.)
(𝜑 → 𝑀 ∈ ℤ)    &   (𝜑 → 𝑁 ∈ ℤ)    ⇒   (𝜑 → (𝑀 gcd 𝑁) = (𝑁 gcd 𝑀))
 
21-Aug-2024dvds2addd 11769 Deduction form of dvds2add 11765. (Contributed by SN, 21-Aug-2024.)
(𝜑 → 𝐾 ∈ ℤ)    &   (𝜑 → 𝑀 ∈ ℤ)    &   (𝜑 → 𝑁 ∈ ℤ)    &   (𝜑 → 𝐾 ∥ 𝑀)    &   (𝜑 → 𝐾 ∥ 𝑁)    ⇒   (𝜑 → 𝐾 ∥ (𝑀 + 𝑁))
 
17-Aug-2024fprodcl2lem 11546 Finite product closure lemma. (Contributed by Scott Fenton, 14-Dec-2017.) (Revised by Jim Kingdon, 17-Aug-2024.)
(𝜑 → 𝑆 ⊆ ℂ)    &   ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 · 𝑦) ∈ 𝑆)    &   (𝜑 → 𝐴 ∈ Fin)    &   ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑆)    &   (𝜑 → 𝐴 ≠ ∅)    ⇒   (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 ∈ 𝑆)
 
16-Aug-2024if0ab 13687 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(𝜑, 𝐴, ∅) ⊆ 𝐴 and therefore, using elpwg 3567, (𝐴 ∈ 𝑉 → if(𝜑, 𝐴, ∅) ∈ 𝒫 𝐴), from which fmelpw1o 13688 could be derived, yielding an alternative proof. (Contributed by BJ, 16-Aug-2024.)

if(𝜑, 𝐴, ∅) = {𝑥 ∈ 𝐴 ∣ 𝜑}
 
16-Aug-2024fprodunsn 11545 Multiply in an additional term in a finite product. See also fprodsplitsn 11574 which is the same but with a Ⅎ𝑘𝜑 hypothesis in place of the distinct variable condition between 𝜑 and 𝑘. (Contributed by Jim Kingdon, 16-Aug-2024.)
Ⅎ𝑘𝐷    &   (𝜑 → 𝐴 ∈ Fin)    &   (𝜑 → 𝐵 ∈ 𝑉)    &   (𝜑 → ¬ 𝐵 ∈ 𝐴)    &   ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ)    &   (𝜑 → 𝐷 ∈ ℂ)    &   (𝑘 = 𝐵 → 𝐶 = 𝐷)    ⇒   (𝜑 → ∏𝑘 ∈ (𝐴 ∪ {𝐵})𝐶 = (∏𝑘 ∈ 𝐴 𝐶 · 𝐷))
 
15-Aug-2024bj-charfundcALT 13691 Alternate proof of bj-charfundc 13690. It was expected to be much shorter since it uses bj-charfun 13689 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.)
(𝜑 → 𝐹 = (𝑥 ∈ 𝑋 ↦ if(𝑥 ∈ 𝐴, 1o, ∅)))    &   (𝜑 → ∀𝑥 ∈ 𝑋 DECID 𝑥 ∈ 𝐴)    ⇒   (𝜑 → (𝐹:𝑋⟶2o ∧ (∀𝑥 ∈ (𝑋 ∩ 𝐴)(𝐹‘𝑥) = 1o ∧ ∀𝑥 ∈ (𝑋 ∖ 𝐴)(𝐹‘𝑥) = ∅)))
 
15-Aug-2024bj-charfun 13689 Properties of the characteristic function on the class 𝑋 of the class 𝐴. (Contributed by BJ, 15-Aug-2024.)
(𝜑 → 𝐹 = (𝑥 ∈ 𝑋 ↦ if(𝑥 ∈ 𝐴, 1o, ∅)))    ⇒   (𝜑 → ((𝐹:𝑋⟶𝒫 1o ∧ (𝐹 ↾ ((𝑋 ∩ 𝐴) ∪ (𝑋 ∖ 𝐴))):((𝑋 ∩ 𝐴) ∪ (𝑋 ∖ 𝐴))⟶2o) ∧ (∀𝑥 ∈ (𝑋 ∩ 𝐴)(𝐹‘𝑥) = 1o ∧ ∀𝑥 ∈ (𝑋 ∖ 𝐴)(𝐹‘𝑥) = ∅)))
 
15-Aug-2024fmelpw1o 13688 With a formula 𝜑 one can associate an element of 𝒫 1o, which can therefore be thought of as the set of "truth values" (but recall that there are no other genuine truth values than ⊤ and ⊥, by nndc 841, which translate to 1o and ∅ respectively by iftrue 3525 and iffalse 3528, giving pwtrufal 13877).

As proved in if0ab 13687, the associated element of 𝒫 1o is the extension, in 𝒫 1o, of the formula 𝜑. (Contributed by BJ, 15-Aug-2024.)

if(𝜑, 1o, ∅) ∈ 𝒫 1o
 
15-Aug-2024cnstab 8543 Equality of complex numbers is stable. Stability here means ¬ ¬ 𝐴 = 𝐵 → 𝐴 = 𝐵 as defined at df-stab 821. 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.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → STAB 𝐴 = 𝐵)
 
15-Aug-2024subap0d 8542 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.)
(𝜑 → 𝐴 ∈ ℂ)    &   (𝜑 → 𝐵 ∈ ℂ)    &   (𝜑 → 𝐴 # 𝐵)    ⇒   (𝜑 → (𝐴 − 𝐵) # 0)
 
15-Aug-2024ifexd 4462 Existence of a conditional class (deduction form). (Contributed by BJ, 15-Aug-2024.)
(𝜑 → 𝐴 ∈ 𝑉)    &   (𝜑 → 𝐵 ∈ 𝑊)    ⇒   (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ V)
 
15-Aug-2024ifelpwun 4461 Existence of a conditional class, quantitative version (inference form). (Contributed by BJ, 15-Aug-2024.)
𝐴 ∈ V    &   𝐵 ∈ V    ⇒   if(𝜑, 𝐴, 𝐵) ∈ 𝒫 (𝐴 ∪ 𝐵)
 
15-Aug-2024ifelpwund 4460 Existence of a conditional class, quantitative version (deduction form). (Contributed by BJ, 15-Aug-2024.)
(𝜑 → 𝐴 ∈ 𝑉)    &   (𝜑 → 𝐵 ∈ 𝑊)    ⇒   (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝒫 (𝐴 ∪ 𝐵))
 
15-Aug-2024ifelpwung 4459 Existence of a conditional class, quantitative version (closed form). (Contributed by BJ, 15-Aug-2024.)
((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → if(𝜑, 𝐴, 𝐵) ∈ 𝒫 (𝐴 ∪ 𝐵))
 
15-Aug-2024ifidss 3535 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(𝜑, 𝐴, 𝐴) ⊆ 𝐴
 
15-Aug-2024ifssun 3534 A conditional class is included in the union of its two alternatives. (Contributed by BJ, 15-Aug-2024.)
if(𝜑, 𝐴, 𝐵) ⊆ (𝐴 ∪ 𝐵)
 
12-Aug-2024exmidontriimlem2 7178 Lemma for exmidontriim 7181. (Contributed by Jim Kingdon, 12-Aug-2024.)
(𝜑 → 𝐵 ∈ On)    &   (𝜑 → EXMID)    &   (𝜑 → ∀𝑦 ∈ 𝐵 (𝐴 ∈ 𝑦 ∨ 𝐴 = 𝑦 ∨ 𝑦 ∈ 𝐴))    ⇒   (𝜑 → (𝐴 ∈ 𝐵 ∨ ∀𝑦 ∈ 𝐵 𝑦 ∈ 𝐴))
 
12-Aug-2024exmidontriimlem1 7177 Lemma for exmidontriim 7181. A variation of r19.30dc 2613. (Contributed by Jim Kingdon, 12-Aug-2024.)
((∀𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓 ∨ 𝜒) ∧ EXMID) → (∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓 ∨ ∀𝑥 ∈ 𝐴 𝜒))
 
11-Aug-2024nndc 841 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 840 over 𝜑 would give "∀𝜑¬ ¬ DECID 𝜑", but EXMID is "∀𝜑DECID 𝜑", so proving ¬ ¬ EXMID would amount to proving "¬ ¬ ∀𝜑DECID 𝜑", which is not implied by the above theorem. Indeed, the converse of nnal 1637 does not hold. Since our system does not allow quantification over formula metavariables, we can reproduce this argument by representing formulas as subsets of 𝒫 1o, like we do in our definition of EXMID (df-exmid 4174): then, we can prove ∀𝑥 ∈ 𝒫 1o¬ ¬ DECID 𝑥 = 1o but we cannot prove ¬ ¬ ∀𝑥 ∈ 𝒫 1oDECID 𝑥 = 1o because the converse of nnral 2456 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 𝜑
 
10-Aug-2024exmidontriim 7181 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 → ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥))
 
10-Aug-2024exmidontriimlem4 7180 Lemma for exmidontriim 7181. The induction step for the induction on 𝐴. (Contributed by Jim Kingdon, 10-Aug-2024.)
(𝜑 → 𝐴 ∈ On)    &   (𝜑 → 𝐵 ∈ On)    &   (𝜑 → EXMID)    &   (𝜑 → ∀𝑧 ∈ 𝐴 ∀𝑦 ∈ On (𝑧 ∈ 𝑦 ∨ 𝑧 = 𝑦 ∨ 𝑦 ∈ 𝑧))    ⇒   (𝜑 → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))
 
10-Aug-2024exmidontriimlem3 7179 Lemma for exmidontriim 7181. What we get to do based on induction on both 𝐴 and 𝐵. (Contributed by Jim Kingdon, 10-Aug-2024.)
(𝜑 → 𝐴 ∈ On)    &   (𝜑 → 𝐵 ∈ On)    &   (𝜑 → EXMID)    &   (𝜑 → ∀𝑧 ∈ 𝐴 ∀𝑦 ∈ On (𝑧 ∈ 𝑦 ∨ 𝑧 = 𝑦 ∨ 𝑦 ∈ 𝑧))    &   (𝜑 → ∀𝑦 ∈ 𝐵 (𝐴 ∈ 𝑦 ∨ 𝐴 = 𝑦 ∨ 𝑦 ∈ 𝐴))    ⇒   (𝜑 → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))
 
10-Aug-2024nnnninf2 7091 Canonical embedding of suc ω into ℕ∞. (Contributed by BJ, 10-Aug-2024.)
(𝑁 ∈ suc ω → (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) ∈ ℕ∞)
 
10-Aug-2024infnninf 7088 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 (ω × {1o}), as fconstmpt 4651 shows. (Contributed by Jim Kingdon, 14-Jul-2022.) Use maps-to notation. (Revised by BJ, 10-Aug-2024.)
(𝑖 ∈ ω ↦ 1o) ∈ ℕ∞
 
9-Aug-2024ss1o0el1o 6878 Reformulation of ss1o0el1 4176 using 1o instead of {∅}. (Contributed by BJ, 9-Aug-2024.)
(𝐴 ⊆ 1o → (∅ ∈ 𝐴 ↔ 𝐴 = 1o))
  Copyright terms: Public domain W3C HTML validation [external]