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∈kp∈q∧q∈m→∃r∈mp∈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∈kp∈q∧q∈m→∃r∈mp∈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∈Ui∈v∧v∈∅→∃u∈∅i∈u∧⋃u⊆w
7 simpl ⊢𝒫A⊆w∧∀i∈A∃v∈Ui∈v∧v∈∅→∃u∈∅i∈u∧⋃u⊆w→𝒫A⊆w
8 7 reximi ⊢∃w∈U𝒫A⊆w∧∀i∈A∃v∈Ui∈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