Home | Metamath
Proof Explorer Theorem List (p. 97 of 426) | < 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-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | r1omtsk 9601 | The set of hereditarily finite sets is a Tarski class. (The Tarski-Grothendieck Axiom is not needed for this theorem.) (Contributed by Mario Carneiro, 28-May-2013.) |
⊢ (𝑅1‘ω) ∈ Tarski | ||
Theorem | tskord 9602 | A Tarski class contains all ordinals smaller than it. (Contributed by Mario Carneiro, 8-Jun-2013.) |
⊢ ((𝑇 ∈ Tarski ∧ 𝐴 ∈ On ∧ 𝐴 ≺ 𝑇) → 𝐴 ∈ 𝑇) | ||
Theorem | tskcard 9603 | An even more direct relationship than r1tskina 9604 to get an inaccessible cardinal out of a Tarski class: the size of any nonempty Tarski class is an inaccessible cardinal. (Contributed by Mario Carneiro, 9-Jun-2013.) |
⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) → (card‘𝑇) ∈ Inacc) | ||
Theorem | r1tskina 9604 | There is a direct relationship between transitive Tarski classes and inaccessible cardinals: the Tarski classes that occur in the cumulative hierarchy are exactly at the strongly inaccessible cardinals. (Contributed by Mario Carneiro, 8-Jun-2013.) |
⊢ (𝐴 ∈ On → ((𝑅1‘𝐴) ∈ Tarski ↔ (𝐴 = ∅ ∨ 𝐴 ∈ Inacc))) | ||
Theorem | tskuni 9605 | The union of an element of a transitive Tarski class is in the set. (Contributed by Mario Carneiro, 22-Jun-2013.) |
⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) → ∪ 𝐴 ∈ 𝑇) | ||
Theorem | tskwun 9606 | A nonempty transitive Tarski class is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝑇 ≠ ∅) → 𝑇 ∈ WUni) | ||
Theorem | tskint 9607 | The intersection of an element of a transitive Tarski class is an element of the class. (Contributed by FL, 17-Apr-2011.) (Revised by Mario Carneiro, 20-Sep-2014.) |
⊢ (((𝑇 ∈ Tarski ∧ Tr 𝑇) ∧ 𝐴 ∈ 𝑇 ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ∈ 𝑇) | ||
Theorem | tskun 9608 | The union of two elements of a transitive Tarski class is in the set. (Contributed by Mario Carneiro, 20-Sep-2014.) |
⊢ (((𝑇 ∈ Tarski ∧ Tr 𝑇) ∧ 𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑇) → (𝐴 ∪ 𝐵) ∈ 𝑇) | ||
Theorem | tskxp 9609 | The Cartesian product of two elements of a transitive Tarski class is an element of the class. JFM CLASSES2 th. 67 (partly). (Contributed by FL, 15-Apr-2011.) (Proof shortened by Mario Carneiro, 20-Sep-2014.) |
⊢ (((𝑇 ∈ Tarski ∧ Tr 𝑇) ∧ 𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑇) → (𝐴 × 𝐵) ∈ 𝑇) | ||
Theorem | tskmap 9610 | Set exponentiation is an element of a transitive Tarski class. JFM CLASSES2 th. 67 (partly). (Contributed by FL, 15-Apr-2011.) (Proof shortened by Mario Carneiro, 20-Sep-2014.) |
⊢ (((𝑇 ∈ Tarski ∧ Tr 𝑇) ∧ 𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑇) → (𝐴 ↑𝑚 𝐵) ∈ 𝑇) | ||
Theorem | tskurn 9611 | A transitive Tarski class is closed under small unions. (Contributed by Mario Carneiro, 22-Jun-2013.) |
⊢ (((𝑇 ∈ Tarski ∧ Tr 𝑇) ∧ 𝐴 ∈ 𝑇 ∧ 𝐹:𝐴⟶𝑇) → ∪ ran 𝐹 ∈ 𝑇) | ||
Syntax | cgru 9612 | Extend class notation to include the class of all Grothendieck universes. |
class Univ | ||
Definition | df-gru 9613* | 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 𝑢 ∧ ∀𝑥 ∈ 𝑢 (𝒫 𝑥 ∈ 𝑢 ∧ ∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢 ∧ ∀𝑦 ∈ (𝑢 ↑𝑚 𝑥)∪ ran 𝑦 ∈ 𝑢))} | ||
Theorem | elgrug 9614* | Properties of a Grothendieck universe. (Contributed by Mario Carneiro, 9-Jun-2013.) |
⊢ (𝑈 ∈ 𝑉 → (𝑈 ∈ Univ ↔ (Tr 𝑈 ∧ ∀𝑥 ∈ 𝑈 (𝒫 𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∈ 𝑈 ∧ ∀𝑦 ∈ (𝑈 ↑𝑚 𝑥)∪ ran 𝑦 ∈ 𝑈)))) | ||
Theorem | grutr 9615 | A Grothendieck universe is transitive. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ (𝑈 ∈ Univ → Tr 𝑈) | ||
Theorem | gruelss 9616 | A Grothendieck universe is transitive, so each element is a subset of the universe. (Contributed by Mario Carneiro, 9-Jun-2013.) |
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈) → 𝐴 ⊆ 𝑈) | ||
Theorem | grupw 9617 | A Grothendieck universe contains the powerset of each of its members. (Contributed by Mario Carneiro, 9-Jun-2013.) |
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈) → 𝒫 𝐴 ∈ 𝑈) | ||
Theorem | gruss 9618 | Any subset of an element of a Grothendieck universe is also an element. (Contributed by Mario Carneiro, 9-Jun-2013.) |
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ 𝑈) | ||
Theorem | grupr 9619 | A Grothendieck universe contains pairs derived from its elements. (Contributed by Mario Carneiro, 9-Jun-2013.) |
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈) → {𝐴, 𝐵} ∈ 𝑈) | ||
Theorem | gruurn 9620 | A Grothendieck universe contains the range of any function which takes values in the universe (see gruiun 9621 for a more intuitive version). (Contributed by Mario Carneiro, 9-Jun-2013.) |
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐹:𝐴⟶𝑈) → ∪ ran 𝐹 ∈ 𝑈) | ||
Theorem | gruiun 9621* | 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 9622 | A Grothendieck universe contains unions of its elements. (Contributed by Mario Carneiro, 17-Jun-2013.) |
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈) → ∪ 𝐴 ∈ 𝑈) | ||
Theorem | grurn 9623 | A Grothendieck universe contains the range of any function which takes values in the universe (see gruiun 9621 for a more intuitive version). (Contributed by Mario Carneiro, 9-Jun-2013.) |
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐹:𝐴⟶𝑈) → ran 𝐹 ∈ 𝑈) | ||
Theorem | gruima 9624 | A Grothendieck universe contains image sets drawn from its members. (Contributed by Mario Carneiro, 9-Jun-2013.) |
⊢ ((𝑈 ∈ Univ ∧ Fun 𝐹 ∧ (𝐹 “ 𝐴) ⊆ 𝑈) → (𝐴 ∈ 𝑈 → (𝐹 “ 𝐴) ∈ 𝑈)) | ||
Theorem | gruel 9625 | 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 9626 | A Grothendieck universe contains the singletons of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.) |
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈) → {𝐴} ∈ 𝑈) | ||
Theorem | gruop 9627 | A Grothendieck universe contains ordered pairs of its elements. (Contributed by Mario Carneiro, 10-Jun-2013.) |
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈) → 〈𝐴, 𝐵〉 ∈ 𝑈) | ||
Theorem | gruun 9628 | A Grothendieck universe contains binary unions of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.) |
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈) → (𝐴 ∪ 𝐵) ∈ 𝑈) | ||
Theorem | gruxp 9629 | A Grothendieck universe contains binary cartesian products of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.) |
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈) → (𝐴 × 𝐵) ∈ 𝑈) | ||
Theorem | grumap 9630 | A Grothendieck universe contains all powers of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.) |
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈) → (𝐴 ↑𝑚 𝐵) ∈ 𝑈) | ||
Theorem | gruixp 9631* | A Grothendieck universe contains indexed cartesian products of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.) |
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑈) → X𝑥 ∈ 𝐴 𝐵 ∈ 𝑈) | ||
Theorem | gruiin 9632* | A Grothendieck universe contains indexed intersections of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.) |
⊢ ((𝑈 ∈ Univ ∧ ∃𝑥 ∈ 𝐴 𝐵 ∈ 𝑈) → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑈) | ||
Theorem | gruf 9633 | A Grothendieck universe contains all functions on its elements. (Contributed by Mario Carneiro, 10-Jun-2013.) |
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐹:𝐴⟶𝑈) → 𝐹 ∈ 𝑈) | ||
Theorem | gruen 9634 | 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 9635 | A nonempty Grothendieck universe is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → 𝑈 ∈ WUni) | ||
Theorem | intgru 9636 | The intersection of a family of universes is a universe. (Contributed by Mario Carneiro, 9-Jun-2013.) |
⊢ ((𝐴 ⊆ Univ ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ∈ Univ) | ||
Theorem | ingru 9637* | 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 9638 | The wellfounded part of a universe is another universe. (Contributed by Mario Carneiro, 17-Jun-2013.) |
⊢ (𝑈 ∈ Univ → (𝑈 ∩ ∪ (𝑅1 “ On)) ∈ Univ) | ||
Theorem | grudomon 9639 | 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 9640 | 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 9641 | A characterization of Grothendieck universes, part 1. (Contributed by Mario Carneiro, 23-Jun-2013.) |
⊢ 𝐴 = (𝑈 ∩ On) ⇒ ⊢ (𝑈 ∈ Univ → (𝑅1‘𝐴) ⊆ 𝑈) | ||
Theorem | grur1 9642 | A characterization of Grothendieck universes, part 2. (Contributed by Mario Carneiro, 24-Jun-2013.) |
⊢ 𝐴 = (𝑈 ∩ On) ⇒ ⊢ ((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) → 𝑈 = (𝑅1‘𝐴)) | ||
Theorem | grutsk1 9643 | Grothendieck universes are the same as transitive Tarski classes, part one: a transitive Tarski class is a universe. (The hard work is in tskuni 9605.) (Contributed by Mario Carneiro, 17-Jun-2013.) |
⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇) → 𝑇 ∈ Univ) | ||
Theorem | grutsk 9644 | 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 9645* | 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 9656. An open problem is finding a shorter equivalent. (Contributed by NM, 18-Mar-2007.) |
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦) ∧ ∃𝑤 ∈ 𝑦 ∀𝑣(𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → (𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦))) | ||
Theorem | axgroth5 9646* | The Tarski-Grothendieck axiom using abbreviations. (Contributed by NM, 22-Jun-2009.) |
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ ∃𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤) ∧ ∀𝑧 ∈ 𝒫 𝑦(𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦)) | ||
Theorem | axgroth2 9647* | Alternate version of the Tarski-Grothendieck Axiom. (Contributed by NM, 18-Mar-2007.) |
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦) ∧ ∃𝑤 ∈ 𝑦 ∀𝑣(𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → (𝑦 ≼ 𝑧 ∨ 𝑧 ∈ 𝑦))) | ||
Theorem | grothpw 9648* | Derive the Axiom of Power Sets ax-pow 4843 from the Tarski-Grothendieck axiom ax-groth 9645. That it follows is mentioned by Bob Solovay at http://www.cs.nyu.edu/pipermail/fom/2008-March/012783.html. Note that ax-pow 4843 is not used by the proof. (Contributed by Gérard Lang, 22-Jun-2009.) (New usage is discouraged.) |
⊢ ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) | ||
Theorem | grothpwex 9649 | Derive the Axiom of Power Sets from the Tarski-Grothendieck axiom ax-groth 9645. Note that ax-pow 4843 is not used by the proof. Use axpweq 4842 to obtain ax-pow 4843. Use pwex 4848 or pwexg 4850 instead. (Contributed by Gérard Lang, 22-Jun-2009.) (New usage is discouraged.) |
⊢ 𝒫 𝑥 ∈ V | ||
Theorem | axgroth6 9650* | 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 9651 | The Tarski-Grothendieck Axiom implies the Axiom of Infinity (in the form of omex 8540). 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 9652 | The Tarski-Grothendieck Axiom implies the Axiom of Choice (in the form of cardeqv 9291). This can be put in a more conventional form via ween 8858 and dfac8 8957. 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). (Contributed by Mario Carneiro, 19-Apr-2013.) (New usage is discouraged.) |
⊢ dom card = V | ||
Theorem | axgroth3 9653* | Alternate version of the Tarski-Grothendieck Axiom. ax-cc 9257 is used to derive this version. (Contributed by NM, 26-Mar-2007.) |
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦) ∧ ∃𝑤 ∈ 𝑦 ∀𝑣(𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦))) | ||
Theorem | axgroth4 9654* | Alternate version of the Tarski-Grothendieck Axiom. ax-ac 9281 is used to derive this version. (Contributed by NM, 16-Apr-2007.) |
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∃𝑣 ∈ 𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦))) | ||
Theorem | grothprimlem 9655* | Lemma for grothprim 9656. Expand the membership of an unordered pair into primitives. (Contributed by NM, 29-Mar-2007.) |
⊢ ({𝑢, 𝑣} ∈ 𝑤 ↔ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣)))) | ||
Theorem | grothprim 9656* | The Tarski-Grothendieck Axiom ax-groth 9645 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 9657 | The Tarski-Grothendieck Axiom, using abbreviations. (Contributed by Mario Carneiro, 28-May-2013.) |
⊢ ∪ Tarski = V | ||
Theorem | inaprc 9658 | 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 9659 | Extend class definition to include the map whose value is the smallest Tarski class. |
class tarskiMap | ||
Definition | df-tskm 9660* | 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 9661* | Value of our tarski map. (Contributed by FL, 30-Dec-2010.) (Revised by Mario Carneiro, 20-Sep-2014.) |
⊢ (𝐴 ∈ 𝑉 → (tarskiMap‘𝐴) = ∩ {𝑥 ∈ Tarski ∣ 𝐴 ∈ 𝑥}) | ||
Theorem | tskmid 9662 | 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 9663 | 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 9664* | Being a part of (tarskiMap‘𝐴). (Contributed by FL, 17-Apr-2011.) (Proof shortened by Mario Carneiro, 20-Sep-2014.) |
⊢ (𝐴 ∈ 𝑉 → (𝐵 ⊆ (tarskiMap‘𝐴) ↔ ∀𝑥 ∈ Tarski (𝐴 ∈ 𝑥 → 𝐵 ⊆ 𝑥))) | ||
Theorem | eltskm 9665* | 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 9993). After that, we derive their basic properties, various operations like addition (df-add 9947) and sine (df-sin 14800), and subsets such as the integers (df-z 11378) and natural numbers (df-nn 11021). | ||
Syntax | cnpi 9666 |
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 9965. The actual set of Dedekind cuts is defined by df-np 9803. |
class N | ||
Syntax | cpli 9667 | Positive integer addition. |
class +N | ||
Syntax | cmi 9668 | Positive integer multiplication. |
class ·N | ||
Syntax | clti 9669 | Positive integer ordering relation. |
class <N | ||
Syntax | cplpq 9670 | Positive pre-fraction addition. |
class +pQ | ||
Syntax | cmpq 9671 | Positive pre-fraction multiplication. |
class ·pQ | ||
Syntax | cltpq 9672 | Positive pre-fraction ordering relation. |
class <pQ | ||
Syntax | ceq 9673 | Equivalence class used to construct positive fractions. |
class ~Q | ||
Syntax | cnq 9674 | Set of positive fractions. |
class Q | ||
Syntax | c1q 9675 | The positive fraction constant 1. |
class 1Q | ||
Syntax | cerq 9676 | Positive fraction equivalence class. |
class [Q] | ||
Syntax | cplq 9677 | Positive fraction addition. |
class +Q | ||
Syntax | cmq 9678 | Positive fraction multiplication. |
class ·Q | ||
Syntax | crq 9679 | Positive fraction reciprocal operation. |
class *Q | ||
Syntax | cltq 9680 | Positive fraction ordering relation. |
class <Q | ||
Syntax | cnp 9681 | Set of positive reals. |
class P | ||
Syntax | c1p 9682 | Positive real constant 1. |
class 1P | ||
Syntax | cpp 9683 | Positive real addition. |
class +P | ||
Syntax | cmp 9684 | Positive real multiplication. |
class ·P | ||
Syntax | cltp 9685 | Positive real ordering relation. |
class <P | ||
Syntax | cer 9686 | Equivalence class used to construct signed reals. |
class ~R | ||
Syntax | cnr 9687 | Set of signed reals. |
class R | ||
Syntax | c0r 9688 | The signed real constant 0. |
class 0R | ||
Syntax | c1r 9689 | The signed real constant 1. |
class 1R | ||
Syntax | cm1r 9690 | The signed real constant -1. |
class -1R | ||
Syntax | cplr 9691 | Signed real addition. |
class +R | ||
Syntax | cmr 9692 | Signed real multiplication. |
class ·R | ||
Syntax | cltr 9693 | Signed real ordering relation. |
class <R | ||
Definition | df-ni 9694 | Define the class of positive integers. This is a "temporary" set used in the construction of complex numbers df-c 9942, and is intended to be used only by the construction. (Contributed by NM, 15-Aug-1995.) (New usage is discouraged.) |
⊢ N = (ω ∖ {∅}) | ||
Definition | df-pli 9695 | Define addition on positive integers. This is a "temporary" set used in the construction of complex numbers df-c 9942, and is intended to be used only by the construction. (Contributed by NM, 26-Aug-1995.) (New usage is discouraged.) |
⊢ +N = ( +𝑜 ↾ (N × N)) | ||
Definition | df-mi 9696 | Define multiplication on positive integers. This is a "temporary" set used in the construction of complex numbers df-c 9942, and is intended to be used only by the construction. (Contributed by NM, 26-Aug-1995.) (New usage is discouraged.) |
⊢ ·N = ( ·𝑜 ↾ (N × N)) | ||
Definition | df-lti 9697 | Define 'less than' on positive integers. This is a "temporary" set used in the construction of complex numbers df-c 9942, 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 9698 | Membership in the class of positive integers. (Contributed by NM, 15-Aug-1995.) (New usage is discouraged.) |
⊢ (𝐴 ∈ N ↔ (𝐴 ∈ ω ∧ 𝐴 ≠ ∅)) | ||
Theorem | elni2 9699 | Membership in the class of positive integers. (Contributed by NM, 27-Nov-1995.) (New usage is discouraged.) |
⊢ (𝐴 ∈ N ↔ (𝐴 ∈ ω ∧ ∅ ∈ 𝐴)) | ||
Theorem | pinn 9700 | A positive integer is a natural number. (Contributed by NM, 15-Aug-1995.) (New usage is discouraged.) |
⊢ (𝐴 ∈ N → 𝐴 ∈ ω) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |