Description: Define the universal
class. Definition 5.20 of [TakeutiZaring] p. 21.
Also Definition 2.9 of [Quine] p. 19. The
class can be described
as the "class of all sets"; vprc4440
proves that is not itself a set
in ZFC. We will frequently use the expression as a short way
to say " is a set", and isset3010 proves that this expression has the
same meaning as .
The class is called the "von
Neumann universe", however, the letter "V" is not a tribute
to the name of
von Neumann. The letter "V" was used earlier by Peano in 1889
for the
universe of sets, where the letter V is derived from the word
"Verum".
Peano's notation V was adopted by Whitehead and Russell in Principia
Mathematica for the class of all sets in 1910. For a general discussion
of the theory of classes, see
http://us.metamath.org/mpeuni/mmset.html#class.
(Contributed by NM,
5-Aug-1993.)