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 e. Fin /\ B e. Fin ) -> ( A X. B ) e. Fin )

Proof

Step Hyp Ref Expression
1 unfi 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( A u. B ) e. Fin )
2 pwfi 
 |-  ( ( A u. B ) e. Fin <-> ~P ( A u. B ) e. Fin )
3 pwfi 
 |-  ( ~P ( A u. B ) e. Fin <-> ~P ~P ( A u. B ) e. Fin )
4 2 3 bitri 
 |-  ( ( A u. B ) e. Fin <-> ~P ~P ( A u. B ) e. Fin )
5 1 4 sylib 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ~P ~P ( A u. B ) e. Fin )
6 xpsspw 
 |-  ( A X. B ) C_ ~P ~P ( A u. B )
7 ssfi 
 |-  ( ( ~P ~P ( A u. B ) e. Fin /\ ( A X. B ) C_ ~P ~P ( A u. B ) ) -> ( A X. B ) e. Fin )
8 5 6 7 sylancl 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( A X. B ) e. Fin )