HomeHome Intuitionistic Logic Explorer
Theorem List (p. 73 of 154)
< Previous  Next >
Bad symbols? Try the
GIF version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 7201-7300   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremlpowlpo 7201 LPO implies WLPO. Easy corollary of the more general omniwomnimkv 7200. There is an analogue in terms of analytic omniscience principles at tridceq 15292. (Contributed by Jim Kingdon, 24-Jul-2024.)
(ω ∈ Omni → ω ∈ WOmni)
 
Theoremenwomnilem 7202 Lemma for enwomni 7203. One direction of the biconditional. (Contributed by Jim Kingdon, 20-Jun-2024.)
(𝐴𝐵 → (𝐴 ∈ WOmni → 𝐵 ∈ WOmni))
 
Theoremenwomni 7203 Weak omniscience is invariant with respect to equinumerosity. For example, this means that we can express the Weak Limited Principle of Omniscience as either ω ∈ WOmni or 0 ∈ WOmni. The former is a better match to conventional notation in the sense that df2o3 6459 says that 2o = {∅, 1o} whereas the corresponding relationship does not exist between 2 and {0, 1}. (Contributed by Jim Kingdon, 20-Jun-2024.)
(𝐴𝐵 → (𝐴 ∈ WOmni ↔ 𝐵 ∈ WOmni))
 
Theoremnninfdcinf 7204* The Weak Limited Principle of Omniscience (WLPO) implies that it is decidable whether an element of equals the point at infinity. (Contributed by Jim Kingdon, 3-Dec-2024.)
(𝜑 → ω ∈ WOmni)    &   (𝜑𝑁 ∈ ℕ)       (𝜑DECID 𝑁 = (𝑖 ∈ ω ↦ 1o))
 
Theoremnninfwlporlemd 7205* Given two countably infinite sequences of zeroes and ones, they are equal if and only if a sequence formed by pointwise comparing them is all ones. (Contributed by Jim Kingdon, 6-Dec-2024.)
(𝜑𝑋:ω⟶2o)    &   (𝜑𝑌:ω⟶2o)    &   𝐷 = (𝑖 ∈ ω ↦ if((𝑋𝑖) = (𝑌𝑖), 1o, ∅))       (𝜑 → (𝑋 = 𝑌𝐷 = (𝑖 ∈ ω ↦ 1o)))
 
Theoremnninfwlporlem 7206* Lemma for nninfwlpor 7207. The result. (Contributed by Jim Kingdon, 7-Dec-2024.)
(𝜑𝑋:ω⟶2o)    &   (𝜑𝑌:ω⟶2o)    &   𝐷 = (𝑖 ∈ ω ↦ if((𝑋𝑖) = (𝑌𝑖), 1o, ∅))    &   (𝜑 → ω ∈ WOmni)       (𝜑DECID 𝑋 = 𝑌)
 
Theoremnninfwlpor 7207* The Weak Limited Principle of Omniscience (WLPO) implies that equality for is decidable. (Contributed by Jim Kingdon, 7-Dec-2024.)
(ω ∈ WOmni → ∀𝑥 ∈ ℕ𝑦 ∈ ℕ DECID 𝑥 = 𝑦)
 
Theoremnninfwlpoimlemg 7208* Lemma for nninfwlpoim 7211. (Contributed by Jim Kingdon, 8-Dec-2024.)
(𝜑𝐹:ω⟶2o)    &   𝐺 = (𝑖 ∈ ω ↦ if(∃𝑥 ∈ suc 𝑖(𝐹𝑥) = ∅, ∅, 1o))       (𝜑𝐺 ∈ ℕ)
 
Theoremnninfwlpoimlemginf 7209* Lemma for nninfwlpoim 7211. (Contributed by Jim Kingdon, 8-Dec-2024.)
(𝜑𝐹:ω⟶2o)    &   𝐺 = (𝑖 ∈ ω ↦ if(∃𝑥 ∈ suc 𝑖(𝐹𝑥) = ∅, ∅, 1o))       (𝜑 → (𝐺 = (𝑖 ∈ ω ↦ 1o) ↔ ∀𝑛 ∈ ω (𝐹𝑛) = 1o))
 
