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

Metamath Proof Explorer

Theorem 3xpfi

Description: The Cartesian product of three finite sets is a finite set. (Contributed by Alexander van der Vekens, 11-Mar-2018)

Ref Expression
Assertion 3xpfi ⊢ V ∈ Fin → V × V × V ∈ Fin

Proof

Step Hyp Ref Expression
1 xpfi ⊢ V ∈ Fin ∧ V ∈ Fin → V × V ∈ Fin
2 1 anidms ⊢ V ∈ Fin → V × V ∈ Fin
3 xpfi ⊢ V × V ∈ Fin ∧ V ∈ Fin → V × V × V ∈ Fin
4 2 3 mpancom ⊢ V ∈ Fin → V × V × V ∈ Fin