Metamath Proof Explorer

Theorem grupw

Description: A Grothendieck universe contains the powerset of each of its members. (Contributed by Mario Carneiro, 9-Jun-2013)

Ref Expression
Assertion grupw 
|- ( ( U e. Univ /\ A e. U ) -> ~P A e. U )

Proof

Step Hyp Ref Expression
1 elgrug 
 |-  ( U e. Univ -> ( U e. Univ <-> ( Tr U /\ A. y e. U ( ~P y e. U /\ A. x e. U { y , x } e. U /\ A. x e. ( U ^m y ) U. ran x e. U ) ) ) )
2 1 ibi 
 |-  ( U e. Univ -> ( Tr U /\ A. y e. U ( ~P y e. U /\ A. x e. U { y , x } e. U /\ A. x e. ( U ^m y ) U. ran x e. U ) ) )
3 2 simprd 
 |-  ( U e. Univ -> A. y e. U ( ~P y e. U /\ A. x e. U { y , x } e. U /\ A. x e. ( U ^m y ) U. ran x e. U ) )
4 simp1 
 |-  ( ( ~P y e. U /\ A. x e. U { y , x } e. U /\ A. x e. ( U ^m y ) U. ran x e. U ) -> ~P y e. U )
5 4 ralimi 
 |-  ( A. y e. U ( ~P y e. U /\ A. x e. U { y , x } e. U /\ A. x e. ( U ^m y ) U. ran x e. U ) -> A. y e. U ~P y e. U )
6 pweq 
 |-  ( y = A -> ~P y = ~P A )
7 6 eleq1d 
 |-  ( y = A -> ( ~P y e. U <-> ~P A e. U ) )
8 7 rspccv 
 |-  ( A. y e. U ~P y e. U -> ( A e. U -> ~P A e. U ) )
9 3 5 8 3syl 
 |-  ( U e. Univ -> ( A e. U -> ~P A e. U ) )
10 9 imp 
 |-  ( ( U e. Univ /\ A e. U ) -> ~P A e. U )