Theorem hfdm

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

	Ref	Expression
Assertion	hfdm	|- ( A e. HF -> dom A e. HF )

Proof

Step	Hyp	Ref	Expression
1		hfuni	|- ( A e. HF -> U. A e. HF )
2		hfuni	|- ( U. A e. HF -> U. U. A e. HF )
3		ssun1	|- dom A C_ ( dom A u. ran A )
4		dmrnssfld	|- ( dom A u. ran A ) C_ U. U. A
5	3 4	sstri	|- dom A C_ U. U. A
6		hfsshf	|- ( ( dom A C_ U. U. A /\ U. U. A e. HF ) -> dom A e. HF )
7	5 6	mpan	|- ( U. U. A e. HF -> dom A e. HF )
8	1 2 7	3syl	|- ( A e. HF -> dom A e. HF )