This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem wunpw

Description: A weak universe is closed under powerset. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses wununi.1 
|- ( ph -> U e. WUni )
wununi.2 
|- ( ph -> A e. U )
Assertion wunpw 
|- ( ph -> ~P A e. U )

Proof

Step Hyp Ref Expression
1 wununi.1 
 |-  ( ph -> U e. WUni )
2 wununi.2 
 |-  ( ph -> A e. U )
3 pweq 
 |-  ( x = A -> ~P x = ~P A )
4 3 eleq1d 
 |-  ( x = A -> ( ~P x e. U <-> ~P A e. U ) )
5 iswun 
 |-  ( U e. WUni -> ( U e. WUni <-> ( Tr U /\ U =/= (/) /\ A. x e. U ( U. x e. U /\ ~P x e. U /\ A. y e. U { x , y } e. U ) ) ) )
6 5 ibi 
 |-  ( U e. WUni -> ( Tr U /\ U =/= (/) /\ A. x e. U ( U. x e. U /\ ~P x e. U /\ A. y e. U { x , y } e. U ) ) )
7 6 simp3d 
 |-  ( U e. WUni -> A. x e. U ( U. x e. U /\ ~P x e. U /\ A. y e. U { x , y } e. U ) )
8 simp2 
 |-  ( ( U. x e. U /\ ~P x e. U /\ A. y e. U { x , y } e. U ) -> ~P x e. U )
9 8 ralimi 
 |-  ( A. x e. U ( U. x e. U /\ ~P x e. U /\ A. y e. U { x , y } e. U ) -> A. x e. U ~P x e. U )
10 1 7 9 3syl 
 |-  ( ph -> A. x e. U ~P x e. U )
11 4 10 2 rspcdva 
 |-  ( ph -> ~P A e. U )