Theorem gruxp

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

	Ref	Expression
Assertion	gruxp	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈 ) → ( 𝐴 × 𝐵 ) ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		gruun	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈 ) → ( 𝐴 ∪ 𝐵 ) ∈ 𝑈 )
2		grupw	⊢ ( ( 𝑈 ∈ Univ ∧ ( 𝐴 ∪ 𝐵 ) ∈ 𝑈 ) → 𝒫 ( 𝐴 ∪ 𝐵 ) ∈ 𝑈 )
3		grupw	⊢ ( ( 𝑈 ∈ Univ ∧ 𝒫 ( 𝐴 ∪ 𝐵 ) ∈ 𝑈 ) → 𝒫 𝒫 ( 𝐴 ∪ 𝐵 ) ∈ 𝑈 )
4		xpsspw	⊢ ( 𝐴 × 𝐵 ) ⊆ 𝒫 𝒫 ( 𝐴 ∪ 𝐵 )
5		gruss	⊢ ( ( 𝑈 ∈ Univ ∧ 𝒫 𝒫 ( 𝐴 ∪ 𝐵 ) ∈ 𝑈 ∧ ( 𝐴 × 𝐵 ) ⊆ 𝒫 𝒫 ( 𝐴 ∪ 𝐵 ) ) → ( 𝐴 × 𝐵 ) ∈ 𝑈 )
6	4 5	mp3an3	⊢ ( ( 𝑈 ∈ Univ ∧ 𝒫 𝒫 ( 𝐴 ∪ 𝐵 ) ∈ 𝑈 ) → ( 𝐴 × 𝐵 ) ∈ 𝑈 )
7	3 6	syldan	⊢ ( ( 𝑈 ∈ Univ ∧ 𝒫 ( 𝐴 ∪ 𝐵 ) ∈ 𝑈 ) → ( 𝐴 × 𝐵 ) ∈ 𝑈 )
8	2 7	syldan	⊢ ( ( 𝑈 ∈ Univ ∧ ( 𝐴 ∪ 𝐵 ) ∈ 𝑈 ) → ( 𝐴 × 𝐵 ) ∈ 𝑈 )
9	8	3ad2antl1	⊢ ( ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈 ) ∧ ( 𝐴 ∪ 𝐵 ) ∈ 𝑈 ) → ( 𝐴 × 𝐵 ) ∈ 𝑈 )
10	1 9	mpdan	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈 ) → ( 𝐴 × 𝐵 ) ∈ 𝑈 )