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 5-Oct-2024 at 6:42 AM ET.
Recent Additions to the Intuitionistic Logic Explorer
DateLabelDescription
Theorem
 
1-Oct-2024infex2g 6978 Existence of infimum. (Contributed by Jim Kingdon, 1-Oct-2024.)
(𝐴 ∈ 𝐶 → inf(𝐵, 𝐴, 𝑅) ∈ V)
 
30-Sep-2024unbendc 12185 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 12006 Primality is decidable. (Contributed by Jim Kingdon, 30-Sep-2024.)
(𝑁 ∈ ℕ → DECID 𝑁 ∈ ℙ)
 
30-Sep-2024dcfi 6925 Decidability of a family of propositions indexed by a finite set. (Contributed by Jim Kingdon, 30-Sep-2024.)
((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 DECID 𝜑) → DECID ∀𝑥 ∈ 𝐴 𝜑)
 
29-Sep-2024ssnnct 12176 A decidable subset of ℕ is countable. (Contributed by Jim Kingdon, 29-Sep-2024.)
((𝐴 ⊆ ℕ ∧ ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴) → ∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o))
 
29-Sep-2024ssnnctlemct 12175 Lemma for ssnnct 12176. The result. (Contributed by Jim Kingdon, 29-Sep-2024.)
𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 1)    ⇒   ((𝐴 ⊆ ℕ ∧ ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴) → ∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o))
 
28-Sep-2024nninfdcex 11838 A decidable set of natural numbers has an infimum. (Contributed by Jim Kingdon, 28-Sep-2024.)
(𝜑 → 𝐴 ⊆ ℕ)    &   (𝜑 → ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴)    &   (𝜑 → ∃𝑦 𝑦 ∈ 𝐴)    ⇒   (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))
 
27-Sep-2024infregelbex 9509 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 12181 Lemma for nninfdc 12184. 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 12178 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 12177. (Contributed by Jim Kingdon, 26-Sep-2024.)
((𝐴 ⊆ ℕ ∧ ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐴) → inf(𝐴, ℝ, < ) ≤ 𝐵)
 
25-Sep-2024nninfdclemcl 12179 Lemma for nninfdc 12184. (Contributed by Jim Kingdon, 25-Sep-2024.)
(𝜑 → 𝐴 ⊆ ℕ)    &   (𝜑 → ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴)    &   (𝜑 → ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝐴 𝑚 < 𝑛)    &   (𝜑 → 𝑃 ∈ 𝐴)    &   (𝜑 → 𝑄 ∈ 𝐴)    ⇒   (𝜑 → (𝑃(𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ≥‘(𝑦 + 1))), ℝ, < ))𝑄) ∈ 𝐴)
 
24-Sep-2024nninfdclemlt 12182 Lemma for nninfdc 12184. The function from nninfdclemf 12180 is strictly monotonic. (Contributed by Jim Kingdon, 24-Sep-2024.)
(𝜑 → 𝐴 ⊆ ℕ)    &   (𝜑 → ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴)    &   (𝜑 → ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝐴 𝑚 < 𝑛)    &   (𝜑 → (𝐽 ∈ 𝐴 ∧ 1 < 𝐽))    &   𝐹 = seq1((𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ≥‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽))    &   (𝜑 → 𝑈 ∈ ℕ)    &   (𝜑 → 𝑉 ∈ ℕ)    &   (𝜑 → 𝑈 < 𝑉)    ⇒   (𝜑 → (𝐹‘𝑈) < (𝐹‘𝑉))
 
23-Sep-2024nninfdc 12184 An unbounded decidable set of positive integers is infinite. (Contributed by Jim Kingdon, 23-Sep-2024.)
((𝐴 ⊆ ℕ ∧ ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴 ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝐴 𝑚 < 𝑛) → ω ≼ 𝐴)
 
