Did Grothendieck prove that Grothendieck universes are equivalent to transitive Tarski classes?

122 Views Asked by At

There is a page in Metamath (updated link) that claims the following:

Later Grothendieck invented the concept of Grothendieck's universes and showed they were equal to transitive Tarski's classes.

Transitive Tarski classes are mentioned, e.g. in this post. A Tarski class $U$ satisfies the following conditions (given here):

  1. If $A\in U$ and $B \subseteq A$, then $B \in U$;
  2. If $A\in U$, then $P(A)\in U$;
  3. If $A \subseteq U$, and $|A|\neq|U|$, then $A \in U$.

A transitive Tarski class additionally satisfies:

  1. If $A\in U$ and $a\in A$, then $a\in U$.

Is anyone aware of the exact reference for this claim? Or, in other words: Where can I find Grothendieck's proof?