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 )