Theoremnninfwlpoimlemdc 7210* Lemma for nninfwlpoim 7211. (Contributed by Jim Kingdon, 8-Dec-2024.)
(𝜑𝐹:ω⟶2o)    &   𝐺 = (𝑖 ∈ ω ↦ if(∃𝑥 ∈ suc 𝑖(𝐹𝑥) = ∅, ∅, 1o))    &   (𝜑 → ∀𝑥 ∈ ℕ𝑦 ∈ ℕ DECID 𝑥 = 𝑦)       (𝜑DECID𝑛 ∈ ω (𝐹𝑛) = 1o)
 
Theoremnninfwlpoim 7211* Decidable equality for implies the Weak Limited Principle of Omniscience (WLPO). (Contributed by Jim Kingdon, 9-Dec-2024.)
(∀𝑥 ∈ ℕ𝑦 ∈ ℕ DECID 𝑥 = 𝑦 → ω ∈ WOmni)
 
Theoremnninfwlpo 7212* Decidability of equality for is equivalent to the Weak Limited Principle of Omniscience (WLPO). (Contributed by Jim Kingdon, 3-Dec-2024.)
(∀𝑥 ∈ ℕ𝑦 ∈ ℕ DECID 𝑥 = 𝑦 ↔ ω ∈ WOmni)
 
2.6.41  Cardinal numbers
 
Syntaxccrd 7213 Extend class definition to include the cardinal size function.
class card
 
Definitiondf-card 7214* Define the cardinal number function. The cardinal number of a set is the least ordinal number equinumerous to it. In other words, it is the "size" of the set. Definition of [Enderton] p. 197. Our notation is from Enderton. Other textbooks often use a double bar over the set to express this function. (Contributed by NM, 21-Oct-2003.)
card = (𝑥 ∈ V ↦ {𝑦 ∈ On ∣ 𝑦𝑥})
 
Theoremcardcl 7215* The cardinality of a well-orderable set is an ordinal. (Contributed by Jim Kingdon, 30-Aug-2021.)
(∃𝑦 ∈ On 𝑦𝐴 → (card‘𝐴) ∈ On)
 
Theoremisnumi 7216 A set equinumerous to an ordinal is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.)
((𝐴 ∈ On ∧ 𝐴𝐵) → 𝐵 ∈ dom card)
 
Theoremfinnum 7217 Every finite set is numerable. (Contributed by Mario Carneiro, 4-Feb-2013.) (Revised by Mario Carneiro, 29-Apr-2015.)
(𝐴 ∈ Fin → 𝐴 ∈ dom card)
 
Theoremonenon 7218 Every ordinal number is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.)
(𝐴 ∈ On → 𝐴 ∈ dom card)
 
Theoremcardval3ex 7219* The value of (card‘𝐴). (Contributed by Jim Kingdon, 30-Aug-2021.)
(∃𝑥 ∈ On 𝑥𝐴 → (card‘𝐴) = {𝑦 ∈ On ∣ 𝑦𝐴})
 
Theoremoncardval 7220* The value of the cardinal number function with an ordinal number as its argument. (Contributed by NM, 24-Nov-2003.) (Revised by Mario Carneiro, 13-Sep-2013.)
(𝐴 ∈ On → (card‘𝐴) = {𝑥 ∈ On ∣ 𝑥𝐴})
 
Theoremcardonle 7221 The cardinal of an ordinal number is less than or equal to the ordinal number. Proposition 10.6(3) of [TakeutiZaring] p. 85. (Contributed by NM, 22-Oct-2003.)
(𝐴 ∈ On → (card‘𝐴) ⊆ 𝐴)
 
Theoremcard0 7222 The cardinality of the empty set is the empty set. (Contributed by NM, 25-Oct-2003.)
(card‘∅) = ∅
 
Theoremcarden2bex 7223* If two numerable sets are equinumerous, then they have equal cardinalities. (Contributed by Jim Kingdon, 30-Aug-2021.)
((𝐴𝐵 ∧ ∃𝑥 ∈ On 𝑥𝐴) → (card‘𝐴) = (card‘𝐵))
 
