Metamath Proof Explorer


Theorem xpfi

Description: The Cartesian product of two finite sets is finite. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 12-Mar-2015) Avoid ax-pow . (Revised by BTernaryTau, 10-Jan-2025)

Ref Expression
Assertion xpfi A Fin B Fin A × B Fin

Proof

Step Hyp Ref Expression
1 unfi A Fin B Fin A B Fin
2 pwfi A B Fin 𝒫 A B Fin
3 pwfi 𝒫 A B Fin 𝒫 𝒫 A B Fin
4 2 3 bitri A B Fin 𝒫 𝒫 A B Fin
5 1 4 sylib A Fin B Fin 𝒫 𝒫 A B Fin
6 xpsspw A × B 𝒫 𝒫 A B
7 ssfi 𝒫 𝒫 A B Fin A × B 𝒫 𝒫 A B A × B Fin
8 5 6 7 sylancl A Fin B Fin A × B Fin