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

Metamath Proof Explorer

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 )