Theorem mnusnd

Description: Minimal universes are closed under singletons. (Contributed by Rohan Ridenour, 13-Aug-2023)

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

Proof

Step	Hyp	Ref	Expression
1		mnusnd.1	$$⊢M=\left\{k|\forall l\in k\left(𝒫l\subseteq k\wedge \forall m\exists n\in k\left(𝒫l\subseteq n\wedge \forall p\in l\left(\exists q\in k\left(p\in q\wedge q\in m\right)\to \exists r\in m\left(p\in r\wedge \bigcup r\subseteq n\right)\right)\right)\right)\right\}$$
2		mnusnd.2	$$⊢\phi \to U\in M$$
3		mnusnd.3	$$⊢\phi \to A\in U$$
4	1 2 3	mnupwd	$$⊢\phi \to 𝒫A\in U$$
5		snsspw	$$⊢\left\{A\right\}\subseteq 𝒫A$$
6	5	a1i	$$⊢\phi \to \left\{A\right\}\subseteq 𝒫A$$
7	1 2 4 6	mnussd	$$⊢\phi \to \left\{A\right\}\in U$$