P. 105 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 10401-10500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	wundif 10401	A weak universe is closed under class difference. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝐴 ∖ 𝐵) ∈ 𝑈)
Theorem	wunint 10402	A weak universe is closed under nonempty intersections. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ∈ 𝑈)
Theorem	wunsn 10403	A weak universe is closed under singletons. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → {𝐴} ∈ 𝑈)
Theorem	wunsuc 10404	A weak universe is closed under successors. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → suc 𝐴 ∈ 𝑈)
Theorem	wun0 10405	A weak universe contains the empty set. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    ⇒   ⊢ (𝜑 → ∅ ∈ 𝑈)
Theorem	wunr1om 10406	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 10407	A weak universe contains all the finite ordinals, and hence is infinite. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    ⇒   ⊢ (𝜑 → ω ⊆ 𝑈)
Theorem	wunfi 10408	A weak universe contains all finite sets with elements drawn from the universe. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑈)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝑈)
Theorem	wunop 10409	A weak universe is closed under ordered pairs. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ⟨𝐴, 𝐵⟩ ∈ 𝑈)
Theorem	wunot 10410	A weak universe is closed under ordered triples. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ⟨𝐴, 𝐵, 𝐶⟩ ∈ 𝑈)
Theorem	wunxp 10411	A weak universe is closed under cartesian products. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝐴 × 𝐵) ∈ 𝑈)
Theorem	wunpm 10412	A weak universe is closed under partial mappings. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝐴 ↑pm 𝐵) ∈ 𝑈)
Theorem	wunmap 10413	A weak universe is closed under mappings. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝐴 ↑m 𝐵) ∈ 𝑈)
Theorem	wunf 10414	A weak universe is closed under functions with known domain and codomain. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    ⇒   ⊢ (𝜑 → 𝐹 ∈ 𝑈)
Theorem	wundm 10415	A weak universe is closed under the domain operator. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → dom 𝐴 ∈ 𝑈)
Theorem	wunrn 10416	A weak universe is closed under the range operator. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ran 𝐴 ∈ 𝑈)
Theorem	wuncnv 10417	A weak universe is closed under the converse operator. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ◡𝐴 ∈ 𝑈)
Theorem	wunres 10418	A weak universe is closed under restrictions. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝐴 ↾ 𝐵) ∈ 𝑈)
Theorem	wunfv 10419	A weak universe is closed under the function value operator. (Contributed by Mario Carneiro, 3-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝐴‘𝐵) ∈ 𝑈)
Theorem	wunco 10420	A weak universe is closed under composition. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝐴 ∘ 𝐵) ∈ 𝑈)
Theorem	wuntpos 10421	A weak universe is closed under transposition. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → tpos 𝐴 ∈ 𝑈)
Theorem	intwun 10422	The intersection of a collection of weak universes is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ ((𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ∈ WUni)
Theorem	r1limwun 10423	Each limit stage in the cumulative hierarchy is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ ((𝐴 ∈ 𝑉 ∧ Lim 𝐴) → (𝑅1‘𝐴) ∈ WUni)
Theorem	r1wunlim 10424	The weak universes in the cumulative hierarchy are exactly the limit ordinals. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝐴 ∈ 𝑉 → ((𝑅1‘𝐴) ∈ WUni ↔ Lim 𝐴))
Theorem	wunex2 10425*	Construct a weak universe from a given set. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝐹 = (rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1o)) ↾ ω)    &   ⊢ 𝑈 = ∪ ran 𝐹    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝑈 ∈ WUni ∧ 𝐴 ⊆ 𝑈))
Theorem	wunex 10426*	Construct a weak universe from a given set. See also wunex2 10425. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑢 ∈ WUni 𝐴 ⊆ 𝑢)
Theorem	uniwun 10427	Every set is contained in a weak universe. This is the analogue of grothtsk 10522 for weak universes, but it is provable in ZF without the Tarski-Grothendieck axiom, contrary to grothtsk 10522. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ ∪ WUni = V
Theorem	wunex3 10428	Construct a weak universe from a given set. This version of wunex 10426 has a simpler proof, but requires the axiom of regularity. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ 𝑈 = (𝑅1‘((rank‘𝐴) +o ω))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝑈 ∈ WUni ∧ 𝐴 ⊆ 𝑈))
Theorem	wuncval 10429*	Value of the weak universe closure operator. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝐴 ∈ 𝑉 → (wUniCl‘𝐴) = ∩ {𝑢 ∈ WUni ∣ 𝐴 ⊆ 𝑢})
Theorem	wuncid 10430	The weak universe closure of a set contains the set. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝐴 ∈ 𝑉 → 𝐴 ⊆ (wUniCl‘𝐴))
Theorem	wunccl 10431	The weak universe closure of a set is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝐴 ∈ 𝑉 → (wUniCl‘𝐴) ∈ WUni)
Theorem	wuncss 10432	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 10433	The weak universe closure is idempotent. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝐴 ∈ 𝑉 → (wUniCl‘(wUniCl‘𝐴)) = (wUniCl‘𝐴))
Theorem	wuncval2 10434*	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 10435	Extend class definition to include the class of all Tarski classes.
class Tarski
Definition	df-tsk 10436*	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 10510 and the equivalent axioms). Axiom A was first presented in Tarski's article Ueber unerreichbare Kardinalzahlen. Tarski introduced the axiom A to enable ZFC to manage inaccessible cardinals. Later Grothendieck introduced the concept of Grothendieck universes and showed they were equal to transitive Tarski classes. (Contributed by FL, 30-Dec-2010.)
⊢ Tarski = {𝑦 ∣ (∀𝑧 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ ∃𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤) ∧ ∀𝑧 ∈ 𝒫 𝑦(𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦))}
Theorem	eltskg 10437*	Properties of a Tarski class. (Contributed by FL, 30-Dec-2010.)
⊢ (𝑇 ∈ 𝑉 → (𝑇 ∈ Tarski ↔ (∀𝑧 ∈ 𝑇 (𝒫 𝑧 ⊆ 𝑇 ∧ ∃𝑤 ∈ 𝑇 𝒫 𝑧 ⊆ 𝑤) ∧ ∀𝑧 ∈ 𝒫 𝑇(𝑧 ≈ 𝑇 ∨ 𝑧 ∈ 𝑇))))
Theorem	eltsk2g 10438*	Properties of a Tarski class. (Contributed by FL, 30-Dec-2010.) (Revised by Mario Carneiro, 20-Sep-2014.)
⊢ (𝑇 ∈ 𝑉 → (𝑇 ∈ Tarski ↔ (∀𝑧 ∈ 𝑇 (𝒫 𝑧 ⊆ 𝑇 ∧ 𝒫 𝑧 ∈ 𝑇) ∧ ∀𝑧 ∈ 𝒫 𝑇(𝑧 ≈ 𝑇 ∨ 𝑧 ∈ 𝑇))))
Theorem	tskpwss 10439	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 10440	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 10441	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 10442	The empty set is a (transitive) Tarski class. (Contributed by FL, 30-Dec-2010.)
⊢ ∅ ∈ Tarski
Theorem	tsksdom 10443	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 10444	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 10445	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 10446	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 10447	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 10448	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 10449	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 10450	A nonempty Tarski class contains the empty set. (Contributed by FL, 30-Dec-2010.) (Revised by Mario Carneiro, 18-Jun-2013.)
⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) → ∅ ∈ 𝑇)
Theorem	tsk1 10451	One is an element of a nonempty Tarski class. (Contributed by FL, 22-Feb-2011.)
⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) → 1o ∈ 𝑇)
Theorem	tsk2 10452	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 10453	If a Tarski class is not empty, it has more than two elements. (Contributed by FL, 22-Feb-2011.)
⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) → 2o ≺ 𝑇)
Theorem	tskr1om 10454	A nonempty Tarski class is infinite, because it contains all the finite levels of the cumulative hierarchy. (This proof does not use ax-inf 9326.) (Contributed by Mario Carneiro, 24-Jun-2013.)
⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) → (𝑅1 “ ω) ⊆ 𝑇)
Theorem	tskr1om2 10455	A nonempty Tarski class contains the whole finite cumulative hierarchy. (This proof does not use ax-inf 9326.) (Contributed by NM, 22-Feb-2011.)
⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) → ∪ (𝑅1 “ ω) ⊆ 𝑇)
Theorem	tskinf 10456	A nonempty Tarski class is infinite. (Contributed by FL, 22-Feb-2011.)
⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) → ω ≼ 𝑇)
Theorem	tskpr 10457	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 10458	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 10459	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 10460	A Tarski class is well-orderable. (Contributed by Mario Carneiro, 20-Jun-2013.)
⊢ (𝑇 ∈ Tarski → 𝑇 ∈ dom card)
Theorem	inttsk 10461	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 10462	(𝑅1‘𝐴) for 𝐴 a strongly inaccessible cardinal is equipotent to 𝐴. (Contributed by Mario Carneiro, 6-Jun-2013.)
⊢ (𝐴 ∈ Inacc → (𝑅1‘𝐴) ≈ 𝐴)
Theorem	r1omALT 10463	Alternate proof of r1om 9931, shorter as a consequence of inar1 10462, but requiring AC. (Contributed by Mario Carneiro, 27-May-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑅1‘ω) ≈ ω
Theorem	rankcf 10464	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 10465	(𝑅1‘𝐴) for 𝐴 a strongly inaccessible cardinal is a Tarski class. (Contributed by Mario Carneiro, 8-Jun-2013.)
⊢ (𝐴 ∈ Inacc → (𝑅1‘𝐴) ∈ Tarski)
Theorem	r1omtsk 10466	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 10467	A Tarski class contains all ordinals smaller than it. (Contributed by Mario Carneiro, 8-Jun-2013.)
⊢ ((𝑇 ∈ Tarski ∧ 𝐴 ∈ On ∧ 𝐴 ≺ 𝑇) → 𝐴 ∈ 𝑇)
Theorem	tskcard 10468	An even more direct relationship than r1tskina 10469 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 10469	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 10470	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 10471	A nonempty transitive Tarski class is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝑇 ≠ ∅) → 𝑇 ∈ WUni)
Theorem	tskint 10472	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 10473	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 10474	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 10475	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 10476	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 10477	Extend class notation to include the class of all Grothendieck universes.
class Univ
Definition	df-gru 10478*	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 10479*	Properties of a Grothendieck universe. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ (𝑈 ∈ 𝑉 → (𝑈 ∈ Univ ↔ (Tr 𝑈 ∧ ∀𝑥 ∈ 𝑈 (𝒫 𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∈ 𝑈 ∧ ∀𝑦 ∈ (𝑈 ↑m 𝑥)∪ ran 𝑦 ∈ 𝑈))))
Theorem	grutr 10480	A Grothendieck universe is transitive. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝑈 ∈ Univ → Tr 𝑈)
Theorem	gruelss 10481	A Grothendieck universe is transitive, so each element is a subset of the universe. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈) → 𝐴 ⊆ 𝑈)
Theorem	grupw 10482	A Grothendieck universe contains the powerset of each of its members. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈) → 𝒫 𝐴 ∈ 𝑈)
Theorem	gruss 10483	Any subset of an element of a Grothendieck universe is also an element. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ 𝑈)
Theorem	grupr 10484	A Grothendieck universe contains pairs derived from its elements. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈) → {𝐴, 𝐵} ∈ 𝑈)
Theorem	gruurn 10485	A Grothendieck universe contains the range of any function which takes values in the universe (see gruiun 10486 for a more intuitive version). (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐹:𝐴⟶𝑈) → ∪ ran 𝐹 ∈ 𝑈)
Theorem	gruiun 10486*	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 10487	A Grothendieck universe contains unions of its elements. (Contributed by Mario Carneiro, 17-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈) → ∪ 𝐴 ∈ 𝑈)
Theorem	grurn 10488	A Grothendieck universe contains the range of any function which takes values in the universe (see gruiun 10486 for a more intuitive version). (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐹:𝐴⟶𝑈) → ran 𝐹 ∈ 𝑈)
Theorem	gruima 10489	A Grothendieck universe contains image sets drawn from its members. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ Fun 𝐹 ∧ (𝐹 “ 𝐴) ⊆ 𝑈) → (𝐴 ∈ 𝑈 → (𝐹 “ 𝐴) ∈ 𝑈))
Theorem	gruel 10490	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 10491	A Grothendieck universe contains the singletons of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈) → {𝐴} ∈ 𝑈)
Theorem	gruop 10492	A Grothendieck universe contains ordered pairs of its elements. (Contributed by Mario Carneiro, 10-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈) → ⟨𝐴, 𝐵⟩ ∈ 𝑈)
Theorem	gruun 10493	A Grothendieck universe contains binary unions of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈) → (𝐴 ∪ 𝐵) ∈ 𝑈)
Theorem	gruxp 10494	A Grothendieck universe contains binary cartesian products of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈) → (𝐴 × 𝐵) ∈ 𝑈)
Theorem	grumap 10495	A Grothendieck universe contains all powers of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈) → (𝐴 ↑m 𝐵) ∈ 𝑈)
Theorem	gruixp 10496*	A Grothendieck universe contains indexed cartesian products of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑈) → X𝑥 ∈ 𝐴 𝐵 ∈ 𝑈)
Theorem	gruiin 10497*	A Grothendieck universe contains indexed intersections of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ ∃𝑥 ∈ 𝐴 𝐵 ∈ 𝑈) → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑈)
Theorem	gruf 10498	A Grothendieck universe contains all functions on its elements. (Contributed by Mario Carneiro, 10-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐹:𝐴⟶𝑈) → 𝐹 ∈ 𝑈)
Theorem	gruen 10499	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 10500	A nonempty Grothendieck universe is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → 𝑈 ∈ WUni)