 Home Intuitionistic Logic ExplorerTheorem List (p. 68 of 114) < 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 - 6701-6800   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremdjur 6701* A member of a disjoint union can be mapped from one of the classes which produced it. (Contributed by Jim Kingdon, 23-Jun-2022.)
(𝐶 ∈ (𝐴𝐵) → (∃𝑥𝐴 𝐶 = (inl‘𝑥) ∨ ∃𝑥𝐵 𝐶 = (inr‘𝑥)))

Theoremdjuunr 6702 The disjoint union of two classes is the union of the images of those two classes under right and left injection. (Contributed by Jim Kingdon, 22-Jun-2022.) (Proof shortened by BJ, 6-Jul-2022.)
(ran (inl ↾ 𝐴) ∪ ran (inr ↾ 𝐵)) = (𝐴𝐵)

Theoremeldju 6703* Element of a disjoint union. (Contributed by BJ and Jim Kingdon, 23-Jun-2022.)
(𝐶 ∈ (𝐴𝐵) ↔ (∃𝑥𝐴 𝐶 = ((inl ↾ 𝐴)‘𝑥) ∨ ∃𝑥𝐵 𝐶 = ((inr ↾ 𝐵)‘𝑥)))

Theoremdjuun 6704 The disjoint union of two classes is the union of the images of those two classes under right and left injection. (Contributed by Jim Kingdon, 22-Jun-2022.) (Proof shortened by BJ, 6-Jul-2022.)
((inl “ 𝐴) ∪ (inr “ 𝐵)) = (𝐴𝐵)

2.6.33.3  Universal property of the disjoint union

Theoremdjuss 6705 A disjoint union is a subset of a Cartesian product. (Contributed by AV, 25-Jun-2022.)
(𝐴𝐵) ⊆ ({∅, 1𝑜} × (𝐴𝐵))

Theoremeldju1st 6706 The first component of an element of a disjoint union is either or 1𝑜. (Contributed by AV, 26-Jun-2022.)
(𝑋 ∈ (𝐴𝐵) → ((1st𝑋) = ∅ ∨ (1st𝑋) = 1𝑜))

Theoremeldju2ndl 6707 The second component of an element of a disjoint union is an element of the left class of the disjoint union if its first component is the empty set. (Contributed by AV, 26-Jun-2022.)
((𝑋 ∈ (𝐴𝐵) ∧ (1st𝑋) = ∅) → (2nd𝑋) ∈ 𝐴)

Theoremeldju2ndr 6708 The second component of an element of a disjoint union is an element of the right class of the disjoint union if its first component is not the empty set. (Contributed by AV, 26-Jun-2022.)
((𝑋 ∈ (𝐴𝐵) ∧ (1st𝑋) ≠ ∅) → (2nd𝑋) ∈ 𝐵)

Theorem1stinl 6709 The first component of the value of a left injection is the empty set. (Contributed by AV, 27-Jun-2022.)
(𝑋𝑉 → (1st ‘(inl‘𝑋)) = ∅)

Theorem2ndinl 6710 The second component of the value of a left injection is its argument. (Contributed by AV, 27-Jun-2022.)
(𝑋𝑉 → (2nd ‘(inl‘𝑋)) = 𝑋)

Theorem1stinr 6711 The first component of the value of a right injection is 1𝑜. (Contributed by AV, 27-Jun-2022.)
(𝑋𝑉 → (1st ‘(inr‘𝑋)) = 1𝑜)

Theorem2ndinr 6712 The second component of the value of a right injection is its argument. (Contributed by AV, 27-Jun-2022.)
(𝑋𝑉 → (2nd ‘(inr‘𝑋)) = 𝑋)

Theoremdjune 6713 Left and right injection never produce equal values. (Contributed by Jim Kingdon, 2-Jul-2022.)
((𝐴𝑉𝐵𝑊) → (inl‘𝐴) ≠ (inr‘𝐵))

Theoremupdjudhf 6714* The mapping of an element of the disjoint union to the value of the corresponding function is a function. (Contributed by AV, 26-Jun-2022.)
(𝜑𝐹:𝐴𝐶)    &   (𝜑𝐺:𝐵𝐶)    &   𝐻 = (𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))       (𝜑𝐻:(𝐴𝐵)⟶𝐶)