23-Sep-2024nninfdclemf1 12183 Lemma for nninfdc 12184. The function from nninfdclemf 12180 is one-to-one. (Contributed by Jim Kingdon, 23-Sep-2024.)
(𝜑 → 𝐴 ⊆ ℕ)    &   (𝜑 → ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴)    &   (𝜑 → ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝐴 𝑚 < 𝑛)    &   (𝜑 → (𝐽 ∈ 𝐴 ∧ 1 < 𝐽))    &   𝐹 = seq1((𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ≥‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽))    ⇒   (𝜑 → 𝐹:ℕ–1-1→𝐴)
 
23-Sep-2024nninfdclemf 12180 Lemma for nninfdc 12184. A function from the natural numbers into 𝐴. (Contributed by Jim Kingdon, 23-Sep-2024.)
(𝜑 → 𝐴 ⊆ ℕ)    &   (𝜑 → ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴)    &   (𝜑 → ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝐴 𝑚 < 𝑛)    &   (𝜑 → (𝐽 ∈ 𝐴 ∧ 1 < 𝐽))    &   𝐹 = seq1((𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ≥‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽))    ⇒   (𝜑 → 𝐹:ℕ⟶𝐴)
 
23-Sep-2024nnmindc 12177 An inhabited decidable subset of the natural numbers has a minimum. (Contributed by Jim Kingdon, 23-Sep-2024.)
((𝐴 ⊆ ℕ ∧ ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ 𝐴) → inf(𝐴, ℝ, < ) ∈ 𝐴)
 
19-Sep-2024ssomct 12174 A decidable subset of ω is countable. (Contributed by Jim Kingdon, 19-Sep-2024.)
((𝐴 ⊆ ω ∧ ∀𝑥 ∈ ω DECID 𝑥 ∈ 𝐴) → ∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o))
 
14-Sep-2024nnpredlt 4583 The predecessor (see nnpredcl 4582) of a nonzero natural number is less than (see df-iord 4326) that number. (Contributed by Jim Kingdon, 14-Sep-2024.)
((𝐴 ∈ ω ∧ 𝐴 ≠ ∅) → ∪ 𝐴 ∈ 𝐴)
 
13-Sep-2024nninfisollemeq 7075 Lemma for nninfisol 7076. The case where 𝑁 is a successor and 𝑁 and 𝑋 are equal. (Contributed by Jim Kingdon, 13-Sep-2024.)
(𝜑 → 𝑋 ∈ ℕ∞)    &   (𝜑 → (𝑋‘𝑁) = ∅)    &   (𝜑 → 𝑁 ∈ ω)    &   (𝜑 → 𝑁 ≠ ∅)    &   (𝜑 → (𝑋‘∪ 𝑁) = 1o)    ⇒   (𝜑 → DECID (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋)
 
13-Sep-2024nninfisollemne 7074 Lemma for nninfisol 7076. A case where 𝑁 is a successor and 𝑁 and 𝑋 are not equal. (Contributed by Jim Kingdon, 13-Sep-2024.)
(𝜑 → 𝑋 ∈ ℕ∞)    &   (𝜑 → (𝑋‘𝑁) = ∅)    &   (𝜑 → 𝑁 ∈ ω)    &   (𝜑 → 𝑁 ≠ ∅)    &   (𝜑 → (𝑋‘∪ 𝑁) = ∅)    ⇒   (𝜑 → DECID (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋)
 
13-Sep-2024nninfisollem0 7073 Lemma for nninfisol 7076. The case where 𝑁 is zero. (Contributed by Jim Kingdon, 13-Sep-2024.)
(𝜑 → 𝑋 ∈ ℕ∞)    &   (𝜑 → (𝑋‘𝑁) = ∅)    &   (𝜑 → 𝑁 ∈ ω)    &   (𝜑 → 𝑁 = ∅)    ⇒   (𝜑 → DECID (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋)
 
12-Sep-2024nninfisol 7076 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 12102 Lemma for eulerth 12107. 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 10544 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 12105 Lemma for eulerth 12107. 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 12106 Lemma for eulerth 12107. 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 12104 Lemma for eulerth 12107. (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 12103 Lemma for eulerth 12107. 𝑁 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 11533 A finite product of terms apart from zero is apart from zero. A version of fprodap0 11518 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 11526 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 7178 Ordinal trichotomy is equivalent to excluded middle. (Contributed by Jim Kingdon, 26-Aug-2024.)
(EXMID ↔ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥))
 
26-Aug-2024exmidontri 7174 Ordinal trichotomy is equivalent to excluded middle. (Contributed by Jim Kingdon, 26-Aug-2024.)
(EXMID ↔ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥))
 
26-Aug-2024ontri2orexmidim 4531 Ordinal trichotomy implies excluded middle. Closed form of ordtri2or2exmid 4530. (Contributed by Jim Kingdon, 26-Aug-2024.)
(∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥) → DECID 𝜑)
 
26-Aug-2024ontriexmidim 4481 Ordinal trichotomy implies excluded middle. Closed form of ordtriexmid 4480. (Contributed by Jim Kingdon, 26-Aug-2024.)
(∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) → DECID 𝜑)
 
