Theorem wun0

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

	Ref	Expression
Hypothesis	wun0.1	⊢ ( 𝜑 → 𝑈 ∈ WUni )
Assertion	wun0	⊢ ( 𝜑 → ∅ ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		wun0.1	⊢ ( 𝜑 → 𝑈 ∈ WUni )
2		iswun	⊢ ( 𝑈 ∈ WUni → ( 𝑈 ∈ WUni ↔ ( Tr 𝑈 ∧ 𝑈 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑈 ( ∪ 𝑥 ∈ 𝑈 ∧ 𝒫 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ) ) ) )
3	2	ibi	⊢ ( 𝑈 ∈ WUni → ( Tr 𝑈 ∧ 𝑈 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑈 ( ∪ 𝑥 ∈ 𝑈 ∧ 𝒫 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ) ) )
4	3	simp2d	⊢ ( 𝑈 ∈ WUni → 𝑈 ≠ ∅ )
5	1 4	syl	⊢ ( 𝜑 → 𝑈 ≠ ∅ )
6		n0	⊢ ( 𝑈 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝑈 )
7	5 6	sylib	⊢ ( 𝜑 → ∃ 𝑥 𝑥 ∈ 𝑈 )
8	1	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) → 𝑈 ∈ WUni )
9		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) → 𝑥 ∈ 𝑈 )
10		0ss	⊢ ∅ ⊆ 𝑥
11	10	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) → ∅ ⊆ 𝑥 )
12	8 9 11	wunss	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) → ∅ ∈ 𝑈 )
13	7 12	exlimddv	⊢ ( 𝜑 → ∅ ∈ 𝑈 )