Theoremupdjudhcoinlf 6715* The composition of the mapping of an element of the disjoint union to the value of the corresponding function and the left injection equals the first function. (Contributed by AV, 27-Jun-2022.)
(𝜑𝐹:𝐴𝐶)    &   (𝜑𝐺:𝐵𝐶)    &   𝐻 = (𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))       (𝜑 → (𝐻 ∘ (inl ↾ 𝐴)) = 𝐹)

Theoremupdjudhcoinrg 6716* The composition of the mapping of an element of the disjoint union to the value of the corresponding function and the right injection equals the second function. (Contributed by AV, 27-Jun-2022.)
(𝜑𝐹:𝐴𝐶)    &   (𝜑𝐺:𝐵𝐶)    &   𝐻 = (𝑥 ∈ (𝐴𝐵) ↦ if((1st𝑥) = ∅, (𝐹‘(2nd𝑥)), (𝐺‘(2nd𝑥))))       (𝜑 → (𝐻 ∘ (inr ↾ 𝐵)) = 𝐺)

Theoremupdjud 6717* Universal property of the disjoint union. (Proposed by BJ, 25-Jun-2022.) (Contributed by AV, 28-Jun-2022.)
(𝜑𝐹:𝐴𝐶)    &   (𝜑𝐺:𝐵𝐶)    &   (𝜑𝐴𝑉)    &   (𝜑𝐵𝑊)       (𝜑 → ∃!(:(𝐴𝐵)⟶𝐶 ∧ ( ∘ (inl ↾ 𝐴)) = 𝐹 ∧ ( ∘ (inr ↾ 𝐵)) = 𝐺))

Syntaxcdjucase 6718 Syntax for the "case" construction.
class case(𝑅, 𝑆)

Definitiondf-case 6719 The "case" construction: if 𝐹:𝐴𝑋 and 𝐺:𝐵𝑋 are functions, then case(𝐹, 𝐺):(𝐴𝐵)⟶𝑋 is the natural function obtained by a definition by cases, hence the name. It is the unique function whose existence is asserted by the universal property of disjoint unions. The definition is adapted to make sense also for binary relations (where the universal property also holds). (Contributed by MC and BJ, 10-Jul-2022.)
case(𝑅, 𝑆) = ((𝑅inl) ∪ (𝑆inr))

Theoremcasefun 6720 The "case" construction of two functions is a function. (Contributed by BJ, 10-Jul-2022.)
(𝜑 → Fun 𝐹)    &   (𝜑 → Fun 𝐺)       (𝜑 → Fun case(𝐹, 𝐺))

Theoremcasedm 6721 The domain of the "case" construction is the disjoint union of the domains. TODO (although less important): ran case(𝐹, 𝐺) = (ran 𝐹 ∪ ran 𝐺). (Contributed by BJ, 10-Jul-2022.)
dom case(𝐹, 𝐺) = (dom 𝐹 ⊔ dom 𝐺)

Theoremcaserel 6722 The "case" construction of two relations is a relation, with bounds on its domain and codomain. Typically, the "case" construction is used when both relations have a common codomain. (Contributed by BJ, 10-Jul-2022.)
case(𝑅, 𝑆) ⊆ ((dom 𝑅 ⊔ dom 𝑆) × (ran 𝑅 ∪ ran 𝑆))

Theoremcasef 6723 The "case" construction of two functions is a function on the disjoint union of their domains. (Contributed by BJ, 10-Jul-2022.)
(𝜑𝐹:𝐴𝑋)    &   (𝜑𝐺:𝐵𝑋)       (𝜑 → case(𝐹, 𝐺):(𝐴𝐵)⟶𝑋)

Theoremcaseinj 6724 The "case" construction of two injective relations with disjoint ranges is an injective relation. (Contributed by BJ, 10-Jul-2022.)
(𝜑 → Fun 𝑅)    &   (𝜑 → Fun 𝑆)    &   (𝜑 → (ran 𝑅 ∩ ran 𝑆) = ∅)       (𝜑 → Fun case(𝑅, 𝑆))

Theoremcasef1 6725 The "case" construction of two injective functions with disjoint ranges is an injective function. (Contributed by BJ, 10-Jul-2022.)
(𝜑𝐹:𝐴1-1𝑋)    &   (𝜑𝐺:𝐵1-1𝑋)    &   (𝜑 → (ran 𝐹 ∩ ran 𝐺) = ∅)       (𝜑 → case(𝐹, 𝐺):(𝐴𝐵)–1-1𝑋)

2.6.33.4  Older definition temporarily kept for comparison, to be deleted

Syntaxcdjud 6726 Syntax for the domain-disjoint-union of two relations.
class (𝑅d 𝑆)

