Theorem grumap

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

	Ref	Expression
Assertion	grumap	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈 ) → ( 𝐴 ↑m 𝐵 ) ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈 ) → 𝑈 ∈ Univ )
2		gruxp	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐵 ∈ 𝑈 ∧ 𝐴 ∈ 𝑈 ) → ( 𝐵 × 𝐴 ) ∈ 𝑈 )
3	2	3com23	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈 ) → ( 𝐵 × 𝐴 ) ∈ 𝑈 )
4		grupw	⊢ ( ( 𝑈 ∈ Univ ∧ ( 𝐵 × 𝐴 ) ∈ 𝑈 ) → 𝒫 ( 𝐵 × 𝐴 ) ∈ 𝑈 )
5	1 3 4	syl2anc	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈 ) → 𝒫 ( 𝐵 × 𝐴 ) ∈ 𝑈 )
6		mapsspw	⊢ ( 𝐴 ↑m 𝐵 ) ⊆ 𝒫 ( 𝐵 × 𝐴 )
7	6	a1i	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈 ) → ( 𝐴 ↑m 𝐵 ) ⊆ 𝒫 ( 𝐵 × 𝐴 ) )
8		gruss	⊢ ( ( 𝑈 ∈ Univ ∧ 𝒫 ( 𝐵 × 𝐴 ) ∈ 𝑈 ∧ ( 𝐴 ↑m 𝐵 ) ⊆ 𝒫 ( 𝐵 × 𝐴 ) ) → ( 𝐴 ↑m 𝐵 ) ∈ 𝑈 )
9	1 5 7 8	syl3anc	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈 ) → ( 𝐴 ↑m 𝐵 ) ∈ 𝑈 )