Home | Metamath
Proof Explorer Theorem List (p. 103 of 449) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | cgru 10201 | Extend class notation to include the class of all Grothendieck universes. |
class Univ | ||
Definition | df-gru 10202* | A Grothendieck universe is a set that is closed with respect to all the operations that are common in set theory: pairs, powersets, unions, intersections, Cartesian products etc. Grothendieck and alii, Séminaire de Géométrie Algébrique 4, Exposé I, p. 185. It was designed to give a precise meaning to the concepts of categories of sets, groups... (Contributed by Mario Carneiro, 9-Jun-2013.) |
⊢ Univ = {𝑢 ∣ (Tr 𝑢 ∧ ∀𝑥 ∈ 𝑢 (𝒫 𝑥 ∈ 𝑢 ∧ ∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢 ∧ ∀𝑦 ∈ (𝑢 ↑m 𝑥)∪ ran 𝑦 ∈ 𝑢))} | ||
Theorem | elgrug 10203* | Properties of a Grothendieck universe. (Contributed by Mario Carneiro, 9-Jun-2013.) |
⊢ (𝑈 ∈ 𝑉 → (𝑈 ∈ Univ ↔ (Tr 𝑈 ∧ ∀𝑥 ∈ 𝑈 (𝒫 𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∈ 𝑈 ∧ ∀𝑦 ∈ (𝑈 ↑m 𝑥)∪ ran 𝑦 ∈ 𝑈)))) | ||
Theorem | grutr 10204 | A Grothendieck universe is transitive. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ (𝑈 ∈ Univ → Tr 𝑈) | ||
Theorem | gruelss 10205 | A Grothendieck universe is transitive, so each element is a subset of the universe. (Contributed by Mario Carneiro, 9-Jun-2013.) |
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈) → 𝐴 ⊆ 𝑈) | ||
Theorem | grupw 10206 | A Grothendieck universe contains the powerset of each of its members. (Contributed by Mario Carneiro, 9-Jun-2013.) |
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈) → 𝒫 𝐴 ∈ 𝑈) | ||
Theorem | gruss 10207 | Any subset of an element of a Grothendieck universe is also an element. (Contributed by Mario Carneiro, 9-Jun-2013.) |
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ 𝑈) | ||
Theorem | grupr 10208 | A Grothendieck universe contains pairs derived from its elements. (Contributed by Mario Carneiro, 9-Jun-2013.) |
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈) → {𝐴, 𝐵} ∈ 𝑈) | ||
Theorem | gruurn 10209 | A Grothendieck universe contains the range of any function which takes values in the universe (see gruiun 10210 for a more intuitive version). (Contributed by Mario Carneiro, 9-Jun-2013.) |
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐹:𝐴⟶𝑈) → ∪ ran 𝐹 ∈ 𝑈) | ||
Theorem | gruiun 10210* | If 𝐵(𝑥) is a family of elements of 𝑈 and the index set 𝐴 is an element of 𝑈, then the indexed union ∪ 𝑥 ∈ 𝐴𝐵 is also an element of 𝑈, where 𝑈 is a Grothendieck universe. (Contributed by Mario Carneiro, 9-Jun-2013.) |
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑈) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑈) | ||
Theorem | gruuni 10211 | A Grothendieck universe contains unions of its elements. (Contributed by Mario Carneiro, 17-Jun-2013.) |
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈) → ∪ 𝐴 ∈ 𝑈) | ||
Theorem | grurn 10212 | A Grothendieck universe contains the range of any function which takes values in the universe (see gruiun 10210 for a more intuitive version). (Contributed by Mario Carneiro, 9-Jun-2013.) |
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐹:𝐴⟶𝑈) → ran 𝐹 ∈ 𝑈) | ||
Theorem | gruima 10213 | A Grothendieck universe contains image sets drawn from its members. (Contributed by Mario Carneiro, 9-Jun-2013.) |
⊢ ((𝑈 ∈ Univ ∧ Fun 𝐹 ∧ (𝐹 “ 𝐴) ⊆ 𝑈) → (𝐴 ∈ 𝑈 → (𝐹 “ 𝐴) ∈ 𝑈)) | ||
Theorem | gruel 10214 | Any element of an element of a Grothendieck universe is also an element of the universe. (Contributed by Mario Carneiro, 9-Jun-2013.) |
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ 𝑈) | ||
Theorem | grusn 10215 | A Grothendieck universe contains the singletons of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.) |
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈) → {𝐴} ∈ 𝑈) | ||
Theorem | gruop 10216 | A Grothendieck universe contains ordered pairs of its elements. (Contributed by Mario Carneiro, 10-Jun-2013.) |
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈) → 〈𝐴, 𝐵〉 ∈ 𝑈) | ||
Theorem | gruun 10217 | A Grothendieck universe contains binary unions of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.) |
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈) → (𝐴 ∪ 𝐵) ∈ 𝑈) | ||
Theorem | gruxp 10218 | A Grothendieck universe contains binary cartesian products of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.) |
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈) → (𝐴 × 𝐵) ∈ 𝑈) | ||
Theorem | grumap 10219 | A Grothendieck universe contains all powers of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.) |
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈) → (𝐴 ↑m 𝐵) ∈ 𝑈) | ||
Theorem | gruixp 10220* | A Grothendieck universe contains indexed cartesian products of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.) |
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑈) → X𝑥 ∈ 𝐴 𝐵 ∈ 𝑈) | ||
Theorem | gruiin 10221* | A Grothendieck universe contains indexed intersections of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.) |
⊢ ((𝑈 ∈ Univ ∧ ∃𝑥 ∈ 𝐴 𝐵 ∈ 𝑈) → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑈) | ||
Theorem | gruf 10222 | A Grothendieck universe contains all functions on its elements. (Contributed by Mario Carneiro, 10-Jun-2013.) |
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐹:𝐴⟶𝑈) → 𝐹 ∈ 𝑈) | ||
Theorem | gruen 10223 | A Grothendieck universe contains all subsets of itself that are equipotent to an element of the universe. (Contributed by Mario Carneiro, 9-Jun-2013.) |
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ⊆ 𝑈 ∧ (𝐵 ∈ 𝑈 ∧ 𝐵 ≈ 𝐴)) → 𝐴 ∈ 𝑈) | ||
Theorem | gruwun 10224 | A nonempty Grothendieck universe is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → 𝑈 ∈ WUni) | ||
Theorem | intgru 10225 | The intersection of a family of universes is a universe. (Contributed by Mario Carneiro, 9-Jun-2013.) |
⊢ ((𝐴 ⊆ Univ ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ∈ Univ) | ||
Theorem | ingru 10226* | The intersection of a universe with a class that acts like a universe is another universe. (Contributed by Mario Carneiro, 10-Jun-2013.) |
⊢ ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝒫 𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 {𝑥, 𝑦} ∈ 𝐴 ∧ ∀𝑦(𝑦:𝑥⟶𝐴 → ∪ ran 𝑦 ∈ 𝐴))) → (𝑈 ∈ Univ → (𝑈 ∩ 𝐴) ∈ Univ)) | ||
Theorem | wfgru 10227 | The wellfounded part of a universe is another universe. (Contributed by Mario Carneiro, 17-Jun-2013.) |
⊢ (𝑈 ∈ Univ → (𝑈 ∩ ∪ (𝑅1 “ On)) ∈ Univ) | ||
Theorem | grudomon 10228 | Each ordinal that is comparable with an element of the universe is in the universe. (Contributed by Mario Carneiro, 10-Jun-2013.) |
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ On ∧ (𝐵 ∈ 𝑈 ∧ 𝐴 ≼ 𝐵)) → 𝐴 ∈ 𝑈) | ||
Theorem | gruina 10229 | If a Grothendieck universe 𝑈 is nonempty, then the height of the ordinals in 𝑈 is a strongly inaccessible cardinal. (Contributed by Mario Carneiro, 17-Jun-2013.) |
⊢ 𝐴 = (𝑈 ∩ On) ⇒ ⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → 𝐴 ∈ Inacc) | ||
Theorem | grur1a 10230 | A characterization of Grothendieck universes, part 1. (Contributed by Mario Carneiro, 23-Jun-2013.) |
⊢ 𝐴 = (𝑈 ∩ On) ⇒ ⊢ (𝑈 ∈ Univ → (𝑅1‘𝐴) ⊆ 𝑈) | ||
Theorem | grur1 10231 | A characterization of Grothendieck universes, part 2. (Contributed by Mario Carneiro, 24-Jun-2013.) |
⊢ 𝐴 = (𝑈 ∩ On) ⇒ ⊢ ((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) → 𝑈 = (𝑅1‘𝐴)) | ||
Theorem | grutsk1 10232 | Grothendieck universes are the same as transitive Tarski classes, part one: a transitive Tarski class is a universe. (The hard work is in tskuni 10194.) (Contributed by Mario Carneiro, 17-Jun-2013.) |
⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇) → 𝑇 ∈ Univ) | ||
Theorem | grutsk 10233 | Grothendieck universes are the same as transitive Tarski classes. (The proof in the forward direction requires Foundation.) (Contributed by Mario Carneiro, 24-Jun-2013.) |
⊢ Univ = {𝑥 ∈ Tarski ∣ Tr 𝑥} | ||
Axiom | ax-groth 10234* | The Tarski-Grothendieck Axiom. For every set 𝑥 there is an inaccessible cardinal 𝑦 such that 𝑦 is not in 𝑥. The addition of this axiom to ZFC set theory provides a framework for category theory, thus for all practical purposes giving us a complete foundation for "all of mathematics." This version of the axiom is used by the Mizar project (http://www.mizar.org/JFM/Axiomatics/tarski.html). Unlike the ZFC axioms, this axiom is very long when expressed in terms of primitive symbols - see grothprim 10245. An open problem is finding a shorter equivalent. (Contributed by NM, 18-Mar-2007.) |
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦) ∧ ∃𝑤 ∈ 𝑦 ∀𝑣(𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → (𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦))) | ||
Theorem | axgroth5 10235* | The Tarski-Grothendieck axiom using abbreviations. (Contributed by NM, 22-Jun-2009.) |
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ ∃𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤) ∧ ∀𝑧 ∈ 𝒫 𝑦(𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦)) | ||
Theorem | axgroth2 10236* | Alternate version of the Tarski-Grothendieck Axiom. (Contributed by NM, 18-Mar-2007.) |
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦) ∧ ∃𝑤 ∈ 𝑦 ∀𝑣(𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → (𝑦 ≼ 𝑧 ∨ 𝑧 ∈ 𝑦))) | ||
Theorem | grothpw 10237* | Derive the Axiom of Power Sets ax-pow 5258 from the Tarski-Grothendieck axiom ax-groth 10234. That it follows is mentioned by Bob Solovay at http://www.cs.nyu.edu/pipermail/fom/2008-March/012783.html 10234. Note that ax-pow 5258 is not used by the proof. (Contributed by Gérard Lang, 22-Jun-2009.) (New usage is discouraged.) |
⊢ ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) | ||
Theorem | grothpwex 10238 | Derive the Axiom of Power Sets from the Tarski-Grothendieck axiom ax-groth 10234. Note that ax-pow 5258 is not used by the proof. Use axpweq 5257 to obtain ax-pow 5258. Use pwex 5273 or pwexg 5271 instead. (Contributed by Gérard Lang, 22-Jun-2009.) (New usage is discouraged.) |
⊢ 𝒫 𝑥 ∈ V | ||
Theorem | axgroth6 10239* | The Tarski-Grothendieck axiom using abbreviations. This version is called Tarski's axiom: given a set 𝑥, there exists a set 𝑦 containing 𝑥, the subsets of the members of 𝑦, the power sets of the members of 𝑦, and the subsets of 𝑦 of cardinality less than that of 𝑦. (Contributed by NM, 21-Jun-2009.) |
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ 𝒫 𝑧 ∈ 𝑦) ∧ ∀𝑧 ∈ 𝒫 𝑦(𝑧 ≺ 𝑦 → 𝑧 ∈ 𝑦)) | ||
Theorem | grothomex 10240 | The Tarski-Grothendieck Axiom implies the Axiom of Infinity (in the form of omex 9095). Note that our proof depends on neither the Axiom of Infinity nor Regularity. (Contributed by Mario Carneiro, 19-Apr-2013.) (New usage is discouraged.) |
⊢ ω ∈ V | ||
Theorem | grothac 10241 | The Tarski-Grothendieck Axiom implies the Axiom of Choice (in the form of cardeqv 9880). This can be put in a more conventional form via ween 9450 and dfac8 9550. Note that the mere existence of strongly inaccessible cardinals doesn't imply AC, but rather the particular form of the Tarski-Grothendieck axiom (see http://www.cs.nyu.edu/pipermail/fom/2008-March/012783.html 9550). (Contributed by Mario Carneiro, 19-Apr-2013.) (New usage is discouraged.) |
⊢ dom card = V | ||
Theorem | axgroth3 10242* | Alternate version of the Tarski-Grothendieck Axiom. ax-cc 9846 is used to derive this version. (Contributed by NM, 26-Mar-2007.) |
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦) ∧ ∃𝑤 ∈ 𝑦 ∀𝑣(𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦))) | ||
Theorem | axgroth4 10243* | Alternate version of the Tarski-Grothendieck Axiom. ax-ac 9870 is used to derive this version. (Contributed by NM, 16-Apr-2007.) |
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∃𝑣 ∈ 𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦))) | ||
Theorem | grothprimlem 10244* | Lemma for grothprim 10245. Expand the membership of an unordered pair into primitives. (Contributed by NM, 29-Mar-2007.) |
⊢ ({𝑢, 𝑣} ∈ 𝑤 ↔ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣)))) | ||
Theorem | grothprim 10245* | The Tarski-Grothendieck Axiom ax-groth 10234 expanded into set theory primitives using 163 symbols (allowing the defined symbols ∧, ∨, ↔, and ∃). An open problem is whether a shorter equivalent exists (when expanded to primitives). (Contributed by NM, 16-Apr-2007.) |
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧((𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))) ∧ ∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦)))) | ||
Theorem | grothtsk 10246 | The Tarski-Grothendieck Axiom, using abbreviations. (Contributed by Mario Carneiro, 28-May-2013.) |
⊢ ∪ Tarski = V | ||
Theorem | inaprc 10247 | An equivalent to the Tarski-Grothendieck Axiom: there is a proper class of inaccessible cardinals. (Contributed by Mario Carneiro, 9-Jun-2013.) |
⊢ Inacc ∉ V | ||
Syntax | ctskm 10248 | Extend class definition to include the map whose value is the smallest Tarski class. |
class tarskiMap | ||
Definition | df-tskm 10249* | A function that maps a set 𝑥 to the smallest Tarski class that contains the set. (Contributed by FL, 30-Dec-2010.) |
⊢ tarskiMap = (𝑥 ∈ V ↦ ∩ {𝑦 ∈ Tarski ∣ 𝑥 ∈ 𝑦}) | ||
Theorem | tskmval 10250* | Value of our tarski map. (Contributed by FL, 30-Dec-2010.) (Revised by Mario Carneiro, 20-Sep-2014.) |
⊢ (𝐴 ∈ 𝑉 → (tarskiMap‘𝐴) = ∩ {𝑥 ∈ Tarski ∣ 𝐴 ∈ 𝑥}) | ||
Theorem | tskmid 10251 | The set 𝐴 is an element of the smallest Tarski class that contains 𝐴. CLASSES1 th. 5. (Contributed by FL, 30-Dec-2010.) (Proof shortened by Mario Carneiro, 21-Sep-2014.) |
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ (tarskiMap‘𝐴)) | ||
Theorem | tskmcl 10252 | A Tarski class that contains 𝐴 is a Tarski class. (Contributed by FL, 17-Apr-2011.) (Proof shortened by Mario Carneiro, 21-Sep-2014.) |
⊢ (tarskiMap‘𝐴) ∈ Tarski | ||
Theorem | sstskm 10253* | Being a part of (tarskiMap‘𝐴). (Contributed by FL, 17-Apr-2011.) (Proof shortened by Mario Carneiro, 20-Sep-2014.) |
⊢ (𝐴 ∈ 𝑉 → (𝐵 ⊆ (tarskiMap‘𝐴) ↔ ∀𝑥 ∈ Tarski (𝐴 ∈ 𝑥 → 𝐵 ⊆ 𝑥))) | ||
Theorem | eltskm 10254* | Belonging to (tarskiMap‘𝐴). (Contributed by FL, 17-Apr-2011.) (Proof shortened by Mario Carneiro, 21-Sep-2014.) |
⊢ (𝐴 ∈ 𝑉 → (𝐵 ∈ (tarskiMap‘𝐴) ↔ ∀𝑥 ∈ Tarski (𝐴 ∈ 𝑥 → 𝐵 ∈ 𝑥))) | ||
This section derives the basics of real and complex numbers. We first construct and axiomatize real and complex numbers (e.g., ax-resscn 10583). After that, we derive their basic properties, various operations like addition (df-add 10537) and sine (df-sin 15413), and subsets such as the integers (df-z 11971) and natural numbers (df-nn 11628). | ||
Syntax | cnpi 10255 |
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. The last lemma of the construction is mulcnsrec 10555. The actual set of Dedekind cuts is defined by df-np 10392. |
class N | ||
Syntax | cpli 10256 | Positive integer addition. |
class +N | ||
Syntax | cmi 10257 | Positive integer multiplication. |
class ·N | ||
Syntax | clti 10258 | Positive integer ordering relation. |
class <N | ||
Syntax | cplpq 10259 | Positive pre-fraction addition. |
class +pQ | ||
Syntax | cmpq 10260 | Positive pre-fraction multiplication. |
class ·pQ | ||
Syntax | cltpq 10261 | Positive pre-fraction ordering relation. |
class <pQ | ||
Syntax | ceq 10262 | Equivalence class used to construct positive fractions. |
class ~Q | ||
Syntax | cnq 10263 | Set of positive fractions. |
class Q | ||
Syntax | c1q 10264 | The positive fraction constant 1. |
class 1Q | ||
Syntax | cerq 10265 | Positive fraction equivalence class. |
class [Q] | ||
Syntax | cplq 10266 | Positive fraction addition. |
class +Q | ||
Syntax | cmq 10267 | Positive fraction multiplication. |
class ·Q | ||
Syntax | crq 10268 | Positive fraction reciprocal operation. |
class *Q | ||
Syntax | cltq 10269 | Positive fraction ordering relation. |
class <Q | ||
Syntax | cnp 10270 | Set of positive reals. |
class P | ||
Syntax | c1p 10271 | Positive real constant 1. |
class 1P | ||
Syntax | cpp 10272 | Positive real addition. |
class +P | ||
Syntax | cmp 10273 | Positive real multiplication. |
class ·P | ||
Syntax | cltp 10274 | Positive real ordering relation. |
class <P | ||
Syntax | cer 10275 | Equivalence class used to construct signed reals. |
class ~R | ||
Syntax | cnr 10276 | Set of signed reals. |
class R | ||
Syntax | c0r 10277 | The signed real constant 0. |
class 0R | ||
Syntax | c1r 10278 | The signed real constant 1. |
class 1R | ||
Syntax | cm1r 10279 | The signed real constant -1. |
class -1R | ||
Syntax | cplr 10280 | Signed real addition. |
class +R | ||
Syntax | cmr 10281 | Signed real multiplication. |
class ·R | ||
Syntax | cltr 10282 | Signed real ordering relation. |
class <R | ||
Definition | df-ni 10283 | Define the class of positive integers. This is a "temporary" set used in the construction of complex numbers df-c 10532, and is intended to be used only by the construction. (Contributed by NM, 15-Aug-1995.) (New usage is discouraged.) |
⊢ N = (ω ∖ {∅}) | ||
Definition | df-pli 10284 | Define addition on positive integers. This is a "temporary" set used in the construction of complex numbers df-c 10532, and is intended to be used only by the construction. (Contributed by NM, 26-Aug-1995.) (New usage is discouraged.) |
⊢ +N = ( +o ↾ (N × N)) | ||
Definition | df-mi 10285 | Define multiplication on positive integers. This is a "temporary" set used in the construction of complex numbers df-c 10532, and is intended to be used only by the construction. (Contributed by NM, 26-Aug-1995.) (New usage is discouraged.) |
⊢ ·N = ( ·o ↾ (N × N)) | ||
Definition | df-lti 10286 | Define 'less than' on positive integers. This is a "temporary" set used in the construction of complex numbers df-c 10532, and is intended to be used only by the construction. (Contributed by NM, 6-Feb-1996.) (New usage is discouraged.) |
⊢ <N = ( E ∩ (N × N)) | ||
Theorem | elni 10287 | Membership in the class of positive integers. (Contributed by NM, 15-Aug-1995.) (New usage is discouraged.) |
⊢ (𝐴 ∈ N ↔ (𝐴 ∈ ω ∧ 𝐴 ≠ ∅)) | ||
Theorem | elni2 10288 | Membership in the class of positive integers. (Contributed by NM, 27-Nov-1995.) (New usage is discouraged.) |
⊢ (𝐴 ∈ N ↔ (𝐴 ∈ ω ∧ ∅ ∈ 𝐴)) | ||
Theorem | pinn 10289 | A positive integer is a natural number. (Contributed by NM, 15-Aug-1995.) (New usage is discouraged.) |
⊢ (𝐴 ∈ N → 𝐴 ∈ ω) | ||
Theorem | pion 10290 | A positive integer is an ordinal number. (Contributed by NM, 23-Mar-1996.) (New usage is discouraged.) |
⊢ (𝐴 ∈ N → 𝐴 ∈ On) | ||
Theorem | piord 10291 | A positive integer is ordinal. (Contributed by NM, 29-Jan-1996.) (New usage is discouraged.) |
⊢ (𝐴 ∈ N → Ord 𝐴) | ||
Theorem | niex 10292 | The class of positive integers is a set. (Contributed by NM, 15-Aug-1995.) (New usage is discouraged.) |
⊢ N ∈ V | ||
Theorem | 0npi 10293 | The empty set is not a positive integer. (Contributed by NM, 26-Aug-1995.) (New usage is discouraged.) |
⊢ ¬ ∅ ∈ N | ||
Theorem | 1pi 10294 | Ordinal 'one' is a positive integer. (Contributed by NM, 29-Oct-1995.) (New usage is discouraged.) |
⊢ 1o ∈ N | ||
Theorem | addpiord 10295 | Positive integer addition in terms of ordinal addition. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 +N 𝐵) = (𝐴 +o 𝐵)) | ||
Theorem | mulpiord 10296 | Positive integer multiplication in terms of ordinal multiplication. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 ·N 𝐵) = (𝐴 ·o 𝐵)) | ||
Theorem | mulidpi 10297 | 1 is an identity element for multiplication on positive integers. (Contributed by NM, 4-Mar-1996.) (Revised by Mario Carneiro, 17-Nov-2014.) (New usage is discouraged.) |
⊢ (𝐴 ∈ N → (𝐴 ·N 1o) = 𝐴) | ||
Theorem | ltpiord 10298 | Positive integer 'less than' in terms of ordinal membership. (Contributed by NM, 6-Feb-1996.) (Revised by Mario Carneiro, 28-Apr-2015.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 <N 𝐵 ↔ 𝐴 ∈ 𝐵)) | ||
Theorem | ltsopi 10299 | Positive integer 'less than' is a strict ordering. (Contributed by NM, 8-Feb-1996.) (Proof shortened by Mario Carneiro, 10-Jul-2014.) (New usage is discouraged.) |
⊢ <N Or N | ||
Theorem | ltrelpi 10300 | Positive integer 'less than' is a relation on positive integers. (Contributed by NM, 8-Feb-1996.) (New usage is discouraged.) |
⊢ <N ⊆ (N × N) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |