Metamath Proof Explorer

Theorem mnupwd

Description: Minimal universes are closed under powersets. (Contributed by Rohan Ridenour, 13-Aug-2023)

Ref Expression
Hypotheses mnupwd.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
mnupwd.2 ⊢ φ → U ∈ M
mnupwd.3 ⊢ φ → A ∈ U
Assertion mnupwd ⊢ φ → 𝒫 A ∈ U

Proof

Step Hyp Ref Expression
1 mnupwd.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 mnupwd.2 ⊢ φ → U ∈ M
3 mnupwd.3 ⊢ φ → A ∈ U
4 0ex ⊢ ∅ ∈ V
5 4 a1i ⊢ φ → ∅ ∈ V
6 1 2 3 5 mnuop23d ⊢ φ → ∃ w ∈ U 𝒫 A ⊆ w ∧ ∀ i ∈ A ∃ v ∈ U i ∈ v ∧ v ∈ ∅ → ∃ u ∈ ∅ i ∈ u ∧ ⋃ u ⊆ w
7 simpl ⊢ 𝒫 A ⊆ w ∧ ∀ i ∈ A ∃ v ∈ U i ∈ v ∧ v ∈ ∅ → ∃ u ∈ ∅ i ∈ u ∧ ⋃ u ⊆ w → 𝒫 A ⊆ w
8 7 reximi ⊢ ∃ w ∈ U 𝒫 A ⊆ w ∧ ∀ i ∈ A ∃ v ∈ U i ∈ v ∧ v ∈ ∅ → ∃ u ∈ ∅ i ∈ u ∧ ⋃ u ⊆ w → ∃ w ∈ U 𝒫 A ⊆ w
9 6 8 syl ⊢ φ → ∃ w ∈ U 𝒫 A ⊆ w
10 1 2 9 mnuss2d ⊢ φ → 𝒫 A ∈ U