# Metamath Proof Explorer

## Theorem iswun

Description: Properties of a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017)

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

### Proof

Step Hyp Ref Expression
1 treq ${⊢}{u}={U}\to \left(\mathrm{Tr}{u}↔\mathrm{Tr}{U}\right)$
2 neeq1 ${⊢}{u}={U}\to \left({u}\ne \varnothing ↔{U}\ne \varnothing \right)$
3 eleq2 ${⊢}{u}={U}\to \left(\bigcup {x}\in {u}↔\bigcup {x}\in {U}\right)$
4 eleq2 ${⊢}{u}={U}\to \left(𝒫{x}\in {u}↔𝒫{x}\in {U}\right)$
5 eleq2 ${⊢}{u}={U}\to \left(\left\{{x},{y}\right\}\in {u}↔\left\{{x},{y}\right\}\in {U}\right)$
6 5 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)$
7 3 4 6 3anbi123d ${⊢}{u}={U}\to \left(\left(\bigcup {x}\in {u}\wedge 𝒫{x}\in {u}\wedge \forall {y}\in {u}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in {u}\right)↔\left(\bigcup {x}\in {U}\wedge 𝒫{x}\in {U}\wedge \forall {y}\in {U}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in {U}\right)\right)$
8 7 raleqbi1dv ${⊢}{u}={U}\to \left(\forall {x}\in {u}\phantom{\rule{.4em}{0ex}}\left(\bigcup {x}\in {u}\wedge 𝒫{x}\in {u}\wedge \forall {y}\in {u}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in {u}\right)↔\forall {x}\in {U}\phantom{\rule{.4em}{0ex}}\left(\bigcup {x}\in {U}\wedge 𝒫{x}\in {U}\wedge \forall {y}\in {U}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in {U}\right)\right)$
9 1 2 8 3anbi123d ${⊢}{u}={U}\to \left(\left(\mathrm{Tr}{u}\wedge {u}\ne \varnothing \wedge \forall {x}\in {u}\phantom{\rule{.4em}{0ex}}\left(\bigcup {x}\in {u}\wedge 𝒫{x}\in {u}\wedge \forall {y}\in {u}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in {u}\right)\right)↔\left(\mathrm{Tr}{U}\wedge {U}\ne \varnothing \wedge \forall {x}\in {U}\phantom{\rule{.4em}{0ex}}\left(\bigcup {x}\in {U}\wedge 𝒫{x}\in {U}\wedge \forall {y}\in {U}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in {U}\right)\right)\right)$
10 df-wun ${⊢}\mathrm{WUni}=\left\{{u}|\left(\mathrm{Tr}{u}\wedge {u}\ne \varnothing \wedge \forall {x}\in {u}\phantom{\rule{.4em}{0ex}}\left(\bigcup {x}\in {u}\wedge 𝒫{x}\in {u}\wedge \forall {y}\in {u}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in {u}\right)\right)\right\}$
11 9 10 elab2g ${⊢}{U}\in {V}\to \left({U}\in \mathrm{WUni}↔\left(\mathrm{Tr}{U}\wedge {U}\ne \varnothing \wedge \forall {x}\in {U}\phantom{\rule{.4em}{0ex}}\left(\bigcup {x}\in {U}\wedge 𝒫{x}\in {U}\wedge \forall {y}\in {U}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in {U}\right)\right)\right)$