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	Could not format assertion : No typesetting found for |- ( ( A e. HF /\ B e. HF ) -> ( A X. B ) e. HF ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		hfun	Could not format ( ( A e. HF /\ B e. HF ) -> ( A u. B ) e. HF ) : No typesetting found for |- ( ( A e. HF /\ B e. HF ) -> ( A u. B ) e. HF ) with typecode |-
2		hfpw	Could not format ( ( A u. B ) e. HF -> ~P ( A u. B ) e. HF ) : No typesetting found for |- ( ( A u. B ) e. HF -> ~P ( A u. B ) e. HF ) with typecode |-
3		hfpw	Could not format ( ~P ( A u. B ) e. HF -> ~P ~P ( A u. B ) e. HF ) : No typesetting found for |- ( ~P ( A u. B ) e. HF -> ~P ~P ( A u. B ) e. HF ) with typecode |-
4		xpsspw	$$⊢A\times B\subseteq 𝒫𝒫\left(A\cup B\right)$$
5		hfsshf	Could not format ( ( ( A X. B ) C_ ~P ~P ( A u. B ) /\ ~P ~P ( A u. B ) e. HF ) -> ( A X. B ) e. HF ) : No typesetting found for |- ( ( ( A X. B ) C_ ~P ~P ( A u. B ) /\ ~P ~P ( A u. B ) e. HF ) -> ( A X. B ) e. HF ) with typecode |-
6	4 5	mpan	Could not format ( ~P ~P ( A u. B ) e. HF -> ( A X. B ) e. HF ) : No typesetting found for |- ( ~P ~P ( A u. B ) e. HF -> ( A X. B ) e. HF ) with typecode |-
7	1 2 3 6	4syl	Could not format ( ( A e. HF /\ B e. HF ) -> ( A X. B ) e. HF ) : No typesetting found for |- ( ( A e. HF /\ B e. HF ) -> ( A X. B ) e. HF ) with typecode |-