Metamath Proof Explorer

Theorem grumap

Description: A Grothendieck universe contains all powers of its elements. (Contributed by Mario Carneiro, 9-Jun-2013)

Ref Expression
Assertion grumap 
|- ( ( U e. Univ /\ A e. U /\ B e. U ) -> ( A ^m B ) e. U )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( U e. Univ /\ A e. U /\ B e. U ) -> U e. Univ )
2 gruxp 
 |-  ( ( U e. Univ /\ B e. U /\ A e. U ) -> ( B X. A ) e. U )
3 2 3com23 
 |-  ( ( U e. Univ /\ A e. U /\ B e. U ) -> ( B X. A ) e. U )
4 grupw 
 |-  ( ( U e. Univ /\ ( B X. A ) e. U ) -> ~P ( B X. A ) e. U )
5 1 3 4 syl2anc 
 |-  ( ( U e. Univ /\ A e. U /\ B e. U ) -> ~P ( B X. A ) e. U )
6 mapsspw 
 |-  ( A ^m B ) C_ ~P ( B X. A )
7 6 a1i 
 |-  ( ( U e. Univ /\ A e. U /\ B e. U ) -> ( A ^m B ) C_ ~P ( B X. A ) )
8 gruss 
 |-  ( ( U e. Univ /\ ~P ( B X. A ) e. U /\ ( A ^m B ) C_ ~P ( B X. A ) ) -> ( A ^m B ) e. U )
9 1 5 7 8 syl3anc 
 |-  ( ( U e. Univ /\ A e. U /\ B e. U ) -> ( A ^m B ) e. U )