This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )