grumap

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

		Ref	Expression
	Assertion	grumap	$⊢ (U \in Univ \land A \in U \land B \in U) \to A^{B} \in U$

Step	Hyp	Ref	Expression
1		simp1	$⊢ (U \in Univ \land A \in U \land B \in U) \to U \in Univ$
2		gruxp	$⊢ (U \in Univ \land B \in U \land A \in U) \to B \times A \in U$
3	2	3com23	$⊢ (U \in Univ \land A \in U \land B \in U) \to B \times A \in U$
4		grupw	$⊢ (U \in Univ \land B \times A \in U) \to 𝒫 (B \times A) \in U$
5	1 3 4	syl2anc	$⊢ (U \in Univ \land A \in U \land B \in U) \to 𝒫 (B \times A) \in U$
6		mapsspw	$⊢ A^{B} \subseteq 𝒫 (B \times A)$
7	6	a1i	$⊢ (U \in Univ \land A \in U \land B \in U) \to A^{B} \subseteq 𝒫 (B \times A)$
8		gruss	$⊢ (U \in Univ \land 𝒫 (B \times A) \in U \land A^{B} \subseteq 𝒫 (B \times A)) \to A^{B} \in U$
9	1 5 7 8	syl3anc	$⊢ (U \in Univ \land A \in U \land B \in U) \to A^{B} \in U$

Metamath Proof Explorer