Theorem mnussd

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

	Ref	Expression
Hypotheses	mnussd.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\}$$
	mnussd.2	$$⊢\phi \to U\in M$$
	mnussd.3	$$⊢\phi \to A\in U$$
	mnussd.4	$$⊢\phi \to B\subseteq A$$
Assertion	mnussd	$$⊢\phi \to B\in U$$

Proof

Step	Hyp	Ref	Expression
1		mnussd.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		mnussd.2	$$⊢\phi \to U\in M$$
3		mnussd.3	$$⊢\phi \to A\in U$$
4		mnussd.4	$$⊢\phi \to B\subseteq A$$
5	1 2 3	mnuop123d	$$⊢\phi \to \left(𝒫A\subseteq U\wedge \forall f\exists w\in U\left(𝒫A\subseteq w\wedge \forall i\in A\left(\exists v\in U\left(i\in v\wedge v\in f\right)\to \exists u\in f\left(i\in u\wedge \bigcup u\subseteq w\right)\right)\right)\right)$$
6	5	simpld	$$⊢\phi \to 𝒫A\subseteq U$$
7	3 4	sselpwd	$$⊢\phi \to B\in 𝒫A$$
8	6 7	sseldd	$$⊢\phi \to B\in U$$