Definitiondf-djud 6727 The "domain-disjoint-union" of two relations: if 𝑅 ⊆ (𝐴 × 𝑋) and 𝑆 ⊆ (𝐵 × 𝑋) are two binary relations, then (𝑅d 𝑆) is the binary relation from (𝐴𝐵) to 𝑋 having the universal property of disjoint unions.

Remark: the restrictions to dom 𝑅 (resp. dom 𝑆) are not necessary since extra stuff would be thrown away in the post-composition with 𝑅 (resp. 𝑆), but they are explicitly written for clarity. (Contributed by MC and BJ, 10-Jul-2022.)

(𝑅d 𝑆) = ((𝑅(inl ↾ dom 𝑅)) ∪ (𝑆(inr ↾ dom 𝑆)))

Theoremdjufun 6728 The "domain-disjoint-union" of two functions is a function. (Contributed by BJ, 10-Jul-2022.)
(𝜑 → Fun 𝐹)    &   (𝜑 → Fun 𝐺)       (𝜑 → Fun (𝐹d 𝐺))

Theoremdjudm 6729 The domain of the "domain-disjoint-union" is the disjoint union of the domains. Remark: its range is the (standard) union of the ranges. (Contributed by BJ, 10-Jul-2022.)
dom (𝐹d 𝐺) = (dom 𝐹 ⊔ dom 𝐺)

Theoremdjuinj 6730 The "domain-disjoint-union" of two injective relations with disjoint ranges is an injective relation. (Contributed by BJ, 10-Jul-2022.)
(𝜑 → Fun 𝑅)    &   (𝜑 → Fun 𝑆)    &   (𝜑 → (ran 𝑅 ∩ ran 𝑆) = ∅)       (𝜑 → Fun (𝑅d 𝑆))

Theoremdjudom 6731 Dominance law for disjoint union. (Contributed by Jim Kingdon, 25-Jul-2022.)
((𝐴𝐵𝐶𝐷) → (𝐴𝐶) ≼ (𝐵𝐷))

2.6.34  Omniscient sets

Syntaxcomni 6732 Extend class definition to include the class of omniscient sets.
class Omni

Syntaxxnninf 6733 Set of nonincreasing sequences in 2𝑜𝑚 ω.
class

Definitiondf-omni 6734* An omniscient set is one where we can decide whether a predicate (here represented by a function 𝑓) holds (is equal to 1𝑜) for all elements or fails to hold (is equal to ) for some element. Definition 3.1 of [Pierik], p. 14.

In particular, ω ∈ Omni is known as the Lesser Principle of Omniscience (LPO). (Contributed by Jim Kingdon, 28-Jun-2022.)

Omni = {𝑦 ∣ ∀𝑓(𝑓:𝑦⟶2𝑜 → (∃𝑥𝑦 (𝑓𝑥) = ∅ ∨ ∀𝑥𝑦 (𝑓𝑥) = 1𝑜))}

Definitiondf-nninf 6735* Define the set of nonincreasing sequences in 2𝑜𝑚 ω. Definition in Section 3.1 of [Pierik], p. 15. If we assumed excluded middle, this would be essentially the same as 0* as defined at df-xnn0 8670 but in its absence the relationship between the two is more complicated. This definition would function much the same whether we used ω or 0, but the former allows us to take advantage of 2𝑜 = {∅, 1𝑜} (df2o3 6149) so we adopt it. (Contributed by Jim Kingdon, 14-Jul-2022.)
= {𝑓 ∈ (2𝑜𝑚 ω) ∣ ∀𝑖 ∈ ω (𝑓‘suc 𝑖) ⊆ (𝑓𝑖)}

Theoremisomni 6736* The predicate of being omniscient. (Contributed by Jim Kingdon, 28-Jun-2022.)
(𝐴𝑉 → (𝐴 ∈ Omni ↔ ∀𝑓(𝑓:𝐴⟶2𝑜 → (∃𝑥𝐴 (𝑓𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑓𝑥) = 1𝑜))))

Theoremisomnimap 6737* The predicate of being omniscient stated in terms of set exponentiation. (Contributed by Jim Kingdon, 13-Jul-2022.)
(𝐴𝑉 → (𝐴 ∈ Omni ↔ ∀𝑓 ∈ (2𝑜𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = ∅ ∨ ∀𝑥𝐴 (𝑓𝑥) = 1𝑜)))

