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

Metamath Proof Explorer

Theorem ixpfi

Description: A Cartesian product of finitely many finite sets is finite. (Contributed by Jeff Madsen, 19-Jun-2011)

Ref Expression
Assertion ixpfi 
|- ( ( A e. Fin /\ A. x e. A B e. Fin ) -> X_ x e. A B e. Fin )

Proof

Step Hyp Ref Expression
1 iunfi 
 |-  ( ( A e. Fin /\ A. x e. A B e. Fin ) -> U_ x e. A B e. Fin )
2 simpl 
 |-  ( ( A e. Fin /\ A. x e. A B e. Fin ) -> A e. Fin )
3 mapfi 
 |-  ( ( U_ x e. A B e. Fin /\ A e. Fin ) -> ( U_ x e. A B ^m A ) e. Fin )
4 1 2 3 syl2anc 
 |-  ( ( A e. Fin /\ A. x e. A B e. Fin ) -> ( U_ x e. A B ^m A ) e. Fin )
5 ixpssmap2g 
 |-  ( U_ x e. A B e. Fin -> X_ x e. A B C_ ( U_ x e. A B ^m A ) )
6 1 5 syl 
 |-  ( ( A e. Fin /\ A. x e. A B e. Fin ) -> X_ x e. A B C_ ( U_ x e. A B ^m A ) )
7 4 6 ssfid 
 |-  ( ( A e. Fin /\ A. x e. A B e. Fin ) -> X_ x e. A B e. Fin )