P. 108 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 10701-10800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	inatsk 10701	(𝑅1‘𝐴) for 𝐴 a strongly inaccessible cardinal is a Tarski class. (Contributed by Mario Carneiro, 8-Jun-2013.)
⊢ (𝐴 ∈ Inacc → (𝑅1‘𝐴) ∈ Tarski)
Theorem	r1omtsk 10702	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 10703	A Tarski class contains all ordinals smaller than it. (Contributed by Mario Carneiro, 8-Jun-2013.)
⊢ ((𝑇 ∈ Tarski ∧ 𝐴 ∈ On ∧ 𝐴 ≺ 𝑇) → 𝐴 ∈ 𝑇)
Theorem	tskcard 10704	An even more direct relationship than r1tskina 10705 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 10705	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 10706	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 10707	A nonempty transitive Tarski class is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝑇 ≠ ∅) → 𝑇 ∈ WUni)
Theorem	tskint 10708	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 10709	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 10710	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 10711	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 𝑇) ∧ 𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑇) → (𝐴 ↑m 𝐵) ∈ 𝑇)
Theorem	tskurn 10712	A transitive Tarski class is closed under small unions. (Contributed by Mario Carneiro, 22-Jun-2013.)
⊢ (((𝑇 ∈ Tarski ∧ Tr 𝑇) ∧ 𝐴 ∈ 𝑇 ∧ 𝐹:𝐴⟶𝑇) → ∪ ran 𝐹 ∈ 𝑇)
4.1.4  Grothendieck universes
Syntax	cgru 10713	Extend class notation to include the class of all Grothendieck universes.
class Univ
Definition	df-gru 10714*	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 10715*	Properties of a Grothendieck universe. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ (𝑈 ∈ 𝑉 → (𝑈 ∈ Univ ↔ (Tr 𝑈 ∧ ∀𝑥 ∈ 𝑈 (𝒫 𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∈ 𝑈 ∧ ∀𝑦 ∈ (𝑈 ↑m 𝑥)∪ ran 𝑦 ∈ 𝑈))))
Theorem	grutr 10716	A Grothendieck universe is transitive. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝑈 ∈ Univ → Tr 𝑈)
Theorem	gruelss 10717	A Grothendieck universe is transitive, so each element is a subset of the universe. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈) → 𝐴 ⊆ 𝑈)
Theorem	grupw 10718	A Grothendieck universe contains the powerset of each of its members. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈) → 𝒫 𝐴 ∈ 𝑈)
Theorem	gruss 10719	Any subset of an element of a Grothendieck universe is also an element. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ 𝑈)
Theorem	grupr 10720	A Grothendieck universe contains pairs derived from its elements. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈) → {𝐴, 𝐵} ∈ 𝑈)
Theorem	gruurn 10721	A Grothendieck universe contains the range of any function which takes values in the universe (see gruiun 10722 for a more intuitive version). (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐹:𝐴⟶𝑈) → ∪ ran 𝐹 ∈ 𝑈)
Theorem	gruiun 10722*	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 10723	A Grothendieck universe contains unions of its elements. (Contributed by Mario Carneiro, 17-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈) → ∪ 𝐴 ∈ 𝑈)
Theorem	grurn 10724	A Grothendieck universe contains the range of any function which takes values in the universe (see gruiun 10722 for a more intuitive version). (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐹:𝐴⟶𝑈) → ran 𝐹 ∈ 𝑈)
Theorem	gruima 10725	A Grothendieck universe contains image sets drawn from its members. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ Fun 𝐹 ∧ (𝐹 “ 𝐴) ⊆ 𝑈) → (𝐴 ∈ 𝑈 → (𝐹 “ 𝐴) ∈ 𝑈))
Theorem	gruel 10726	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 10727	A Grothendieck universe contains the singletons of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈) → {𝐴} ∈ 𝑈)
Theorem	gruop 10728	A Grothendieck universe contains ordered pairs of its elements. (Contributed by Mario Carneiro, 10-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈) → ⟨𝐴, 𝐵⟩ ∈ 𝑈)
Theorem	gruun 10729	A Grothendieck universe contains binary unions of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈) → (𝐴 ∪ 𝐵) ∈ 𝑈)
Theorem	gruxp 10730	A Grothendieck universe contains binary cartesian products of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈) → (𝐴 × 𝐵) ∈ 𝑈)
Theorem	grumap 10731	A Grothendieck universe contains all powers of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈) → (𝐴 ↑m 𝐵) ∈ 𝑈)
Theorem	gruixp 10732*	A Grothendieck universe contains indexed cartesian products of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑈) → X𝑥 ∈ 𝐴 𝐵 ∈ 𝑈)
Theorem	gruiin 10733*	A Grothendieck universe contains indexed intersections of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ ∃𝑥 ∈ 𝐴 𝐵 ∈ 𝑈) → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑈)
Theorem	gruf 10734	A Grothendieck universe contains all functions on its elements. (Contributed by Mario Carneiro, 10-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐹:𝐴⟶𝑈) → 𝐹 ∈ 𝑈)
Theorem	gruen 10735	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 10736	A nonempty Grothendieck universe is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → 𝑈 ∈ WUni)
Theorem	intgru 10737	The intersection of a family of universes is a universe. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝐴 ⊆ Univ ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ∈ Univ)
Theorem	ingru 10738*	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 10739	The wellfounded part of a universe is another universe. (Contributed by Mario Carneiro, 17-Jun-2013.)
⊢ (𝑈 ∈ Univ → (𝑈 ∩ ∪ (𝑅1 “ On)) ∈ Univ)
Theorem	grudomon 10740	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 10741	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 10742	A characterization of Grothendieck universes, part 1. (Contributed by Mario Carneiro, 23-Jun-2013.)
⊢ 𝐴 = (𝑈 ∩ On)    ⇒   ⊢ (𝑈 ∈ Univ → (𝑅1‘𝐴) ⊆ 𝑈)
Theorem	grur1 10743	A characterization of Grothendieck universes, part 2. (Contributed by Mario Carneiro, 24-Jun-2013.)
⊢ 𝐴 = (𝑈 ∩ On)    ⇒   ⊢ ((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) → 𝑈 = (𝑅1‘𝐴))
Theorem	grutsk1 10744	Grothendieck universes are the same as transitive Tarski classes, part one: a transitive Tarski class is a universe. (The hard work is in tskuni 10706.) (Contributed by Mario Carneiro, 17-Jun-2013.)
⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇) → 𝑇 ∈ Univ)
Theorem	grutsk 10745	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 𝑥}
4.2  ZFC Set Theory plus the Tarski-Grothendieck Axiom
4.2.1  Introduce the Tarski-Grothendieck Axiom
Axiom	ax-groth 10746*	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 10757). An open problem is finding a shorter equivalent. (Contributed by NM, 18-Mar-2007.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦) ∧ ∃𝑤 ∈ 𝑦 ∀𝑣(𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → (𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦)))
Theorem	axgroth5 10747*	The Tarski-Grothendieck axiom using abbreviations. (Contributed by NM, 22-Jun-2009.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ ∃𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤) ∧ ∀𝑧 ∈ 𝒫 𝑦(𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦))
Theorem	axgroth2 10748*	Alternate version of the Tarski-Grothendieck Axiom. (Contributed by NM, 18-Mar-2007.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦) ∧ ∃𝑤 ∈ 𝑦 ∀𝑣(𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → (𝑦 ≼ 𝑧 ∨ 𝑧 ∈ 𝑦)))
4.2.2  Derive the Power Set, Infinity and Choice Axioms
Theorem	grothpw 10749*	Derive the Axiom of Power Sets ax-pow 5312 from the Tarski-Grothendieck axiom ax-groth 10746. That it follows is mentioned by Bob Solovay at http://www.cs.nyu.edu/pipermail/fom/2008-March/012783.html 10746. Note that ax-pow 5312 is not used by the proof. (Contributed by Gérard Lang, 22-Jun-2009.) (New usage is discouraged.)
⊢ ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
Theorem	grothpwex 10750	Derive the Axiom of Power Sets from the Tarski-Grothendieck axiom ax-groth 10746. Note that ax-pow 5312 is not used by the proof. Use axpweq 5298 to obtain ax-pow 5312. Use pwex 5327 or pwexg 5325 instead. (Contributed by Gérard Lang, 22-Jun-2009.) (New usage is discouraged.)
⊢ 𝒫 𝑥 ∈ V
Theorem	axgroth6 10751*	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 10752	The Tarski-Grothendieck Axiom implies the Axiom of Infinity (in the form of omex 9564). 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 10753	The Tarski-Grothendieck Axiom implies the Axiom of Choice (in the form of cardeqv 10391). This can be put in a more conventional form via ween 9957 and dfac8 10058. 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 10058). (Contributed by Mario Carneiro, 19-Apr-2013.) (New usage is discouraged.)
⊢ dom card = V
Theorem	axgroth3 10754*	Alternate version of the Tarski-Grothendieck Axiom. ax-cc 10357 is used to derive this version. (Contributed by NM, 26-Mar-2007.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦) ∧ ∃𝑤 ∈ 𝑦 ∀𝑣(𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦)))
Theorem	axgroth4 10755*	Alternate version of the Tarski-Grothendieck Axiom. ax-ac 10381 is used to derive this version. (Contributed by NM, 16-Apr-2007.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∃𝑣 ∈ 𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦)))
Theorem	grothprimlem 10756*	Lemma for grothprim 10757. Expand the membership of an unordered pair into primitives. (Contributed by NM, 29-Mar-2007.)
⊢ ({𝑢, 𝑣} ∈ 𝑤 ↔ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))
Theorem	grothprim 10757*	The Tarski-Grothendieck Axiom ax-groth 10746 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 10758	The Tarski-Grothendieck Axiom, using abbreviations. (Contributed by Mario Carneiro, 28-May-2013.)
⊢ ∪ Tarski = V
Theorem	inaprc 10759	An equivalent to the Tarski-Grothendieck Axiom: there is a proper class of inaccessible cardinals. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ Inacc ∉ V
4.2.3  Tarski map function
Syntax	ctskm 10760	Extend class definition to include the map whose value is the smallest Tarski class.
class tarskiMap
Definition	df-tskm 10761*	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 10762*	Value of our tarski map. (Contributed by FL, 30-Dec-2010.) (Revised by Mario Carneiro, 20-Sep-2014.)
⊢ (𝐴 ∈ 𝑉 → (tarskiMap‘𝐴) = ∩ {𝑥 ∈ Tarski ∣ 𝐴 ∈ 𝑥})
Theorem	tskmid 10763	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 10764	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 10765*	Being a part of (tarskiMap‘𝐴). (Contributed by FL, 17-Apr-2011.) (Proof shortened by Mario Carneiro, 20-Sep-2014.)
⊢ (𝐴 ∈ 𝑉 → (𝐵 ⊆ (tarskiMap‘𝐴) ↔ ∀𝑥 ∈ Tarski (𝐴 ∈ 𝑥 → 𝐵 ⊆ 𝑥)))
Theorem	eltskm 10766*	Belonging to (tarskiMap‘𝐴). (Contributed by FL, 17-Apr-2011.) (Proof shortened by Mario Carneiro, 21-Sep-2014.)
⊢ (𝐴 ∈ 𝑉 → (𝐵 ∈ (tarskiMap‘𝐴) ↔ ∀𝑥 ∈ Tarski (𝐴 ∈ 𝑥 → 𝐵 ∈ 𝑥)))
PART 5  REAL AND COMPLEX NUMBERS This section derives the basics of real and complex numbers. We first construct and axiomatize real and complex numbers (e.g., ax-resscn 11095). After that, we derive their basic properties, various operations like addition (df-add 11049) and sine (df-sin 16004), and subsets such as the integers (df-z 12501) and natural numbers (df-nn 12158).
5.1  Construction and axiomatization of real and complex numbers
5.1.1  Dedekind-cut construction of real and complex numbers
Syntax	cnpi 10767	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 11067. The actual set of Dedekind cuts is defined by df-np 10904.
class N
Syntax	cpli 10768	Positive integer addition.
class +N
Syntax	cmi 10769	Positive integer multiplication.
class ·N
Syntax	clti 10770	Positive integer ordering relation.
class <N
Syntax	cplpq 10771	Positive pre-fraction addition.
class +pQ
Syntax	cmpq 10772	Positive pre-fraction multiplication.
class ·pQ
Syntax	cltpq 10773	Positive pre-fraction ordering relation.
class <pQ
Syntax	ceq 10774	Equivalence class used to construct positive fractions.
class ~Q
Syntax	cnq 10775	Set of positive fractions.
class Q
Syntax	c1q 10776	The positive fraction constant 1.
class 1Q
Syntax	cerq 10777	Positive fraction equivalence class.
class [Q]
Syntax	cplq 10778	Positive fraction addition.
class +Q
Syntax	cmq 10779	Positive fraction multiplication.
class ·Q
Syntax	crq 10780	Positive fraction reciprocal operation.
class *Q
Syntax	cltq 10781	Positive fraction ordering relation.
class <Q
Syntax	cnp 10782	Set of positive reals.
class P
Syntax	c1p 10783	Positive real constant 1.
class 1P
Syntax	cpp 10784	Positive real addition.
class +P
Syntax	cmp 10785	Positive real multiplication.
class ·P
Syntax	cltp 10786	Positive real ordering relation.
class <P
Syntax	cer 10787	Equivalence class used to construct signed reals.
class ~R
Syntax	cnr 10788	Set of signed reals.
class R
Syntax	c0r 10789	The signed real constant 0.
class 0R
Syntax	c1r 10790	The signed real constant 1.
class 1R
Syntax	cm1r 10791	The signed real constant -1.
class -1R
Syntax	cplr 10792	Signed real addition.
class +R
Syntax	cmr 10793	Signed real multiplication.
class ·R
Syntax	cltr 10794	Signed real ordering relation.
class <R
Definition	df-ni 10795	Define the class of positive integers. This is a "temporary" set used in the construction of complex numbers df-c 11044, and is intended to be used only by the construction. (Contributed by NM, 15-Aug-1995.) (New usage is discouraged.)
⊢ N = (ω ∖ {∅})
Definition	df-pli 10796	Define addition on positive integers. This is a "temporary" set used in the construction of complex numbers df-c 11044, 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 10797	Define multiplication on positive integers. This is a "temporary" set used in the construction of complex numbers df-c 11044, 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 10798	Define 'less than' on positive integers. This is a "temporary" set used in the construction of complex numbers df-c 11044, 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 10799	Membership in the class of positive integers. (Contributed by NM, 15-Aug-1995.) (New usage is discouraged.)
⊢ (𝐴 ∈ N ↔ (𝐴 ∈ ω ∧ 𝐴 ≠ ∅))
Theorem	elni2 10800	Membership in the class of positive integers. (Contributed by NM, 27-Nov-1995.) (New usage is discouraged.)
⊢ (𝐴 ∈ N ↔ (𝐴 ∈ ω ∧ ∅ ∈ 𝐴))