Theorempm54.43 7224 Theorem *54.43 of [WhiteheadRussell] p. 360. (Contributed by NM, 4-Apr-2007.)
((𝐴 ≈ 1o𝐵 ≈ 1o) → ((𝐴𝐵) = ∅ ↔ (𝐴𝐵) ≈ 2o))
 
Theorempr2nelem 7225 Lemma for pr2ne 7226. (Contributed by FL, 17-Aug-2008.)
((𝐴𝐶𝐵𝐷𝐴𝐵) → {𝐴, 𝐵} ≈ 2o)
 
Theorempr2ne 7226 If an unordered pair has two elements they are different. (Contributed by FL, 14-Feb-2010.)
((𝐴𝐶𝐵𝐷) → ({𝐴, 𝐵} ≈ 2o𝐴𝐵))
 
Theoremexmidonfinlem 7227* Lemma for exmidonfin 7228. (Contributed by Andrew W Swan and Jim Kingdon, 9-Mar-2024.)
𝐴 = {{𝑥 ∈ {∅} ∣ 𝜑}, {𝑥 ∈ {∅} ∣ ¬ 𝜑}}       (ω = (On ∩ Fin) → DECID 𝜑)
 
Theoremexmidonfin 7228 If a finite ordinal is a natural number, excluded middle follows. That excluded middle implies that a finite ordinal is a natural number is proved in the Metamath Proof Explorer. That a natural number is a finite ordinal is shown at nnfi 6904 and nnon 4630. (Contributed by Andrew W Swan and Jim Kingdon, 9-Mar-2024.)
(ω = (On ∩ Fin) → EXMID)
 
Theoremen2eleq 7229 Express a set of pair cardinality as the unordered pair of a given element and the other element. (Contributed by Stefan O'Rear, 22-Aug-2015.)
((𝑋𝑃𝑃 ≈ 2o) → 𝑃 = {𝑋, (𝑃 ∖ {𝑋})})
 
Theoremen2other2 7230 Taking the other element twice in a pair gets back to the original element. (Contributed by Stefan O'Rear, 22-Aug-2015.)
((𝑋𝑃𝑃 ≈ 2o) → (𝑃 ∖ { (𝑃 ∖ {𝑋})}) = 𝑋)
 
Theoremdju1p1e2 7231 Disjoint union version of one plus one equals two. (Contributed by Jim Kingdon, 1-Jul-2022.)
(1o ⊔ 1o) ≈ 2o
 
Theoreminfpwfidom 7232 The collection of finite subsets of a set dominates the set. (We use the weaker sethood assumption (𝒫 𝐴 ∩ Fin) ∈ V because this theorem also implies that 𝐴 is a set if 𝒫 𝐴 ∩ Fin is.) (Contributed by Mario Carneiro, 17-May-2015.)
((𝒫 𝐴 ∩ Fin) ∈ V → 𝐴 ≼ (𝒫 𝐴 ∩ Fin))
 
Theoremexmidfodomrlemeldju 7233 Lemma for exmidfodomr 7238. A variant of djur 7102. (Contributed by Jim Kingdon, 2-Jul-2022.)
(𝜑𝐴 ⊆ 1o)    &   (𝜑𝐵 ∈ (𝐴 ⊔ 1o))       (𝜑 → (𝐵 = (inl‘∅) ∨ 𝐵 = (inr‘∅)))
 
Theoremexmidfodomrlemreseldju 7234 Lemma for exmidfodomrlemrALT 7237. A variant of eldju 7101. (Contributed by Jim Kingdon, 9-Jul-2022.)
(𝜑𝐴 ⊆ 1o)    &   (𝜑𝐵 ∈ (𝐴 ⊔ 1o))       (𝜑 → ((∅ ∈ 𝐴𝐵 = ((inl ↾ 𝐴)‘∅)) ∨ 𝐵 = ((inr ↾ 1o)‘∅)))
 
Theoremexmidfodomrlemim 7235* Excluded middle implies the existence of a mapping from any set onto any inhabited set that it dominates. Proposition 1.1 of [PradicBrown2022], p. 2. (Contributed by Jim Kingdon, 1-Jul-2022.)
(EXMID → ∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦))
 
Theoremexmidfodomrlemr 7236* The existence of a mapping from any set onto any inhabited set that it dominates implies excluded middle. Proposition 1.2 of [PradicBrown2022], p. 2. (Contributed by Jim Kingdon, 1-Jul-2022.)
(∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) → EXMID)
 
TheoremexmidfodomrlemrALT 7237* The existence of a mapping from any set onto any inhabited set that it dominates implies excluded middle. Proposition 1.2 of [PradicBrown2022], p. 2. An alternative proof of exmidfodomrlemr 7236. In particular, this proof uses eldju 7101 instead of djur 7102 and avoids djulclb 7088. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Jim Kingdon, 9-Jul-2022.)
(∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) → EXMID)
 
Theoremexmidfodomr 7238* Excluded middle is equivalent to the existence of a mapping from any set onto any inhabited set that it dominates. (Contributed by Jim Kingdon, 1-Jul-2022.)
(EXMID ↔ ∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦))
 
2.6.42  Axiom of Choice equivalents
 
Syntaxwac 7239 Formula for an abbreviation of the axiom of choice.
wff CHOICE
 
Definitiondf-ac 7240* The expression CHOICE will be used as a readable shorthand for any form of the axiom of choice; all concrete forms are long, cryptic, have dummy variables, or all three, making it useful to have a short name. Similar to the Axiom of Choice (first form) of [Enderton] p. 49.

There are some decisions about how to write this definition especially around whether ax-setind 4557 is needed to show equivalence to other ways of stating choice, and about whether choice functions are available for nonempty sets or inhabited sets. (Contributed by Mario Carneiro, 22-Feb-2015.)

(CHOICE ↔ ∀𝑥𝑓(𝑓𝑥𝑓 Fn dom 𝑥))
 
Theoremacfun 7241* A convenient form of choice. The goal here is to state choice as the existence of a choice function on a set of inhabited sets, while making full use of our notation around functions and function values. (Contributed by Jim Kingdon, 20-Nov-2023.)
(𝜑CHOICE)    &   (𝜑𝐴𝑉)    &   (𝜑 → ∀𝑥𝐴𝑤 𝑤𝑥)       (𝜑 → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝑥))
 
Theoremexmidaclem 7242* Lemma for exmidac 7243. The result, with a few hypotheses to break out commonly used expressions. (Contributed by Jim Kingdon, 21-Nov-2023.)
𝐴 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝑦 = {∅})}    &   𝐵 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝑦 = {∅})}    &   𝐶 = {𝐴, 𝐵}       (CHOICEEXMID)
 
Theoremexmidac 7243 The axiom of choice implies excluded middle. See acexmid 5899 for more discussion of this theorem and a way of stating it without using CHOICE or EXMID. (Contributed by Jim Kingdon, 21-Nov-2023.)
(CHOICEEXMID)
 
2.6.43  Cardinal number arithmetic
 
Theoremendjudisj 7244 Equinumerosity of a disjoint union and a union of two disjoint sets. (Contributed by Jim Kingdon, 30-Jul-2023.)
((𝐴𝑉𝐵𝑊 ∧ (𝐴𝐵) = ∅) → (𝐴𝐵) ≈ (𝐴𝐵))
 
Theoremdjuen 7245 Disjoint unions of equinumerous sets are equinumerous. (Contributed by Jim Kingdon, 30-Jul-2023.)
((𝐴𝐵𝐶𝐷) → (𝐴𝐶) ≈ (𝐵𝐷))
 
Theoremdjuenun 7246 Disjoint union is equinumerous to union for disjoint sets. (Contributed by Mario Carneiro, 29-Apr-2015.) (Revised by Jim Kingdon, 19-Aug-2023.)
((𝐴𝐵𝐶𝐷 ∧ (𝐵𝐷) = ∅) → (𝐴𝐶) ≈ (𝐵𝐷))
 