25-Aug-2024onntri2or 7181 Double negated ordinal trichotomy. (Contributed by Jim Kingdon, 25-Aug-2024.)
(¬ ¬ EXMID ↔ ∀𝑥 ∈ On ∀𝑦 ∈ On ¬ ¬ (𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥))
 
25-Aug-2024onntri3or 7180 Double negated ordinal trichotomy. (Contributed by Jim Kingdon, 25-Aug-2024.)
(¬ ¬ EXMID ↔ ∀𝑥 ∈ On ∀𝑦 ∈ On ¬ ¬ (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥))
 
25-Aug-2024csbcow 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.)
⦋𝐴 / 𝑦⦌⦋𝑦 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵
 
25-Aug-2024cbvreuvw 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.)
(𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐴 𝜓)
 
25-Aug-2024cbvrexvw 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.)
(𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)
 
25-Aug-2024cbvralvw 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.)
(𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)
 
25-Aug-2024cbvabw 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.)
Ⅎ𝑦𝜑    &   Ⅎ𝑥𝜓    &   (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓}
 
25-Aug-2024nfsbv 1927 If 𝑧 is not free in 𝜑, it is not free in [𝑦 / 𝑥]𝜑 when 𝑧 is distinct from 𝑥 and 𝑦. Version of nfsb 1926 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 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.)
(𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   (∃𝑥𝜑 ↔ ∃𝑦𝜓)
 
25-Aug-2024cbvalvw 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.)
(𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   (∀𝑥𝜑 ↔ ∀𝑦𝜓)
 
25-Aug-2024nfal 1556 If 𝑥 is not free in 𝜑, it is not free in ∀𝑦𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) Remove dependency on ax-4 1490. (Revised by Gino Giotto, 25-Aug-2024.)
Ⅎ𝑥𝜑    ⇒   Ⅎ𝑥∀𝑦𝜑
 
24-Aug-2024gcdcomd 11857 The gcd operator is commutative, deduction version. (Contributed by SN, 24-Aug-2024.)
(𝜑 → 𝑀 ∈ ℤ)    &   (𝜑 → 𝑁 ∈ ℤ)    ⇒   (𝜑 → (𝑀 gcd 𝑁) = (𝑁 gcd 𝑀))
 
17-Aug-2024fprodcl2lem 11502 Finite product closure lemma. (Contributed by Scott Fenton, 14-Dec-2017.) (Revised by Jim Kingdon, 17-Aug-2024.)
(𝜑 → 𝑆 ⊆ ℂ)    &   ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 · 𝑦) ∈ 𝑆)    &   (𝜑 → 𝐴 ∈ Fin)    &   ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑆)    &   (𝜑 → 𝐴 ≠ ∅)    ⇒   (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 ∈ 𝑆)
 
