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