# 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 ${⊢}\left({A}\in \mathrm{Fin}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in \mathrm{Fin}\right)\to \underset{{x}\in {A}}{⨉}{B}\in \mathrm{Fin}$

### Proof

Step Hyp Ref Expression
1 iunfi ${⊢}\left({A}\in \mathrm{Fin}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in \mathrm{Fin}\right)\to \bigcup _{{x}\in {A}}{B}\in \mathrm{Fin}$
2 simpl ${⊢}\left({A}\in \mathrm{Fin}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in \mathrm{Fin}\right)\to {A}\in \mathrm{Fin}$
3 mapfi ${⊢}\left(\bigcup _{{x}\in {A}}{B}\in \mathrm{Fin}\wedge {A}\in \mathrm{Fin}\right)\to {\bigcup _{{x}\in {A}}{B}}^{{A}}\in \mathrm{Fin}$
4 1 2 3 syl2anc ${⊢}\left({A}\in \mathrm{Fin}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in \mathrm{Fin}\right)\to {\bigcup _{{x}\in {A}}{B}}^{{A}}\in \mathrm{Fin}$
5 ixpssmap2g ${⊢}\bigcup _{{x}\in {A}}{B}\in \mathrm{Fin}\to \underset{{x}\in {A}}{⨉}{B}\subseteq {\bigcup _{{x}\in {A}}{B}}^{{A}}$
6 1 5 syl ${⊢}\left({A}\in \mathrm{Fin}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in \mathrm{Fin}\right)\to \underset{{x}\in {A}}{⨉}{B}\subseteq {\bigcup _{{x}\in {A}}{B}}^{{A}}$
7 4 6 ssfid ${⊢}\left({A}\in \mathrm{Fin}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in \mathrm{Fin}\right)\to \underset{{x}\in {A}}{⨉}{B}\in \mathrm{Fin}$