Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 hfun 
 |-  ( ( A e. HF /\ B e. HF ) -> ( A u. B ) e. HF )
2 hfpw 
 |-  ( ( A u. B ) e. HF -> ~P ( A u. B ) e. HF )
3 hfpw 
 |-  ( ~P ( A u. B ) e. HF -> ~P ~P ( A u. B ) e. HF )
4 xpsspw 
 |-  ( A X. B ) C_ ~P ~P ( A u. B )
5 hfsshf 
 |-  ( ( ( A X. B ) C_ ~P ~P ( A u. B ) /\ ~P ~P ( A u. B ) e. HF ) -> ( A X. B ) e. HF )
6 4 5 mpan 
 |-  ( ~P ~P ( A u. B ) e. HF -> ( A X. B ) e. HF )
7 1 2 3 6 4syl 
 |-  ( ( A e. HF /\ B e. HF ) -> ( A X. B ) e. HF )