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	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to A\times B\in \mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		unfi	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to A\cup B\in \mathrm{Fin}$$
2		pwfi	$$⊢A\cup B\in \mathrm{Fin}\leftrightarrow 𝒫\left(A\cup B\right)\in \mathrm{Fin}$$
3		pwfi	$$⊢𝒫\left(A\cup B\right)\in \mathrm{Fin}\leftrightarrow 𝒫𝒫\left(A\cup B\right)\in \mathrm{Fin}$$
4	2 3	bitri	$$⊢A\cup B\in \mathrm{Fin}\leftrightarrow 𝒫𝒫\left(A\cup B\right)\in \mathrm{Fin}$$
5	1 4	sylib	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to 𝒫𝒫\left(A\cup B\right)\in \mathrm{Fin}$$
6		xpsspw	$$⊢A\times B\subseteq 𝒫𝒫\left(A\cup B\right)$$
7		ssfi	$$⊢\left(𝒫𝒫\left(A\cup B\right)\in \mathrm{Fin}\wedge A\times B\subseteq 𝒫𝒫\left(A\cup B\right)\right)\to A\times B\in \mathrm{Fin}$$
8	5 6 7	sylancl	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to A\times B\in \mathrm{Fin}$$