# Metamath Proof Explorer

## Theorem mnu0eld

Description: A nonempty minimal universe contains the empty set. (Contributed by Rohan Ridenour, 13-Aug-2023)

Ref Expression
Hypotheses mnu0eld.1 ${⊢}{M}=\left\{{k}|\forall {l}\in {k}\phantom{\rule{.4em}{0ex}}\left(𝒫{l}\subseteq {k}\wedge \forall {m}\phantom{\rule{.4em}{0ex}}\exists {n}\in {k}\phantom{\rule{.4em}{0ex}}\left(𝒫{l}\subseteq {n}\wedge \forall {p}\in {l}\phantom{\rule{.4em}{0ex}}\left(\exists {q}\in {k}\phantom{\rule{.4em}{0ex}}\left({p}\in {q}\wedge {q}\in {m}\right)\to \exists {r}\in {m}\phantom{\rule{.4em}{0ex}}\left({p}\in {r}\wedge \bigcup {r}\subseteq {n}\right)\right)\right)\right)\right\}$
mnu0eld.2 ${⊢}{\phi }\to {U}\in {M}$
mnu0eld.3 ${⊢}{\phi }\to {A}\in {U}$
Assertion mnu0eld ${⊢}{\phi }\to \varnothing \in {U}$

### Proof

Step Hyp Ref Expression
1 mnu0eld.1 ${⊢}{M}=\left\{{k}|\forall {l}\in {k}\phantom{\rule{.4em}{0ex}}\left(𝒫{l}\subseteq {k}\wedge \forall {m}\phantom{\rule{.4em}{0ex}}\exists {n}\in {k}\phantom{\rule{.4em}{0ex}}\left(𝒫{l}\subseteq {n}\wedge \forall {p}\in {l}\phantom{\rule{.4em}{0ex}}\left(\exists {q}\in {k}\phantom{\rule{.4em}{0ex}}\left({p}\in {q}\wedge {q}\in {m}\right)\to \exists {r}\in {m}\phantom{\rule{.4em}{0ex}}\left({p}\in {r}\wedge \bigcup {r}\subseteq {n}\right)\right)\right)\right)\right\}$
2 mnu0eld.2 ${⊢}{\phi }\to {U}\in {M}$
3 mnu0eld.3 ${⊢}{\phi }\to {A}\in {U}$
4 0ss ${⊢}\varnothing \subseteq {A}$
5 4 a1i ${⊢}{\phi }\to \varnothing \subseteq {A}$
6 1 2 3 5 mnussd ${⊢}{\phi }\to \varnothing \in {U}$