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

Proof

Step	Hyp	Ref	Expression
1		hffi	|- ( B e. HF -> B e. Fin )
2		ssfi	|- ( ( B e. Fin /\ A C_ B ) -> A e. Fin )
3	2	ancoms	|- ( ( A C_ B /\ B e. Fin ) -> A e. Fin )
4	1 3	sylan2	|- ( ( A C_ B /\ B e. HF ) -> A e. Fin )
5		elhf3	|- ( B e. HF <-> ( B e. Fin /\ B C_ HF ) )
6	5	simprbi	|- ( B e. HF -> B C_ HF )
7		sstr	|- ( ( A C_ B /\ B C_ HF ) -> A C_ HF )
8	6 7	sylan2	|- ( ( A C_ B /\ B e. HF ) -> A C_ HF )
9		elhf3	|- ( A e. HF <-> ( A e. Fin /\ A C_ HF ) )
10	4 8 9	sylanbrc	|- ( ( A C_ B /\ B e. HF ) -> A e. HF )