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 | A. l e. k ( ~P l C_ k /\ A. m E. n e. k ( ~P l C_ n /\ A. p e. l ( E. q e. k ( p e. q /\ q e. m ) -> E. r e. m ( p e. r /\ U. r C_ n ) ) ) ) }
mnupwd.2
|- ( ph -> U e. M )
mnupwd.3
|- ( ph -> A e. U )
Assertion mnupwd
|- ( ph -> ~P A e. U )

Proof

Step Hyp Ref Expression
1 mnupwd.1
 |-  M = { k | A. l e. k ( ~P l C_ k /\ A. m E. n e. k ( ~P l C_ n /\ A. p e. l ( E. q e. k ( p e. q /\ q e. m ) -> E. r e. m ( p e. r /\ U. r C_ n ) ) ) ) }
2 mnupwd.2
 |-  ( ph -> U e. M )
3 mnupwd.3
 |-  ( ph -> A e. U )
4 0ex
 |-  (/) e. _V
5 4 a1i
 |-  ( ph -> (/) e. _V )
6 1 2 3 5 mnuop23d
 |-  ( ph -> E. w e. U ( ~P A C_ w /\ A. i e. A ( E. v e. U ( i e. v /\ v e. (/) ) -> E. u e. (/) ( i e. u /\ U. u C_ w ) ) ) )
7 simpl
 |-  ( ( ~P A C_ w /\ A. i e. A ( E. v e. U ( i e. v /\ v e. (/) ) -> E. u e. (/) ( i e. u /\ U. u C_ w ) ) ) -> ~P A C_ w )
8 7 reximi
 |-  ( E. w e. U ( ~P A C_ w /\ A. i e. A ( E. v e. U ( i e. v /\ v e. (/) ) -> E. u e. (/) ( i e. u /\ U. u C_ w ) ) ) -> E. w e. U ~P A C_ w )
9 6 8 syl
 |-  ( ph -> E. w e. U ~P A C_ w )
10 1 2 9 mnuss2d
 |-  ( ph -> ~P A e. U )