This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ∅ ∈ 𝑈 )