a set x. Let x0 = x, and for each n, let be the union of the elements of xn. Let y = . By (C), there is a strongly inaccessible cardinal such that |y| < κ. Let be the universe of the previous paragraph. x is strictly of type κ, so . To show that the universe axiom (U) implies the large cardinal axiom (C), choose a cardinal . is a set, so it is an element of a Grothendieck universe U. The cardinality of U is strongly inaccessible and strictly larger than that of . In fact, any Grothendieck universe is of the form for some . This gives another form of the equivalence between Grothendieck universes and strongly inaccessible cardinals: For any Grothendieck universe U, |U| is either zero, , or a strongly inaccessible cardinal. And if is zero, , or a strongly inaccessible cardinal, then there is a Grothendieck universe . Furthermore, u(|U|) = U, and |u(κ)| = κ. Since the existence of strongly inaccessible cardinals cannot be proved from the axioms of Zermelo–Fraenkel set theory (ZFC), the existence of universes other than the empty set and cannot be proved from ZFC either. However, strongly inaccessible cardinals are on the lower end of the list of large cardinals; thus, most set theories that use large cardinals (such as "ZFC plus there is a measurable cardinal", "ZFC plus there are infinitely many Woodin cardinals") will prove that Grothendieck universes exist. See also Constructible universe Universe (mathematics) Von Neumann universe Notes References Set-theoretic universes Category theory Large cardinals