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 e. Univ /\ A e. U /\ A. x e. A B e. U ) -> X_ x e. A B e. U )

Proof

Step	Hyp	Ref	Expression
1		simp1	|- ( ( U e. Univ /\ A e. U /\ A. x e. A B e. U ) -> U e. Univ )
2		gruiun	|- ( ( U e. Univ /\ A e. U /\ A. x e. A B e. U ) -> U_ x e. A B e. U )
3		simp2	|- ( ( U e. Univ /\ A e. U /\ A. x e. A B e. U ) -> A e. U )
4		grumap	|- ( ( U e. Univ /\ U_ x e. A B e. U /\ A e. U ) -> ( U_ x e. A B ^m A ) e. U )
5	1 2 3 4	syl3anc	|- ( ( U e. Univ /\ A e. U /\ A. x e. A B e. U ) -> ( U_ x e. A B ^m A ) e. U )
6		ixpssmapg	|- ( A. x e. A B e. U -> X_ x e. A B C_ ( U_ x e. A B ^m A ) )
7	6	3ad2ant3	|- ( ( U e. Univ /\ A e. U /\ A. x e. A B e. U ) -> X_ x e. A B C_ ( U_ x e. A B ^m A ) )
8		gruss	|- ( ( U e. Univ /\ ( U_ x e. A B ^m A ) e. U /\ X_ x e. A B C_ ( U_ x e. A B ^m A ) ) -> X_ x e. A B e. U )
9	1 5 7 8	syl3anc	|- ( ( U e. Univ /\ A e. U /\ A. x e. A B e. U ) -> X_ x e. A B e. U )