Theoremdju1en 7247 Cardinal addition with cardinal one (which is the same as ordinal one). Used in proof of Theorem 6J of [Enderton] p. 143. (Contributed by NM, 28-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
((𝐴𝑉 ∧ ¬ 𝐴𝐴) → (𝐴 ⊔ 1o) ≈ suc 𝐴)
 
Theoremdju0en 7248 Cardinal addition with cardinal zero (the empty set). Part (a1) of proof of Theorem 6J of [Enderton] p. 143. (Contributed by NM, 27-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
(𝐴𝑉 → (𝐴 ⊔ ∅) ≈ 𝐴)
 
Theoremxp2dju 7249 Two times a cardinal number. Exercise 4.56(g) of [Mendelson] p. 258. (Contributed by NM, 27-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
(2o × 𝐴) = (𝐴𝐴)
 
Theoremdjucomen 7250 Commutative law for cardinal addition. Exercise 4.56(c) of [Mendelson] p. 258. (Contributed by NM, 24-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
((𝐴𝑉𝐵𝑊) → (𝐴𝐵) ≈ (𝐵𝐴))
 
Theoremdjuassen 7251 Associative law for cardinal addition. Exercise 4.56(c) of [Mendelson] p. 258. (Contributed by NM, 26-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
((𝐴𝑉𝐵𝑊𝐶𝑋) → ((𝐴𝐵) ⊔ 𝐶) ≈ (𝐴 ⊔ (𝐵𝐶)))
 
Theoremxpdjuen 7252 Cardinal multiplication distributes over cardinal addition. Theorem 6I(3) of [Enderton] p. 142. (Contributed by NM, 26-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
((𝐴𝑉𝐵𝑊𝐶𝑋) → (𝐴 × (𝐵𝐶)) ≈ ((𝐴 × 𝐵) ⊔ (𝐴 × 𝐶)))
 
Theoremdjudoml 7253 A set is dominated by its disjoint union with another. (Contributed by Jim Kingdon, 11-Jul-2023.)
((𝐴𝑉𝐵𝑊) → 𝐴 ≼ (𝐴𝐵))
 
Theoremdjudomr 7254 A set is dominated by its disjoint union with another. (Contributed by Jim Kingdon, 11-Jul-2023.)
((𝐴𝑉𝐵𝑊) → 𝐵 ≼ (𝐴𝐵))
 
2.6.44  Ordinal trichotomy
 
Theoremexmidontriimlem1 7255 Lemma for exmidontriim 7259. A variation of r19.30dc 2637. (Contributed by Jim Kingdon, 12-Aug-2024.)
((∀𝑥𝐴 (𝜑𝜓𝜒) ∧ EXMID) → (∃𝑥𝐴 𝜑 ∨ ∃𝑥𝐴 𝜓 ∨ ∀𝑥𝐴 𝜒))
 
Theoremexmidontriimlem2 7256* Lemma for exmidontriim 7259. (Contributed by Jim Kingdon, 12-Aug-2024.)
(𝜑𝐵 ∈ On)    &   (𝜑EXMID)    &   (𝜑 → ∀𝑦𝐵 (𝐴𝑦𝐴 = 𝑦𝑦𝐴))       (𝜑 → (𝐴𝐵 ∨ ∀𝑦𝐵 𝑦𝐴))
 
Theoremexmidontriimlem3 7257* Lemma for exmidontriim 7259. What we get to do based on induction on both 𝐴 and 𝐵. (Contributed by Jim Kingdon, 10-Aug-2024.)
(𝜑𝐴 ∈ On)    &   (𝜑𝐵 ∈ On)    &   (𝜑EXMID)    &   (𝜑 → ∀𝑧𝐴𝑦 ∈ On (𝑧𝑦𝑧 = 𝑦𝑦𝑧))    &   (𝜑 → ∀𝑦𝐵 (𝐴𝑦𝐴 = 𝑦𝑦𝐴))       (𝜑 → (𝐴𝐵𝐴 = 𝐵𝐵𝐴))
 
Theoremexmidontriimlem4 7258* Lemma for exmidontriim 7259. The induction step for the induction on 𝐴. (Contributed by Jim Kingdon, 10-Aug-2024.)
(𝜑𝐴 ∈ On)    &   (𝜑𝐵 ∈ On)    &   (𝜑EXMID)    &   (𝜑 → ∀𝑧𝐴𝑦 ∈ On (𝑧𝑦𝑧 = 𝑦𝑦𝑧))       (𝜑 → (𝐴𝐵𝐴 = 𝐵𝐵𝐴))
 
Theoremexmidontriim 7259* 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 (𝑥𝑦𝑥 = 𝑦𝑦𝑥))
 
2.6.45  Excluded middle and the power set of a singleton
 
Theorempw1on 7260 The power set of 1o is an ordinal. (Contributed by Jim Kingdon, 29-Jul-2024.)
𝒫 1o ∈ On
 
Theorempw1dom2 7261 The power set of 1o dominates 2o. Also see pwpw0ss 3822 which is similar. (Contributed by Jim Kingdon, 21-Sep-2022.)
2o ≼ 𝒫 1o
 
Theorempw1ne0 7262 The power set of 1o is not zero. (Contributed by Jim Kingdon, 30-Jul-2024.)
𝒫 1o ≠ ∅
 
Theorempw1ne1 7263 The power set of 1o is not one. (Contributed by Jim Kingdon, 30-Jul-2024.)
𝒫 1o ≠ 1o
 
Theorempw1ne3 7264 The power set of 1o is not three. (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.)
𝒫 1o ≠ 3o
 
Theorempw1nel3 7265 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)
 
Theoremsucpw1ne3 7266 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)
 
Theoremsucpw1nel3 7267 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
 
Theorem3nelsucpw1 7268 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
 
Theoremsucpw1nss3 7269 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)
 
Theorem3nsssucpw1 7270 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)
 
Theoremonntri35 7271* 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 7272), (3) implies (5) (onntri35 7271), (5) implies (1) (onntri51 7274), (2) implies (4) (onntri24 7276), (4) implies (5) (onntri45 7275), and (5) implies (2) (onntri52 7278).

