Theorem uniixp

Description: The union of an infinite Cartesian product is included in a Cartesian product. (Contributed by NM, 28-Sep-2006) (Revised by Mario Carneiro, 24-Jun-2015)

	Ref	Expression
Assertion	uniixp	|- U. X_ x e. A B C_ ( A X. U_ x e. A B )

Proof

Step	Hyp	Ref	Expression
1		ixpf	|- ( f e. X_ x e. A B -> f : A --> U_ x e. A B )
2		fssxp	|- ( f : A --> U_ x e. A B -> f C_ ( A X. U_ x e. A B ) )
3	1 2	syl	|- ( f e. X_ x e. A B -> f C_ ( A X. U_ x e. A B ) )
4		velpw	|- ( f e. ~P ( A X. U_ x e. A B ) <-> f C_ ( A X. U_ x e. A B ) )
5	3 4	sylibr	|- ( f e. X_ x e. A B -> f e. ~P ( A X. U_ x e. A B ) )
6	5	ssriv	|- X_ x e. A B C_ ~P ( A X. U_ x e. A B )
7		sspwuni	|- ( X_ x e. A B C_ ~P ( A X. U_ x e. A B ) <-> U. X_ x e. A B C_ ( A X. U_ x e. A B ) )
8	6 7	mpbi	|- U. X_ x e. A B C_ ( A X. U_ x e. A B )