Metamath Proof Explorer

Definition df-tsk

Description: The class of all Tarski classes. Tarski classes is a phrase coined by Grzegorz Bancerek in his articleTarski'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 and the equivalent axioms). Axiom A was first presented in Tarski's articleUeber 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)

Ref Expression
Assertion df-tsk ⊢Tarski=y|∀z∈y𝒫z⊆y∧∃w∈y𝒫z⊆w∧∀z∈𝒫yz≈y∨z∈y

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctsk classTarski
1 vy setvary
2 vz setvarz
3 1 cv setvary
4 2 cv setvarz
5 4 cpw class𝒫z
6 5 3 wss wff𝒫z⊆y
7 vw setvarw
8 7 cv setvarw
9 5 8 wss wff𝒫z⊆w
10 9 7 3 wrex wff∃w∈y𝒫z⊆w
11 6 10 wa wff𝒫z⊆y∧∃w∈y𝒫z⊆w
12 11 2 3 wral wff∀z∈y𝒫z⊆y∧∃w∈y𝒫z⊆w
13 3 cpw class𝒫y
14 cen class≈
15 4 3 14 wbr wffz≈y
16 4 3 wcel wffz∈y
17 15 16 wo wffz≈y∨z∈y
18 17 2 13 wral wff∀z∈𝒫yz≈y∨z∈y
19 12 18 wa wff∀z∈y𝒫z⊆y∧∃w∈y𝒫z⊆w∧∀z∈𝒫yz≈y∨z∈y
20 19 1 cab classy|∀z∈y𝒫z⊆y∧∃w∈y𝒫z⊆w∧∀z∈𝒫yz≈y∨z∈y
21 0 20 wceq wffTarski=y|∀z∈y𝒫z⊆y∧∃w∈y𝒫z⊆w∧∀z∈𝒫yz≈y∨z∈y