Another way of stating this is that EXMID is equivalent to trichotomy, either the 𝑥𝑦𝑥 = 𝑦𝑦𝑥 or the 𝑥𝑦𝑦𝑥 form, as shown in exmidontri 7273 and exmidontri2or 7277, respectively. Thus ¬ ¬ EXMID is equivalent to (1) or (2). In addition, ¬ ¬ EXMID is equivalent to (3) by onntri3or 7279 and (4) by onntri2or 7280.

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

(∀𝑥 ∈ On ∀𝑦 ∈ On ¬ ¬ (𝑥𝑦𝑥 = 𝑦𝑦𝑥) → ¬ ¬ EXMID)
 
Theoremonntri13 7272 Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
(¬ ¬ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥𝑦𝑥 = 𝑦𝑦𝑥) → ∀𝑥 ∈ On ∀𝑦 ∈ On ¬ ¬ (𝑥𝑦𝑥 = 𝑦𝑦𝑥))
 
Theoremexmidontri 7273* Ordinal trichotomy is equivalent to excluded middle. (Contributed by Jim Kingdon, 26-Aug-2024.)
(EXMID ↔ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥𝑦𝑥 = 𝑦𝑦𝑥))
 
Theoremonntri51 7274* Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
(¬ ¬ EXMID → ¬ ¬ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥𝑦𝑥 = 𝑦𝑦𝑥))
 
Theoremonntri45 7275* Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
(∀𝑥 ∈ On ∀𝑦 ∈ On ¬ ¬ (𝑥𝑦𝑦𝑥) → ¬ ¬ EXMID)
 
Theoremonntri24 7276 Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
(¬ ¬ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥𝑦𝑦𝑥) → ∀𝑥 ∈ On ∀𝑦 ∈ On ¬ ¬ (𝑥𝑦𝑦𝑥))
 