Theoremenomnilem 6738 Lemma for enomni 6739. One direction of the biconditional. (Contributed by Jim Kingdon, 13-Jul-2022.)
(𝐴𝐵 → (𝐴 ∈ Omni → 𝐵 ∈ Omni))

Theoremenomni 6739 Omniscience is invariant with respect to equinumerosity. For example, this means that we can express the Lesser Principle of Omniscience as either ω ∈ Omni or 0 ∈ Omni. The former is a better match to conventional notation in the sense that df2o3 6149 says that 2𝑜 = {∅, 1𝑜} whereas the corresponding relationship does not exist between 2 and {0, 1}. (Contributed by Jim Kingdon, 13-Jul-2022.)
(𝐴𝐵 → (𝐴 ∈ Omni ↔ 𝐵 ∈ Omni))

Theoremfinomni 6740 A finite set is omniscient. Remark right after Definition 3.1 of [Pierik], p. 14. (Contributed by Jim Kingdon, 28-Jun-2022.)
(𝐴 ∈ Fin → 𝐴 ∈ Omni)

Theoremexmidomniim 6741 Given excluded middle, every set is omniscient. Remark following Definition 3.1 of [Pierik], p. 14. This is one direction of the biconditional exmidomni 6742. (Contributed by Jim Kingdon, 29-Jun-2022.)
(EXMID → ∀𝑥 𝑥 ∈ Omni)

Theoremexmidomni 6742 Excluded middle is equivalent to every set being omniscient. (Contributed by BJ and Jim Kingdon, 30-Jun-2022.)
(EXMID ↔ ∀𝑥 𝑥 ∈ Omni)

Theoremfodjuomnilemdc 6743* Lemma for fodjuomni 6748. Decidability of a condition we use in various lemmas. (Contributed by Jim Kingdon, 27-Jul-2022.)
(𝜑𝐹:𝑂onto→(𝐴𝐵))       ((𝜑𝑋𝑂) → DECID𝑧𝐴 (𝐹𝑋) = (inl‘𝑧))

Theoremfodjuomnilemf 6744* Lemma for fodjuomni 6748. Domain and range of 𝑃. (Contributed by Jim Kingdon, 27-Jul-2022.)
(𝜑𝑂 ∈ Omni)    &   (𝜑𝐹:𝑂onto→(𝐴𝐵))    &   𝑃 = (𝑦𝑂 ↦ if(∃𝑧𝐴 (𝐹𝑦) = (inl‘𝑧), ∅, 1𝑜))       (𝜑𝑃 ∈ (2𝑜𝑚 𝑂))

Theoremfodjuomnilemm 6745* Lemma for fodjuomni 6748. The case where A is inhabited. (Contributed by Jim Kingdon, 27-Jul-2022.)
(𝜑𝑂 ∈ Omni)    &   (𝜑𝐹:𝑂onto→(𝐴𝐵))    &   𝑃 = (𝑦𝑂 ↦ if(∃𝑧𝐴 (𝐹𝑦) = (inl‘𝑧), ∅, 1𝑜))    &   (𝜑 → ∃𝑤𝑂 (𝑃𝑤) = ∅)       (𝜑 → ∃𝑥 𝑥𝐴)

Theoremfodjuomnilem0 6746* Lemma for fodjuomni 6748. The case where A is empty. (Contributed by Jim Kingdon, 27-Jul-2022.)
(𝜑𝑂 ∈ Omni)    &   (𝜑𝐹:𝑂onto→(𝐴𝐵))    &   𝑃 = (𝑦𝑂 ↦ if(∃𝑧𝐴 (𝐹𝑦) = (inl‘𝑧), ∅, 1𝑜))    &   (𝜑 → ∀𝑤𝑂 (𝑃𝑤) = 1𝑜)       (𝜑𝐴 = ∅)

Theoremfodjuomnilemres 6747* Lemma for fodjuomni 6748. The final result with 𝑃 broken out into a hypothesis. (Contributed by Jim Kingdon, 29-Jul-2022.)
(𝜑𝑂 ∈ Omni)    &   (𝜑𝐹:𝑂onto→(𝐴𝐵))    &   𝑃 = (𝑦𝑂 ↦ if(∃𝑧𝐴 (𝐹𝑦) = (inl‘𝑧), ∅, 1𝑜))       (𝜑 → (∃𝑥 𝑥𝐴𝐴 = ∅))

