Home | Intuitionistic Logic Explorer Theorem 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 |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | djur 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‘𝑥))) | ||
Theorem | djuunr 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 ↾ 𝐵)) = (𝐴 ⊔ 𝐵) | ||
Theorem | eldju 6703* | Element of a disjoint union. (Contributed by BJ and Jim Kingdon, 23-Jun-2022.) |
⊢ (𝐶 ∈ (𝐴 ⊔ 𝐵) ↔ (∃𝑥 ∈ 𝐴 𝐶 = ((inl ↾ 𝐴)‘𝑥) ∨ ∃𝑥 ∈ 𝐵 𝐶 = ((inr ↾ 𝐵)‘𝑥))) | ||
Theorem | djuun 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 “ 𝐵)) = (𝐴 ⊔ 𝐵) | ||
Theorem | djuss 6705 | A disjoint union is a subset of a Cartesian product. (Contributed by AV, 25-Jun-2022.) |
⊢ (𝐴 ⊔ 𝐵) ⊆ ({∅, 1_{𝑜}} × (𝐴 ∪ 𝐵)) | ||
Theorem | eldju1st 6706 | The first component of an element of a disjoint union is either ∅ or 1_{𝑜}. (Contributed by AV, 26-Jun-2022.) |
⊢ (𝑋 ∈ (𝐴 ⊔ 𝐵) → ((1^{st} ‘𝑋) = ∅ ∨ (1^{st} ‘𝑋) = 1_{𝑜})) | ||
Theorem | eldju2ndl 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.) |
⊢ ((𝑋 ∈ (𝐴 ⊔ 𝐵) ∧ (1^{st} ‘𝑋) = ∅) → (2^{nd} ‘𝑋) ∈ 𝐴) | ||
Theorem | eldju2ndr 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.) |
⊢ ((𝑋 ∈ (𝐴 ⊔ 𝐵) ∧ (1^{st} ‘𝑋) ≠ ∅) → (2^{nd} ‘𝑋) ∈ 𝐵) | ||
Theorem | 1stinl 6709 | The first component of the value of a left injection is the empty set. (Contributed by AV, 27-Jun-2022.) |
⊢ (𝑋 ∈ 𝑉 → (1^{st} ‘(inl‘𝑋)) = ∅) | ||
Theorem | 2ndinl 6710 | The second component of the value of a left injection is its argument. (Contributed by AV, 27-Jun-2022.) |
⊢ (𝑋 ∈ 𝑉 → (2^{nd} ‘(inl‘𝑋)) = 𝑋) | ||
Theorem | 1stinr 6711 | The first component of the value of a right injection is 1_{𝑜}. (Contributed by AV, 27-Jun-2022.) |
⊢ (𝑋 ∈ 𝑉 → (1^{st} ‘(inr‘𝑋)) = 1_{𝑜}) | ||
Theorem | 2ndinr 6712 | The second component of the value of a right injection is its argument. (Contributed by AV, 27-Jun-2022.) |
⊢ (𝑋 ∈ 𝑉 → (2^{nd} ‘(inr‘𝑋)) = 𝑋) | ||
Theorem | djune 6713 | Left and right injection never produce equal values. (Contributed by Jim Kingdon, 2-Jul-2022.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (inl‘𝐴) ≠ (inr‘𝐵)) | ||
Theorem | updjudhf 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((1^{st} ‘𝑥) = ∅, (𝐹‘(2^{nd} ‘𝑥)), (𝐺‘(2^{nd} ‘𝑥)))) ⇒ ⊢ (𝜑 → 𝐻:(𝐴 ⊔ 𝐵)⟶𝐶) | ||
Theorem | updjudhcoinlf 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((1^{st} ‘𝑥) = ∅, (𝐹‘(2^{nd} ‘𝑥)), (𝐺‘(2^{nd} ‘𝑥)))) ⇒ ⊢ (𝜑 → (𝐻 ∘ (inl ↾ 𝐴)) = 𝐹) | ||
Theorem | updjudhcoinrg 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((1^{st} ‘𝑥) = ∅, (𝐹‘(2^{nd} ‘𝑥)), (𝐺‘(2^{nd} ‘𝑥)))) ⇒ ⊢ (𝜑 → (𝐻 ∘ (inr ↾ 𝐵)) = 𝐺) | ||
Theorem | updjud 6717* | Universal property of the disjoint union. (Proposed by BJ, 25-Jun-2022.) (Contributed by AV, 28-Jun-2022.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐶) & ⊢ (𝜑 → 𝐺:𝐵⟶𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → ∃!ℎ(ℎ:(𝐴 ⊔ 𝐵)⟶𝐶 ∧ (ℎ ∘ (inl ↾ 𝐴)) = 𝐹 ∧ (ℎ ∘ (inr ↾ 𝐵)) = 𝐺)) | ||
Syntax | cdjucase 6718 | Syntax for the "case" construction. |
class case(𝑅, 𝑆) | ||
Definition | df-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)) | ||
Theorem | casefun 6720 | The "case" construction of two functions is a function. (Contributed by BJ, 10-Jul-2022.) |
⊢ (𝜑 → Fun 𝐹) & ⊢ (𝜑 → Fun 𝐺) ⇒ ⊢ (𝜑 → Fun case(𝐹, 𝐺)) | ||
Theorem | casedm 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 𝐺) | ||
Theorem | caserel 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 𝑆)) | ||
Theorem | casef 6723 | The "case" construction of two functions is a function on the disjoint union of their domains. (Contributed by BJ, 10-Jul-2022.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝑋) & ⊢ (𝜑 → 𝐺:𝐵⟶𝑋) ⇒ ⊢ (𝜑 → case(𝐹, 𝐺):(𝐴 ⊔ 𝐵)⟶𝑋) | ||
Theorem | caseinj 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(𝑅, 𝑆)) | ||
Theorem | casef1 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→𝑋) | ||
Syntax | cdjud 6726 | Syntax for the domain-disjoint-union of two relations. |
class (𝑅 ⊔_{d} 𝑆) | ||
Definition | df-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 𝑆))) | ||
Theorem | djufun 6728 | The "domain-disjoint-union" of two functions is a function. (Contributed by BJ, 10-Jul-2022.) |
⊢ (𝜑 → Fun 𝐹) & ⊢ (𝜑 → Fun 𝐺) ⇒ ⊢ (𝜑 → Fun (𝐹 ⊔_{d} 𝐺)) | ||
Theorem | djudm 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 𝐺) | ||
Theorem | djuinj 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} 𝑆)) | ||
Theorem | djudom 6731 | Dominance law for disjoint union. (Contributed by Jim Kingdon, 25-Jul-2022.) |
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐶 ≼ 𝐷) → (𝐴 ⊔ 𝐶) ≼ (𝐵 ⊔ 𝐷)) | ||
Syntax | comni 6732 | Extend class definition to include the class of omniscient sets. |
class Omni | ||
Syntax | xnninf 6733 | Set of nonincreasing sequences in 2_{𝑜} ↑_{𝑚} ω. |
class ℕ_{∞} | ||
Definition | df-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_{𝑜}))} | ||
Definition | df-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 𝑖) ⊆ (𝑓‘𝑖)} | ||
Theorem | isomni 6736* | The predicate of being omniscient. (Contributed by Jim Kingdon, 28-Jun-2022.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Omni ↔ ∀𝑓(𝑓:𝐴⟶2_{𝑜} → (∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1_{𝑜})))) | ||
Theorem | isomnimap 6737* | The predicate of being omniscient stated in terms of set exponentiation. (Contributed by Jim Kingdon, 13-Jul-2022.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Omni ↔ ∀𝑓 ∈ (2_{𝑜} ↑_{𝑚} 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1_{𝑜}))) | ||
Theorem | enomnilem 6738 | Lemma for enomni 6739. One direction of the biconditional. (Contributed by Jim Kingdon, 13-Jul-2022.) |
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ Omni → 𝐵 ∈ Omni)) | ||
Theorem | enomni 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)) | ||
Theorem | finomni 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) | ||
Theorem | exmidomniim 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) | ||
Theorem | exmidomni 6742 | Excluded middle is equivalent to every set being omniscient. (Contributed by BJ and Jim Kingdon, 30-Jun-2022.) |
⊢ (EXMID ↔ ∀𝑥 𝑥 ∈ Omni) | ||
Theorem | fodjuomnilemdc 6743* | Lemma for fodjuomni 6748. Decidability of a condition we use in various lemmas. (Contributed by Jim Kingdon, 27-Jul-2022.) |
⊢ (𝜑 → 𝐹:𝑂–onto→(𝐴 ⊔ 𝐵)) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑂) → DECID ∃𝑧 ∈ 𝐴 (𝐹‘𝑋) = (inl‘𝑧)) | ||
Theorem | fodjuomnilemf 6744* | Lemma for fodjuomni 6748. Domain and range of 𝑃. (Contributed by Jim Kingdon, 27-Jul-2022.) |
⊢ (𝜑 → 𝑂 ∈ Omni) & ⊢ (𝜑 → 𝐹:𝑂–onto→(𝐴 ⊔ 𝐵)) & ⊢ 𝑃 = (𝑦 ∈ 𝑂 ↦ if(∃𝑧 ∈ 𝐴 (𝐹‘𝑦) = (inl‘𝑧), ∅, 1_{𝑜})) ⇒ ⊢ (𝜑 → 𝑃 ∈ (2_{𝑜} ↑_{𝑚} 𝑂)) | ||
Theorem | fodjuomnilemm 6745* | Lemma for fodjuomni 6748. The case where A is inhabited. (Contributed by Jim Kingdon, 27-Jul-2022.) |
⊢ (𝜑 → 𝑂 ∈ Omni) & ⊢ (𝜑 → 𝐹:𝑂–onto→(𝐴 ⊔ 𝐵)) & ⊢ 𝑃 = (𝑦 ∈ 𝑂 ↦ if(∃𝑧 ∈ 𝐴 (𝐹‘𝑦) = (inl‘𝑧), ∅, 1_{𝑜})) & ⊢ (𝜑 → ∃𝑤 ∈ 𝑂 (𝑃‘𝑤) = ∅) ⇒ ⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴) | ||
Theorem | fodjuomnilem0 6746* | Lemma for fodjuomni 6748. The case where A is empty. (Contributed by Jim Kingdon, 27-Jul-2022.) |
⊢ (𝜑 → 𝑂 ∈ Omni) & ⊢ (𝜑 → 𝐹:𝑂–onto→(𝐴 ⊔ 𝐵)) & ⊢ 𝑃 = (𝑦 ∈ 𝑂 ↦ if(∃𝑧 ∈ 𝐴 (𝐹‘𝑦) = (inl‘𝑧), ∅, 1_{𝑜})) & ⊢ (𝜑 → ∀𝑤 ∈ 𝑂 (𝑃‘𝑤) = 1_{𝑜}) ⇒ ⊢ (𝜑 → 𝐴 = ∅) | ||
Theorem | fodjuomnilemres 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_{𝑜})) ⇒ ⊢ (𝜑 → (∃𝑥 𝑥 ∈ 𝐴 ∨ 𝐴 = ∅)) | ||
Theorem | fodjuomni 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→(𝐴 ⊔ 𝐵)) ⇒ ⊢ (𝜑 → (∃𝑥 𝑥 ∈ 𝐴 ∨ 𝐴 = ∅)) | ||
Theorem | infnninf 6749 | The point at infinity in ℕ_{∞} (the constant sequence equal to 1_{𝑜}). (Contributed by Jim Kingdon, 14-Jul-2022.) |
⊢ (ω × {1_{𝑜}}) ∈ ℕ_{∞} | ||
Theorem | nnnninf 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_{𝑜}, ∅)) ∈ ℕ_{∞}) | ||
Syntax | ccrd 6751 | Extend class definition to include the cardinal size function. |
class card | ||
Definition | df-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 ∣ 𝑦 ≈ 𝑥}) | ||
Theorem | cardcl 6753* | The cardinality of a well-orderable set is an ordinal. (Contributed by Jim Kingdon, 30-Aug-2021.) |
⊢ (∃𝑦 ∈ On 𝑦 ≈ 𝐴 → (card‘𝐴) ∈ On) | ||
Theorem | isnumi 6754 | A set equinumerous to an ordinal is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.) |
⊢ ((𝐴 ∈ On ∧ 𝐴 ≈ 𝐵) → 𝐵 ∈ dom card) | ||
Theorem | finnum 6755 | Every finite set is numerable. (Contributed by Mario Carneiro, 4-Feb-2013.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ (𝐴 ∈ Fin → 𝐴 ∈ dom card) | ||
Theorem | onenon 6756 | Every ordinal number is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.) |
⊢ (𝐴 ∈ On → 𝐴 ∈ dom card) | ||
Theorem | cardval3ex 6757* | The value of (card‘𝐴). (Contributed by Jim Kingdon, 30-Aug-2021.) |
⊢ (∃𝑥 ∈ On 𝑥 ≈ 𝐴 → (card‘𝐴) = ∩ {𝑦 ∈ On ∣ 𝑦 ≈ 𝐴}) | ||
Theorem | oncardval 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 ∣ 𝑥 ≈ 𝐴}) | ||
Theorem | cardonle 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‘𝐴) ⊆ 𝐴) | ||
Theorem | card0 6760 | The cardinality of the empty set is the empty set. (Contributed by NM, 25-Oct-2003.) |
⊢ (card‘∅) = ∅ | ||
Theorem | carden2bex 6761* | If two numerable sets are equinumerous, then they have equal cardinalities. (Contributed by Jim Kingdon, 30-Aug-2021.) |
⊢ ((𝐴 ≈ 𝐵 ∧ ∃𝑥 ∈ On 𝑥 ≈ 𝐴) → (card‘𝐴) = (card‘𝐵)) | ||
Theorem | pm54.43 6762 | Theorem *54.43 of [WhiteheadRussell] p. 360. (Contributed by NM, 4-Apr-2007.) |
⊢ ((𝐴 ≈ 1_{𝑜} ∧ 𝐵 ≈ 1_{𝑜}) → ((𝐴 ∩ 𝐵) = ∅ ↔ (𝐴 ∪ 𝐵) ≈ 2_{𝑜})) | ||
Theorem | pr2nelem 6763 | Lemma for pr2ne 6764. (Contributed by FL, 17-Aug-2008.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵) → {𝐴, 𝐵} ≈ 2_{𝑜}) | ||
Theorem | pr2ne 6764 | If an unordered pair has two elements they are different. (Contributed by FL, 14-Feb-2010.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ({𝐴, 𝐵} ≈ 2_{𝑜} ↔ 𝐴 ≠ 𝐵)) | ||
Theorem | en2eleq 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_{𝑜}) → 𝑃 = {𝑋, ∪ (𝑃 ∖ {𝑋})}) | ||
Theorem | en2other2 6766 | Taking the other element twice in a pair gets back to the original element. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2_{𝑜}) → ∪ (𝑃 ∖ {∪ (𝑃 ∖ {𝑋})}) = 𝑋) | ||
Theorem | dju1p1e2 6767 | Disjoint union version of one plus one equals two. (Contributed by Jim Kingdon, 1-Jul-2022.) |
⊢ (1_{𝑜} ⊔ 1_{𝑜}) ≈ 2_{𝑜} | ||
Theorem | infpwfidom 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)) | ||
Theorem | exmidfodomrlemeldju 6769 | Lemma for exmidfodomr 6774. A variant of djur 6701. (Contributed by Jim Kingdon, 2-Jul-2022.) |
⊢ (𝜑 → 𝐴 ⊆ 1_{𝑜}) & ⊢ (𝜑 → 𝐵 ∈ (𝐴 ⊔ 1_{𝑜})) ⇒ ⊢ (𝜑 → (𝐵 = (inl‘∅) ∨ 𝐵 = (inr‘∅))) | ||
Theorem | exmidfodomrlemreseldju 6770 | Lemma for exmidfodomrlemrALT 6773. A variant of eldju 6703. (Contributed by Jim Kingdon, 9-Jul-2022.) |
⊢ (𝜑 → 𝐴 ⊆ 1_{𝑜}) & ⊢ (𝜑 → 𝐵 ∈ (𝐴 ⊔ 1_{𝑜})) ⇒ ⊢ (𝜑 → ((∅ ∈ 𝐴 ∧ 𝐵 = ((inl ↾ 𝐴)‘∅)) ∨ 𝐵 = ((inr ↾ 1_{𝑜})‘∅))) | ||
Theorem | exmidfodomrlemim 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→𝑦)) | ||
Theorem | exmidfodomrlemr 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) | ||
Theorem | exmidfodomrlemrALT 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) | ||
Theorem | exmidfodomr 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→𝑦)) | ||
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". | ||
Syntax | cnpi 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 | ||
Syntax | cpli 6776 | Positive integer addition. |
class +_{N} | ||
Syntax | cmi 6777 | Positive integer multiplication. |
class ·_{N} | ||
Syntax | clti 6778 | Positive integer ordering relation. |
class <_{N} | ||
Syntax | cplpq 6779 | Positive pre-fraction addition. |
class +_{pQ} | ||
Syntax | cmpq 6780 | Positive pre-fraction multiplication. |
class ·_{pQ} | ||
Syntax | cltpq 6781 | Positive pre-fraction ordering relation. |
class <_{pQ} | ||
Syntax | ceq 6782 | Equivalence class used to construct positive fractions. |
class ~_{Q} | ||
Syntax | cnq 6783 | Set of positive fractions. |
class Q | ||
Syntax | c1q 6784 | The positive fraction constant 1. |
class 1_{Q} | ||
Syntax | cplq 6785 | Positive fraction addition. |
class +_{Q} | ||
Syntax | cmq 6786 | Positive fraction multiplication. |
class ·_{Q} | ||
Syntax | crq 6787 | Positive fraction reciprocal operation. |
class *_{Q} | ||
Syntax | cltq 6788 | Positive fraction ordering relation. |
class <_{Q} | ||
Syntax | ceq0 6789 | Equivalence class used to construct non-negative fractions. |
class ~_{Q0} | ||
Syntax | cnq0 6790 | Set of non-negative fractions. |
class Q_{0} | ||
Syntax | c0q0 6791 | The non-negative fraction constant 0. |
class 0_{Q0} | ||
Syntax | cplq0 6792 | Non-negative fraction addition. |
class +_{Q0} | ||
Syntax | cmq0 6793 | Non-negative fraction multiplication. |
class ·_{Q0} | ||
Syntax | cnp 6794 | Set of positive reals. |
class P | ||
Syntax | c1p 6795 | Positive real constant 1. |
class 1_{P} | ||
Syntax | cpp 6796 | Positive real addition. |
class +_{P} | ||
Syntax | cmp 6797 | Positive real multiplication. |
class ·_{P} | ||
Syntax | cltp 6798 | Positive real ordering relation. |
class <_{P} | ||
Syntax | cer 6799 | Equivalence class used to construct signed reals. |
class ~_{R} | ||
Syntax | cnr 6800 | Set of signed reals. |
class R |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |