Theorem wunun

Description: A weak universe is closed under binary union. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Hypotheses	wununi.1	$$⊢\phi \to U\in \mathrm{WUni}$$
	wununi.2	$$⊢\phi \to A\in U$$
	wunpr.3	$$⊢\phi \to B\in U$$
Assertion	wunun	$$⊢\phi \to A\cup B\in U$$

Proof

Step	Hyp	Ref	Expression
1		wununi.1	$$⊢\phi \to U\in \mathrm{WUni}$$
2		wununi.2	$$⊢\phi \to A\in U$$
3		wunpr.3	$$⊢\phi \to B\in U$$
4		uniprg	$$⊢\left(A\in U\wedge B\in U\right)\to \bigcup \left\{A,B\right\}=A\cup B$$
5	2 3 4	syl2anc	$$⊢\phi \to \bigcup \left\{A,B\right\}=A\cup B$$
6	1 2 3	wunpr	$$⊢\phi \to \left\{A,B\right\}\in U$$
7	1 6	wununi	$$⊢\phi \to \bigcup \left\{A,B\right\}\in U$$
8	5 7	eqeltrrd	$$⊢\phi \to A\cup B\in U$$