Theoremfodjuomni 6748* A condition which ensures 𝐴 is either inhabited or empty. Lemma 3.2 of [PradicBrown2022], p. 4. (Contributed by Jim Kingdon, 27-Jul-2022.)
(𝜑𝑂 ∈ Omni)    &   (𝜑𝐹:𝑂onto→(𝐴𝐵))       (𝜑 → (∃𝑥 𝑥𝐴𝐴 = ∅))

Theoreminfnninf 6749 The point at infinity in (the constant sequence equal to 1𝑜). (Contributed by Jim Kingdon, 14-Jul-2022.)
(ω × {1𝑜}) ∈ ℕ

Theoremnnnninf 6750* Elements of corresponding to natural numbers. The natural number 𝑁 corresponds to a sequence of 𝑁 ones followed by zeroes. Contrast to a sequence which is all ones as seen at infnninf 6749. Remark/TODO: the theorem still holds if 𝑁 = ω, that is, the antecedent could be weakened to 𝑁 ∈ suc ω. (Contributed by Jim Kingdon, 14-Jul-2022.)
(𝑁 ∈ ω → (𝑖 ∈ ω ↦ if(𝑖𝑁, 1𝑜, ∅)) ∈ ℕ)

2.6.35  Cardinal numbers

Syntaxccrd 6751 Extend class definition to include the cardinal size function.
class card

Definitiondf-card 6752* 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 6753* The cardinality of a well-orderable set is an ordinal. (Contributed by Jim Kingdon, 30-Aug-2021.)
(∃𝑦 ∈ On 𝑦𝐴 → (card‘𝐴) ∈ On)

Theoremisnumi 6754 A set equinumerous to an ordinal is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.)
((𝐴 ∈ On ∧ 𝐴𝐵) → 𝐵 ∈ dom card)

Theoremfinnum 6755 Every finite set is numerable. (Contributed by Mario Carneiro, 4-Feb-2013.) (Revised by Mario Carneiro, 29-Apr-2015.)
(𝐴 ∈ Fin → 𝐴 ∈ dom card)

Theoremonenon 6756 Every ordinal number is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.)
(𝐴 ∈ On → 𝐴 ∈ dom card)

Theoremcardval3ex 6757* The value of (card‘𝐴). (Contributed by Jim Kingdon, 30-Aug-2021.)
(∃𝑥 ∈ On 𝑥𝐴 → (card‘𝐴) = {𝑦 ∈ On ∣ 𝑦𝐴})

Theoremoncardval 6758* 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 6759 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 6760 The cardinality of the empty set is the empty set. (Contributed by NM, 25-Oct-2003.)
(card‘∅) = ∅

Theoremcarden2bex 6761* If two numerable sets are equinumerous, then they have equal cardinalities. (Contributed by Jim Kingdon, 30-Aug-2021.)
((𝐴𝐵 ∧ ∃𝑥 ∈ On 𝑥𝐴) → (card‘𝐴) = (card‘𝐵))

Theorempm54.43 6762 Theorem *54.43 of [WhiteheadRussell] p. 360. (Contributed by NM, 4-Apr-2007.)
((𝐴 ≈ 1𝑜𝐵 ≈ 1𝑜) → ((𝐴𝐵) = ∅ ↔ (𝐴𝐵) ≈ 2𝑜))

Theorempr2nelem 6763 Lemma for pr2ne 6764. (Contributed by FL, 17-Aug-2008.)
((𝐴𝐶𝐵𝐷𝐴𝐵) → {𝐴, 𝐵} ≈ 2𝑜)

Theorempr2ne 6764 If an unordered pair has two elements they are different. (Contributed by FL, 14-Feb-2010.)
((𝐴𝐶𝐵𝐷) → ({𝐴, 𝐵} ≈ 2𝑜𝐴𝐵))

Theoremen2eleq 6765 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.)
((𝑋𝑃𝑃 ≈ 2𝑜) → 𝑃 = {𝑋, (𝑃 ∖ {𝑋})})

