Theorem hfxp

Description: The Cartesian product of two hereditarily finite sets is a hereditarily finite set. (Contributed by Eric Schmidt, 26-Sep-2026)

	Ref	Expression
Assertion	hfxp	⊢ ( ( 𝐴 ∈ HF ∧ 𝐵 ∈ HF ) → ( 𝐴 × 𝐵 ) ∈ HF )

Proof

Step	Hyp	Ref	Expression
1		hfun	⊢ ( ( 𝐴 ∈ HF ∧ 𝐵 ∈ HF ) → ( 𝐴 ∪ 𝐵 ) ∈ HF )
2		hfpw	⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ HF → 𝒫 ( 𝐴 ∪ 𝐵 ) ∈ HF )
3		hfpw	⊢ ( 𝒫 ( 𝐴 ∪ 𝐵 ) ∈ HF → 𝒫 𝒫 ( 𝐴 ∪ 𝐵 ) ∈ HF )
4		xpsspw	⊢ ( 𝐴 × 𝐵 ) ⊆ 𝒫 𝒫 ( 𝐴 ∪ 𝐵 )
5		hfsshf	⊢ ( ( ( 𝐴 × 𝐵 ) ⊆ 𝒫 𝒫 ( 𝐴 ∪ 𝐵 ) ∧ 𝒫 𝒫 ( 𝐴 ∪ 𝐵 ) ∈ HF ) → ( 𝐴 × 𝐵 ) ∈ HF )
6	4 5	mpan	⊢ ( 𝒫 𝒫 ( 𝐴 ∪ 𝐵 ) ∈ HF → ( 𝐴 × 𝐵 ) ∈ HF )
7	1 2 3 6	4syl	⊢ ( ( 𝐴 ∈ HF ∧ 𝐵 ∈ HF ) → ( 𝐴 × 𝐵 ) ∈ HF )