Theorem hfdm

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

	Ref	Expression
Assertion	hfdm	⊢ ( 𝐴 ∈ HF → dom 𝐴 ∈ HF )

Proof

Step	Hyp	Ref	Expression
1		hfuni	⊢ ( 𝐴 ∈ HF → ∪ 𝐴 ∈ HF )
2		hfuni	⊢ ( ∪ 𝐴 ∈ HF → ∪ ∪ 𝐴 ∈ HF )
3		ssun1	⊢ dom 𝐴 ⊆ ( dom 𝐴 ∪ ran 𝐴 )
4		dmrnssfld	⊢ ( dom 𝐴 ∪ ran 𝐴 ) ⊆ ∪ ∪ 𝐴
5	3 4	sstri	⊢ dom 𝐴 ⊆ ∪ ∪ 𝐴
6		hfsshf	⊢ ( ( dom 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ HF ) → dom 𝐴 ∈ HF )
7	5 6	mpan	⊢ ( ∪ ∪ 𝐴 ∈ HF → dom 𝐴 ∈ HF )
8	1 2 7	3syl	⊢ ( 𝐴 ∈ HF → dom 𝐴 ∈ HF )