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 e. Fin -> ( ( V X. V ) X. V ) e. Fin )

Proof

Step Hyp Ref Expression
1 xpfi 
 |-  ( ( V e. Fin /\ V e. Fin ) -> ( V X. V ) e. Fin )
2 1 anidms 
 |-  ( V e. Fin -> ( V X. V ) e. Fin )
3 xpfi 
 |-  ( ( ( V X. V ) e. Fin /\ V e. Fin ) -> ( ( V X. V ) X. V ) e. Fin )
4 2 3 mpancom 
 |-  ( V e. Fin -> ( ( V X. V ) X. V ) e. Fin )