Metamath Proof Explorer

Theorem gruixp

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

Ref Expression
Assertion gruixp ⊢ U ∈ Univ ∧ A ∈ U ∧ ∀ x ∈ A B ∈ U → ⨉ x ∈ A B ∈ U

Proof

Step Hyp Ref Expression
1 simp1 ⊢ U ∈ Univ ∧ A ∈ U ∧ ∀ x ∈ A B ∈ U → U ∈ Univ
2 gruiun ⊢ U ∈ Univ ∧ A ∈ U ∧ ∀ x ∈ A B ∈ U → ⋃ x ∈ A B ∈ U
3 simp2 ⊢ U ∈ Univ ∧ A ∈ U ∧ ∀ x ∈ A B ∈ U → A ∈ U
4 grumap ⊢ U ∈ Univ ∧ ⋃ x ∈ A B ∈ U ∧ A ∈ U → ⋃ x ∈ A B A ∈ U
5 1 2 3 4 syl3anc ⊢ U ∈ Univ ∧ A ∈ U ∧ ∀ x ∈ A B ∈ U → ⋃ x ∈ A B A ∈ U
6 ixpssmapg ⊢ ∀ x ∈ A B ∈ U → ⨉ x ∈ A B ⊆ ⋃ x ∈ A B A
7 6 3ad2ant3 ⊢ U ∈ Univ ∧ A ∈ U ∧ ∀ x ∈ A B ∈ U → ⨉ x ∈ A B ⊆ ⋃ x ∈ A B A
8 gruss ⊢ U ∈ Univ ∧ ⋃ x ∈ A B A ∈ U ∧ ⨉ x ∈ A B ⊆ ⋃ x ∈ A B A → ⨉ x ∈ A B ∈ U
9 1 5 7 8 syl3anc ⊢ U ∈ Univ ∧ A ∈ U ∧ ∀ x ∈ A B ∈ U → ⨉ x ∈ A B ∈ U