Theorem ixpexg

Description: The existence of an infinite Cartesian product. x is normally a free-variable parameter in B . Remark in Enderton p. 54. (Contributed by NM, 28-Sep-2006) (Revised by Mario Carneiro, 25-Jan-2015)

	Ref	Expression
Assertion	ixpexg	|- ( A. x e. A B e. V -> X_ x e. A B e. _V )

Proof

Step	Hyp	Ref	Expression
1		uniixp	|- U. X_ x e. A B C_ ( A X. U_ x e. A B )
2		iunexg	|- ( ( A e. _V /\ A. x e. A B e. V ) -> U_ x e. A B e. _V )
3		xpexg	|- ( ( A e. _V /\ U_ x e. A B e. _V ) -> ( A X. U_ x e. A B ) e. _V )
4	2 3	syldan	|- ( ( A e. _V /\ A. x e. A B e. V ) -> ( A X. U_ x e. A B ) e. _V )
5		ssexg	|- ( ( U. X_ x e. A B C_ ( A X. U_ x e. A B ) /\ ( A X. U_ x e. A B ) e. _V ) -> U. X_ x e. A B e. _V )
6	1 4 5	sylancr	|- ( ( A e. _V /\ A. x e. A B e. V ) -> U. X_ x e. A B e. _V )
7		uniexb	|- ( X_ x e. A B e. _V <-> U. X_ x e. A B e. _V )
8	6 7	sylibr	|- ( ( A e. _V /\ A. x e. A B e. V ) -> X_ x e. A B e. _V )
9		ixpprc	|- ( -. A e. _V -> X_ x e. A B = (/) )
10		0ex	|- (/) e. _V
11	9 10	eqeltrdi	|- ( -. A e. _V -> X_ x e. A B e. _V )
12	11	adantr	|- ( ( -. A e. _V /\ A. x e. A B e. V ) -> X_ x e. A B e. _V )
13	8 12	pm2.61ian	|- ( A. x e. A B e. V -> X_ x e. A B e. _V )