Theorem ixpfi

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

	Ref	Expression
Assertion	ixpfi	⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ Fin ) → X 𝑥 ∈ 𝐴 𝐵 ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		iunfi	⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ Fin ) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ Fin )
2		simpl	⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ Fin ) → 𝐴 ∈ Fin )
3		mapfi	⊢ ( ( ∪ 𝑥 ∈ 𝐴 𝐵 ∈ Fin ∧ 𝐴 ∈ Fin ) → ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐴 ) ∈ Fin )
4	1 2 3	syl2anc	⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ Fin ) → ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐴 ) ∈ Fin )
5		ixpssmap2g	⊢ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∈ Fin → X 𝑥 ∈ 𝐴 𝐵 ⊆ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐴 ) )
6	1 5	syl	⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ Fin ) → X 𝑥 ∈ 𝐴 𝐵 ⊆ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐴 ) )
7	4 6	ssfid	⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ Fin ) → X 𝑥 ∈ 𝐴 𝐵 ∈ Fin )