Metamath Proof Explorer

Theorem mnu0eld

Description: A nonempty minimal universe contains the empty set. (Contributed by Rohan Ridenour, 13-Aug-2023)

Ref Expression
Hypotheses mnu0eld.1 ⊢ M = k | ∀ l ∈ k 𝒫 l ⊆ k ∧ ∀ m ∃ n ∈ k 𝒫 l ⊆ n ∧ ∀ p ∈ l ∃ q ∈ k p ∈ q ∧ q ∈ m → ∃ r ∈ m p ∈ r ∧ ⋃ r ⊆ n
mnu0eld.2 ⊢ φ → U ∈ M
mnu0eld.3 ⊢ φ → A ∈ U
Assertion mnu0eld ⊢ φ → ∅ ∈ U

Proof

Step Hyp Ref Expression
1 mnu0eld.1 ⊢ M = k | ∀ l ∈ k 𝒫 l ⊆ k ∧ ∀ m ∃ n ∈ k 𝒫 l ⊆ n ∧ ∀ p ∈ l ∃ q ∈ k p ∈ q ∧ q ∈ m → ∃ r ∈ m p ∈ r ∧ ⋃ r ⊆ n
2 mnu0eld.2 ⊢ φ → U ∈ M
3 mnu0eld.3 ⊢ φ → A ∈ U
4 0ss ⊢ ∅ ⊆ A
5 4 a1i ⊢ φ → ∅ ⊆ A
6 1 2 3 5 mnussd ⊢ φ → ∅ ∈ U