Theorem gruixp

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

	Ref	Expression
Assertion	gruixp	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑈 ) → X 𝑥 ∈ 𝐴 𝐵 ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑈 ) → 𝑈 ∈ Univ )
2		gruiun	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑈 ) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑈 )
3		simp2	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑈 ) → 𝐴 ∈ 𝑈 )
4		grumap	⊢ ( ( 𝑈 ∈ Univ ∧ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑈 ∧ 𝐴 ∈ 𝑈 ) → ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐴 ) ∈ 𝑈 )
5	1 2 3 4	syl3anc	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑈 ) → ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐴 ) ∈ 𝑈 )
6		ixpssmapg	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑈 → X 𝑥 ∈ 𝐴 𝐵 ⊆ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐴 ) )
7	6	3ad2ant3	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑈 ) → X 𝑥 ∈ 𝐴 𝐵 ⊆ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐴 ) )
8		gruss	⊢ ( ( 𝑈 ∈ Univ ∧ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐴 ) ∈ 𝑈 ∧ X 𝑥 ∈ 𝐴 𝐵 ⊆ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐴 ) ) → X 𝑥 ∈ 𝐴 𝐵 ∈ 𝑈 )
9	1 5 7 8	syl3anc	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑈 ) → X 𝑥 ∈ 𝐴 𝐵 ∈ 𝑈 )