Theorem wunint

Description: A weak universe is closed under nonempty intersections. (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$$
Assertion	wunint	$$⊢\left(\phi \wedge A\ne \varnothing \right)\to \bigcap A\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	1	adantr	$$⊢\left(\phi \wedge A\ne \varnothing \right)\to U\in \mathrm{WUni}$$
4	1 2	wununi	$$⊢\phi \to \bigcup A\in U$$
5	4	adantr	$$⊢\left(\phi \wedge A\ne \varnothing \right)\to \bigcup A\in U$$
6		intssuni	$$⊢A\ne \varnothing \to \bigcap A\subseteq \bigcup A$$
7	6	adantl	$$⊢\left(\phi \wedge A\ne \varnothing \right)\to \bigcap A\subseteq \bigcup A$$
8	3 5 7	wunss	$$⊢\left(\phi \wedge A\ne \varnothing \right)\to \bigcap A\in U$$