wun0

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

		Ref	Expression
	Hypothesis	wun0.1	$⊢ φ \to U \in WUni$
	Assertion	wun0	$⊢ φ \to \emptyset \in U$

Step	Hyp	Ref	Expression
1		wun0.1	$⊢ φ \to U \in WUni$
2		iswun	$⊢ U \in WUni \to (U \in WUni \leftrightarrow (Tr U \land U \neq \emptyset \land \forall x \in U (⋃ x \in U \land 𝒫 x \in U \land \forall y \in U \{x, y\} \in U)))$
3	2	ibi	$⊢ U \in WUni \to (Tr U \land U \neq \emptyset \land \forall x \in U (⋃ x \in U \land 𝒫 x \in U \land \forall y \in U \{x, y\} \in U))$
4	3	simp2d	$⊢ U \in WUni \to U \neq \emptyset$
5	1 4	syl	$⊢ φ \to U \neq \emptyset$
6		n0	$⊢ U \neq \emptyset \leftrightarrow \exists x x \in U$
7	5 6	sylib	$⊢ φ \to \exists x x \in U$
8	1	adantr	$⊢ (φ \land x \in U) \to U \in WUni$
9		simpr	$⊢ (φ \land x \in U) \to x \in U$
10		0ss	$⊢ \emptyset \subseteq x$
11	10	a1i	$⊢ (φ \land x \in U) \to \emptyset \subseteq x$
12	8 9 11	wunss	$⊢ (φ \land x \in U) \to \emptyset \in U$
13	7 12	exlimddv	$⊢ φ \to \emptyset \in U$

Metamath Proof Explorer