This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ 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 )