Theorem mnu0eld

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

	Ref	Expression
Hypotheses	mnu0eld.1	⊢ 𝑀 = { 𝑘 ∣ ∀ 𝑙 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑘 ∧ ∀ 𝑚 ∃ 𝑛 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑛 ∧ ∀ 𝑝 ∈ 𝑙 ( ∃ 𝑞 ∈ 𝑘 ( 𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚 ) → ∃ 𝑟 ∈ 𝑚 ( 𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛 ) ) ) ) }
	mnu0eld.2	⊢ ( 𝜑 → 𝑈 ∈ 𝑀 )
	mnu0eld.3	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
Assertion	mnu0eld	⊢ ( 𝜑 → ∅ ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		mnu0eld.1	⊢ 𝑀 = { 𝑘 ∣ ∀ 𝑙 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑘 ∧ ∀ 𝑚 ∃ 𝑛 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑛 ∧ ∀ 𝑝 ∈ 𝑙 ( ∃ 𝑞 ∈ 𝑘 ( 𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚 ) → ∃ 𝑟 ∈ 𝑚 ( 𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛 ) ) ) ) }
2		mnu0eld.2	⊢ ( 𝜑 → 𝑈 ∈ 𝑀 )
3		mnu0eld.3	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
4		0ss	⊢ ∅ ⊆ 𝐴
5	4	a1i	⊢ ( 𝜑 → ∅ ⊆ 𝐴 )
6	1 2 3 5	mnussd	⊢ ( 𝜑 → ∅ ∈ 𝑈 )