Theorem mnutrcld

Description: Minimal universes contain the elements of their elements. (Contributed by Rohan Ridenour, 13-Aug-2023)

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

Proof

Step	Hyp	Ref	Expression
1		mnutrcld.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		mnutrcld.2	$$⊢\phi \to U\in M$$
3		mnutrcld.3	$$⊢\phi \to A\in U$$
4		mnutrcld.4	$$⊢\phi \to B\in A$$
5	1 2 3	mnuunid	$$⊢\phi \to \bigcup A\in U$$
6		elssuni	$$⊢B\in A\to B\subseteq \bigcup A$$
7	4 6	syl	$$⊢\phi \to B\subseteq \bigcup A$$
8	1 2 5 7	mnussd	$$⊢\phi \to B\in U$$