ixpfi

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

		Ref	Expression
	Assertion	ixpfi	$⊢ (A \in Fin \land \forall x \in A B \in Fin) \to \underset{x \in A}{⨉} B \in Fin$

Step	Hyp	Ref	Expression
1		iunfi	$⊢ (A \in Fin \land \forall x \in A B \in Fin) \to ⋃_{x \in A} B \in Fin$
2		simpl	$⊢ (A \in Fin \land \forall x \in A B \in Fin) \to A \in Fin$
3		mapfi	$⊢ (⋃_{x \in A} B \in Fin \land A \in Fin) \to {⋃_{x \in A} B}^{A} \in Fin$
4	1 2 3	syl2anc	$⊢ (A \in Fin \land \forall x \in A B \in Fin) \to {⋃_{x \in A} B}^{A} \in Fin$
5		ixpssmap2g	$⊢ ⋃_{x \in A} B \in Fin \to \underset{x \in A}{⨉} B \subseteq {⋃_{x \in A} B}^{A}$
6	1 5	syl	$⊢ (A \in Fin \land \forall x \in A B \in Fin) \to \underset{x \in A}{⨉} B \subseteq {⋃_{x \in A} B}^{A}$
7	4 6	ssfid	$⊢ (A \in Fin \land \forall x \in A B \in Fin) \to \underset{x \in A}{⨉} B \in Fin$

Metamath Proof Explorer