Theoremexmidontri2or 7277* Ordinal trichotomy is equivalent to excluded middle. (Contributed by Jim Kingdon, 26-Aug-2024.)
(EXMID ↔ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥𝑦𝑦𝑥))
 
Theoremonntri52 7278* Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
(¬ ¬ EXMID → ¬ ¬ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥𝑦𝑦𝑥))
 
Theoremonntri3or 7279* Double negated ordinal trichotomy. (Contributed by Jim Kingdon, 25-Aug-2024.)
(¬ ¬ EXMID ↔ ∀𝑥 ∈ On ∀𝑦 ∈ On ¬ ¬ (𝑥𝑦𝑥 = 𝑦𝑦𝑥))
 
Theoremonntri2or 7280* Double negated ordinal trichotomy. (Contributed by Jim Kingdon, 25-Aug-2024.)
(¬ ¬ EXMID ↔ ∀𝑥 ∈ On ∀𝑦 ∈ On ¬ ¬ (𝑥𝑦𝑦𝑥))
 
2.6.46  Apartness relations
 
Syntaxwap 7281 Apartness predicate symbol.
wff 𝑅 Ap 𝐴
 
Definitiondf-pap 7282* Apartness predicate. A relation 𝑅 is an apartness if it is irreflexive, symmetric, and cotransitive. (Contributed by Jim Kingdon, 14-Feb-2025.)
(𝑅 Ap 𝐴 ↔ ((𝑅 ⊆ (𝐴 × 𝐴) ∧ ∀𝑥𝐴 ¬ 𝑥𝑅𝑥) ∧ (∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑥) ∧ ∀𝑥𝐴𝑦𝐴𝑧𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑦𝑅𝑧)))))
 
Syntaxwtap 7283 Tight apartness predicate symbol.
wff 𝑅 TAp 𝐴
 
Definitiondf-tap 7284* Tight apartness predicate. A relation 𝑅 is a tight apartness if it is irreflexive, symmetric, cotransitive, and tight. (Contributed by Jim Kingdon, 5-Feb-2025.)
(𝑅 TAp 𝐴 ↔ (𝑅 Ap 𝐴 ∧ ∀𝑥𝐴𝑦𝐴𝑥𝑅𝑦𝑥 = 𝑦)))
 
Theoremdftap2 7285* Tight apartness with the apartness properties from df-pap 7282 expanded. (Contributed by Jim Kingdon, 21-Feb-2025.)
(𝑅 TAp 𝐴 ↔ (𝑅 ⊆ (𝐴 × 𝐴) ∧ (∀𝑥𝐴 ¬ 𝑥𝑅𝑥 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑦𝑅𝑥)) ∧ (∀𝑥𝐴𝑦𝐴𝑧𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑦𝑅𝑧)) ∧ ∀𝑥𝐴𝑦𝐴𝑥𝑅𝑦𝑥 = 𝑦))))
 
Theoremtapeq1 7286 Equality theorem for tight apartness predicate. (Contributed by Jim Kingdon, 8-Feb-2025.)
(𝑅 = 𝑆 → (𝑅 TAp 𝐴𝑆 TAp 𝐴))
 
Theoremtapeq2 7287 Equality theorem for tight apartness predicate. (Contributed by Jim Kingdon, 15-Feb-2025.)
(𝐴 = 𝐵 → (𝑅 TAp 𝐴𝑅 TAp 𝐵))
 
Theoremnetap 7288* Negated equality on a set with decidable equality is a tight apartness. (Contributed by Jim Kingdon, 5-Feb-2025.)
(∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦 → {⟨𝑢, 𝑣⟩ ∣ ((𝑢𝐴𝑣𝐴) ∧ 𝑢𝑣)} TAp 𝐴)
 
Theorem2onetap 7289* Negated equality is a tight apartness on 2o. (Contributed by Jim Kingdon, 6-Feb-2025.)
{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ 𝑢𝑣)} TAp 2o
 
Theorem2oneel 7290* and 1o are two unequal elements of 2o. (Contributed by Jim Kingdon, 8-Feb-2025.)
⟨∅, 1o⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ 𝑢𝑣)}
 
