P. 107 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 10601-10700   *Has distinct variable group(s)

Type	Label	Description
Statement
4.1.2  Weak universes
Syntax	cwun 10601	Extend class definition to include the class of all weak universes.
class WUni
Syntax	cwunm 10602	Extend class definition to include the map whose value is the smallest weak universe of which the given set is a subset.
class wUniCl
Definition	df-wun 10603*	The class of all weak universes. A weak universe is a nonempty transitive class closed under union, pairing, and powerset. The advantage of weak universes over Grothendieck universes is that one can prove that every set is contained in a weak universe in ZF (see uniwun 10641) whereas the analogue for Grothendieck universes requires ax-groth 10724 (see grothtsk 10736). (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ WUni = {𝑢 ∣ (Tr 𝑢 ∧ 𝑢 ≠ ∅ ∧ ∀𝑥 ∈ 𝑢 (∪ 𝑥 ∈ 𝑢 ∧ 𝒫 𝑥 ∈ 𝑢 ∧ ∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢))}
Definition	df-wunc 10604*	A function that maps a set 𝑥 to the smallest weak universe that contains the elements of the set. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ wUniCl = (𝑥 ∈ V ↦ ∩ {𝑢 ∈ WUni ∣ 𝑥 ⊆ 𝑢})
Theorem	iswun 10605*	Properties of a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝑈 ∈ 𝑉 → (𝑈 ∈ WUni ↔ (Tr 𝑈 ∧ 𝑈 ≠ ∅ ∧ ∀𝑥 ∈ 𝑈 (∪ 𝑥 ∈ 𝑈 ∧ 𝒫 𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∈ 𝑈))))
Theorem	wuntr 10606	A weak universe is transitive. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝑈 ∈ WUni → Tr 𝑈)
Theorem	wununi 10607	A weak universe is closed under union. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ∪ 𝐴 ∈ 𝑈)
Theorem	wunpw 10608	A weak universe is closed under powerset. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → 𝒫 𝐴 ∈ 𝑈)
Theorem	wunelss 10609	The elements of a weak universe are also subsets of it. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝑈)
Theorem	wunpr 10610	A weak universe is closed under pairing. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    ⇒   ⊢ (𝜑 → {𝐴, 𝐵} ∈ 𝑈)
Theorem	wunun 10611	A weak universe is closed under binary union. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝐴 ∪ 𝐵) ∈ 𝑈)
Theorem	wuntp 10612	A weak universe is closed under unordered triple. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    ⇒   ⊢ (𝜑 → {𝐴, 𝐵, 𝐶} ∈ 𝑈)
Theorem	wunss 10613	A weak universe is closed under subsets. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → 𝐵 ∈ 𝑈)
Theorem	wunin 10614	A weak universe is closed under binary intersections. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝐴 ∩ 𝐵) ∈ 𝑈)
Theorem	wundif 10615	A weak universe is closed under class difference. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝐴 ∖ 𝐵) ∈ 𝑈)
Theorem	wunint 10616	A weak universe is closed under nonempty intersections. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ∈ 𝑈)
Theorem	wunsn 10617	A weak universe is closed under singletons. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → {𝐴} ∈ 𝑈)
Theorem	wunsuc 10618	A weak universe is closed under successors. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → suc 𝐴 ∈ 𝑈)
Theorem	wun0 10619	A weak universe contains the empty set. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    ⇒   ⊢ (𝜑 → ∅ ∈ 𝑈)
Theorem	wunr1om 10620	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 10621	A weak universe contains all the finite ordinals, and hence is infinite. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    ⇒   ⊢ (𝜑 → ω ⊆ 𝑈)
Theorem	wunfi 10622	A weak universe contains all finite sets with elements drawn from the universe. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑈)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝑈)
Theorem	wunop 10623	A weak universe is closed under ordered pairs. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ⟨𝐴, 𝐵⟩ ∈ 𝑈)
Theorem	wunot 10624	A weak universe is closed under ordered triples. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ⟨𝐴, 𝐵, 𝐶⟩ ∈ 𝑈)
Theorem	wunxp 10625	A weak universe is closed under cartesian products. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝐴 × 𝐵) ∈ 𝑈)
Theorem	wunpm 10626	A weak universe is closed under partial mappings. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝐴 ↑pm 𝐵) ∈ 𝑈)
Theorem	wunmap 10627	A weak universe is closed under mappings. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝐴 ↑m 𝐵) ∈ 𝑈)
Theorem	wunf 10628	A weak universe is closed under functions with known domain and codomain. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    ⇒   ⊢ (𝜑 → 𝐹 ∈ 𝑈)
Theorem	wundm 10629	A weak universe is closed under the domain operator. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → dom 𝐴 ∈ 𝑈)
Theorem	wunrn 10630	A weak universe is closed under the range operator. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ran 𝐴 ∈ 𝑈)
Theorem	wuncnv 10631	A weak universe is closed under the converse operator. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ◡𝐴 ∈ 𝑈)
Theorem	wunres 10632	A weak universe is closed under restrictions. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝐴 ↾ 𝐵) ∈ 𝑈)
Theorem	wunfv 10633	A weak universe is closed under the function value operator. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝐴‘𝐵) ∈ 𝑈)
Theorem	wunco 10634	A weak universe is closed under composition. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝐴 ∘ 𝐵) ∈ 𝑈)
Theorem	wuntpos 10635	A weak universe is closed under transposition. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → tpos 𝐴 ∈ 𝑈)
Theorem	intwun 10636	The intersection of a collection of weak universes is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ ((𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ∈ WUni)
Theorem	r1limwun 10637	Each limit stage in the cumulative hierarchy is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ ((𝐴 ∈ 𝑉 ∧ Lim 𝐴) → (𝑅1‘𝐴) ∈ WUni)
Theorem	r1wunlim 10638	The weak universes in the cumulative hierarchy are exactly the limit ordinals. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝐴 ∈ 𝑉 → ((𝑅1‘𝐴) ∈ WUni ↔ Lim 𝐴))
Theorem	wunex2 10639*	Construct a weak universe from a given set. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐹 = (rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1o)) ↾ ω)    &   ⊢ 𝑈 = ∪ ran 𝐹    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝑈 ∈ WUni ∧ 𝐴 ⊆ 𝑈))
Theorem	wunex 10640*	Construct a weak universe from a given set. See also wunex2 10639. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑢 ∈ WUni 𝐴 ⊆ 𝑢)
Theorem	uniwun 10641	Every set is contained in a weak universe. This is the analogue of grothtsk 10736 for weak universes, but it is provable in ZF without the Tarski-Grothendieck axiom, contrary to grothtsk 10736. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ ∪ WUni = V
Theorem	wunex3 10642	Construct a weak universe from a given set. This version of wunex 10640 has a simpler proof, but requires the axiom of regularity. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝑈 = (𝑅1‘((rank‘𝐴) +o ω))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝑈 ∈ WUni ∧ 𝐴 ⊆ 𝑈))
Theorem	wuncval 10643*	Value of the weak universe closure operator. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝐴 ∈ 𝑉 → (wUniCl‘𝐴) = ∩ {𝑢 ∈ WUni ∣ 𝐴 ⊆ 𝑢})
Theorem	wuncid 10644	The weak universe closure of a set contains the set. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝐴 ∈ 𝑉 → 𝐴 ⊆ (wUniCl‘𝐴))
Theorem	wunccl 10645	The weak universe closure of a set is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝐴 ∈ 𝑉 → (wUniCl‘𝐴) ∈ WUni)
Theorem	wuncss 10646	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 10647	The weak universe closure is idempotent. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝐴 ∈ 𝑉 → (wUniCl‘(wUniCl‘𝐴)) = (wUniCl‘𝐴))
Theorem	wuncval2 10648*	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 10649	Extend class definition to include the class of all Tarski classes.
class Tarski
Definition	df-tsk 10650*	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 10724 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 10651*	Properties of a Tarski class. (Contributed by FL, 30-Dec-2010.)
⊢ (𝑇 ∈ 𝑉 → (𝑇 ∈ Tarski ↔ (∀𝑧 ∈ 𝑇 (𝒫 𝑧 ⊆ 𝑇 ∧ ∃𝑤 ∈ 𝑇 𝒫 𝑧 ⊆ 𝑤) ∧ ∀𝑧 ∈ 𝒫 𝑇(𝑧 ≈ 𝑇 ∨ 𝑧 ∈ 𝑇))))
Theorem	eltsk2g 10652*	Properties of a Tarski class. (Contributed by FL, 30-Dec-2010.) (Revised by Mario Carneiro, 20-Sep-2014.)
⊢ (𝑇 ∈ 𝑉 → (𝑇 ∈ Tarski ↔ (∀𝑧 ∈ 𝑇 (𝒫 𝑧 ⊆ 𝑇 ∧ 𝒫 𝑧 ∈ 𝑇) ∧ ∀𝑧 ∈ 𝒫 𝑇(𝑧 ≈ 𝑇 ∨ 𝑧 ∈ 𝑇))))
Theorem	tskpwss 10653	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 10654	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 10655	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 10656	The empty set is a (transitive) Tarski class. (Contributed by FL, 30-Dec-2010.)
⊢ ∅ ∈ Tarski
Theorem	tsksdom 10657	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 10658	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 10659	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 10660	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 10661	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 10662	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 10663	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 10664	A nonempty Tarski class contains the empty set. (Contributed by FL, 30-Dec-2010.) (Revised by Mario Carneiro, 18-Jun-2013.)
⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) → ∅ ∈ 𝑇)
Theorem	tsk1 10665	One is an element of a nonempty Tarski class. (Contributed by FL, 22-Feb-2011.)
⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) → 1o ∈ 𝑇)
Theorem	tsk2 10666	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 10667	If a Tarski class is not empty, it has more than two elements. (Contributed by FL, 22-Feb-2011.)
⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) → 2o ≺ 𝑇)
Theorem	tskr1om 10668	A nonempty Tarski class is infinite, because it contains all the finite levels of the cumulative hierarchy. (This proof does not use ax-inf 9538.) (Contributed by Mario Carneiro, 24-Jun-2013.)
⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) → (𝑅1 “ ω) ⊆ 𝑇)
Theorem	tskr1om2 10669	A nonempty Tarski class contains the whole finite cumulative hierarchy. (This proof does not use ax-inf 9538.) (Contributed by NM, 22-Feb-2011.)
⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) → ∪ (𝑅1 “ ω) ⊆ 𝑇)
Theorem	tskinf 10670	A nonempty Tarski class is infinite. (Contributed by FL, 22-Feb-2011.)
⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) → ω ≼ 𝑇)
Theorem	tskpr 10671	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 10672	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 10673	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 10674	A Tarski class is well-orderable. (Contributed by Mario Carneiro, 20-Jun-2013.)
⊢ (𝑇 ∈ Tarski → 𝑇 ∈ dom card)
Theorem	inttsk 10675	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 10676	(𝑅1‘𝐴) for 𝐴 a strongly inaccessible cardinal is equipotent to 𝐴. (Contributed by Mario Carneiro, 6-Jun-2013.)
⊢ (𝐴 ∈ Inacc → (𝑅1‘𝐴) ≈ 𝐴)
Theorem	r1omALT 10677	Alternate proof of r1om 10144, shorter as a consequence of inar1 10676, but requiring AC. (Contributed by Mario Carneiro, 27-May-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑅1‘ω) ≈ ω
Theorem	rankcf 10678	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 10679	(𝑅1‘𝐴) for 𝐴 a strongly inaccessible cardinal is a Tarski class. (Contributed by Mario Carneiro, 8-Jun-2013.)
⊢ (𝐴 ∈ Inacc → (𝑅1‘𝐴) ∈ Tarski)
Theorem	r1omtsk 10680	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 10681	A Tarski class contains all ordinals smaller than it. (Contributed by Mario Carneiro, 8-Jun-2013.)
⊢ ((𝑇 ∈ Tarski ∧ 𝐴 ∈ On ∧ 𝐴 ≺ 𝑇) → 𝐴 ∈ 𝑇)
Theorem	tskcard 10682	An even more direct relationship than r1tskina 10683 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 10683	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 10684	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 10685	A nonempty transitive Tarski class is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝑇 ≠ ∅) → 𝑇 ∈ WUni)
Theorem	tskint 10686	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 10687	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 10688	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 10689	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 10690	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 10691	Extend class notation to include the class of all Grothendieck universes.
class Univ
Definition	df-gru 10692*	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 10693*	Properties of a Grothendieck universe. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ (𝑈 ∈ 𝑉 → (𝑈 ∈ Univ ↔ (Tr 𝑈 ∧ ∀𝑥 ∈ 𝑈 (𝒫 𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∈ 𝑈 ∧ ∀𝑦 ∈ (𝑈 ↑m 𝑥)∪ ran 𝑦 ∈ 𝑈))))
Theorem	grutr 10694	A Grothendieck universe is transitive. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝑈 ∈ Univ → Tr 𝑈)
Theorem	gruelss 10695	A Grothendieck universe is transitive, so each element is a subset of the universe. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈) → 𝐴 ⊆ 𝑈)
Theorem	grupw 10696	A Grothendieck universe contains the powerset of each of its members. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈) → 𝒫 𝐴 ∈ 𝑈)
Theorem	gruss 10697	Any subset of an element of a Grothendieck universe is also an element. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ 𝑈)
Theorem	grupr 10698	A Grothendieck universe contains pairs derived from its elements. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈) → {𝐴, 𝐵} ∈ 𝑈)
Theorem	gruurn 10699	A Grothendieck universe contains the range of any function which takes values in the universe (see gruiun 10700 for a more intuitive version). (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐹:𝐴⟶𝑈) → ∪ ran 𝐹 ∈ 𝑈)
Theorem	gruiun 10700*	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 ∧ 𝐴 ∈ 𝑈 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑈) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑈)