# Metamath Proof Explorer

## Theorem gruwun

Description: A nonempty Grothendieck universe is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Assertion gruwun ${⊢}\left({U}\in \mathrm{Univ}\wedge {U}\ne \varnothing \right)\to {U}\in \mathrm{WUni}$

### Proof

Step Hyp Ref Expression
1 grutr ${⊢}{U}\in \mathrm{Univ}\to \mathrm{Tr}{U}$
2 1 adantr ${⊢}\left({U}\in \mathrm{Univ}\wedge {U}\ne \varnothing \right)\to \mathrm{Tr}{U}$
3 simpr ${⊢}\left({U}\in \mathrm{Univ}\wedge {U}\ne \varnothing \right)\to {U}\ne \varnothing$
4 gruuni ${⊢}\left({U}\in \mathrm{Univ}\wedge {x}\in {U}\right)\to \bigcup {x}\in {U}$
5 4 adantlr ${⊢}\left(\left({U}\in \mathrm{Univ}\wedge {U}\ne \varnothing \right)\wedge {x}\in {U}\right)\to \bigcup {x}\in {U}$
6 grupw ${⊢}\left({U}\in \mathrm{Univ}\wedge {x}\in {U}\right)\to 𝒫{x}\in {U}$
7 6 adantlr ${⊢}\left(\left({U}\in \mathrm{Univ}\wedge {U}\ne \varnothing \right)\wedge {x}\in {U}\right)\to 𝒫{x}\in {U}$
8 grupr ${⊢}\left({U}\in \mathrm{Univ}\wedge {x}\in {U}\wedge {y}\in {U}\right)\to \left\{{x},{y}\right\}\in {U}$
9 8 ad4ant134 ${⊢}\left(\left(\left({U}\in \mathrm{Univ}\wedge {U}\ne \varnothing \right)\wedge {x}\in {U}\right)\wedge {y}\in {U}\right)\to \left\{{x},{y}\right\}\in {U}$
10 9 ralrimiva ${⊢}\left(\left({U}\in \mathrm{Univ}\wedge {U}\ne \varnothing \right)\wedge {x}\in {U}\right)\to \forall {y}\in {U}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in {U}$
11 5 7 10 3jca ${⊢}\left(\left({U}\in \mathrm{Univ}\wedge {U}\ne \varnothing \right)\wedge {x}\in {U}\right)\to \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)$
12 11 ralrimiva ${⊢}\left({U}\in \mathrm{Univ}\wedge {U}\ne \varnothing \right)\to \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)$
13 iswun ${⊢}{U}\in \mathrm{Univ}\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)$
14 13 adantr ${⊢}\left({U}\in \mathrm{Univ}\wedge {U}\ne \varnothing \right)\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)$
15 2 3 12 14 mpbir3and ${⊢}\left({U}\in \mathrm{Univ}\wedge {U}\ne \varnothing \right)\to {U}\in \mathrm{WUni}$