Theorem2omotaplemap 7291* Lemma for 2omotap 7293. (Contributed by Jim Kingdon, 6-Feb-2025.)
(¬ ¬ 𝜑 → {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o𝑣 ∈ 2o) ∧ (𝜑𝑢𝑣))} TAp 2o)
 
Theorem2omotaplemst 7292* Lemma for 2omotap 7293. (Contributed by Jim Kingdon, 6-Feb-2025.)
((∃*𝑟 𝑟 TAp 2o ∧ ¬ ¬ 𝜑) → 𝜑)
 
Theorem2omotap 7293 If there is at most one tight apartness on 2o, excluded middle follows. Based on online discussions by Tom de Jong, Andrew W Swan, and Martin Escardo. (Contributed by Jim Kingdon, 6-Feb-2025.)
(∃*𝑟 𝑟 TAp 2oEXMID)
 
Theoremexmidapne 7294* Excluded middle implies there is only one tight apartness on any class, namely negated equality. (Contributed by Jim Kingdon, 14-Feb-2025.)
(EXMID → (𝑅 TAp 𝐴𝑅 = {⟨𝑢, 𝑣⟩ ∣ ((𝑢𝐴𝑣𝐴) ∧ 𝑢𝑣)}))
 
Theoremexmidmotap 7295* The proposition that every class has at most one tight apartness is equivalent to excluded middle. (Contributed by Jim Kingdon, 14-Feb-2025.)
(EXMID ↔ ∀𝑥∃*𝑟 𝑟 TAp 𝑥)
 
PART 3  CHOICE PRINCIPLES

We have already introduced the full Axiom of Choice df-ac 7240 but since it implies excluded middle as shown at exmidac 7243, it is not especially relevant to us. In this section we define countable choice and dependent choice, which are not as strong as thus often considered in mathematics which seeks to avoid full excluded middle.

 
3.1  Countable Choice and Dependent Choice
 
3.1.1  Introduce Countable Choice
 
Syntaxwacc 7296 Formula for an abbreviation of countable choice.
wff CCHOICE
 
Definitiondf-cc 7297* The expression CCHOICE will be used as a readable shorthand for any form of countable choice, analogous to df-ac 7240 for full choice. (Contributed by Jim Kingdon, 27-Nov-2023.)
(CCHOICE ↔ ∀𝑥(dom 𝑥 ≈ ω → ∃𝑓(𝑓𝑥𝑓 Fn dom 𝑥)))
 
Theoremccfunen 7298* Existence of a choice function for a countably infinite set. (Contributed by Jim Kingdon, 28-Nov-2023.)
(𝜑CCHOICE)    &   (𝜑𝐴 ≈ ω)    &   (𝜑 → ∀𝑥𝐴𝑤 𝑤𝑥)       (𝜑 → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝑥))
 
Theoremcc1 7299* Countable choice in terms of a choice function on a countably infinite set of inhabited sets. (Contributed by Jim Kingdon, 27-Apr-2024.)
(CCHOICE → ∀𝑥((𝑥 ≈ ω ∧ ∀𝑧𝑥𝑤 𝑤𝑧) → ∃𝑓𝑧𝑥 (𝑓𝑧) ∈ 𝑧))
 
Theoremcc2lem 7300* Lemma for cc2 7301. (Contributed by Jim Kingdon, 27-Apr-2024.)
(𝜑CCHOICE)    &   (𝜑𝐹 Fn ω)    &   (𝜑 → ∀𝑥 ∈ ω ∃𝑤 𝑤 ∈ (𝐹𝑥))    &   𝐴 = (𝑛 ∈ ω ↦ ({𝑛} × (𝐹𝑛)))    &   𝐺 = (𝑛 ∈ ω ↦ (2nd ‘(𝑓‘(𝐴𝑛))))       (𝜑 → ∃𝑔(𝑔 Fn ω ∧ ∀𝑛 ∈ ω (𝑔𝑛) ∈ (𝐹𝑛)))
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14900 150 14901-15000 151 15001-15100 152 15101-15200 153 15201-15300 154 15301-15320
  Copyright terms: Public domain < Previous  Next >