Theoremen2other2 6766 Taking the other element twice in a pair gets back to the original element. (Contributed by Stefan O'Rear, 22-Aug-2015.)
((𝑋𝑃𝑃 ≈ 2𝑜) → (𝑃 ∖ { (𝑃 ∖ {𝑋})}) = 𝑋)

Theoremdju1p1e2 6767 Disjoint union version of one plus one equals two. (Contributed by Jim Kingdon, 1-Jul-2022.)
(1𝑜 ⊔ 1𝑜) ≈ 2𝑜

Theoreminfpwfidom 6768 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 6769 Lemma for exmidfodomr 6774. A variant of djur 6701. (Contributed by Jim Kingdon, 2-Jul-2022.)
(𝜑𝐴 ⊆ 1𝑜)    &   (𝜑𝐵 ∈ (𝐴 ⊔ 1𝑜))       (𝜑 → (𝐵 = (inl‘∅) ∨ 𝐵 = (inr‘∅)))

Theoremexmidfodomrlemreseldju 6770 Lemma for exmidfodomrlemrALT 6773. A variant of eldju 6703. (Contributed by Jim Kingdon, 9-Jul-2022.)
(𝜑𝐴 ⊆ 1𝑜)    &   (𝜑𝐵 ∈ (𝐴 ⊔ 1𝑜))       (𝜑 → ((∅ ∈ 𝐴𝐵 = ((inl ↾ 𝐴)‘∅)) ∨ 𝐵 = ((inr ↾ 1𝑜)‘∅)))

Theoremexmidfodomrlemim 6771* 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 6772* 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 6773* 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 6772. In particular, this proof uses eldju 6703 instead of djur 6701 and avoids djulclb 6691. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Jim Kingdon, 9-Jul-2022.)
(∀𝑥𝑦((∃𝑧 𝑧𝑦𝑦𝑥) → ∃𝑓 𝑓:𝑥onto𝑦) → EXMID)

Theoremexmidfodomr 6774* 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𝑦))

PART 3  REAL AND COMPLEX NUMBERS

This section derives the basics of real and complex numbers.

To construct the real numbers constructively, we follow two main sources. The first is Metamath Proof Explorer, which has the advantage of being already formalized in metamath. Its disadvantage, for our purposes, is that it assumes the law of the excluded middle throughout. Since we have already developed natural numbers ( for example, nna0 6189 and similar theorems ), going from there to positive integers (df-ni 6807) and then positive rational numbers (df-nqqs 6851) does not involve a major change in approach compared with the Metamath Proof Explorer.

It is when we proceed to Dedekind cuts that we bring in more material from Section 11.2 of [HoTT], which focuses on the aspects of Dedekind cuts which are different without excluded middle. With excluded middle, it is natural to define the cut as the lower set only (as Metamath Proof Explorer does), but we define the cut as a pair of both the lower and upper sets, as [HoTT] does. There are also differences in how we handle order and replacing "not equal to zero" with "apart from zero".

3.1  Construction and axiomatization of real and complex numbers

3.1.1  Dedekind-cut construction of real and complex numbers

Syntaxcnpi 6775 The set of positive integers, which is the set of natural numbers ω with 0 removed.

Note: This is the start of the Dedekind-cut construction of real and _complex numbers.

class N

Syntaxcpli 6776 Positive integer addition.
class +N

Syntaxcmi 6777 Positive integer multiplication.
class ·N

Syntaxclti 6778 Positive integer ordering relation.
class <N

Syntaxcplpq 6779 Positive pre-fraction addition.
class +pQ

Syntaxcmpq 6780 Positive pre-fraction multiplication.
class ·pQ

Syntaxcltpq 6781 Positive pre-fraction ordering relation.
class <pQ

Syntaxceq 6782 Equivalence class used to construct positive fractions.
class ~Q

Syntaxcnq 6783 Set of positive fractions.
class Q

Syntaxc1q 6784 The positive fraction constant 1.
class 1Q

Syntaxcplq 6785 Positive fraction addition.
class +Q

Syntaxcmq 6786 Positive fraction multiplication.
class ·Q

Syntaxcrq 6787 Positive fraction reciprocal operation.
class *Q

Syntaxcltq 6788 Positive fraction ordering relation.
class <Q

Syntaxceq0 6789 Equivalence class used to construct non-negative fractions.
class ~Q0

Syntaxcnq0 6790 Set of non-negative fractions.
class Q0

Syntaxc0q0 6791 The non-negative fraction constant 0.
class 0Q0

Syntaxcplq0 6792 Non-negative fraction addition.
class +Q0

Syntaxcmq0 6793 Non-negative fraction multiplication.
class ·Q0

Syntaxcnp 6794 Set of positive reals.
class P

Syntaxc1p 6795 Positive real constant 1.
class 1P

Syntaxcpp 6796 Positive real addition.
class +P

Syntaxcmp 6797 Positive real multiplication.
class ·P

Syntaxcltp 6798 Positive real ordering relation.
class <P

Syntaxcer 6799 Equivalence class used to construct signed reals.
class ~R

Syntaxcnr 6800 Set of signed reals.
class R

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-11363
 Copyright terms: Public domain < Previous  Next >