===== Grothendieck universe =====
==== Collection ====
| @#FFBB00: definiendum | @#FFBB00: ${\mathfrak G}$ in it |
| @#55EE55: postulate   | @#55EE55: ${\mathfrak G}$ ... set |
| @#FFFDDD: forall      | @#FFFDDD: $X\in{\mathfrak G}$ |
| @#55EE55: postulate   | @#55EE55: $\mathcal{P}(X) \subseteq{\mathfrak G}$ |
| @#FFFDDD: forall      | @#FFFDDD: $x\in X$ |
| @#55EE55: postulate   | @#55EE55: $x\in{\mathfrak G}$ |
| @#FFFDDD: exists      | @#FFFDDD: $P\in{\mathfrak G}$ |
| @#55EE55: postulate   | @#55EE55: $\mathcal{P}(X) \subseteq P$ |
| @#FFFDDD: forall      | @#FFFDDD: $Y$ ... set |
| @#55EE55: postulate   | @#55EE55: $Y \subseteq {\mathfrak G} \implies Y\ {\approx}\ {\mathfrak G}\lor Y \in {\mathfrak G} $ |

-----
=== Discussion ===
== Formalities ==
The symbol ${\approx}$ in the last postulate is an abbreviation. For subsets $Y$ of ${\mathfrak G}$, equinumerosity can be defined as the existence of a set of pairs, $f=\{\{y,u\},\{y',u'\},\dots\}$, which puts elements $y\in Y$ uniquely in correspondence with $u\in{\mathfrak G}$:

>I reverse-engineered this from the metamath page, so it needs to be checked

$Y\ {\approx}\ {\mathfrak G}\equiv\exists f. \forall x.\left((x \in Y) \implies \exists!u.\ \{x, u\} \in f\right) \land \left((x \in {\mathfrak G}\setminus Y) \implies \exists(y \in Y).\ \{y,x\} \in f\right)$

The first clause says $f$ corresponds to a function $F$ and moreover implies $F(b) \in Y \implies F(F(b))=b$. The second says $F$ is surjective into ${\mathfrak G}\setminus Y$.

>strangely, to me, the metamath defintion doesn't include transitivity in an obvious way, and I can't see it... I added it here anyway, since it's part of any other definition I've seen.

=== Reference ===
Wikipedia: 
[[http://en.wikipedia.org/wiki/Grothendieck_universe|Grothendieck universe]], [[http://en.wikipedia.org/wiki/Universe_%28mathematics%29|Universe (Mathematics)]]

They have the corresponding axiom in pure first order logic language and 6 shorter version on metamath.

Metamath: 
[[http://us.metamath.org/mpeuni/grothprim.html|grothprim]] (long),
[[http://us.metamath.org/mpeuni/axgroth5.html|axgroth5]] (the one above)

nLab: 
[[http://ncatlab.org/nlab/show/Grothendieck+universe|Grothendieck universe]]

-----
=== Requirements ===
[[Bijective function]], [[Power set]]