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 )