16-Aug-2024if0ab 13380 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 3551, (𝐴 ∈ 𝑉 → if(𝜑, 𝐴, ∅) ∈ 𝒫 𝐴), from which fmelpw1o 13381 could be derived, yielding an alternative proof. (Contributed by BJ, 16-Aug-2024.)

if(𝜑, 𝐴, ∅) = {𝑥 ∈ 𝐴 ∣ 𝜑}
 
16-Aug-2024fprodunsn 11501 Multiply in an additional term in a finite product. See also fprodsplitsn 11530 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 13384 Alternate proof of bj-charfundc 13383. It was expected to be much shorter since it uses bj-charfun 13382 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 13382 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 13381 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 837, which translate to 1o and ∅ respectively by iftrue 3510 and iffalse 3513, giving pwtrufal 13569).

As proved in if0ab 13380, 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 8520 Equality of complex numbers is stable. Stability here means ¬ ¬ 𝐴 = 𝐵 → 𝐴 = 𝐵 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.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → STAB 𝐴 = 𝐵)
 
15-Aug-2024subap0d 8519 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 4444 Existence of a conditional class (deduction form). (Contributed by BJ, 15-Aug-2024.)
(𝜑 → 𝐴 ∈ 𝑉)    &   (𝜑 → 𝐵 ∈ 𝑊)    ⇒   (𝜑 → if(𝜑, 𝐴, 𝐵) ∈ V)
 
15-Aug-2024ifelpwun 4443 Existence of a conditional class, quantitative version (inference form). (Contributed by BJ, 15-Aug-2024.)
𝐴 ∈ V    &   𝐵 ∈ V    ⇒   if(𝜑, 𝐴, 𝐵) ∈ 𝒫 (𝐴 ∪ 𝐵)
 
15-Aug-2024ifelpwund 4442 Existence of a conditional class, quantitative version (deduction form). (Contributed by BJ, 15-Aug-2024.)
(𝜑 → 𝐴 ∈ 𝑉)    &   (𝜑 → 𝐵 ∈ 𝑊)    ⇒   (𝜑 → if(𝜑, 𝐴, 𝐵) ∈ 𝒫 (𝐴 ∪ 𝐵))
 
15-Aug-2024ifelpwung 4441 Existence of a conditional class, quantitative version (closed form). (Contributed by BJ, 15-Aug-2024.)
((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → if(𝜑, 𝐴, 𝐵) ∈ 𝒫 (𝐴 ∪ 𝐵))
 
15-Aug-2024ifidss 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(𝜑, 𝐴, 𝐴) ⊆ 𝐴
 
15-Aug-2024ifssun 3519 A conditional class is included in the union of its two alternatives. (Contributed by BJ, 15-Aug-2024.)
if(𝜑, 𝐴, 𝐵) ⊆ (𝐴 ∪ 𝐵)
 
12-Aug-2024exmidontriimlem2 7157 Lemma for exmidontriim 7160. (Contributed by Jim Kingdon, 12-Aug-2024.)
(𝜑 → 𝐵 ∈ On)    &   (𝜑 → EXMID)    &   (𝜑 → ∀𝑦 ∈ 𝐵 (𝐴 ∈ 𝑦 ∨ 𝐴 = 𝑦 ∨ 𝑦 ∈ 𝐴))    ⇒   (𝜑 → (𝐴 ∈ 𝐵 ∨ ∀𝑦 ∈ 𝐵 𝑦 ∈ 𝐴))
 
12-Aug-2024exmidontriimlem1 7156 Lemma for exmidontriim 7160. A variation of r19.30dc 2604. (Contributed by Jim Kingdon, 12-Aug-2024.)
((∀𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓 ∨ 𝜒) ∧ EXMID) → (∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓 ∨ ∀𝑥 ∈ 𝐴 𝜒))
 
