P. 109 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 10801-10900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	wunint 10801	A weak universe is closed under nonempty intersections. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ∈ 𝑈)
Theorem	wunsn 10802	A weak universe is closed under singletons. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → {𝐴} ∈ 𝑈)
Theorem	wunsuc 10803	A weak universe is closed under successors. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → suc 𝐴 ∈ 𝑈)
Theorem	wun0 10804	A weak universe contains the empty set. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    ⇒   ⊢ (𝜑 → ∅ ∈ 𝑈)
Theorem	wunr1om 10805	A weak universe is infinite, because it contains all the finite levels of the cumulative hierarchy. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    ⇒   ⊢ (𝜑 → (𝑅1 “ ω) ⊆ 𝑈)
Theorem	wunom 10806	A weak universe contains all the finite ordinals, and hence is infinite. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    ⇒   ⊢ (𝜑 → ω ⊆ 𝑈)
Theorem	wunfi 10807	A weak universe contains all finite sets with elements drawn from the universe. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑈)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝑈)
Theorem	wunop 10808	A weak universe is closed under ordered pairs. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ⟨𝐴, 𝐵⟩ ∈ 𝑈)
Theorem	wunot 10809	A weak universe is closed under ordered triples. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ⟨𝐴, 𝐵, 𝐶⟩ ∈ 𝑈)
Theorem	wunxp 10810	A weak universe is closed under cartesian products. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝐴 × 𝐵) ∈ 𝑈)
Theorem	wunpm 10811	A weak universe is closed under partial mappings. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝐴 ↑pm 𝐵) ∈ 𝑈)
Theorem	wunmap 10812	A weak universe is closed under mappings. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝐴 ↑m 𝐵) ∈ 𝑈)
Theorem	wunf 10813	A weak universe is closed under functions with known domain and codomain. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    ⇒   ⊢ (𝜑 → 𝐹 ∈ 𝑈)
Theorem	wundm 10814	A weak universe is closed under the domain operator. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → dom 𝐴 ∈ 𝑈)
Theorem	wunrn 10815	A weak universe is closed under the range operator. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ran 𝐴 ∈ 𝑈)
Theorem	wuncnv 10816	A weak universe is closed under the converse operator. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ◡𝐴 ∈ 𝑈)
Theorem	wunres 10817	A weak universe is closed under restrictions. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝐴 ↾ 𝐵) ∈ 𝑈)
Theorem	wunfv 10818	A weak universe is closed under the function value operator. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝐴‘𝐵) ∈ 𝑈)
Theorem	wunco 10819	A weak universe is closed under composition. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝐴 ∘ 𝐵) ∈ 𝑈)
Theorem	wuntpos 10820	A weak universe is closed under transposition. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → tpos 𝐴 ∈ 𝑈)
Theorem	intwun 10821	The intersection of a collection of weak universes is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ ((𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ∈ WUni)
Theorem	r1limwun 10822	Each limit stage in the cumulative hierarchy is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ ((𝐴 ∈ 𝑉 ∧ Lim 𝐴) → (𝑅1‘𝐴) ∈ WUni)
Theorem	r1wunlim 10823	The stages of the cumulative hierarchy of sets that are weak universes are exactly the stages at the limit ordinals. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝐴 ∈ 𝑉 → ((𝑅1‘𝐴) ∈ WUni ↔ Lim 𝐴))
Theorem	wunex2 10824*	Construct a weak universe from a given set. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐹 = (rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1o)) ↾ ω)    &   ⊢ 𝑈 = ∪ ran 𝐹    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝑈 ∈ WUni ∧ 𝐴 ⊆ 𝑈))
Theorem	wunex 10825*	Construct a weak universe from a given set. See also wunex2 10824. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑢 ∈ WUni 𝐴 ⊆ 𝑢)
Theorem	uniwun 10826	Every set is contained in a weak universe. This is the analogue of grothtsk 10921 for weak universes, but it is provable in ZF without the Tarski-Grothendieck axiom, contrary to grothtsk 10921. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ ∪ WUni = V
Theorem	wunex3 10827	Construct a weak universe from a given set. This version of wunex 10825 has a simpler proof, but requires the axiom of regularity. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝑈 = (𝑅1‘((rank‘𝐴) +o ω))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝑈 ∈ WUni ∧ 𝐴 ⊆ 𝑈))
Theorem	wuncval 10828*	Value of the weak universe closure operator. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝐴 ∈ 𝑉 → (wUniCl‘𝐴) = ∩ {𝑢 ∈ WUni ∣ 𝐴 ⊆ 𝑢})
Theorem	wuncid 10829	The weak universe closure of a set contains the set. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝐴 ∈ 𝑉 → 𝐴 ⊆ (wUniCl‘𝐴))
Theorem	wunccl 10830	The weak universe closure of a set is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝐴 ∈ 𝑉 → (wUniCl‘𝐴) ∈ WUni)
Theorem	wuncss 10831	The weak universe closure is a subset of any other weak universe containing the set. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ ((𝑈 ∈ WUni ∧ 𝐴 ⊆ 𝑈) → (wUniCl‘𝐴) ⊆ 𝑈)
Theorem	wuncidm 10832	The weak universe closure is idempotent. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝐴 ∈ 𝑉 → (wUniCl‘(wUniCl‘𝐴)) = (wUniCl‘𝐴))
Theorem	wuncval2 10833*	Our earlier expression for a containing weak universe is in fact the weak universe closure. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐹 = (rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1o)) ↾ ω)    &   ⊢ 𝑈 = ∪ ran 𝐹    ⇒   ⊢ (𝐴 ∈ 𝑉 → (wUniCl‘𝐴) = 𝑈)
4.1.3  Tarski classes
Syntax	ctsk 10834	Extend class definition to include the class of all Tarski classes.
class Tarski
Definition	df-tsk 10835*	The class of all Tarski classes. Tarski classes is a phrase coined by Grzegorz Bancerek in his article Tarski's Classes and Ranks, Journal of Formalized Mathematics, Vol 1, No 3, May-August 1990. A Tarski class is a set whose existence is ensured by Tarski's Axiom A (see ax-groth 10909 and the equivalent axioms). Axiom A was first presented in Tarski's article Ueber unerreichbare Kardinalzahlen. Tarski introduced Axiom A to allow reasoning with inaccessible cardinals in ZFC. Later, Grothendieck introduced the concept of (Grothendieck) universes and showed they were exactly transitive Tarski classes. (Contributed by FL, 30-Dec-2010.)
⊢ Tarski = {𝑦 ∣ (∀𝑧 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ ∃𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤) ∧ ∀𝑧 ∈ 𝒫 𝑦(𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦))}
Theorem	eltskg 10836*	Properties of a Tarski class. (Contributed by FL, 30-Dec-2010.)
⊢ (𝑇 ∈ 𝑉 → (𝑇 ∈ Tarski ↔ (∀𝑧 ∈ 𝑇 (𝒫 𝑧 ⊆ 𝑇 ∧ ∃𝑤 ∈ 𝑇 𝒫 𝑧 ⊆ 𝑤) ∧ ∀𝑧 ∈ 𝒫 𝑇(𝑧 ≈ 𝑇 ∨ 𝑧 ∈ 𝑇))))
Theorem	eltsk2g 10837*	Properties of a Tarski class. (Contributed by FL, 30-Dec-2010.) (Revised by Mario Carneiro, 20-Sep-2014.)
⊢ (𝑇 ∈ 𝑉 → (𝑇 ∈ Tarski ↔ (∀𝑧 ∈ 𝑇 (𝒫 𝑧 ⊆ 𝑇 ∧ 𝒫 𝑧 ∈ 𝑇) ∧ ∀𝑧 ∈ 𝒫 𝑇(𝑧 ≈ 𝑇 ∨ 𝑧 ∈ 𝑇))))
Theorem	tskpwss 10838	First axiom of a Tarski class. The subsets of an element of a Tarski class belong to the class. (Contributed by FL, 30-Dec-2010.) (Proof shortened by Mario Carneiro, 20-Sep-2014.)
⊢ ((𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇) → 𝒫 𝐴 ⊆ 𝑇)
Theorem	tskpw 10839	Second axiom of a Tarski class. The powerset of an element of a Tarski class belongs to the class. (Contributed by FL, 30-Dec-2010.) (Proof shortened by Mario Carneiro, 20-Sep-2014.)
⊢ ((𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇) → 𝒫 𝐴 ∈ 𝑇)
Theorem	tsken 10840	Third axiom of a Tarski class. A subset of a Tarski class is either equipotent to the class or an element of the class. (Contributed by FL, 30-Dec-2010.) (Revised by Mario Carneiro, 20-Sep-2014.)
⊢ ((𝑇 ∈ Tarski ∧ 𝐴 ⊆ 𝑇) → (𝐴 ≈ 𝑇 ∨ 𝐴 ∈ 𝑇))
Theorem	0tsk 10841	The empty set is a (transitive) Tarski class. (Contributed by FL, 30-Dec-2010.)
⊢ ∅ ∈ Tarski
Theorem	tsksdom 10842	An element of a Tarski class is strictly dominated by the class. JFM CLASSES2 th. 1. (Contributed by FL, 22-Feb-2011.) (Revised by Mario Carneiro, 18-Jun-2013.)
⊢ ((𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇) → 𝐴 ≺ 𝑇)
Theorem	tskssel 10843	A part of a Tarski class strictly dominated by the class is an element of the class. JFM CLASSES2 th. 2. (Contributed by FL, 22-Feb-2011.) (Proof shortened by Mario Carneiro, 20-Sep-2014.)
⊢ ((𝑇 ∈ Tarski ∧ 𝐴 ⊆ 𝑇 ∧ 𝐴 ≺ 𝑇) → 𝐴 ∈ 𝑇)
Theorem	tskss 10844	The subsets of an element of a Tarski class belong to the class. (Contributed by FL, 30-Dec-2010.) (Revised by Mario Carneiro, 18-Jun-2013.)
⊢ ((𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇 ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ 𝑇)
Theorem	tskin 10845	The intersection of two elements of a Tarski class belongs to the class. (Contributed by FL, 30-Dec-2010.) (Proof shortened by Mario Carneiro, 20-Sep-2014.)
⊢ ((𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇) → (𝐴 ∩ 𝐵) ∈ 𝑇)
Theorem	tsksn 10846	A singleton of an element of a Tarski class belongs to the class. JFM CLASSES2 th. 2 (partly). (Contributed by FL, 22-Feb-2011.) (Revised by Mario Carneiro, 18-Jun-2013.)
⊢ ((𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇) → {𝐴} ∈ 𝑇)
Theorem	tsktrss 10847	A transitive element of a Tarski class is a part of the class. JFM CLASSES2 th. 8. (Contributed by FL, 22-Feb-2011.) (Revised by Mario Carneiro, 20-Sep-2014.)
⊢ ((𝑇 ∈ Tarski ∧ Tr 𝐴 ∧ 𝐴 ∈ 𝑇) → 𝐴 ⊆ 𝑇)
Theorem	tsksuc 10848	If an element of a Tarski class is an ordinal number, its successor is an element of the class. JFM CLASSES2 th. 6 (partly). (Contributed by FL, 22-Feb-2011.) (Proof shortened by Mario Carneiro, 20-Sep-2014.)
⊢ ((𝑇 ∈ Tarski ∧ 𝐴 ∈ On ∧ 𝐴 ∈ 𝑇) → suc 𝐴 ∈ 𝑇)
Theorem	tsk0 10849	A nonempty Tarski class contains the empty set. (Contributed by FL, 30-Dec-2010.) (Revised by Mario Carneiro, 18-Jun-2013.)
⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) → ∅ ∈ 𝑇)
Theorem	tsk1 10850	One is an element of a nonempty Tarski class. (Contributed by FL, 22-Feb-2011.)
⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) → 1o ∈ 𝑇)
Theorem	tsk2 10851	Two is an element of a nonempty Tarski class. (Contributed by FL, 22-Feb-2011.) (Proof shortened by Mario Carneiro, 20-Sep-2014.)
⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) → 2o ∈ 𝑇)
Theorem	2domtsk 10852	If a Tarski class is not empty, it has more than two elements. (Contributed by FL, 22-Feb-2011.)
⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) → 2o ≺ 𝑇)
Theorem	tskr1om 10853	A nonempty Tarski class is infinite, because it contains all the finite levels of the cumulative hierarchy. (This proof does not use ax-inf 9640.) (Contributed by Mario Carneiro, 24-Jun-2013.)
⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) → (𝑅1 “ ω) ⊆ 𝑇)
Theorem	tskhf 10854	A nonempty Tarski class contains the whole finite cumulative hierarchy. (This proof does not use ax-inf 9640.) (Contributed by NM, 22-Feb-2011.) Restate using the defined HF symbol. (Revised by Eric Schmidt, 24-Sep-2026.)
⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) → HF ⊆ 𝑇)
Theorem	tskinf 10855	A nonempty Tarski class is infinite. (Contributed by FL, 22-Feb-2011.)
⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) → ω ≼ 𝑇)
Theorem	tskpr 10856	If 𝐴 and 𝐵 are members of a Tarski class, their unordered pair is also an element of the class. JFM CLASSES2 th. 3 (partly). (Contributed by FL, 22-Feb-2011.) (Proof shortened by Mario Carneiro, 20-Jun-2013.)
⊢ ((𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑇) → {𝐴, 𝐵} ∈ 𝑇)
Theorem	tskop 10857	If 𝐴 and 𝐵 are members of a Tarski class, their ordered pair is also an element of the class. JFM CLASSES2 th. 4. (Contributed by FL, 22-Feb-2011.)
⊢ ((𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑇) → ⟨𝐴, 𝐵⟩ ∈ 𝑇)
Theorem	tskxpss 10858	A Cartesian product of two parts of a Tarski class is a part of the class. (Contributed by FL, 22-Feb-2011.) (Proof shortened by Mario Carneiro, 20-Jun-2013.)
⊢ ((𝑇 ∈ Tarski ∧ 𝐴 ⊆ 𝑇 ∧ 𝐵 ⊆ 𝑇) → (𝐴 × 𝐵) ⊆ 𝑇)
Theorem	tskwe2 10859	A Tarski class is well-orderable. (Contributed by Mario Carneiro, 20-Jun-2013.)
⊢ (𝑇 ∈ Tarski → 𝑇 ∈ dom card)
Theorem	inttsk 10860	The intersection of a collection of Tarski classes is a Tarski class. (Contributed by FL, 17-Apr-2011.) (Proof shortened by Mario Carneiro, 20-Sep-2014.)
⊢ ((𝐴 ⊆ Tarski ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ∈ Tarski)
Theorem	inar1 10861	(𝑅1‘𝐴) for 𝐴 a strongly inaccessible cardinal is equipotent to 𝐴. (Contributed by Mario Carneiro, 6-Jun-2013.)
⊢ (𝐴 ∈ Inacc → (𝑅1‘𝐴) ≈ 𝐴)
Theorem	hfomALT 10862	Alternate proof of hfom 10322, shorter as a consequence of inar1 10861, but requiring AC. (Contributed by Mario Carneiro, 27-May-2013.) Restate using the defined HF symbol. (Revised by Eric Schmidt, 24-Sep-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ HF ≈ ω
Theorem	rankcf 10863	Any set must be at least as large as the cofinality of its rank, because the ranks of the elements of 𝐴 form a cofinal map into (rank‘𝐴). (Contributed by Mario Carneiro, 27-May-2013.)
⊢ ¬ 𝐴 ≺ (cf‘(rank‘𝐴))
Theorem	inatsk 10864	(𝑅1‘𝐴) for 𝐴 a strongly inaccessible cardinal is a Tarski class. (Contributed by Mario Carneiro, 8-Jun-2013.)
⊢ (𝐴 ∈ Inacc → (𝑅1‘𝐴) ∈ Tarski)
Theorem	hftsk 10865	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.) Restate using the defined HF symbol. (Revised by Eric Schmidt, 24-Sep-2026.)
⊢ HF ∈ Tarski
Theorem	tskord 10866	A Tarski class contains all ordinals smaller than it. (Contributed by Mario Carneiro, 8-Jun-2013.)
⊢ ((𝑇 ∈ Tarski ∧ 𝐴 ∈ On ∧ 𝐴 ≺ 𝑇) → 𝐴 ∈ 𝑇)
Theorem	tskcard 10867	An even more direct relationship than r1tskina 10868 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 10868	There is a direct relationship between transitive Tarski classes and inaccessible cardinals: the stages of the cumulative hierarchy of sets that are Tarski classes are exactly the stages at the strongly inaccessible cardinals. (Contributed by Mario Carneiro, 8-Jun-2013.)
⊢ (𝐴 ∈ On → ((𝑅1‘𝐴) ∈ Tarski ↔ (𝐴 = ∅ ∨ 𝐴 ∈ Inacc)))
Theorem	tskuni 10869	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 10870	A nonempty transitive Tarski class is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝑇 ≠ ∅) → 𝑇 ∈ WUni)
Theorem	tskint 10871	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 10872	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 10873	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 10874	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 10875	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 10876	Extend class notation to include the class of all Grothendieck universes.
class Univ
Definition	df-gru 10877*	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 10878*	Properties of a Grothendieck universe. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ (𝑈 ∈ 𝑉 → (𝑈 ∈ Univ ↔ (Tr 𝑈 ∧ ∀𝑥 ∈ 𝑈 (𝒫 𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∈ 𝑈 ∧ ∀𝑦 ∈ (𝑈 ↑m 𝑥)∪ ran 𝑦 ∈ 𝑈))))
Theorem	grutr 10879	A Grothendieck universe is transitive. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝑈 ∈ Univ → Tr 𝑈)
Theorem	gruelss 10880	A Grothendieck universe is transitive, so each element is a subset of the universe. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈) → 𝐴 ⊆ 𝑈)
Theorem	grupw 10881	A Grothendieck universe contains the powerset of each of its members. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈) → 𝒫 𝐴 ∈ 𝑈)
Theorem	gruss 10882	Any subset of an element of a Grothendieck universe is also an element. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ 𝑈)
Theorem	grupr 10883	A Grothendieck universe contains pairs derived from its elements. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈) → {𝐴, 𝐵} ∈ 𝑈)
Theorem	gruurn 10884	A Grothendieck universe contains the range of any function which takes values in the universe (see gruiun 10885 for a more intuitive version). (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐹:𝐴⟶𝑈) → ∪ ran 𝐹 ∈ 𝑈)
Theorem	gruiun 10885*	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 10886	A Grothendieck universe contains unions of its elements. (Contributed by Mario Carneiro, 17-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈) → ∪ 𝐴 ∈ 𝑈)
Theorem	grurn 10887	A Grothendieck universe contains the range of any function which takes values in the universe (see gruiun 10885 for a more intuitive version). (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐹:𝐴⟶𝑈) → ran 𝐹 ∈ 𝑈)
Theorem	gruima 10888	A Grothendieck universe contains image sets drawn from its members. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ Fun 𝐹 ∧ (𝐹 “ 𝐴) ⊆ 𝑈) → (𝐴 ∈ 𝑈 → (𝐹 “ 𝐴) ∈ 𝑈))
Theorem	gruel 10889	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 10890	A Grothendieck universe contains the singletons of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈) → {𝐴} ∈ 𝑈)
Theorem	gruop 10891	A Grothendieck universe contains ordered pairs of its elements. (Contributed by Mario Carneiro, 10-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈) → ⟨𝐴, 𝐵⟩ ∈ 𝑈)
Theorem	gruun 10892	A Grothendieck universe contains binary unions of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈) → (𝐴 ∪ 𝐵) ∈ 𝑈)
Theorem	gruxp 10893	A Grothendieck universe contains binary cartesian products of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈) → (𝐴 × 𝐵) ∈ 𝑈)
Theorem	grumap 10894	A Grothendieck universe contains all powers of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈) → (𝐴 ↑m 𝐵) ∈ 𝑈)
Theorem	gruixp 10895*	A Grothendieck universe contains indexed cartesian products of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑈) → X𝑥 ∈ 𝐴 𝐵 ∈ 𝑈)
Theorem	gruiin 10896*	A Grothendieck universe contains indexed intersections of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ ∃𝑥 ∈ 𝐴 𝐵 ∈ 𝑈) → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑈)
Theorem	gruf 10897	A Grothendieck universe contains all functions on its elements. (Contributed by Mario Carneiro, 10-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐹:𝐴⟶𝑈) → 𝐹 ∈ 𝑈)
Theorem	gruen 10898	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 10899	A nonempty Grothendieck universe is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → 𝑈 ∈ WUni)
Theorem	intgru 10900	The intersection of a family of universes is a universe. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝐴 ⊆ Univ ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ∈ Univ)