# Metamath Proof Explorer

## Theorem elgrug

Description: Properties of a Grothendieck universe. (Contributed by Mario Carneiro, 9-Jun-2013)

Ref Expression
Assertion elgrug ${⊢}{U}\in {V}\to \left({U}\in \mathrm{Univ}↔\left(\mathrm{Tr}{U}\wedge \forall {x}\in {U}\phantom{\rule{.4em}{0ex}}\left(𝒫{x}\in {U}\wedge \forall {y}\in {U}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in {U}\wedge \forall {y}\in \left({{U}}^{{x}}\right)\phantom{\rule{.4em}{0ex}}\bigcup \mathrm{ran}{y}\in {U}\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 treq ${⊢}{u}={U}\to \left(\mathrm{Tr}{u}↔\mathrm{Tr}{U}\right)$
2 eleq2 ${⊢}{u}={U}\to \left(𝒫{x}\in {u}↔𝒫{x}\in {U}\right)$
3 eleq2 ${⊢}{u}={U}\to \left(\left\{{x},{y}\right\}\in {u}↔\left\{{x},{y}\right\}\in {U}\right)$
4 3 raleqbi1dv ${⊢}{u}={U}\to \left(\forall {y}\in {u}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in {u}↔\forall {y}\in {U}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in {U}\right)$
5 oveq1 ${⊢}{u}={U}\to {{u}}^{{x}}={{U}}^{{x}}$
6 eleq2 ${⊢}{u}={U}\to \left(\bigcup \mathrm{ran}{y}\in {u}↔\bigcup \mathrm{ran}{y}\in {U}\right)$
7 5 6 raleqbidv ${⊢}{u}={U}\to \left(\forall {y}\in \left({{u}}^{{x}}\right)\phantom{\rule{.4em}{0ex}}\bigcup \mathrm{ran}{y}\in {u}↔\forall {y}\in \left({{U}}^{{x}}\right)\phantom{\rule{.4em}{0ex}}\bigcup \mathrm{ran}{y}\in {U}\right)$
8 2 4 7 3anbi123d ${⊢}{u}={U}\to \left(\left(𝒫{x}\in {u}\wedge \forall {y}\in {u}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in {u}\wedge \forall {y}\in \left({{u}}^{{x}}\right)\phantom{\rule{.4em}{0ex}}\bigcup \mathrm{ran}{y}\in {u}\right)↔\left(𝒫{x}\in {U}\wedge \forall {y}\in {U}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in {U}\wedge \forall {y}\in \left({{U}}^{{x}}\right)\phantom{\rule{.4em}{0ex}}\bigcup \mathrm{ran}{y}\in {U}\right)\right)$
9 8 raleqbi1dv ${⊢}{u}={U}\to \left(\forall {x}\in {u}\phantom{\rule{.4em}{0ex}}\left(𝒫{x}\in {u}\wedge \forall {y}\in {u}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in {u}\wedge \forall {y}\in \left({{u}}^{{x}}\right)\phantom{\rule{.4em}{0ex}}\bigcup \mathrm{ran}{y}\in {u}\right)↔\forall {x}\in {U}\phantom{\rule{.4em}{0ex}}\left(𝒫{x}\in {U}\wedge \forall {y}\in {U}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in {U}\wedge \forall {y}\in \left({{U}}^{{x}}\right)\phantom{\rule{.4em}{0ex}}\bigcup \mathrm{ran}{y}\in {U}\right)\right)$
10 1 9 anbi12d ${⊢}{u}={U}\to \left(\left(\mathrm{Tr}{u}\wedge \forall {x}\in {u}\phantom{\rule{.4em}{0ex}}\left(𝒫{x}\in {u}\wedge \forall {y}\in {u}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in {u}\wedge \forall {y}\in \left({{u}}^{{x}}\right)\phantom{\rule{.4em}{0ex}}\bigcup \mathrm{ran}{y}\in {u}\right)\right)↔\left(\mathrm{Tr}{U}\wedge \forall {x}\in {U}\phantom{\rule{.4em}{0ex}}\left(𝒫{x}\in {U}\wedge \forall {y}\in {U}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in {U}\wedge \forall {y}\in \left({{U}}^{{x}}\right)\phantom{\rule{.4em}{0ex}}\bigcup \mathrm{ran}{y}\in {U}\right)\right)\right)$
11 df-gru ${⊢}\mathrm{Univ}=\left\{{u}|\left(\mathrm{Tr}{u}\wedge \forall {x}\in {u}\phantom{\rule{.4em}{0ex}}\left(𝒫{x}\in {u}\wedge \forall {y}\in {u}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in {u}\wedge \forall {y}\in \left({{u}}^{{x}}\right)\phantom{\rule{.4em}{0ex}}\bigcup \mathrm{ran}{y}\in {u}\right)\right)\right\}$
12 10 11 elab2g ${⊢}{U}\in {V}\to \left({U}\in \mathrm{Univ}↔\left(\mathrm{Tr}{U}\wedge \forall {x}\in {U}\phantom{\rule{.4em}{0ex}}\left(𝒫{x}\in {U}\wedge \forall {y}\in {U}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in {U}\wedge \forall {y}\in \left({{U}}^{{x}}\right)\phantom{\rule{.4em}{0ex}}\bigcup \mathrm{ran}{y}\in {U}\right)\right)\right)$