Theorem mnuund

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

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

Proof

Step	Hyp	Ref	Expression
1		mnuund.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		mnuund.2	$$⊢\phi \to U\in M$$
3		mnuund.3	$$⊢\phi \to A\in U$$
4		mnuund.4	$$⊢\phi \to B\in U$$
5		uniprg	$$⊢\left(A\in U\wedge B\in U\right)\to \bigcup \left\{A,B\right\}=A\cup B$$
6	3 4 5	syl2anc	$$⊢\phi \to \bigcup \left\{A,B\right\}=A\cup B$$
7	1 2 3 4	mnuprd	$$⊢\phi \to \left\{A,B\right\}\in U$$
8	1 2 7	mnuunid	$$⊢\phi \to \bigcup \left\{A,B\right\}\in U$$
9	6 8	eqeltrrd	$$⊢\phi \to A\cup B\in U$$