Theorem hfsshf

Description: Any subset of a hereditarily finite set is itself a hereditarily finite set. (Contributed by BTernaryTau, 17-Sep-2026)

	Ref	Expression
Assertion	hfsshf	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ HF ) → 𝐴 ∈ HF )

Proof

Step	Hyp	Ref	Expression
1		hffi	⊢ ( 𝐵 ∈ HF → 𝐵 ∈ Fin )
2		ssfi	⊢ ( ( 𝐵 ∈ Fin ∧ 𝐴 ⊆ 𝐵 ) → 𝐴 ∈ Fin )
3	2	ancoms	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ Fin ) → 𝐴 ∈ Fin )
4	1 3	sylan2	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ HF ) → 𝐴 ∈ Fin )
5		elhf3	⊢ ( 𝐵 ∈ HF ↔ ( 𝐵 ∈ Fin ∧ 𝐵 ⊆ HF ) )
6	5	simprbi	⊢ ( 𝐵 ∈ HF → 𝐵 ⊆ HF )
7		sstr	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ HF ) → 𝐴 ⊆ HF )
8	6 7	sylan2	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ HF ) → 𝐴 ⊆ HF )
9		elhf3	⊢ ( 𝐴 ∈ HF ↔ ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ HF ) )
10	4 8 9	sylanbrc	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ HF ) → 𝐴 ∈ HF )