Metamath Proof Explorer

Description: A minimal universe contains pairs of subsets of an element of the universe. (Contributed by Rohan Ridenour, 13-Aug-2023)

Ref Expression
Hypotheses mnuprssd.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\}$
mnuprssd.2 ${⊢}{\phi }\to {U}\in {M}$
mnuprssd.3 ${⊢}{\phi }\to {C}\in {U}$
mnuprssd.4 ${⊢}{\phi }\to {A}\subseteq {C}$
mnuprssd.5 ${⊢}{\phi }\to {B}\subseteq {C}$
Assertion mnuprssd ${⊢}{\phi }\to \left\{{A},{B}\right\}\in {U}$

Proof

Step Hyp Ref Expression
1 mnuprssd.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 mnuprssd.2 ${⊢}{\phi }\to {U}\in {M}$
3 mnuprssd.3 ${⊢}{\phi }\to {C}\in {U}$
4 mnuprssd.4 ${⊢}{\phi }\to {A}\subseteq {C}$
5 mnuprssd.5 ${⊢}{\phi }\to {B}\subseteq {C}$
6 1 2 3 mnupwd ${⊢}{\phi }\to 𝒫{C}\in {U}$
7 3 4 sselpwd ${⊢}{\phi }\to {A}\in 𝒫{C}$
8 3 5 sselpwd ${⊢}{\phi }\to {B}\in 𝒫{C}$
9 7 8 prssd ${⊢}{\phi }\to \left\{{A},{B}\right\}\subseteq 𝒫{C}$
10 1 2 6 9 mnussd ${⊢}{\phi }\to \left\{{A},{B}\right\}\in {U}$