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	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( 𝐴 × 𝐵 ) ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		unfi	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( 𝐴 ∪ 𝐵 ) ∈ Fin )
2		pwfi	⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ Fin ↔ 𝒫 ( 𝐴 ∪ 𝐵 ) ∈ Fin )
3		pwfi	⊢ ( 𝒫 ( 𝐴 ∪ 𝐵 ) ∈ Fin ↔ 𝒫 𝒫 ( 𝐴 ∪ 𝐵 ) ∈ Fin )
4	2 3	bitri	⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ Fin ↔ 𝒫 𝒫 ( 𝐴 ∪ 𝐵 ) ∈ Fin )
5	1 4	sylib	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → 𝒫 𝒫 ( 𝐴 ∪ 𝐵 ) ∈ Fin )
6		xpsspw	⊢ ( 𝐴 × 𝐵 ) ⊆ 𝒫 𝒫 ( 𝐴 ∪ 𝐵 )
7		ssfi	⊢ ( ( 𝒫 𝒫 ( 𝐴 ∪ 𝐵 ) ∈ Fin ∧ ( 𝐴 × 𝐵 ) ⊆ 𝒫 𝒫 ( 𝐴 ∪ 𝐵 ) ) → ( 𝐴 × 𝐵 ) ∈ Fin )
8	5 6 7	sylancl	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( 𝐴 × 𝐵 ) ∈ Fin )