Theorem wun0

Description: A weak universe contains the empty set. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Hypothesis	wun0.1	$$⊢\phi \to U\in \mathrm{WUni}$$
Assertion	wun0	$$⊢\phi \to \varnothing \in U$$

Proof

Step	Hyp	Ref	Expression
1		wun0.1	$$⊢\phi \to U\in \mathrm{WUni}$$
2		iswun	$$⊢U\in \mathrm{WUni}\to \left(U\in \mathrm{WUni}\leftrightarrow \left(\mathrm{Tr}U\wedge U\ne \varnothing \wedge \forall x\in U\left(\bigcup x\in U\wedge 𝒫x\in U\wedge \forall y\in U\left\{x,y\right\}\in U\right)\right)\right)$$
3	2	ibi	$$⊢U\in \mathrm{WUni}\to \left(\mathrm{Tr}U\wedge U\ne \varnothing \wedge \forall x\in U\left(\bigcup x\in U\wedge 𝒫x\in U\wedge \forall y\in U\left\{x,y\right\}\in U\right)\right)$$
4	3	simp2d	$$⊢U\in \mathrm{WUni}\to U\ne \varnothing$$
5	1 4	syl	$$⊢\phi \to U\ne \varnothing$$
6		n0	$$⊢U\ne \varnothing \leftrightarrow \exists xx\in U$$
7	5 6	sylib	$$⊢\phi \to \exists xx\in U$$
8	1	adantr	$$⊢\left(\phi \wedge x\in U\right)\to U\in \mathrm{WUni}$$
9		simpr	$$⊢\left(\phi \wedge x\in U\right)\to x\in U$$
10		0ss	$$⊢\varnothing \subseteq x$$
11	10	a1i	$$⊢\left(\phi \wedge x\in U\right)\to \varnothing \subseteq x$$
12	8 9 11	wunss	$$⊢\left(\phi \wedge x\in U\right)\to \varnothing \in U$$
13	7 12	exlimddv	$$⊢\phi \to \varnothing \in U$$