11-Aug-2024nndc 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 𝜑 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 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 𝒫 1o, like we do in our definition of EXMID (df-exmid 4156): then, we can prove ∀𝑥 ∈ 𝒫 1o¬ ¬ DECID 𝑥 = 1o but we cannot prove ¬ ¬ ∀𝑥 ∈ 𝒫 1oDECID 𝑥 = 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 𝜑
 
10-Aug-2024exmidontriim 7160 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 7159 Lemma for exmidontriim 7160. The induction step for the induction on 𝐴. (Contributed by Jim Kingdon, 10-Aug-2024.)
(𝜑 → 𝐴 ∈ On)    &   (𝜑 → 𝐵 ∈ On)    &   (𝜑 → EXMID)    &   (𝜑 → ∀𝑧 ∈ 𝐴 ∀𝑦 ∈ On (𝑧 ∈ 𝑦 ∨ 𝑧 = 𝑦 ∨ 𝑦 ∈ 𝑧))    ⇒   (𝜑 → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))
 
10-Aug-2024exmidontriimlem3 7158 Lemma for exmidontriim 7160. 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 7070 Canonical embedding of suc ω into ℕ∞. (Contributed by BJ, 10-Aug-2024.)
(𝑁 ∈ suc ω → (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) ∈ ℕ∞)
 
10-Aug-2024infnninf 7067 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 4633 shows. (Contributed by Jim Kingdon, 14-Jul-2022.) Use maps-to notation. (Revised by BJ, 10-Aug-2024.)
(𝑖 ∈ ω ↦ 1o) ∈ ℕ∞
 
9-Aug-2024ss1o0el1o 6857 Reformulation of ss1o0el1 4158 using 1o instead of {∅}. (Contributed by BJ, 9-Aug-2024.)
(𝐴 ⊆ 1o → (∅ ∈ 𝐴 ↔ 𝐴 = 1o))
 
9-Aug-2024pw1dc0el 6856 Another equivalent of excluded middle, which is a mere reformulation of the definition. (Contributed by BJ, 9-Aug-2024.)
(EXMID ↔ ∀𝑥 ∈ 𝒫 1oDECID ∅ ∈ 𝑥)
 
9-Aug-2024ss1o0el1 4158 A subclass of {∅} contains the empty set if and only if it equals {∅}. (Contributed by BJ and Jim Kingdon, 9-Aug-2024.)
(𝐴 ⊆ {∅} → (∅ ∈ 𝐴 ↔ 𝐴 = {∅}))
 
8-Aug-2024pw1dc1 6858 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 ↔ ∀𝑥 ∈ 𝒫 1oDECID 𝑥 = 1o)
 
7-Aug-2024pw1fin 6855 Excluded middle is equivalent to the power set of 1o being finite. (Contributed by SN and Jim Kingdon, 7-Aug-2024.)
(EXMID ↔ 𝒫 1o ∈ Fin)
 
7-Aug-2024elomssom 4564 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 4565. (Revised by BJ, 7-Aug-2024.)
(𝐴 ∈ ω → 𝐴 ⊆ ω)
 
6-Aug-2024bj-charfunbi 13386 In an ambient set 𝑋, if membership in 𝐴 is stable, then it is decidable if and only if 𝐴 has a characteristic function.

This characterization can be applied to singletons when the set 𝑋 has stable equality, which is the case as soon as it has a tight apartness relation. (Contributed by BJ, 6-Aug-2024.)

(𝜑 → 𝑋 ∈ 𝑉)    &   (𝜑 → ∀𝑥 ∈ 𝑋 STAB 𝑥 ∈ 𝐴)    ⇒   (𝜑 → (∀𝑥 ∈ 𝑋 DECID 𝑥 ∈ 𝐴 ↔ ∃𝑓 ∈ (2o ↑𝑚 𝑋)(∀𝑥 ∈ (𝑋 ∩ 𝐴)(𝑓‘𝑥) = 1o ∧ ∀𝑥 ∈ (𝑋 ∖ 𝐴)(𝑓‘𝑥) = ∅)))
 
