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 ∈ Fin ∧ ∀ x ∈ A B ∈ Fin → ⨉ x ∈ A B ∈ Fin

Proof

Step Hyp Ref Expression
1 iunfi ⊢ A ∈ Fin ∧ ∀ x ∈ A B ∈ Fin → ⋃ x ∈ A B ∈ Fin
2 simpl ⊢ A ∈ Fin ∧ ∀ x ∈ A B ∈ Fin → A ∈ Fin
3 mapfi ⊢ ⋃ x ∈ A B ∈ Fin ∧ A ∈ Fin → ⋃ x ∈ A B A ∈ Fin
4 1 2 3 syl2anc ⊢ A ∈ Fin ∧ ∀ x ∈ A B ∈ Fin → ⋃ x ∈ A B A ∈ Fin
5 ixpssmap2g ⊢ ⋃ x ∈ A B ∈ Fin → ⨉ x ∈ A B ⊆ ⋃ x ∈ A B A
6 1 5 syl ⊢ A ∈ Fin ∧ ∀ x ∈ A B ∈ Fin → ⨉ x ∈ A B ⊆ ⋃ x ∈ A B A
7 4 6 ssfid ⊢ A ∈ Fin ∧ ∀ x ∈ A B ∈ Fin → ⨉ x ∈ A B ∈ Fin