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 )