6-Aug-2024bj-charfunr 13385 If a class 𝐴 has a "weak" characteristic function on a class 𝑋, then negated membership in 𝐴 is decidable (in other words, membership in 𝐴 is testable) in 𝑋.

The hypothesis imposes that 𝑋 be a set. As usual, it could be formulated as (𝜑 → (𝐹:𝑋⟶ω ∧ ...)) 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 𝑓 were any class with testable equality to the point where (𝑋 ∖ 𝐴) is sent. (Contributed by BJ, 6-Aug-2024.)

(𝜑 → ∃𝑓 ∈ (ω ↑𝑚 𝑋)(∀𝑥 ∈ (𝑋 ∩ 𝐴)(𝑓‘𝑥) ≠ ∅ ∧ ∀𝑥 ∈ (𝑋 ∖ 𝐴)(𝑓‘𝑥) = ∅))    ⇒   (𝜑 → ∀𝑥 ∈ 𝑋 DECID ¬ 𝑥 ∈ 𝐴)
 
6-Aug-2024bj-charfundc 13383 Properties of the characteristic function on the class 𝑋 of the class 𝐴, provided membership in 𝐴 is decidable in 𝑋. (Contributed by BJ, 6-Aug-2024.)
(𝜑 → 𝐹 = (𝑥 ∈ 𝑋 ↦ if(𝑥 ∈ 𝐴, 1o, ∅)))    &   (𝜑 → ∀𝑥 ∈ 𝑋 DECID 𝑥 ∈ 𝐴)    ⇒   (𝜑 → (𝐹:𝑋⟶2o ∧ (∀𝑥 ∈ (𝑋 ∩ 𝐴)(𝐹‘𝑥) = 1o ∧ ∀𝑥 ∈ (𝑋 ∖ 𝐴)(𝐹‘𝑥) = ∅)))
 
6-Aug-2024prodssdc 11486 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.)
(𝜑 → 𝐴 ⊆ 𝐵)    &   ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ)    &   (𝜑 → ∃𝑛 ∈ (ℤ≥‘𝑀)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ (ℤ≥‘𝑀) ↦ if(𝑘 ∈ 𝐵, 𝐶, 1))) ⇝ 𝑦))    &   (𝜑 → ∀𝑗 ∈ (ℤ≥‘𝑀)DECID 𝑗 ∈ 𝐴)    &   (𝜑 → 𝑀 ∈ ℤ)    &   ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ 𝐴)) → 𝐶 = 1)    &   (𝜑 → 𝐵 ⊆ (ℤ≥‘𝑀))    &   (𝜑 → ∀𝑗 ∈ (ℤ≥‘𝑀)DECID 𝑗 ∈ 𝐵)    ⇒   (𝜑 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶)
 
5-Aug-2024fnmptd 13379 The maps-to notation defines a function with domain (deduction form). (Contributed by BJ, 5-Aug-2024.)
(𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵))    &   ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    ⇒   (𝜑 → 𝐹 Fn 𝐴)
 
5-Aug-2024funmptd 13378 The maps-to notation defines a function (deduction form).

Note: one should similarly prove a deduction form of funopab4 5207, then prove funmptd 13378 from it, and then prove funmpt 5208 from that: this would reduce global proof length. (Contributed by BJ, 5-Aug-2024.)

(𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵))    ⇒   (𝜑 → Fun 𝐹)
 
5-Aug-20242ssom 13377 The ordinal 2 is included in the set of natural number ordinals. (Contributed by BJ, 5-Aug-2024.)
2o ⊆ ω
 
5-Aug-2024bj-dcfal 13327 The false truth value is decidable. (Contributed by BJ, 5-Aug-2024.)
DECID ⊥
 
5-Aug-2024bj-dctru 13325 The true truth value is decidable. (Contributed by BJ, 5-Aug-2024.)
DECID ⊤
 
