Theorem mnuprssd

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\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\}$$
	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\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		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$$