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 Univ A U B U A B U

Proof

Step Hyp Ref Expression
1 simp1 U Univ A U B U U Univ
2 gruxp U Univ B U A U B × A U
3 2 3com23 U Univ A U B U B × A U
4 grupw U Univ B × A U 𝒫 B × A U
5 1 3 4 syl2anc U Univ A U B U 𝒫 B × A U
6 mapsspw A B 𝒫 B × A
7 6 a1i U Univ A U B U A B 𝒫 B × A
8 gruss U Univ 𝒫 B × A U A B 𝒫 B × A A B U
9 1 5 7 8 syl3anc U Univ A U B U A B U