5-Aug-2024bj-stfal 13317 The false truth value is stable. (Contributed by BJ, 5-Aug-2024.)
STAB ⊥
 
5-Aug-2024bj-sttru 13315 The true truth value is stable. (Contributed by BJ, 5-Aug-2024.)
STAB ⊤
 
5-Aug-2024prod1dc 11483 Any product of one over a valid set is one. (Contributed by Scott Fenton, 7-Dec-2017.) (Revised by Jim Kingdon, 5-Aug-2024.)
(((𝑀 ∈ ℤ ∧ 𝐴 ⊆ (ℤ≥‘𝑀) ∧ ∀𝑗 ∈ (ℤ≥‘𝑀)DECID 𝑗 ∈ 𝐴) ∨ 𝐴 ∈ Fin) → ∏𝑘 ∈ 𝐴 1 = 1)
 
2-Aug-2024onntri52 7179 Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
(¬ ¬ EXMID → ¬ ¬ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥))
 
2-Aug-2024onntri24 7177 Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
(¬ ¬ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥) → ∀𝑥 ∈ On ∀𝑦 ∈ On ¬ ¬ (𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥))
 
2-Aug-2024onntri45 7176 Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
(∀𝑥 ∈ On ∀𝑦 ∈ On ¬ ¬ (𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥) → ¬ ¬ EXMID)
 
2-Aug-2024onntri51 7175 Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
(¬ ¬ EXMID → ¬ ¬ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥))
 
2-Aug-2024onntri13 7173 Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
(¬ ¬ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) → ∀𝑥 ∈ On ∀𝑦 ∈ On ¬ ¬ (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥))
 
2-Aug-2024onntri35 7172 Double negated ordinal trichotomy.

There are five equivalent statements: (1) ¬ ¬ ∀𝑥 ∈ On∀𝑦 ∈ On(𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥), (2) ¬ ¬ ∀𝑥 ∈ On∀𝑦 ∈ On(𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥), (3) ∀𝑥 ∈ On∀𝑦 ∈ On¬ ¬ (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥), (4) ∀𝑥 ∈ On∀𝑦 ∈ On¬ ¬ (𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥), and (5) ¬ ¬ EXMID. That these are all equivalent is expressed by (1) implies (3) (onntri13 7173), (3) implies (5) (onntri35 7172), (5) implies (1) (onntri51 7175), (2) implies (4) (onntri24 7177), (4) implies (5) (onntri45 7176), and (5) implies (2) (onntri52 7179).

Another way of stating this is that EXMID is equivalent to trichotomy, either the 𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥 or the 𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥 form, as shown in exmidontri 7174 and exmidontri2or 7178, respectively. Thus ¬ ¬ EXMID is equivalent to (1) or (2). In addition, ¬ ¬ EXMID is equivalent to (3) by onntri3or 7180 and (4) by onntri2or 7181.

(Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)

(∀𝑥 ∈ On ∀𝑦 ∈ On ¬ ¬ (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) → ¬ ¬ EXMID)
 
1-Aug-2024nnral 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.)
(¬ ¬ ∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 ¬ ¬ 𝜑)
 
31-Jul-20243nsssucpw1 7171 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 ⊆ suc 𝒫 1o)
 
31-Jul-2024sucpw1nss3 7170 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 𝒫 1o ⊆ 3o)
 
30-Jul-20243nelsucpw1 7169 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 ∈ suc 𝒫 1o
 
30-Jul-2024sucpw1nel3 7168 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 𝒫 1o ∈ 3o
 
30-Jul-2024sucpw1ne3 7167 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 𝒫 1o ≠ 3o)
 
30-Jul-2024pw1nel3 7166 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 → ¬ 𝒫 1o ∈ 3o)
 
30-Jul-2024pw1ne3 7165 The power set of 1o is not three. (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.)
𝒫 1o ≠ 3o
  Copyright terms: Public domain W3C HTML validation [external]